pathAmplitude
plain-language theorem explainer
The path amplitude is defined as the product of a real exponential decay from the integrated J-cost along a recognition path and a unit-modulus phase factor exp(i phi). Physicists deriving measurement weights from actions in Recognition Science models would cite this construction when linking path integrals to complex amplitudes. It is supplied by a direct one-line composition of complex exponentials applied to the real action value and the phase parameter.
Claim. $A[γ, φ] := exp(-C[γ]/2) · exp(i φ)$, where $C[γ] = ∫_0^T J(r(t)) dt$ for a recognition path γ of duration T > 0 with positive rate function r(t).
background
A recognition path consists of a finite duration T > 0 together with a positive rate function r(t) defined on the closed interval [0, T]. The associated recognition action is the integral of the J-cost function evaluated along this rate. The module supplies a minimal interface for paths, actions, and weights while omitting measure-theoretic extensions to keep the build surface stable for paper exports.
proof idea
One-line definition that applies the complex exponential to the negated path action divided by two and multiplies the result by the complex exponential of the phase times the imaginary unit.
why it matters
This definition feeds the modulus-squared identity that recovers the path weight exp(-C[γ]) and the amplitude-modulus bridge used in C2ABridge. It supplies the complex bridge between the real action integral and measurement amplitudes inside the Recognition Science path formalism, consistent with the eight-tick octave and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.