amplitude_modulus_bridge
plain-language theorem explainer
The modulus of the path amplitude equals exp(-rate action) for any two-branch rotation. Workers deriving Born-rule weights from recognition costs cite this to equate amplitude modulus with the square root of the weight. The proof unfolds the amplitude into a product of exponentials, applies complex norm rules, and substitutes the C=2A relation to collapse the real exponent.
Claim. $|𝒜(γ,φ)| = e^{-A}$ where γ is the recognition path built from a two-branch geodesic rotation, A denotes its rate action, and 𝒜(γ,φ) = exp(-C[γ]/2) ⋅ exp(i φ) with C[γ] the integrated J-cost along γ.
background
The module establishes the central C=2A equivalence: for any two-branch geodesic rotation the recognition action C equals twice the rate action A. Path action is the integral of J-cost over the rate profile of the constructed path. Amplitude is defined as exp(-C/2) times a unit-modulus phase factor exp(i φ). The upstream measurement_bridge_C_eq_2A theorem states that pathAction(pathFromRotation rot) = 2 ⋅ rateAction rot exactly.
proof idea
Unfolds pathAmplitude into the product of exp(-pathAction/2) and exp(i φ). Applies Complex.norm_exp_ofReal to obtain the real exponential for the first factor and unit norm for the phase factor. Invokes measurement_bridge_C_eq_2A to replace pathAction with 2 ⋅ rateAction, then uses norm_mul and ring to finish the equality.
why it matters
This supplies the modulus form that lets the weight equal the square of the amplitude modulus, directly supporting the module's main C=2A theorem. It links the J-cost functional to quantum amplitudes inside the Recognition Science framework, where the same unique cost governs measurement. No open scaffolding remains; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.