Measurement Path Action Path Amplitude

Path amplitude

A recognition path is a time-parameterized positive rate function, a discrete record of how strongly recognition events occur over time. The framework assigns each such path an action, the integral of the cost function J over the path's duration. The path weight is the exponential of the negative action, a positive real number that measures how much the path contributes to a sum over histories.

The path amplitude extends this weight to a complex number by taking the square root of the weight and multiplying by a phase factor exp(i φ). In plain language, the amplitude carries both the magnitude (how much the path counts) and a phase (an angle that can interfere with other paths). The central theorem here is that the squared modulus of the amplitude equals the weight: |amplitude|² = weight. This is the Born-rule-like bridge that connects the complex amplitude to a positive probability-like quantity.

In Recognition Science, this declaration establishes the minimal interface for how paths contribute to measurement: each path has a positive weight, and the amplitude is the complex object whose squared size reproduces that weight. The framework models measurement as a sum over such amplitudes, with the phase φ available to encode interference. The theorem amplitude_mod_sq_eq_weight is proved in the machine-checked library of formal theorems, so the bridge is not an assumption but a derived identity.

What this does not claim is substantial. The declaration does not prove that the integral defining the action converges for all paths, nor does it provide the heavy measure-theoretic lemmas (piecewise additivity, domain shifts) that would be needed for a full path integral. It does not assert that the phase φ has any particular physical meaning or that the amplitude satisfies a Schrödinger-like equation. It is a lightweight interface, deliberately omitting the analytic machinery that a complete theory of path integration would require.

The practical consequence is that the framework can now write down a path sum with amplitudes, and the Born-rule bridge holds by construction. But the hard analysis of when such sums converge, and how they relate to conventional quantum mechanics, remains open. The declaration is a definitional choice, not a derivation of quantum theory.

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

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

/-- Amplitude bridge 𝒜[γ] = exp(-C[γ]/2) · exp(i φ). -/
noncomputable def pathAmplitude (γ : RecognitionPath) (φ : ℝ) : ℂ :=
  Complex.exp (- pathAction γ / 2) * Complex.exp (φ * I)

What this page does not claim

The declaration does not prove convergence of the action integral. The phase φ is not assigned a physical meaning. The path amplitude does not satisfy a dynamical equation.

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: