IndisputableMonolith.Verification.TwoOutcomeBornCert

   1import Mathlib
   2import IndisputableMonolith.Measurement.C2ABridge
   3import IndisputableMonolith.Measurement.TwoBranchGeodesic
   4
   5/-!
   6# Two-Outcome Born Certificate (normalized probabilities)
   7
   8This module upgrades the two-branch measurement bridge from a weight identity
   9(`pathWeight = sin² θ`) to **normalized two-outcome probabilities**:
  10
  11- `P_cos = exp(-C_cos) / (exp(-C_cos) + exp(-C_sin)) = cos² θ`
  12- `P_sin = exp(-C_sin) / (exp(-C_cos) + exp(-C_sin)) = sin² θ`
  13
  14where:
  15- `C_sin` is the *recognition action* `pathAction (pathFromRotation rot)` (so `exp(-C_sin)` is the RS path weight),
  16- `C_cos` is the complementary action `-2 log(cos θ)` whose weight is `cos² θ`.
  17
  18This avoids any “measurement axioms” typeclass entirely and relies only on the proven bridge theorems
  19in `Measurement/C2ABridge.lean` and elementary trigonometric identities.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Verification
  24namespace TwoOutcomeBorn
  25
  26open IndisputableMonolith.Measurement
  27open Real
  28
  29/-- Complementary action producing `exp(-C_cos) = cos²(θ_s)`. -/
  30noncomputable def C_cos (rot : TwoBranchRotation) : ℝ :=
  31  -2 * Real.log (Real.cos rot.θ_s)
  32
  33/-- RS action producing `exp(-C_sin) = sin²(θ_s)` via the measurement bridge. -/
  34noncomputable def C_sin (rot : TwoBranchRotation) : ℝ :=
  35  Measurement.pathAction (Measurement.pathFromRotation rot)
  36
  37/-- Normalized probability for the cos-branch. -/
  38noncomputable def P_cos (rot : TwoBranchRotation) : ℝ :=
  39  Real.exp (- C_cos rot) /
  40    (Real.exp (- C_cos rot) + Real.exp (- C_sin rot))
  41
  42/-- Normalized probability for the sin-branch. -/
  43noncomputable def P_sin (rot : TwoBranchRotation) : ℝ :=
  44  Real.exp (- C_sin rot) /
  45    (Real.exp (- C_cos rot) + Real.exp (- C_sin rot))
  46
  47lemma exp_neg_C_cos_eq (rot : TwoBranchRotation) :
  48    Real.exp (- C_cos rot) = Measurement.complementAmplitudeSquared rot := by
  49  -- Same pattern as `born_weight_from_rate`, but for `cos`.
  50  unfold C_cos Measurement.complementAmplitudeSquared
  51  have hcos_pos : 0 < Real.cos rot.θ_s := by
  52    -- θ_s ∈ (0, π/2) ⇒ θ_s ∈ (-π/2, π/2) ⇒ cos θ_s > 0
  53    refine Real.cos_pos_of_mem_Ioo ?_
  54    refine ⟨?_, rot.θ_s_bounds.2⟩
  55    have hpi2 : (0 : ℝ) < Real.pi / 2 := by nlinarith [Real.pi_pos]
  56    linarith [rot.θ_s_bounds.1, hpi2]
  57  calc
  58    Real.exp (-(-2 * Real.log (Real.cos rot.θ_s)))
  59        = Real.exp (2 * Real.log (Real.cos rot.θ_s)) := by ring_nf
  60    _ = Real.exp (Real.log ((Real.cos rot.θ_s) ^ 2)) := by
  61        congr 1
  62        exact (Real.log_pow (Real.cos rot.θ_s) 2).symm
  63    _ = (Real.cos rot.θ_s) ^ 2 := Real.exp_log (pow_pos hcos_pos 2)
  64
  65lemma exp_neg_C_sin_eq (rot : TwoBranchRotation) :
  66    Real.exp (- C_sin rot) = Measurement.initialAmplitudeSquared rot := by
  67  -- `pathWeight = exp(-pathAction)` and `weight_equals_born` gives `pathWeight = sin²`.
  68  have h := Measurement.weight_equals_born rot
  69  simpa [Measurement.pathWeight, C_sin] using h
  70
  71theorem P_cos_eq (rot : TwoBranchRotation) :
  72    P_cos rot = Measurement.complementAmplitudeSquared rot := by
  73  unfold P_cos
  74  rw [exp_neg_C_cos_eq rot, exp_neg_C_sin_eq rot]
  75  -- cos² / (cos² + sin²) = cos²
  76  simp [Measurement.initialAmplitudeSquared, Measurement.complementAmplitudeSquared,
  77    Real.cos_sq_add_sin_sq rot.θ_s]
  78
  79theorem P_sin_eq (rot : TwoBranchRotation) :
  80    P_sin rot = Measurement.initialAmplitudeSquared rot := by
  81  unfold P_sin
  82  rw [exp_neg_C_cos_eq rot, exp_neg_C_sin_eq rot]
  83  -- sin² / (cos² + sin²) = sin²
  84  simp [Measurement.initialAmplitudeSquared, Measurement.complementAmplitudeSquared,
  85    Real.cos_sq_add_sin_sq rot.θ_s]
  86
  87structure TwoOutcomeBornCert where
  88  deriving Repr
  89
  90/-- Verification predicate: the normalized two-outcome probabilities match cos²/sin². -/
  91@[simp] def TwoOutcomeBornCert.verified (_c : TwoOutcomeBornCert) : Prop :=
  92  ∀ rot : TwoBranchRotation,
  93    P_cos rot = Measurement.complementAmplitudeSquared rot
  94      ∧ P_sin rot = Measurement.initialAmplitudeSquared rot
  95
  96@[simp] theorem TwoOutcomeBornCert.verified_any (c : TwoOutcomeBornCert) :
  97    TwoOutcomeBornCert.verified c := by
  98  intro rot
  99  exact ⟨P_cos_eq rot, P_sin_eq rot⟩
 100
 101end TwoOutcomeBorn
 102end Verification
 103end IndisputableMonolith
 104