Measurement Path Action Recognition Path

The recognition path

A recognition path is a way to describe a process that unfolds over time, where at each moment the process has a positive rate of activity. The path is defined on a finite time interval, and the rate is always greater than zero throughout that interval. This is a minimal mathematical structure: it does not assume any particular dynamics, only that something is happening at a measurable intensity at every instant.

From this structure, the framework defines an action, written C[γ] = ∫ J(r(t)) dt, which integrates the recognition cost J at each rate over the duration of the path. The cost J is the unique function forced by the framework's five conditions, so the action is not a free choice but a consequence of that cost. A positive weight is then defined as exp(-C[γ]), and an amplitude as exp(-C[γ]/2) · exp(iφ). The weight is always positive, and the squared modulus of the amplitude equals the weight, a relation that connects the probabilistic and quantum-like descriptions.

In Recognition Science, these definitions provide a bridge between the discrete ledger of recognition events and continuous measurement processes. The path action is the integral of the cost along a trajectory, and the weight and amplitude are its exponential transforms. The framework proves that the amplitude's squared modulus equals the weight, which is the standard Born-rule relation in quantum mechanics, but here it follows from the definitions rather than being postulated.

The declaration deliberately omits heavy measure-theoretic lemmas such as piecewise additivity and domain shifts. This keeps the interface minimal and stable for paper exports. The structure establishes the basic vocabulary for talking about paths and their costs, but it does not claim that any particular path is realized, that the action is minimized, or that the amplitude represents a physical wavefunction. These are targets for further development, not consequences of this declaration.

/-- 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

/-- Recognition action C[γ] = ∫ J(r(t)) dt. -/
noncomputable def pathAction (γ : RecognitionPath) : ℝ :=
  ∫ t in (0)..γ.T, Cost.Jcost (γ.rate t)

/-- 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 declaration does not claim that any particular path is physically realized or that the action is minimized. The amplitude is not claimed to be a physical wavefunction; it is a definitional bridge. The declaration does not claim that the path action is additive over subintervals.

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: