born_normalization
plain-language theorem explainer
The identity sin²θ + cos²θ = 1 supplies the normalization for Born-rule probabilities in the two-orthogonal-branch case of the coherence-collapse model. Researchers deriving quantum measurement from recognition cost C = 2A would cite it to confirm that sin²θ and cos²θ sum to unity when phases are orthogonal. The proof is a direct one-line application of the standard trigonometric identity.
Claim. For any real number θ, sin²θ + cos²θ = 1.
background
The module formalizes the bridge from gravitational coherence collapse to the Born rule via recognition action C[γ] = ∫ J(r(t)) dt and residual rate action A = -ln(sin θ_s). The central claim is C = 2A, from which Born probabilities emerge as P(I) = exp(-C_I)/Σ exp(-C_J) = |α_I|². For two orthogonal branches with θ₁ + θ₂ = π/2 the probabilities reduce to sin²θ and cos²θ. Upstream results supply A as the active-edge count per tick (IntegrationGap.A and Masses.Anchor.A) and the actualization operator that selects the realized configuration (Modal.Actualization.A).
proof idea
One-line wrapper that applies the Mathlib identity Real.sin_sq_add_cos_sq to the supplied real angle theta.
why it matters
The result is invoked inside coherence_collapse_cert to discharge the normalization field of the CoherenceCollapseCert structure. It completes the two-branch case of the Born-rule emergence stated in the module doc-comment, consistent with the framework's derivation of |α|² from recognition cost. It supports the mesoscopic threshold discussion (m_coh ≈ 0.2 ng) where A ≈ 1 separates coherent and classical regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.