born_normalization

formal source

  97/-- Born rule: probability = |amplitude|² = exp(-C) / Σ exp(-C_J).
  98    For the special case of two orthogonal branches (θ₁ + θ₂ = π/2):
  99    P₁ = sin²θ₁, P₂ = cos²θ₁ = sin²θ₂, P₁ + P₂ = 1. -/
 100theorem born_normalization (theta : ℝ) :
 101    Real.sin theta ^ 2 + Real.cos theta ^ 2 = 1 :=
 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) -/
 113def m_coh_kg : ℝ := 2e-13
 114
 115def tau_coh_s : ℝ := 1
 116
 117theorem m_coh_positive : 0 < m_coh_kg := by unfold m_coh_kg; norm_num
 118
 119/-- The threshold is in the nanogram range — accessible to
 120    optomechanical experiments (Aspelmeyer, Romero-Isart). -/
 121theorem m_coh_nanogram_range : m_coh_kg < 1e-9 ∧ m_coh_kg > 1e-15 := by
 122  unfold m_coh_kg; constructor <;> norm_num
 123
 124/-! ## Distinguishing Predictions -/
 125
 126/-- RS prediction: collapse rate PLATEAUS after orthogonality (A → const).
 127    Penrose-Diósi: collapse rate continues growing with 1/d tail.
 128    This is a sharp distinguisher. -/
 129def post_orthogonality_plateau : Prop :=
 130  ∀ theta : ℝ, Real.pi / 2 ≤ theta → theta ≤ Real.pi →