Measurement Path Action

Recognition path action

A recognition path is a time-parameterized positive rate function: it describes how fast a system recognizes events at each moment over a fixed time interval. The recognition action of a path is the integral over time of the recognition cost J applied to the rate. The cost function J is the one proved unique in the framework's core theorem, so action is not an arbitrary choice but the forced consequence of that cost.

The module defines three quantities from this action. The path weight is the exponential of the negative action, w[γ] = exp(-C[γ]), and a lemma proves this weight is always positive. The path amplitude is a complex number built from the same action with an extra phase, A[γ] = exp(-C[γ]/2) · exp(iφ). A theorem shows that the squared modulus of this amplitude equals the weight, |A[γ]|² = w[γ]. In plain language: the amplitude carries the same information as the weight, but in a form that can interfere, exactly as in quantum mechanics where probability is the square of a wave amplitude.

This is a minimal interface, deliberately. The module omits heavy measure-theoretic lemmas such as piecewise additivity and domain shifts, so the build surface stays stable for exports. What it establishes is the bridge between the framework's discrete recognition ledger and a continuous path integral: the weight of a path is its probability-like contribution, and the amplitude provides the phase-coherent version. This is the step that lets Recognition Science speak the language of quantum amplitudes without importing quantum mechanics as an axiom.

/-- A recognition path is a time-parameterized positive rate function. -/
structure RecognitionPath where
  T : ℝ
  T_pos : 0 < T
  rate : ℝ → ℝ
  rate_pos : ∀ t, t ∈ Set.Icc 0 T → 0 < rate t

/-- Weight is positive. -/
lemma pathWeight_pos (γ : RecognitionPath) : 0 < pathWeight γ := by
  unfold pathWeight
  exact Real.exp_pos _

/-- Amplitude modulus squared equals weight. -/
theorem amplitude_mod_sq_eq_weight (γ : RecognitionPath) (φ : ℝ) :
  ‖pathAmplitude γ φ‖ ^ 2 = pathWeight γ := by
  unfold pathAmplitude pathWeight
  have h1 : ‖Complex.exp (-(pathAction γ) / 2)‖ = Real.exp (-(pathAction γ) / 2) := by
    simpa using Complex.norm_exp_ofReal (-(pathAction γ) / 2)
  have h2 := Complex.norm_exp_ofReal_mul_I φ
  rw [norm_mul]
  simp only [h1, h2, mul_one, sq]
  rw [← Real.exp_add]
  ring

What this page does not claim

The module does not prove that the recognition cost J is unique; that is a separate theorem. The path amplitude does not yet include any dynamics or equations of motion beyond the cost integral.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/PathAction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: