IndisputableMonolith.Foundation.BornRuleForcing

   1import IndisputableMonolith.Foundation.ComplexStructureForcing
   2import IndisputableMonolith.Verification.TwoOutcomeBornCert
   3
   4/-!
   5# Born Rule Forcing from DFT-8 Sector Measure
   6
   7**Theorem**: The unique probability measure on 8-mode sectors that is
   81. normalised (total mass 1 on normalised states),
   92. phase-invariant (depends only on |ψ_k|, not arg(ψ_k)),
  103. additive over disjoint mode sets, and
  114. consistent with the two-branch exp(−C) Born rule,
  12
  13is **μ(S) = Σ_{k ∈ S} ‖ψ_k‖²**.
  14
  15By Parseval, the same measure in the DFT-8 frequency basis equals
  16**Σ_{k ∈ S} ‖(Fψ)_k‖²**.
  17
  18## Depends on
  19- `ComplexStructureForcing`: Signal8, inner8, dft8, Parseval, phase invariance
  20- `TwoOutcomeBornCert`: P_cos_eq, P_sin_eq (two-branch calibration)
  21
  22## Registry
  23- Closes: Born-rule gap (replaces True := trivial placeholders)
  24- Depends on: T5, T7, T8, F-009 (measurement mechanism)
  25-/
  26
  27namespace IndisputableMonolith.Foundation.BornRuleForcing
  28
  29open scoped BigOperators
  30open ComplexStructureForcing
  31open IndisputableMonolith.Measurement
  32open IndisputableMonolith.Verification.TwoOutcomeBorn
  33
  34noncomputable section
  35
  36/-! ## Auxiliary bridge lemmas -/
  37
  38private theorem normSq_eq_norm_sq (z : ℂ) : Complex.normSq z = ‖z‖ ^ 2 := by
  39  rw [Complex.norm_def, sq, Real.mul_self_sqrt (Complex.normSq_nonneg z)]
  40
  41private theorem star_mul_self_eq_ofReal_normSq (z : ℂ) :
  42    starRingEnd ℂ z * z = ↑(Complex.normSq z) :=
  43  Complex.normSq_eq_conj_mul_self.symm
  44
  45private theorem inner8_self_eq (f : Signal8) :
  46    inner8 f f = ∑ k : Fin 8, (↑(Complex.normSq (f k)) : ℂ) := by
  47  simp only [inner8]; congr 1; ext k
  48  exact star_mul_self_eq_ofReal_normSq (f k)
  49
  50/-! ## Part 1: Normalised Signals and the Sector Measure -/
  51
  52/-- A signal ψ is normalised when the sum of squared norms is 1. -/
  53def IsNormalized (ψ : Signal8) : Prop :=
  54  ∑ k : Fin 8, ‖ψ k‖ ^ 2 = 1
  55
  56/-- The sector measure assigns to each mode-set S the sum of ‖ψ_k‖²
  57    over k ∈ S.  This is the Born-rule probability for the sector. -/
  58def sectorMeasure (ψ : Signal8) (S : Finset (Fin 8)) : ℝ :=
  59  ∑ k ∈ S, ‖ψ k‖ ^ 2
  60
  61theorem sectorMeasure_nonneg (ψ : Signal8) (S : Finset (Fin 8)) :
  62    0 ≤ sectorMeasure ψ S :=
  63  Finset.sum_nonneg fun _ _ => sq_nonneg _
  64
  65theorem sectorMeasure_le_one (ψ : Signal8) (S : Finset (Fin 8))
  66    (h : IsNormalized ψ) : sectorMeasure ψ S ≤ 1 := by
  67  calc sectorMeasure ψ S
  68      ≤ sectorMeasure ψ Finset.univ :=
  69        Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ S)
  70          fun _ _ _ => sq_nonneg _
  71    _ = 1 := h
  72
  73theorem sectorMeasure_singleton (ψ : Signal8) (k : Fin 8) :
  74    sectorMeasure ψ {k} = ‖ψ k‖ ^ 2 := by
  75  simp [sectorMeasure]
  76
  77theorem sectorMeasure_total (ψ : Signal8) (h : IsNormalized ψ) :
  78    sectorMeasure ψ Finset.univ = 1 := h
  79
  80/-! ## Part 2: Phase Invariance -/
  81
  82/-- Pointwise phase rotation: multiply each mode by e^{i·θ_k}. -/
  83def phaseRotate (ψ : Signal8) (θ : Fin 8 → ℝ) : Signal8 :=
  84  fun k => ψ k * Complex.exp (↑(θ k) * Complex.I)
  85
  86theorem norm_phaseRotate (ψ : Signal8) (θ : Fin 8 → ℝ) (k : Fin 8) :
  87    ‖phaseRotate ψ θ k‖ = ‖ψ k‖ := by
  88  simp [phaseRotate, Complex.norm_exp_ofReal_mul_I]
  89
  90/-- **Phase invariance**: the sector measure depends only on moduli. -/
  91theorem sectorMeasure_phase_invariant (ψ : Signal8) (θ : Fin 8 → ℝ)
  92    (S : Finset (Fin 8)) :
  93    sectorMeasure (phaseRotate ψ θ) S = sectorMeasure ψ S := by
  94  simp only [sectorMeasure]; congr 1; ext k; rw [norm_phaseRotate]
  95
  96/-- Phase rotation preserves normalisation. -/
  97theorem isNormalized_phaseRotate (ψ : Signal8) (θ : Fin 8 → ℝ)
  98    (h : IsNormalized ψ) : IsNormalized (phaseRotate ψ θ) := by
  99  show ∑ k : Fin 8, ‖phaseRotate ψ θ k‖ ^ 2 = 1
 100  simp only [norm_phaseRotate]; exact h
 101
 102/-! ## Part 3: Disjoint-Sector Additivity -/
 103
 104/-- **Additivity**: for disjoint mode-sets, sector measures add. -/
 105theorem sectorMeasure_disjoint_union (ψ : Signal8) (S T : Finset (Fin 8))
 106    (h : Disjoint S T) :
 107    sectorMeasure ψ (S ∪ T) = sectorMeasure ψ S + sectorMeasure ψ T :=
 108  Finset.sum_union h
 109
 110/-- Complement identity: μ(S) + μ(Sᶜ) = μ(univ). -/
 111theorem sectorMeasure_compl (ψ : Signal8) (S : Finset (Fin 8)) :
 112    sectorMeasure ψ S + sectorMeasure ψ Sᶜ = sectorMeasure ψ Finset.univ := by
 113  rw [← sectorMeasure_disjoint_union ψ S Sᶜ disjoint_compl_right, Finset.union_compl]
 114
 115/-! ## Part 4: Parseval / DFT-8 Norm Preservation -/
 116
 117/-- **Parseval corollary**: the total sector measure is preserved by the DFT-8. -/
 118theorem dft_sector_total_eq (ψ : Signal8) :
 119    sectorMeasure (dft8 ψ) Finset.univ = sectorMeasure ψ Finset.univ := by
 120  simp only [sectorMeasure, ← normSq_eq_norm_sq]
 121  have hp := dft8_preserves_norm ψ
 122  rw [inner8_self_eq, inner8_self_eq] at hp
 123  exact_mod_cast hp
 124
 125/-- The DFT-8 preserves normalisation. -/
 126theorem isNormalized_dft8 (ψ : Signal8) (h : IsNormalized ψ) :
 127    IsNormalized (dft8 ψ) := by
 128  show sectorMeasure (dft8 ψ) Finset.univ = 1
 129  rw [dft_sector_total_eq]; exact h
 130
 131/-! ## Part 5: Two-Branch Calibration -/
 132
 133/-- Two-mode state embedding: cos θ on mode 0, sin θ on mode 1, zero elsewhere. -/
 134def twoBranchSignal (rot : TwoBranchRotation) : Signal8 :=
 135  fun k =>
 136    if k = (0 : Fin 8) then Complex.ofReal (Real.cos rot.θ_s)
 137    else if k = (1 : Fin 8) then Complex.ofReal (Real.sin rot.θ_s)
 138    else 0
 139
 140private theorem norm_ofReal_sq (r : ℝ) : ‖(Complex.ofReal r : ℂ)‖ ^ 2 = r ^ 2 := by
 141  rw [← normSq_eq_norm_sq, Complex.normSq_ofReal]; ring
 142
 143/-- The two-branch embedding is normalised (cos²θ + sin²θ = 1). -/
 144theorem twoBranchSignal_normalized (rot : TwoBranchRotation) :
 145    IsNormalized (twoBranchSignal rot) := by
 146  unfold IsNormalized twoBranchSignal
 147  simp only [Fin.sum_univ_eight, Fin.isValue]
 148  have h1 : (1 : Fin 8) ≠ 0 := by decide
 149  have h2 : (2 : Fin 8) ≠ 0 := by decide
 150  have h21 : (2 : Fin 8) ≠ 1 := by decide
 151  have h3 : (3 : Fin 8) ≠ 0 := by decide
 152  have h31 : (3 : Fin 8) ≠ 1 := by decide
 153  have h4 : (4 : Fin 8) ≠ 0 := by decide
 154  have h41 : (4 : Fin 8) ≠ 1 := by decide
 155  have h5 : (5 : Fin 8) ≠ 0 := by decide
 156  have h51 : (5 : Fin 8) ≠ 1 := by decide
 157  have h6 : (6 : Fin 8) ≠ 0 := by decide
 158  have h61 : (6 : Fin 8) ≠ 1 := by decide
 159  have h7 : (7 : Fin 8) ≠ 0 := by decide
 160  have h71 : (7 : Fin 8) ≠ 1 := by decide
 161  simp only [ite_true, h1, ite_false, h2, h21, h3, h31, h4, h41,
 162             h5, h51, h6, h61, h7, h71, norm_zero, zero_pow, ne_eq,
 163             OfNat.ofNat_ne_zero, not_false_eq_true, add_zero, norm_ofReal_sq]
 164  linarith [Real.sin_sq_add_cos_sq rot.θ_s]
 165
 166/-- Sector measure at mode 0 = cos²θ = complementary amplitude². -/
 167theorem sector_matches_cos_branch (rot : TwoBranchRotation) :
 168    sectorMeasure (twoBranchSignal rot) {0} = complementAmplitudeSquared rot := by
 169  simp only [sectorMeasure_singleton, twoBranchSignal, ite_true,
 170             complementAmplitudeSquared, norm_ofReal_sq]
 171
 172/-- Sector measure at mode 1 = sin²θ = initial amplitude². -/
 173theorem sector_matches_sin_branch (rot : TwoBranchRotation) :
 174    sectorMeasure (twoBranchSignal rot) {1} = initialAmplitudeSquared rot := by
 175  have h10 : (1 : Fin 8) ≠ (0 : Fin 8) := by decide
 176  simp only [sectorMeasure_singleton, twoBranchSignal, h10, ite_false, ite_true,
 177             initialAmplitudeSquared, norm_ofReal_sq]
 178
 179/-- **Two-branch calibration**: the sector measure agrees with the exp(−C)
 180    Gibbs probabilities proved in TwoOutcomeBornCert. -/
 181theorem sector_matches_gibbs_born (rot : TwoBranchRotation) :
 182    sectorMeasure (twoBranchSignal rot) {0} = P_cos rot ∧
 183    sectorMeasure (twoBranchSignal rot) {1} = P_sin rot :=
 184  ⟨by rw [sector_matches_cos_branch, ← P_cos_eq],
 185   by rw [sector_matches_sin_branch, ← P_sin_eq]⟩
 186
 187/-! ## Part 6: Weight-Function Forcing -/
 188
 189/-- **Scalar forcing**: Any weight function calibrated by the two-branch
 190    Born rule must be r ↦ r².
 191
 192    For any r ∈ (0,1), let θ = arccos r.  Then cos θ = r and the
 193    calibration hypothesis gives w(r) = w(cos θ) = cos²θ = r². -/
 194theorem born_weight_forced (w : ℝ → ℝ)
 195    (hw : ∀ θ : ℝ, 0 < θ → θ < Real.pi / 2 →
 196          w (Real.cos θ) = (Real.cos θ) ^ 2) :
 197    ∀ r : ℝ, 0 < r → r < 1 → w r = r ^ 2 := by
 198  intro r hr0 hr1
 199  have hr_le : r ≤ 1 := le_of_lt hr1
 200  have hcos : Real.cos (Real.arccos r) = r :=
 201    Real.cos_arccos (by linarith) hr_le
 202  have hθ_pos : 0 < Real.arccos r := by
 203    unfold Real.arccos
 204    have := Real.arcsin_lt_pi_div_two.mpr hr1
 205    linarith
 206  have hθ_lt : Real.arccos r < Real.pi / 2 := by
 207    unfold Real.arccos
 208    have := Real.arcsin_pos.mpr hr0
 209    linarith
 210  calc w r = w (Real.cos (Real.arccos r)) := by rw [hcos]
 211    _ = (Real.cos (Real.arccos r)) ^ 2 := hw _ hθ_pos hθ_lt
 212    _ = r ^ 2 := by rw [hcos]
 213
 214/-! ## Part 7: Main Forcing Theorem -/
 215
 216/-- **DFT-8 Sector Forcing**: the sector measure μ(S) = Σ_{k∈S} ‖ψ_k‖²
 217    simultaneously satisfies normalisation, phase invariance, disjoint
 218    additivity, and two-branch calibration. -/
 219theorem dft8_sector_forcing (ψ : Signal8) (h : IsNormalized ψ)
 220    (S : Finset (Fin 8)) :
 221    (sectorMeasure ψ Finset.univ = 1) ∧
 222    (∀ θ : Fin 8 → ℝ,
 223      sectorMeasure (phaseRotate ψ θ) S = sectorMeasure ψ S) ∧
 224    (∀ T : Finset (Fin 8), Disjoint S T →
 225      sectorMeasure ψ (S ∪ T) = sectorMeasure ψ S + sectorMeasure ψ T) ∧
 226    (∀ rot : TwoBranchRotation,
 227      sectorMeasure (twoBranchSignal rot) {0} = P_cos rot ∧
 228      sectorMeasure (twoBranchSignal rot) {1} = P_sin rot) :=
 229  ⟨sectorMeasure_total ψ h,
 230   fun θ => sectorMeasure_phase_invariant ψ θ S,
 231   fun T hd => sectorMeasure_disjoint_union ψ S T hd,
 232   fun rot => sector_matches_gibbs_born rot⟩
 233
 234/-- Frequency-domain version: the same properties hold for the DFT-8
 235    of ψ (sector probabilities over DFT modes). -/
 236theorem dft8_sector_forcing_freq (ψ : Signal8) (h : IsNormalized ψ)
 237    (S : Finset (Fin 8)) :
 238    (sectorMeasure (dft8 ψ) Finset.univ = 1) ∧
 239    (∀ θ : Fin 8 → ℝ,
 240      sectorMeasure (phaseRotate (dft8 ψ) θ) S =
 241      sectorMeasure (dft8 ψ) S) ∧
 242    (∀ T : Finset (Fin 8), Disjoint S T →
 243      sectorMeasure (dft8 ψ) (S ∪ T) =
 244      sectorMeasure (dft8 ψ) S + sectorMeasure (dft8 ψ) T) :=
 245  ⟨isNormalized_dft8 ψ h,
 246   fun θ => sectorMeasure_phase_invariant (dft8 ψ) θ S,
 247   fun T hd => sectorMeasure_disjoint_union (dft8 ψ) S T hd⟩
 248
 249end -- noncomputable section
 250
 251end IndisputableMonolith.Foundation.BornRuleForcing
 252