IndisputableMonolith.Gravity.SevenGaps.ZqPhaseStructure

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.QuotientFirstZ
   3import IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
   4
   5/-!
   6# Seven Gaps, Lane D3: phase structure on the quotient-first path sum
   7
   8## What this module proves
   9
  10**Status: THEOREM (structure theorems at fixed complexity cap; the
  11continuum limit stays OPEN).**  On the quotient-first object
  12`QuotientFirstZ.Zq` this module adds an explicit oscillatory phase model
  13and proves:
  14
  15* `PhaseModel`: an explicit phase structure, a real phase function on
  16  LABELED configurations together with the stated relabeling-invariance
  17  property, which therefore descends to `TriangulationClass`
  18  (`classPhase`).  The phased weight `exp(i*phase)` has unit modulus
  19  (`phasedWeight_norm`).
  20* **Boundedness / well-definedness at fixed cap** (`Zq_norm_le_totalClassMass`,
  21  `Zq_phased_wellDefined`): for every phase model the phased `Zq` is a
  22  finite sum with the proved modulus bound `‖Zq‖ <= totalClassMass B <=
  23  card(TriangulationClass B)`.
  24* **Conditional cancellation** (`Zq_pairing_decomposition`,
  25  `Zq_pairing_bound`, `Zq_pairing_beats_triangle`): under a STATED
  26  pairing hypothesis (an injection `j` from a subfamily `s` of classes to
  27  classes outside `s` whose measured summands are exactly opposite), the
  28  paired contributions cancel EXACTLY and the modulus bound improves to
  29  `totalClassMass - pairedMass`, STRICTLY better than the triangle
  30  inequality whenever the paired family is nonempty.  These general
  31  theorems are finite-sum arithmetic under the exact-opposite hypothesis;
  32  the cancellation MECHANISM is not derived here, it is supplied by the
  33  hypothesis and discharged concretely by the `B = 2` witness below.
  34* **Two-term phase-pairing arithmetic** (`opposite_phase_pair_cancels`,
  35  `opposite_phase_pair_strict`): equal masses at phases `θ` and `θ + π`
  36  cancel exactly; the triangle inequality is strict there.
  37* **Non-vacuity witness at `B = 2`** (`phased_Zq_pairing_witness`,
  38  `phased_Zq_beats_triangle_witness`): an EXPLICIT phase model (phase 0
  39  on the vertex-free class, phase π elsewhere) whose pairing hypotheses
  40  are DISCHARGED concretely on the empty-complex class and the one-point
  41  class (both of unit symmetry factor, proved), giving the kernel chain
  42  `‖Zq 2 (phasedWeight witnessPhaseModel)‖ <= totalClassMass 2 - 2 <
  43  totalClassMass 2` (single theorem `phased_Zq_witness_chain`), with
  44  `2 <= totalClassMass 2` proved (`two_le_totalClassMass_two`) so the
  45  improved bound is nonnegative and meaningful.  The pairing hypotheses
  46  are therefore satisfiable, not vacuous.
  47
  48## What this module does NOT prove (binding honesty disclosures)
  49
  50* These are STRUCTURE theorems at a FIXED complexity cap `B`.  They are
  51  NOT `Z_RS_continuum_limit`; the continuum limit stays OPEN, and the
  52  complexity cutoff is NOT mesh refinement (standing constraint).
  53* The zero-phase route to regulator removal is DEAD
  54  (`RegulatorRemovalNoGo.not_hasZRSRegulatorRemoval_zeroPhase`, on the
  55  exact-shell quotient object): any well-defined removal needs phase
  56  cancellation.  This module supplies proved cancellation mechanisms at
  57  fixed cap only; it does NOT prove regulator removal or any limit for
  58  any phase.
  59* `Zq` is the QUOTIENT-first convention.  It is never silently equated
  60  with the LABELED `PathSumMeasure.Z`: the exact bridge carries the
  61  labeled fiber factor (`QuotientFirstZ.labeledZ_eq_Zq_plus_fiberExcess`),
  62  and nothing here bypasses it.
  63* The general pairing theorems carry their pairing hypotheses explicitly;
  64  the `B = 2` witness discharges them in one concrete instance and makes
  65  no claim that pairings exist for every phase model or every cap.
  66
  67## Status tiers (honest tagging)
  68
  69**THEOREM (proved below, 0 sorry, 0 new axioms, no `native_decide`):**
  70`Zq_norm_le_totalClassMass`, `Zq_phased_wellDefined`,
  71`Zq_pairing_decomposition`, `Zq_pairing_bound`,
  72`Zq_pairing_beats_triangle`, `opposite_phase_pair_cancels`,
  73`opposite_phase_pair_strict`, `mu_onePointComplex`,
  74`phased_Zq_pairing_witness`, `phased_Zq_beats_triangle_witness`,
  75`two_le_totalClassMass_two`, `phased_Zq_witness_chain`.
  76
  77**MODEL (definitional):** the `PhaseModel` shape itself (a real phase
  78function with relabeling invariance) and the `1/|Aut|` measure inherited
  79from `PathSumMeasure`.
  80
  81**OPEN (recorded, never claimed):** the continuum limit of the phased
  82`Zq`; regulator removal at any oscillatory phase; a substrate-derived
  83phase function.
  84
  85Expected axiom footprint: standard trio
  86`[propext, Classical.choice, Quot.sound]`.
  87-/
  88
  89namespace IndisputableMonolith
  90namespace Gravity
  91namespace SevenGaps
  92namespace ZqPhaseStructure
  93
  94open PathSumMeasure
  95open FiniteQuotient
  96open QuotientFirstZ
  97
  98/-! ## §1. The explicit phase model -/
  99
 100/-- An explicit oscillatory phase model on the scoped configuration
 101class: a real phase on LABELED configurations with the STATED property of
 102relabeling invariance.  MODEL: the phase function itself is an input; a
 103substrate-derived phase is OPEN. -/
 104structure PhaseModel (B : ℕ) where
 105  phase : BoundedComplex B → ℝ
 106  invariant : ∀ K K' : BoundedComplex B, Equivalent K K' → phase K = phase K'
 107
 108/-- The phase descends to the quotient: a well-defined phase on
 109triangulation classes (this is where the stated invariance is used). -/
 110def classPhase {B : ℕ} (P : PhaseModel B) : TriangulationClass B → ℝ :=
 111  Quotient.lift P.phase (fun K K' h => P.invariant K K' h)
 112
 113/-- Descent computes on representatives. -/
 114theorem classPhase_mk {B : ℕ} (P : PhaseModel B) (K : BoundedComplex B) :
 115    classPhase P (Quotient.mk (relabelSetoid B) K) = P.phase K := rfl
 116
 117/-- The unitary class weight of a phase model. -/
 118noncomputable def phasedWeight {B : ℕ} (P : PhaseModel B) :
 119    TriangulationClass B → ℂ :=
 120  fun q => Complex.exp (Complex.I * (classPhase P q : ℂ))
 121
 122/-- **THEOREM.**  The phased weight has modulus exactly 1. -/
 123theorem phasedWeight_norm {B : ℕ} (P : PhaseModel B)
 124    (q : TriangulationClass B) : ‖phasedWeight P q‖ = 1 :=
 125  Complex.norm_exp_I_mul_ofReal _
 126
 127/-! ## §2. Boundedness of the phased Zq at fixed complexity cap -/
 128
 129/-- The total per-class mass at cap `B`: the quotient-side triangle bound
 130for unit-modulus weights. -/
 131noncomputable def totalClassMass (B : ℕ) : ℝ :=
 132  ∑ q : TriangulationClass B, mu (Quotient.out q)
 133
 134/-- The total class mass is strictly positive (the empty-complex class is
 135always present). -/
 136theorem totalClassMass_pos (B : ℕ) : 0 < totalClassMass B := by
 137  unfold totalClassMass
 138  refine Finset.sum_pos (fun q _ => mu_pos _) ?_
 139  exact ⟨Quotient.mk (relabelSetoid B) (emptyComplex B), Finset.mem_univ _⟩
 140
 141/-- The total class mass is bounded by the class count. -/
 142theorem totalClassMass_le_card (B : ℕ) :
 143    totalClassMass B ≤ (Fintype.card (TriangulationClass B) : ℝ) := by
 144  unfold totalClassMass
 145  calc ∑ q : TriangulationClass B, mu (Quotient.out q)
 146      ≤ ∑ _q : TriangulationClass B, (1 : ℝ) :=
 147        Finset.sum_le_sum fun q _ => mu_le_one _
 148    _ = (Fintype.card (TriangulationClass B) : ℝ) := by
 149        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
 150
 151/-- **THEOREM (triangle bound for Zq).**  For any weight of modulus at
 152most 1, the quotient-first path sum is bounded by the total class mass. -/
 153theorem Zq_norm_le_totalClassMass (B : ℕ) (wq : TriangulationClass B → ℂ)
 154    (hw : ∀ q, ‖wq q‖ ≤ 1) :
 155    ‖Zq B wq‖ ≤ totalClassMass B := by
 156  show ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖ ≤ _
 157  calc ‖∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q‖
 158      ≤ ∑ q : TriangulationClass B, ‖(mu (Quotient.out q) : ℂ) * wq q‖ :=
 159        norm_sum_le _ _
 160    _ ≤ ∑ q : TriangulationClass B, mu (Quotient.out q) := by
 161        refine Finset.sum_le_sum fun q _ => ?_
 162        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
 163          abs_of_pos (mu_pos _)]
 164        exact mul_le_of_le_one_right (mu_pos _).le (hw q)
 165    _ = totalClassMass B := rfl
 166
 167/-- **THEOREM (well-definedness of the phased Zq at fixed cap).**  For
 168every phase model, the phased quotient-first path sum has unit-modulus
 169weights and satisfies the proved finiteness bounds.  This is a structure
 170theorem at fixed complexity cap, NOT a continuum-limit statement. -/
 171theorem Zq_phased_wellDefined (B : ℕ) (P : PhaseModel B) :
 172    (∀ q, ‖phasedWeight P q‖ = 1) ∧
 173    ‖Zq B (phasedWeight P)‖ ≤ totalClassMass B ∧
 174    ‖Zq B (phasedWeight P)‖ ≤ (Fintype.card (TriangulationClass B) : ℝ) := by
 175  have hb := Zq_norm_le_totalClassMass B (phasedWeight P)
 176    (fun q => le_of_eq (phasedWeight_norm P q))
 177  exact ⟨phasedWeight_norm P, hb, le_trans hb (totalClassMass_le_card B)⟩
 178
 179/-! ## §3. The pairing cancellation theorems
 180
 181A pairing is an injection `j` from a subfamily `s` of classes to classes
 182OUTSIDE `s` whose measured summands are exactly opposite.  Under this
 183STATED hypothesis the paired contributions cancel exactly, and the
 184modulus bound strictly beats the triangle inequality.  These are
 185finite-sum arithmetic theorems conditional on the exact-opposite
 186hypothesis; they do not derive a pairing, and §5 discharges the
 187hypothesis in one concrete instance. -/
 188
 189/-- **THEOREM (exact pairing cancellation).**  Under the pairing
 190hypothesis, `Zq` equals the sum over the UNPAIRED classes only: the
 191paired contributions cancel exactly. -/
 192theorem Zq_pairing_decomposition (B : ℕ) (wq : TriangulationClass B → ℂ)
 193    (s : Finset (TriangulationClass B))
 194    (j : TriangulationClass B → TriangulationClass B)
 195    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
 196    (hdisj : ∀ q ∈ s, j q ∉ s)
 197    (hcancel : ∀ q ∈ s,
 198      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
 199        = -((mu (Quotient.out q) : ℂ) * wq q)) :
 200    Zq B wq = ∑ q ∈ Finset.univ \ (s ∪ s.image j),
 201      (mu (Quotient.out q) : ℂ) * wq q := by
 202  have hdisjoint : Disjoint s (s.image j) := by
 203    rw [Finset.disjoint_right]
 204    intro a ha
 205    obtain ⟨q, hq, rfl⟩ := Finset.mem_image.mp ha
 206    exact hdisj q hq
 207  have hpair : ∑ q ∈ s ∪ s.image j,
 208      (mu (Quotient.out q) : ℂ) * wq q = 0 := by
 209    rw [Finset.sum_union hdisjoint, Finset.sum_image hinj,
 210      Finset.sum_congr rfl hcancel, Finset.sum_neg_distrib, add_neg_cancel]
 211  have hsplit := Finset.sum_sdiff
 212    (f := fun q => (mu (Quotient.out q) : ℂ) * wq q)
 213    (Finset.subset_univ (s ∪ s.image j))
 214  calc Zq B wq
 215      = ∑ q ∈ Finset.univ, (mu (Quotient.out q) : ℂ) * wq q := rfl
 216    _ = ∑ q ∈ Finset.univ \ (s ∪ s.image j),
 217          (mu (Quotient.out q) : ℂ) * wq q
 218        + ∑ q ∈ s ∪ s.image j, (mu (Quotient.out q) : ℂ) * wq q :=
 219        hsplit.symm
 220    _ = ∑ q ∈ Finset.univ \ (s ∪ s.image j),
 221          (mu (Quotient.out q) : ℂ) * wq q := by
 222        rw [hpair, add_zero]
 223
 224/-- **THEOREM (pairing bound).**  Under the pairing hypothesis, the
 225modulus bound improves from the triangle bound `totalClassMass` to
 226`totalClassMass - pairedMass`. -/
 227theorem Zq_pairing_bound (B : ℕ) (wq : TriangulationClass B → ℂ)
 228    (hw : ∀ q, ‖wq q‖ ≤ 1)
 229    (s : Finset (TriangulationClass B))
 230    (j : TriangulationClass B → TriangulationClass B)
 231    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
 232    (hdisj : ∀ q ∈ s, j q ∉ s)
 233    (hcancel : ∀ q ∈ s,
 234      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
 235        = -((mu (Quotient.out q) : ℂ) * wq q)) :
 236    ‖Zq B wq‖ ≤ totalClassMass B
 237      - ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) := by
 238  rw [Zq_pairing_decomposition B wq s j hinj hdisj hcancel]
 239  have hrest : ∑ q ∈ Finset.univ \ (s ∪ s.image j), mu (Quotient.out q)
 240      = totalClassMass B - ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) :=
 241    eq_sub_of_add_eq (Finset.sum_sdiff (Finset.subset_univ _))
 242  calc ‖∑ q ∈ Finset.univ \ (s ∪ s.image j),
 243        (mu (Quotient.out q) : ℂ) * wq q‖
 244      ≤ ∑ q ∈ Finset.univ \ (s ∪ s.image j),
 245          ‖(mu (Quotient.out q) : ℂ) * wq q‖ := norm_sum_le _ _
 246    _ ≤ ∑ q ∈ Finset.univ \ (s ∪ s.image j), mu (Quotient.out q) := by
 247        refine Finset.sum_le_sum fun q _ => ?_
 248        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs,
 249          abs_of_pos (mu_pos _)]
 250        exact mul_le_of_le_one_right (mu_pos _).le (hw q)
 251    _ = totalClassMass B - ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) :=
 252        hrest
 253
 254/-- **THEOREM (strictly better than the triangle inequality).**  Under the
 255pairing hypothesis with a NONEMPTY paired family, the phased `Zq` is
 256STRICTLY below the triangle bound `totalClassMass`. -/
 257theorem Zq_pairing_beats_triangle (B : ℕ) (wq : TriangulationClass B → ℂ)
 258    (hw : ∀ q, ‖wq q‖ ≤ 1)
 259    (s : Finset (TriangulationClass B))
 260    (j : TriangulationClass B → TriangulationClass B)
 261    (hinj : ∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q')
 262    (hdisj : ∀ q ∈ s, j q ∉ s)
 263    (hcancel : ∀ q ∈ s,
 264      (mu (Quotient.out (j q)) : ℂ) * wq (j q)
 265        = -((mu (Quotient.out q) : ℂ) * wq q))
 266    (hne : s.Nonempty) :
 267    ‖Zq B wq‖ < totalClassMass B := by
 268  have hb := Zq_pairing_bound B wq hw s j hinj hdisj hcancel
 269  have hpos : 0 < ∑ q ∈ s ∪ s.image j, mu (Quotient.out q) := by
 270    obtain ⟨q0, hq0⟩ := hne
 271    exact Finset.sum_pos (fun q _ => mu_pos _)
 272      ⟨q0, Finset.mem_union_left _ hq0⟩
 273  linarith
 274
 275/-! ## §4. Two-term phase-pairing arithmetic -/
 276
 277/-- Advancing a phase by π negates the unitary weight. -/
 278theorem opposite_phase_exp (θ : ℝ) :
 279    Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))
 280      = -Complex.exp (Complex.I * (θ : ℂ)) := by
 281  rw [Complex.ofReal_add, mul_add, Complex.exp_add,
 282    mul_comm Complex.I (Real.pi : ℂ), Complex.exp_pi_mul_I, mul_neg_one]
 283
 284/-- **THEOREM (two-term exact cancellation).**  Equal masses at phases
 285`θ` and `θ + π` cancel exactly. -/
 286theorem opposite_phase_pair_cancels (m θ : ℝ) :
 287    (m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))
 288      + (m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ)) = 0 := by
 289  rw [opposite_phase_exp, mul_neg, add_neg_cancel]
 290
 291/-- **THEOREM (two-term strict improvement).**  For positive mass the
 292paired two-term sum is STRICTLY below its triangle bound. -/
 293theorem opposite_phase_pair_strict (m θ : ℝ) (hm : 0 < m) :
 294    ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))
 295        + (m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖
 296      < ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))‖
 297        + ‖(m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖ := by
 298  rw [opposite_phase_pair_cancels, norm_zero]
 299  have h1 : ‖(m : ℂ) * Complex.exp (Complex.I * (θ : ℂ))‖ = m := by
 300    rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm,
 301      Complex.norm_exp_I_mul_ofReal, mul_one]
 302  have h2 : ‖(m : ℂ) * Complex.exp (Complex.I * ((θ + Real.pi : ℝ) : ℂ))‖
 303      = m := by
 304    rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hm,
 305      Complex.norm_exp_I_mul_ofReal, mul_one]
 306  rw [h1, h2]
 307  linarith
 308
 309/-! ## §5. The non-vacuity witness at B = 2
 310
 311The pairing hypotheses of §3 are satisfiable: an explicit phase model at
 312`B = 2` pairs the empty-complex class (phase 0) with the one-point class
 313(phase π).  Both classes carry unit symmetry factor (proved), so the
 314measured summands are exactly opposite and the paired mass is exactly 2. -/
 315
 316/-- The one-point configuration at cap 2 (one vertex, no incidence).
 317(`abbrev` so the size fields reduce during elaboration.) -/
 318abbrev onePointComplex : BoundedComplex 2 where
 319  nV := 1
 320  nE := 0
 321  nT := 0
 322  hV := one_le_two
 323  hE := Nat.zero_le 2
 324  hT := Nat.zero_le 2
 325  edgeVerts := fun e => e.elim0
 326  tetVerts := fun t => t.elim0
 327
 328/-- The automorphism group of the one-point configuration is trivial:
 329the vertex index type `Fin 1` is a subsingleton and the other index types
 330are empty. -/
 331instance instSubsingletonAutOnePoint : Subsingleton (Aut onePointComplex) :=
 332  ⟨fun _a _b => Relabel.ext
 333    (Equiv.ext fun _x => Subsingleton.elim _ _)
 334    (Equiv.ext fun x => x.elim0)
 335    (Equiv.ext fun x => x.elim0)⟩
 336
 337/-- **THEOREM.**  The one-point configuration has unit symmetry factor. -/
 338theorem mu_onePointComplex : mu onePointComplex = 1 := by
 339  unfold mu
 340  rw [Nat.card_unique]
 341  norm_num
 342
 343/-- The empty-complex class at cap 2. -/
 344def emptyClass : TriangulationClass 2 :=
 345  Quotient.mk (relabelSetoid 2) (emptyComplex 2)
 346
 347/-- The one-point class at cap 2. -/
 348def pointClass : TriangulationClass 2 :=
 349  Quotient.mk (relabelSetoid 2) onePointComplex
 350
 351/-- The two witness classes are distinct (no bijection `Fin 0 ≃ Fin 1`). -/
 352theorem emptyClass_ne_pointClass : emptyClass ≠ pointClass := by
 353  intro h
 354  have hequiv : Equivalent (emptyComplex 2) onePointComplex :=
 355    Quotient.exact h
 356  obtain ⟨r⟩ := hequiv
 357  exact Fin.elim0 (r.vEquiv.symm ⟨0, Nat.succ_pos 0⟩)
 358
 359/-- The representative symmetry factor of the empty-complex class is 1. -/
 360theorem mu_out_emptyClass : mu (Quotient.out emptyClass) = 1 := by
 361  rw [mu_out_eq_of_mk_eq (K := emptyComplex 2) emptyClass rfl]
 362  exact MeasureInvarianceNoGo.mu_emptyComplex 2
 363
 364/-- The representative symmetry factor of the one-point class is 1. -/
 365theorem mu_out_pointClass : mu (Quotient.out pointClass) = 1 := by
 366  rw [mu_out_eq_of_mk_eq (K := onePointComplex) pointClass rfl]
 367  exact mu_onePointComplex
 368
 369/-- The explicit witness phase model at `B = 2`: phase 0 on vertex-free
 370configurations, phase π otherwise.  The vertex count is a relabeling
 371invariant, so the stated invariance property holds. -/
 372noncomputable def witnessPhaseModel : PhaseModel 2 where
 373  phase K := if K.nV = 0 then 0 else Real.pi
 374  invariant K K' h := by
 375    obtain ⟨r⟩ := h
 376    have hnV : K.nV = K'.nV := Fin.equiv_iff_eq.mp ⟨r.vEquiv⟩
 377    rw [hnV]
 378
 379/-- The witness weight on the empty-complex class is `+1`. -/
 380theorem phasedWeight_emptyClass :
 381    phasedWeight witnessPhaseModel emptyClass = 1 := by
 382  have hph : classPhase witnessPhaseModel emptyClass = 0 := by
 383    show (if (emptyComplex 2).nV = 0 then (0 : ℝ) else Real.pi) = 0
 384    rw [if_pos (show (emptyComplex 2).nV = 0 from rfl)]
 385  show Complex.exp (Complex.I * (classPhase witnessPhaseModel emptyClass : ℂ))
 386      = 1
 387  rw [hph, Complex.ofReal_zero, mul_zero, Complex.exp_zero]
 388
 389/-- The witness weight on the one-point class is `-1`. -/
 390theorem phasedWeight_pointClass :
 391    phasedWeight witnessPhaseModel pointClass = -1 := by
 392  have hph : classPhase witnessPhaseModel pointClass = Real.pi := by
 393    show (if onePointComplex.nV = 0 then (0 : ℝ) else Real.pi) = Real.pi
 394    rw [if_neg Nat.one_ne_zero]
 395  show Complex.exp (Complex.I * (classPhase witnessPhaseModel pointClass : ℂ))
 396      = -1
 397  rw [hph, mul_comm Complex.I (Real.pi : ℂ), Complex.exp_pi_mul_I]
 398
 399/-- The witness pairing family: the empty-complex class alone. -/
 400def witnessPaired : Finset (TriangulationClass 2) := {emptyClass}
 401
 402/-- The witness pairing map: everything to the one-point class. -/
 403def witnessPairing : TriangulationClass 2 → TriangulationClass 2 :=
 404  fun _ => pointClass
 405
 406/-- The witness pairing is injective on the paired family. -/
 407theorem witnessPairing_injOn : ∀ q ∈ witnessPaired, ∀ q' ∈ witnessPaired,
 408    witnessPairing q = witnessPairing q' → q = q' := by
 409  intro q hq q' hq' _
 410  rw [witnessPaired, Finset.mem_singleton] at hq hq'
 411  rw [hq, hq']
 412
 413/-- The witness pairing lands outside the paired family. -/
 414theorem witnessPairing_disj : ∀ q ∈ witnessPaired,
 415    witnessPairing q ∉ witnessPaired := by
 416  intro q _ hmem
 417  rw [witnessPaired, Finset.mem_singleton] at hmem
 418  exact emptyClass_ne_pointClass hmem.symm
 419
 420/-- The witness pairing cancels exactly: unit mass at phase π against
 421unit mass at phase 0. -/
 422theorem witnessPairing_cancel : ∀ q ∈ witnessPaired,
 423    (mu (Quotient.out (witnessPairing q)) : ℂ)
 424        * phasedWeight witnessPhaseModel (witnessPairing q)
 425      = -((mu (Quotient.out q) : ℂ) * phasedWeight witnessPhaseModel q) := by
 426  intro q hq
 427  rw [witnessPaired, Finset.mem_singleton] at hq
 428  subst hq
 429  show (mu (Quotient.out pointClass) : ℂ)
 430      * phasedWeight witnessPhaseModel pointClass
 431    = -((mu (Quotient.out emptyClass) : ℂ)
 432      * phasedWeight witnessPhaseModel emptyClass)
 433  rw [mu_out_emptyClass, mu_out_pointClass, phasedWeight_emptyClass,
 434    phasedWeight_pointClass]
 435  norm_num
 436
 437/-- The paired mass of the witness pairing is exactly 2. -/
 438theorem witnessPaired_mass :
 439    ∑ q ∈ witnessPaired ∪ witnessPaired.image witnessPairing,
 440      mu (Quotient.out q) = 2 := by
 441  have himg : witnessPaired.image witnessPairing = {pointClass} := by
 442    rw [witnessPaired]
 443    exact Finset.image_singleton _ _
 444  rw [himg, witnessPaired, ← Finset.insert_eq,
 445    Finset.sum_insert (by
 446      rw [Finset.mem_singleton]
 447      exact emptyClass_ne_pointClass),
 448    Finset.sum_singleton, mu_out_emptyClass, mu_out_pointClass]
 449  norm_num
 450
 451/-- **HEADLINE (non-vacuous quantitative cancellation witness).**  The
 452explicit phase model at `B = 2` beats the triangle bound by EXACTLY the
 453paired mass 2: `‖Zq‖ <= totalClassMass 2 - 2`.  This discharges the
 454pairing hypotheses of the general theorems in one concrete instance. -/
 455theorem phased_Zq_pairing_witness :
 456    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 := by
 457  have hb := Zq_pairing_bound 2 (phasedWeight witnessPhaseModel)
 458    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
 459    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
 460    witnessPairing_cancel
 461  rw [witnessPaired_mass] at hb
 462  exact hb
 463
 464/-- **HEADLINE (strict improvement, witnessed).**  The phased `Zq` of the
 465explicit witness model is STRICTLY below the triangle bound.  Genuine
 466cancellation, not an inequality-shuffling tautology: the bound drop is
 467the exact paired mass. -/
 468theorem phased_Zq_beats_triangle_witness :
 469    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ < totalClassMass 2 :=
 470  Zq_pairing_beats_triangle 2 (phasedWeight witnessPhaseModel)
 471    (fun q => le_of_eq (phasedWeight_norm witnessPhaseModel q))
 472    witnessPaired witnessPairing witnessPairing_injOn witnessPairing_disj
 473    witnessPairing_cancel ⟨emptyClass, Finset.mem_singleton_self _⟩
 474
 475/-- **THEOREM (non-vacuity of the improved bound).**  The total class mass
 476at cap 2 is at least 2 (the two distinct unit-mass witness classes alone
 477contribute 2), so `totalClassMass 2 - 2` is nonnegative and the improved
 478bound is meaningful. -/
 479theorem two_le_totalClassMass_two : (2 : ℝ) ≤ totalClassMass 2 := by
 480  have hsum : ∑ q ∈ ({emptyClass, pointClass} : Finset (TriangulationClass 2)),
 481      mu (Quotient.out q) = 2 := by
 482    rw [Finset.sum_insert (by
 483        rw [Finset.mem_singleton]
 484        exact emptyClass_ne_pointClass),
 485      Finset.sum_singleton, mu_out_emptyClass, mu_out_pointClass]
 486    norm_num
 487  calc (2 : ℝ)
 488      = ∑ q ∈ ({emptyClass, pointClass} : Finset (TriangulationClass 2)),
 489          mu (Quotient.out q) := hsum.symm
 490    _ ≤ ∑ q : TriangulationClass 2, mu (Quotient.out q) :=
 491        Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _)
 492          (fun q _ _ => (mu_pos _).le)
 493    _ = totalClassMass 2 := rfl
 494
 495/-- **HEADLINE (single-theorem chain).**  The full advertised chain in one
 496kernel statement: the witness `Zq` is bounded by `totalClassMass 2 - 2`,
 497that improved bound is strictly below the triangle bound, and it is
 498nonnegative. -/
 499theorem phased_Zq_witness_chain :
 500    ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 ∧
 501    totalClassMass 2 - 2 < totalClassMass 2 ∧
 502    (0 : ℝ) ≤ totalClassMass 2 - 2 :=
 503  ⟨phased_Zq_pairing_witness, by linarith,
 504    by linarith [two_le_totalClassMass_two]⟩
 505
 506/-! ## §6. Status record (honest boundary; RED flags stay RED) -/
 507
 508/-- Status record for the Zq phase-structure wave.  Every `true` flag is
 509tied to its kernel theorem by the grounding theorem below; the RED flags
 510stay false. -/
 511structure ZqPhaseStructureStatus where
 512  /-- §1: `PhaseModel` with stated invariance, descending to classes. -/
 513  phase_model_defined : Bool
 514  /-- §2: `Zq_phased_wellDefined`. -/
 515  phased_Zq_bounded_at_fixed_cap : Bool
 516  /-- §3: `Zq_pairing_decomposition` and `Zq_pairing_beats_triangle`. -/
 517  pairing_cancellation_proved : Bool
 518  /-- §5: `phased_Zq_pairing_witness` (hypotheses discharged at B = 2). -/
 519  pairing_nonvacuity_witnessed : Bool
 520  /-- RED (OPEN): no continuum limit is proved or claimed for any phase;
 521  the complexity cutoff is NOT mesh refinement. -/
 522  Z_RS_continuum_limit : Bool
 523  /-- RED (OPEN): regulator removal at oscillatory phase is not decided
 524  here (the zero-phase route is refuted in `RegulatorRemovalNoGo`). -/
 525  oscillatory_regulator_removal_derived : Bool
 526  /-- RED (OPEN): the phase function is a MODEL input, not derived. -/
 527  substrate_phase_derived : Bool
 528
 529/-- The canonical status record. -/
 530def zqPhaseStructureStatus : ZqPhaseStructureStatus where
 531  phase_model_defined := true
 532  phased_Zq_bounded_at_fixed_cap := true
 533  pairing_cancellation_proved := true
 534  pairing_nonvacuity_witnessed := true
 535  Z_RS_continuum_limit := false
 536  oscillatory_regulator_removal_derived := false
 537  substrate_phase_derived := false
 538
 539/-- **Grounding theorem.**  Every `true` status flag is tied to a kernel
 540statement (the general pairing flag to the GENERAL conditional theorem,
 541not merely the witness); the RED flags remain false. -/
 542theorem zqPhaseStructureStatus_grounded :
 543    (zqPhaseStructureStatus.phase_model_defined = true ∧
 544      ∀ B : ℕ, ∀ P : PhaseModel B,
 545        (∀ K, classPhase P (Quotient.mk (relabelSetoid B) K) = P.phase K) ∧
 546        ∀ q, ‖phasedWeight P q‖ = 1) ∧
 547    (zqPhaseStructureStatus.phased_Zq_bounded_at_fixed_cap = true ∧
 548      ∀ B : ℕ, ∀ P : PhaseModel B,
 549        ‖Zq B (phasedWeight P)‖ ≤ totalClassMass B) ∧
 550    (zqPhaseStructureStatus.pairing_cancellation_proved = true ∧
 551      ∀ (B : ℕ) (wq : TriangulationClass B → ℂ)
 552        (s : Finset (TriangulationClass B))
 553        (j : TriangulationClass B → TriangulationClass B),
 554        (∀ q ∈ s, ∀ q' ∈ s, j q = j q' → q = q') →
 555        (∀ q ∈ s, j q ∉ s) →
 556        (∀ q ∈ s, (mu (Quotient.out (j q)) : ℂ) * wq (j q)
 557            = -((mu (Quotient.out q) : ℂ) * wq q)) →
 558        Zq B wq = ∑ q ∈ Finset.univ \ (s ∪ s.image j),
 559          (mu (Quotient.out q) : ℂ) * wq q) ∧
 560    (zqPhaseStructureStatus.pairing_nonvacuity_witnessed = true ∧
 561      ‖Zq 2 (phasedWeight witnessPhaseModel)‖ ≤ totalClassMass 2 - 2 ∧
 562      ‖Zq 2 (phasedWeight witnessPhaseModel)‖ < totalClassMass 2 ∧
 563      (2 : ℝ) ≤ totalClassMass 2) ∧
 564    zqPhaseStructureStatus.Z_RS_continuum_limit = false ∧
 565    zqPhaseStructureStatus.oscillatory_regulator_removal_derived = false ∧
 566    zqPhaseStructureStatus.substrate_phase_derived = false :=
 567  ⟨⟨rfl, fun _B P => ⟨classPhase_mk P, phasedWeight_norm P⟩⟩,
 568    ⟨rfl, fun B P => (Zq_phased_wellDefined B P).2.1⟩,
 569    ⟨rfl, Zq_pairing_decomposition⟩,
 570    ⟨rfl, phased_Zq_pairing_witness, phased_Zq_beats_triangle_witness,
 571      two_le_totalClassMass_two⟩,
 572    rfl, rfl, rfl⟩
 573
 574#print axioms Zq_norm_le_totalClassMass
 575#print axioms Zq_phased_wellDefined
 576#print axioms Zq_pairing_decomposition
 577#print axioms Zq_pairing_bound
 578#print axioms Zq_pairing_beats_triangle
 579#print axioms opposite_phase_pair_cancels
 580#print axioms opposite_phase_pair_strict
 581#print axioms phased_Zq_pairing_witness
 582#print axioms phased_Zq_beats_triangle_witness
 583#print axioms two_le_totalClassMass_two
 584#print axioms phased_Zq_witness_chain
 585#print axioms zqPhaseStructureStatus_grounded
 586
 587end ZqPhaseStructure
 588end SevenGaps
 589end Gravity
 590end IndisputableMonolith
 591