born_rule_from_C
plain-language theorem explainer
The theorem shows that normalized complex amplitudes α₁ and α₂ linked to a two-branch rotation yield Born probabilities exactly equal to their squared moduli once a two-outcome measurement is built from the corresponding recognition costs. Researchers deriving quantum measurement rules from cost functionals in Recognition Science would cite it to connect path actions to probability assignments. The tactic proof assembles the measurement from a path-action cost and a complementary logarithmic cost, verifies non-negativity with Jcost lemmas, and,
Claim. Let α₁, α₂ ∈ ℂ satisfy |α₁|² + |α₂|² = 1. Let rot be a two-branch rotation such that |α₁|² equals the complement amplitude squared of rot and |α₂|² equals the initial amplitude squared of rot. Then there exists a two-outcome measurement m such that the probability of its first outcome equals |α₁|² and the probability of its second outcome equals |α₂|².
background
The module derives Born's rule P(I) = |α_I|² from the recognition cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ). The central structure is the two-outcome measurement, a record of two recognition costs C₁ and C₂ together with proofs that each is nonnegative; its probabilities are then the normalized exponentials exp(-C_i). Upstream, Jcost_nonneg states that J(x) ≥ 0 for x > 0 by the AM-GM inequality, and this nonnegativity is invoked to certify the integral cost along the rotation path. The path action itself integrates Jcost over positive rates supplied by the rotation.
proof idea
The proof first defines C_sin as the pathAction of the rotation path and C_cos as -2 log(cos θ_s). Nonnegativity of C_sin follows by applying Jcost_nonneg inside the integral after unfolding pathAction. Nonnegativity of C_cos is obtained from log_nonpos and the sign of the prefactor. The measurement object is then assembled with these two costs. Direct calculation reduces exp(-C_cos) to the complement amplitude squared, while weight_equals_born equates exp(-C_sin) to the initial amplitude squared. The probability definitions then simplify to the desired squares via the identity cos² + sin² = 1.
why it matters
This theorem supplies the explicit bridge from recognition costs to Born probabilities inside the Measurement.BornRule module, as announced in the module doc-comment. It therefore occupies a central place in the Recognition Science derivation of quantum measurement from the single functional equation and the J-cost. The result sits downstream of the C=2A bridge imported from C2ABridge and upstream of any further normalization or multi-outcome extensions. No open scaffolding remains in the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.