amplitude_mod_sq_eq_weight
plain-language theorem explainer
The theorem establishes that the squared modulus of the path amplitude equals the path weight for any recognition path γ and phase φ. Researchers modeling quantum amplitudes via recognition paths in the Recognition Science framework would reference this identity to confirm consistency between complex and real formulations. The proof proceeds by unfolding the definitions of pathAmplitude and pathWeight, then applying properties of the complex norm on exponentials and simplifying the resulting real exponential expression.
Claim. For any recognition path γ and real φ, ‖𝒜[γ](φ)‖² = w[γ], where 𝒜[γ](φ) = exp(−C[γ]/2) ⋅ exp(i φ) and w[γ] = exp(−C[γ]), with C[γ] the recognition action ∫₀^T J(r(t)) dt.
background
A recognition path γ is a structure with positive duration T and positive rate function r(t) on [0,T]. The recognition action C[γ] is defined as the integral of the J-cost applied to the rate over that interval. The path amplitude is the complex quantity exp(−C[γ]/2) ⋅ exp(i φ), while the path weight is the positive real exp(−C[γ]).
proof idea
The proof unfolds pathAmplitude and pathWeight. It establishes the norm of the real exponential via the complex norm property for real arguments, applies the norm of the imaginary exponential factor, rewrites the product norm, simplifies using multiplication by one, reduces the sum of exponents via the exponential addition rule, and finishes with algebraic simplification.
why it matters
This identity confirms consistency of the amplitude bridge with the weight in the path integral setting. It supports the minimal measurement interface by ensuring squared amplitudes recover the exponential weights. The result sits inside the Recognition Science path-action layer and aligns with the J-cost definition and the forcing chain that produces the J-function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.