weight_equals_born
plain-language theorem explainer
Equates the recognition path weight for a two-branch rotation to the squared initial amplitude, realizing exp(-2A) = |α₂|². Derivations of the Born rule from the recognition cost functional cite this step. The tactic proof unfolds the definitions, rewrites via the C=2A bridge theorem, and simplifies the resulting exponential identity.
Claim. For a two-branch geodesic rotation ρ, the weight of the associated recognition path equals the squared modulus of the initial amplitude: exp(-2A(ρ)) = |α₂|².
background
The C=2A Measurement Bridge module proves that recognition cost C equals twice the rate action A for any two-branch rotation. This uses the unique cost functional J satisfying the Recognition Composition Law. The upstream measurement_bridge_C_eq_2A theorem establishes that the path action of the constructed geodesic equals twice the rate action. Path weight is the exponential of the negative path action; initialAmplitudeSquared is the Born probability attached to the initial branch.
proof idea
Unfolds pathWeight and initialAmplitudeSquared. Rewrites the path action via measurement_bridge_C_eq_2A to replace it by twice the rate action. Applies born_weight_from_rate to obtain the exponential identity Real.exp(-(2 * rateAction rot)) = initialAmplitudeSquared rot, then simplifies.
why it matters
Supplies the weight-amplitude link required by born_rule_from_C, which derives the full Born rule from the C=2A equivalence. It closes the measurement bridge, confirming that quantum probabilities arise from the same J-cost that governs the forcing chain. The module states that this shows quantum measurement and recognition share the unique cost functional J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.