Measurement Path Action Amplitude Mod Sq Eq Weight

The amplitude bridge

A recognition path is a time-parameterized positive rate function, a record of how recognition intensity changes over a finite interval. The framework assigns each path an action, the integral of the cost function over time, and then defines two derived objects. The path weight is the exponential of the negative action, a positive real number that behaves like a probability weight. The path amplitude is a complex number built from the same action, with a phase factor, so it carries both magnitude and phase information.

The theorem amplitude_mod_sq_eq_weight, proved in the machine-checked library of formal theorems, states that the squared modulus of the path amplitude equals the path weight. In plain terms, if you take the amplitude, multiply it by its complex conjugate, you recover exactly the weight. This is the same relation that holds between a quantum wavefunction and a probability, but here it emerges from the recognition framework's own definitions rather than being assumed as a postulate.

The proof is a direct calculation using the properties of the complex exponential. The magnitude of the amplitude's real exponential factor is the real exponential of half the negative action, and the phase factor has unit modulus. Squaring the product and simplifying yields the weight. The theorem holds for every recognition path and every real phase, with no additional assumptions.

What the theorem does not claim is that the amplitude itself is a physical wavefunction or that the weight is an observed probability. It is a formal identity between two defined quantities. The framework does not derive the Born rule from this relation, nor does it assert that the phase has measurable consequences. The theorem is a bridge between the framework's action-based weights and the complex amplitudes familiar from quantum mechanics, but it does not by itself establish a physical interpretation.

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

/-- Positive weight w[γ] = exp(-C[γ]). -/
noncomputable def pathWeight (γ : RecognitionPath) : ℝ :=
  Real.exp (- pathAction γ)

/-- 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 theorem does not establish that the amplitude is a physical wavefunction. The theorem does not derive the Born rule or observed probabilities. The theorem does not assign measurable consequences to the phase factor.

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: