born_weight_pos

formal source

  80noncomputable def born_weight (C_I : ℝ) : ℝ := Real.exp (-C_I)
  81
  82/-- Born weight is positive. -/
  83theorem born_weight_pos (C_I : ℝ) : 0 < born_weight C_I := Real.exp_pos _
  84
  85/-- For the C = 2A case: born_weight = sin²(θ_s).
  86    This follows from exp(-2A) = exp(2 ln sin θ) = sin²θ. -/
  87theorem born_weight_is_sin_sq (theta_s : ℝ) (h_sin_pos : 0 < Real.sin theta_s) :
  88    born_weight (recognition_action theta_s) =
  89    (Real.sin theta_s) ^ 2 := by
  90  unfold born_weight recognition_action rate_action
  91  rw [show -(2 * -Real.log (Real.sin theta_s)) = 2 * Real.log (Real.sin theta_s) from by ring]
  92  rw [show (2 : ℝ) * Real.log (Real.sin theta_s) =
  93      Real.log ((Real.sin theta_s) ^ 2) from by
  94    rw [Real.log_pow]; ring]
  95  rw [Real.exp_log (sq_pos_of_pos h_sin_pos)]
  96
  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