born_normalization
plain-language theorem explainer
The identity sin²θ + cos²θ = 1 normalizes Born-rule probabilities for the two-branch orthogonal case inside the coherence-collapse model. Workers deriving |α|² from recognition costs C = 2A cite it to close the probability sum after the residual action A = -ln(sin θ_s) is introduced. The proof is a one-line wrapper that invokes Mathlib's sin_sq_add_cos_sq on the supplied angle.
Claim. For real phase separation θ between two orthogonal branches, the probabilities satisfy $sin^2 θ + cos^2 θ = 1$.
background
The CoherenceCollapse module recovers the Born rule from the recognition action C[γ] = ∫ J(r(t)) dt and the residual rate action A = -ln(sin θ_s) via the central identity C = 2A. Sibling definitions born_weight and born_weight_is_sin_sq link the exponential weight exp(-C) to sin²θ for geodesic angle θ, while Jcost supplies the underlying cost functional. The module setting is the gravity-to-measurement bridge in which P(I) = exp(-C_I)/Σ exp(-C_J) equals |α_I|², with mesoscopic threshold m_coh ≈ 0.2 ng for A ≈ 1.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma Real.sin_sq_add_cos_sq directly to the input angle theta.
why it matters
coherence_collapse_cert invokes born_normalization to certify normalization inside the full Born-rule emergence statement. It fills the two-branch case of the module proposition that probabilities equal squared amplitudes once C = 2A is established. The step sits downstream of the J-uniqueness and phi-ladder constructions that define the cost function, and upstream of the mesoscopic threshold claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.