born_normalization
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the sin² form from the J-cost integral.
- Does not extend normalization to three or more branches.
- Does not address non-orthogonal or entangled states.
- Does not compute explicit probability values or thresholds.
Lean usage
theorem use_in_cert (theta : ℝ) : Real.sin theta ^ 2 + Real.cos theta ^ 2 = 1 := born_normalization thetaformal statement (Lean)
100theorem born_normalization (theta : ℝ) :
101 Real.sin theta ^ 2 + Real.cos theta ^ 2 = 1 :=
proof body
Term-mode proof.
102 Real.sin_sq_add_cos_sq theta
103
104/-! ## Mesoscopic Threshold -/
105
106/-- The mesoscopic threshold: the mass at which A ≈ 1 (the transition
107 between quantum coherence and classical behavior).
108
109 m_coh ≈ 0.2 ng = 2e-13 kg for τ ≈ 1 s.
110
111 Below m_coh: quantum superpositions survive (A << 1)
112 Above m_coh: rapid decoherence (A >> 1) -/