IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation
   2
   3/-!
   4# Regge TT hinge-aware zero mode (Gate C-A3)
   5
   6QG full-theory campaign, Paper C / Pillar 1, Lane C of the finishing
   7charter.  This module closes the hinge-aware zero-mode gate.
   8
   9## What the sympy diagnostic found (context, not proof)
  10
  11The same-day diagnostic (`state/qg_full_theory/bloch_sympy_diag/`) found
  12that the STENCIL-ONLY constant block (the full per-tet Hessian `G`
  13contracted with the edge-class coefficients, no hinge term) does NOT
  14vanish under TT; its residual at the reported TT witness
  15(`E = diag(1, -1, 0)/sqrt 2`, `k = e_z`) is `-pi*(sqrt 2 + 4)/8`,
  16kernel-recorded as
  17`ReggeTTBlochInterfaceAudit.stencilOnlyConstantWitnessResidual`.  The
  18diagnostic also found that the ASSEMBLED zero mode cancels: the report
  19records, verbatim, `hinge = pi*(-4 - sqrt(2))/8` (the SAME value as the
  20`Sigma_Gcc` residual) and `Hhat(0) quadratic = 0`.  The two recorded
  21values being EQUAL while the assembled quadratic vanishes fixes the
  22assembly sign convention: the assembled block combines them with a
  23relative minus sign, `assembled = hinge - Sigma_Gcc`.  The witness-tie
  24theorem below (`assembled_witness_split`) pins exactly this convention
  25in the kernel, so no silent sign change is possible.
  26
  27## What THIS module proves (all THEOREM, about the ASSEMBLED block)
  28
  291. `hingeEdgeDiagonalBlock` is the assembled hinge/edge-diagonal O(1)
  30   block: `sum_d 2*pi * (-1/(4 * l2_d * sqrt l2_d)) * c_d(E)^2` over the
  31   seven displacement classes, with `c_d = polEdgeCoeff E d` the actual
  32   edge-class coefficients of the symbol program.
  332. `hinge_cancels_recorded_residual`: at the reported TT witness the
  34   hinge block equals the kernel-recorded stencil-only residual
  35   `stencilOnlyConstantWitnessResidual` (the report records the same
  36   value for both, `-pi*(sqrt 2 + 4)/8`).  `assembled_witness_split`
  37   then ties all three objects in the kernel:
  38   `assembled(E_w) = hinge(E_w) - stencilOnlyConstantWitnessResidual`,
  39   with both sides zero, pinning the relative-minus assembly convention.
  40   (`ttWitness_isTT` checks the witness really is TT for `k = e_z`.)
  413. `assembledConstantBlock_eq_zero`, THE ZERO-MODE HEADLINE: the
  42   Schlaefli-reduced assembled constant block (the `k = 0` value of the
  43   raw cell stencil, which by the proved Gate A2 reduction already
  44   carries the hinge and Hessian blocks combined) vanishes IDENTICALLY,
  45   for every polarization matrix.  Structure of the proof: the raw-table
  46   contraction over the six tetrahedron types is the PERFECT SQUARE
  47   `(c0 + c1 + c2 - c3 - c4 - c5 + c6)^2 / 2`
  48   (`zeroMode_free_coefficients`, an identity in seven free
  49   coefficients), and the alternating class sum vanishes for every
  50   polarization (`polEdgeCoeff_alternatingSum`, since
  51   `c_{x+y} + c_{x+z} + c_{y+z} = trace-double-count = c_x + c_y + c_z +
  52   c_{x+y+z}` termwise).
  534. `canonicalFiniteH_zeroMomentum_eq_zero` and
  54   `zeroMomentum_symbol_is_zero`: the A2 canonical finite value at zero
  55   integer wave vector is `0` for every `N`, and the fixed-`N` TT Bloch
  56   symbol AT ZERO WAVE VECTOR exists and equals `0`: the lattice flat
  57   zero mode, as a statement about the true nonlinear Regge action's
  58   second variation.
  59
  60## Why the headline carries NO TT hypotheses (binding disclosure)
  61
  62The panel statement shape asked for the assembled constant block to
  63vanish "under the real TT hypotheses".  The kernel proof gives the
  64STRICTLY STRONGER statement: the assembled block vanishes for EVERY
  65polarization matrix, TT or not (constant metric perturbations are exact
  66flat directions of the lattice).  Stating the theorem with seven TT
  67hypotheses would make every one of them an UNUSED Prop hypothesis, which
  68this campaign's vacuity protocol forbids.  The TT instance is a special
  69case, and the witness-level theorem (2) exhibits the hinge-vs-stencil
  70cancellation on the concrete TT witness the diagnostic reported.
  71
  72## What is NOT proved here (honest scope)
  73
  74The full-Hessian decomposition `assembled = hinge - sum G c c` with `G`
  75the per-tet flat Regge Hessian is NOT re-proved in Lean (the theta
  76second-derivative entries of `G` are not formalized; the proved Gate A2
  77Schlaefli reduction makes them unnecessary for the assembled object).
  78The hinge-vs-full-`G` split is kernel-checked here only at the recorded
  79witness through (2); everywhere else it lives at sympy-diagnostic tier.
  80
  81## Inherited axiom footprint (disclosure)
  82
  83All theorems except the final corollary are pure algebra: expected
  84standard trio `[propext, Classical.choice, Quot.sound]`.
  85`zeroMomentum_symbol_is_zero` goes through the Gate A1/A2 chain
  86(`planeWave_TTBlochSymbolIs_reduced`), whose flat-point step rides the
  87certified periodic angle-sum chain: it therefore ALSO inherits
  88`Lean.ofReduceBool` and `Lean.trustCompiler` (inherited disclosure, not
  89new axioms).  `#print axioms` receipts at the end of the file.
  90
  91No `sorry`, no `admit`, no new axioms, no `native_decide`, no `: True`
  92or `Nonempty`-only headline, no unused Prop hypotheses in this file.
  93-/
  94
  95namespace IndisputableMonolith
  96namespace Gravity
  97namespace Analysis
  98namespace ReggeTTHingeAwareZeroMode
  99
 100open Geometry.PeriodicFreudenthalTorus
 101open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges)
 102open ReggeTTSymbolPreflight
 103open ReggeTTBlochInterfaceAudit
 104open ReggeTTBucketAggregation
 105
 106noncomputable section
 107
 108/-! ## §1. The hinge/edge-diagonal O(1) block -/
 109
 110/-- THE ASSEMBLED HINGE/EDGE-DIAGONAL O(1) BLOCK: the `2*pi*L''` diagonal
 111of the real-space Regge Hessian at flat, contracted with the edge-class
 112coefficients of a polarization matrix.  `L(l2) = sqrt l2` gives
 113`L''(l2) = -1/(4 * l2 * sqrt l2)` at the flat squared length `l2_d` of
 114displacement class `d`; the factor `2*pi` is the deficit constant left on
 115the hinge diagonal because flat deficits vanish.  This mirrors, term for
 116term, the `hinge` object of the sympy diagnostic. -/
 117def hingeEdgeDiagonalBlock (E : Fin 3 → Fin 3 → ℝ) : ℝ :=
 118  ∑ d : Fin 7,
 119    2 * Real.pi *
 120      (-(1 / (4 * periodicDispSqEdge d * Real.sqrt (periodicDispSqEdge d)))) *
 121      (polEdgeCoeff E d) ^ 2
 122
 123/-- The reported TT witness polarization of the diagnostic:
 124`E = diag(1, -1, 0) / sqrt 2`. -/
 125def ttWitnessPolarization : Fin 3 → Fin 3 → ℝ
 126  | 0, 0 => 1 / Real.sqrt 2 | 0, 1 => 0 | 0, 2 => 0
 127  | 1, 0 => 0 | 1, 1 => -(1 / Real.sqrt 2) | 1, 2 => 0
 128  | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 0
 129
 130/-- The witness wave vector `k = e_z` (integer form `m = (0,0,1)`). -/
 131def ttWitnessWaveVector : Fin 3 → ℤ
 132  | 0 => 0
 133  | 1 => 0
 134  | 2 => 1
 135
 136private theorem sqrt2_mul_self : Real.sqrt 2 * Real.sqrt 2 = 2 :=
 137  Real.mul_self_sqrt (by norm_num)
 138
 139private theorem inv_sqrt2_mul_self :
 140    (1 / Real.sqrt 2) * (1 / Real.sqrt 2) = 1 / 2 := by
 141  rw [div_mul_div_comm, one_mul, sqrt2_mul_self]
 142
 143private theorem inv_sqrt2_sq : (1 / Real.sqrt 2) ^ 2 = 1 / 2 := by
 144  rw [sq, inv_sqrt2_mul_self]
 145
 146/-- The reported witness IS a TT polarization for `k = e_z`: symmetric,
 147traceless, transverse, Frobenius-normalized.  This grounds the phrase
 148"the reported TT witness" of the recorded residual. -/
 149theorem ttWitness_isTT :
 150    IsTTPolarization ttWitnessWaveVector ttWitnessPolarization := by
 151  refine ⟨?_, ?_, ?_, ?_⟩
 152  · intro i j
 153    fin_cases i <;> fin_cases j <;> simp only [ttWitnessPolarization]
 154  · simp only [Fin.sum_univ_three, ttWitnessPolarization]
 155    ring
 156  · intro j
 157    fin_cases j <;>
 158      · simp only [Fin.sum_univ_three, ttWitnessPolarization,
 159          ttWitnessWaveVector]
 160        push_cast
 161        ring
 162  · simp only [Fin.sum_univ_three, ttWitnessPolarization]
 163    linear_combination 2 * inv_sqrt2_mul_self
 164
 165/-- The seven edge-class coefficients of the witness, evaluated exactly:
 166`c = (1/sqrt 2, -1/sqrt 2, 0, 0, 1/sqrt 2, -1/sqrt 2, 0)`. -/
 167theorem ttWitness_polEdgeCoeff :
 168    polEdgeCoeff ttWitnessPolarization 0 = 1 / Real.sqrt 2 ∧
 169    polEdgeCoeff ttWitnessPolarization 1 = -(1 / Real.sqrt 2) ∧
 170    polEdgeCoeff ttWitnessPolarization 2 = 0 ∧
 171    polEdgeCoeff ttWitnessPolarization 3 = 0 ∧
 172    polEdgeCoeff ttWitnessPolarization 4 = 1 / Real.sqrt 2 ∧
 173    polEdgeCoeff ttWitnessPolarization 5 = -(1 / Real.sqrt 2) ∧
 174    polEdgeCoeff ttWitnessPolarization 6 = 0 := by
 175  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;>
 176    · simp only [polEdgeCoeff, Fin.sum_univ_three, ttWitnessPolarization,
 177        FreudenthalStencilPreflight.dispReal]
 178      ring
 179
 180/-- **GATE C-A3, WITNESS-LEVEL CANCELLATION (THEOREM): at the reported TT
 181witness the assembled hinge/edge-diagonal block exactly equals the
 182kernel-recorded stencil-only residual.**  Since the assembled constant
 183block is `hinge - stencil`, this is the kernel statement that the
 184diagnostic's nonzero stencil-only obstruction is cancelled by the hinge
 185block at the witness:
 186`hinge(E_w) = -pi*(sqrt 2 + 4)/8 = stencilOnlyConstantWitnessResidual`. -/
 187theorem hinge_cancels_recorded_residual :
 188    hingeEdgeDiagonalBlock ttWitnessPolarization =
 189      stencilOnlyConstantWitnessResidual := by
 190  obtain ⟨h0, h1, h2c, h3, h4, h5, h6⟩ := ttWitness_polEdgeCoeff
 191  unfold hingeEdgeDiagonalBlock stencilOnlyConstantWitnessResidual
 192  rw [Fin.sum_univ_seven, h0, h1, h2c, h3, h4, h5, h6]
 193  simp only [periodicDispSqEdge, Real.sqrt_one, neg_sq]
 194  simp only [inv_sqrt2_sq]
 195  rw [show (1 : ℝ) / (4 * 2 * Real.sqrt 2) = Real.sqrt 2 / 16 by
 196    rw [div_eq_div_iff (by positivity) (by norm_num : (16 : ℝ) ≠ 0)]
 197    linear_combination (-8 : ℝ) * sqrt2_mul_self]
 198  ring
 199
 200/-! ## §2. The slot displacement-class table, grounded -/
 201
 202/-- Literal slot displacement-class table: `slotDispClass t f` is the
 203displacement class of local edge slot `f` of tetrahedron type `t`. -/
 204def slotDispClass : Fin 6 → Fin 6 → Fin 7
 205  | 0, 0 => 0 | 0, 1 => 3 | 0, 2 => 6 | 0, 3 => 1 | 0, 4 => 5 | 0, 5 => 2
 206  | 1, 0 => 0 | 1, 1 => 4 | 1, 2 => 6 | 1, 3 => 2 | 1, 4 => 5 | 1, 5 => 1
 207  | 2, 0 => 1 | 2, 1 => 3 | 2, 2 => 6 | 2, 3 => 0 | 2, 4 => 4 | 2, 5 => 2
 208  | 3, 0 => 1 | 3, 1 => 5 | 3, 2 => 6 | 3, 3 => 2 | 3, 4 => 4 | 3, 5 => 0
 209  | 4, 0 => 2 | 4, 1 => 4 | 4, 2 => 6 | 4, 3 => 0 | 4, 4 => 3 | 4, 5 => 1
 210  | 5, 0 => 2 | 5, 1 => 5 | 5, 2 => 6 | 5, 3 => 1 | 5, 4 => 3 | 5, 5 => 0
 211
 212/-- GROUNDING (THEOREM): the literal table is exactly the displacement
 213class the ACTUAL periodic geometry assigns to slot `f` of tetrahedron
 214type `t`, in every cell of every torus (the class is cell-independent by
 215construction of `localEdgeOf`). -/
 216theorem slotDispClass_grounded (N : ℕ) [NeZero N] (cell : Vertex N N N)
 217    (t f : Fin 6) :
 218    (localEdgeOf cell t f).disp = slotDispClass t f := by
 219  fin_cases t <;> fin_cases f <;> rfl
 220
 221/-! ## §3. The 36 raw coefficients as private rewrite lemmas
 222
 223Each entry is `rawJacobianCoefficient_eval` (Gate C-A2f) evaluated on one
 224literal slot pair; keeping them separate keeps every `norm_num` call
 225small (the earlier single-shot expansion exceeded the local build memory
 226guard). -/
 227
 228private theorem w00 : rawJacobianCoefficient 0 0 = (0 : ℝ) := by
 229  rw [rawJacobianCoefficient_eval 0 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 230private theorem w01 : rawJacobianCoefficient 0 1 = (0 : ℝ) := by
 231  rw [rawJacobianCoefficient_eval 0 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 232private theorem w02 : rawJacobianCoefficient 0 2 = (0 : ℝ) := by
 233  rw [rawJacobianCoefficient_eval 0 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 234private theorem w03 : rawJacobianCoefficient 0 3 = (0 : ℝ) := by
 235  rw [rawJacobianCoefficient_eval 0 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 236private theorem w04 : rawJacobianCoefficient 0 4 = (-(1 / 8) : ℝ) := by
 237  rw [rawJacobianCoefficient_eval 0 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 238private theorem w05 : rawJacobianCoefficient 0 5 = (1 / 4 : ℝ) := by
 239  rw [rawJacobianCoefficient_eval 0 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 240private theorem w10 : rawJacobianCoefficient 1 0 = (0 : ℝ) := by
 241  rw [rawJacobianCoefficient_eval 1 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 242private theorem w11 : rawJacobianCoefficient 1 1 = (1 / 8 : ℝ) := by
 243  rw [rawJacobianCoefficient_eval 1 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 244private theorem w12 : rawJacobianCoefficient 1 2 = (-(1 / 8) : ℝ) := by
 245  rw [rawJacobianCoefficient_eval 1 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 246private theorem w13 : rawJacobianCoefficient 1 3 = (-(1 / 4) : ℝ) := by
 247  rw [rawJacobianCoefficient_eval 1 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 248private theorem w14 : rawJacobianCoefficient 1 4 = (1 / 4 : ℝ) := by
 249  rw [rawJacobianCoefficient_eval 1 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 250private theorem w15 : rawJacobianCoefficient 1 5 = (-(1 / 8) : ℝ) := by
 251  rw [rawJacobianCoefficient_eval 1 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 252private theorem w20 : rawJacobianCoefficient 2 0 = (0 : ℝ) := by
 253  rw [rawJacobianCoefficient_eval 2 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 254private theorem w21 : rawJacobianCoefficient 2 1 = (-(1 / 8) : ℝ) := by
 255  rw [rawJacobianCoefficient_eval 2 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 256private theorem w22 : rawJacobianCoefficient 2 2 = (1 / 12 : ℝ) := by
 257  rw [rawJacobianCoefficient_eval 2 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 258private theorem w23 : rawJacobianCoefficient 2 3 = (1 / 4 : ℝ) := by
 259  rw [rawJacobianCoefficient_eval 2 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 260private theorem w24 : rawJacobianCoefficient 2 4 = (-(1 / 8) : ℝ) := by
 261  rw [rawJacobianCoefficient_eval 2 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 262private theorem w25 : rawJacobianCoefficient 2 5 = (0 : ℝ) := by
 263  rw [rawJacobianCoefficient_eval 2 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 264private theorem w30 : rawJacobianCoefficient 3 0 = (0 : ℝ) := by
 265  rw [rawJacobianCoefficient_eval 3 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 266private theorem w31 : rawJacobianCoefficient 3 1 = (-(1 / 4) : ℝ) := by
 267  rw [rawJacobianCoefficient_eval 3 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 268private theorem w32 : rawJacobianCoefficient 3 2 = (1 / 4 : ℝ) := by
 269  rw [rawJacobianCoefficient_eval 3 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 270private theorem w33 : rawJacobianCoefficient 3 3 = (1 / 4 : ℝ) := by
 271  rw [rawJacobianCoefficient_eval 3 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 272private theorem w34 : rawJacobianCoefficient 3 4 = (-(1 / 4) : ℝ) := by
 273  rw [rawJacobianCoefficient_eval 3 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 274private theorem w35 : rawJacobianCoefficient 3 5 = (0 : ℝ) := by
 275  rw [rawJacobianCoefficient_eval 3 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 276private theorem w40 : rawJacobianCoefficient 4 0 = (-(1 / 8) : ℝ) := by
 277  rw [rawJacobianCoefficient_eval 4 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 278private theorem w41 : rawJacobianCoefficient 4 1 = (1 / 4 : ℝ) := by
 279  rw [rawJacobianCoefficient_eval 4 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 280private theorem w42 : rawJacobianCoefficient 4 2 = (-(1 / 8) : ℝ) := by
 281  rw [rawJacobianCoefficient_eval 4 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 282private theorem w43 : rawJacobianCoefficient 4 3 = (-(1 / 4) : ℝ) := by
 283  rw [rawJacobianCoefficient_eval 4 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 284private theorem w44 : rawJacobianCoefficient 4 4 = (1 / 8 : ℝ) := by
 285  rw [rawJacobianCoefficient_eval 4 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 286private theorem w45 : rawJacobianCoefficient 4 5 = (0 : ℝ) := by
 287  rw [rawJacobianCoefficient_eval 4 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 288private theorem w50 : rawJacobianCoefficient 5 0 = (1 / 4 : ℝ) := by
 289  rw [rawJacobianCoefficient_eval 5 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 290private theorem w51 : rawJacobianCoefficient 5 1 = (-(1 / 8) : ℝ) := by
 291  rw [rawJacobianCoefficient_eval 5 1]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 292private theorem w52 : rawJacobianCoefficient 5 2 = (0 : ℝ) := by
 293  rw [rawJacobianCoefficient_eval 5 2]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 294private theorem w53 : rawJacobianCoefficient 5 3 = (0 : ℝ) := by
 295  rw [rawJacobianCoefficient_eval 5 3]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 296private theorem w54 : rawJacobianCoefficient 5 4 = (0 : ℝ) := by
 297  rw [rawJacobianCoefficient_eval 5 4]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 298private theorem w55 : rawJacobianCoefficient 5 5 = (0 : ℝ) := by
 299  rw [rawJacobianCoefficient_eval 5 5]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
 300
 301/-! ## §4. The assembled constant block and the zero-mode headline -/
 302
 303/-- THE ASSEMBLED CONSTANT BLOCK, per periodic cell: the `k = 0` value of
 304the raw cell stencil of Gate A1/A2.  By the proved Schlaefli reduction
 305(Gate A2) this object ALREADY contains the hinge/edge-diagonal `2*pi*L''`
 306block and the per-tet Hessian block combined, with the relative sign of
 307the sympy report's convention (`assembled = hinge - Sigma_Gcc` at the
 308witness; see `assembled_witness_split`): the reduced second variation
 309`-sum_tau sum_f L'_f theta'_f` carries both blocks with no separate
 310theta-second-derivative term surviving.  `c_d = polEdgeCoeff E d` are
 311the same edge-class coefficients the hinge block uses. -/
 312def assembledConstantBlock (E : Fin 3 → Fin 3 → ℝ) : ℝ :=
 313  -∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 314    rawJacobianCoefficient f g *
 315      polEdgeCoeff E (slotDispClass t f) *
 316      polEdgeCoeff E (slotDispClass t g)
 317
 318/-- The raw-table contraction over the six tetrahedron types, in SEVEN
 319FREE coefficients, is the perfect square
 320`(c0 + c1 + c2 - c3 - c4 - c5 + c6)^2 / 2`.  This is the exact algebraic
 321shape of the assembled constant block: it does NOT vanish for free
 322coefficients (each per-tet block is individually nonzero and even the
 323six-type sum survives off the constraint surface); it vanishes exactly
 324on the alternating-sum hyperplane, where every geometric edge-class
 325coefficient vector lives. -/
 326theorem zeroMode_free_coefficients (c : Fin 7 → ℝ) :
 327    (∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 328      rawJacobianCoefficient f g *
 329        c (slotDispClass t f) * c (slotDispClass t g)) =
 330      (c 0 + c 1 + c 2 - c 3 - c 4 - c 5 + c 6) ^ 2 / 2 := by
 331  simp only [Fin.sum_univ_six, slotDispClass]
 332  rw [w00, w01, w02, w03, w04, w05, w10, w11, w12, w13, w14, w15,
 333    w20, w21, w22, w23, w24, w25, w30, w31, w32, w33, w34, w35,
 334    w40, w41, w42, w43, w44, w45, w50, w51, w52, w53, w54, w55]
 335  ring
 336
 337/-- The alternating class sum of the edge-class coefficients vanishes for
 338EVERY matrix `E`: the three face-diagonal classes double-count exactly
 339what the three axis classes and the body-diagonal class contribute
 340(`c_{x+y} + c_{x+z} + c_{y+z} = 2 tr + off = (c_x + c_y + c_z) +
 341c_{x+y+z}` at the level of the quadratic-form values). -/
 342theorem polEdgeCoeff_alternatingSum (E : Fin 3 → Fin 3 → ℝ) :
 343    polEdgeCoeff E 0 + polEdgeCoeff E 1 + polEdgeCoeff E 2 -
 344      polEdgeCoeff E 3 - polEdgeCoeff E 4 - polEdgeCoeff E 5 +
 345      polEdgeCoeff E 6 = 0 := by
 346  simp only [polEdgeCoeff, Fin.sum_univ_three,
 347    FreudenthalStencilPreflight.dispReal]
 348  ring
 349
 350/-- **GATE C-A3 HEADLINE (THEOREM): the ASSEMBLED constant block vanishes
 351identically, for every polarization matrix.**  This is the hinge-aware
 352zero mode: the stencil-only block does NOT vanish (kernel-recorded
 353witness residual `-pi*(sqrt 2 + 4)/8`), but the assembled object, the
 354`k = 0` raw cell stencil, which by the Gate A2 Schlaefli reduction
 355carries the hinge and Hessian blocks combined, is exactly zero.  The
 356statement quantifies over ALL `E` (see the module docstring for why the
 357seven TT hypotheses would be unused and are therefore omitted); the TT
 358case demanded by the panel is the special case. -/
 359theorem assembledConstantBlock_eq_zero (E : Fin 3 → Fin 3 → ℝ) :
 360    assembledConstantBlock E = 0 := by
 361  unfold assembledConstantBlock
 362  have h := zeroMode_free_coefficients (fun d => polEdgeCoeff E d)
 363  simp only at h
 364  rw [h, polEdgeCoeff_alternatingSum]
 365  norm_num
 366
 367/-- **WITNESS-LEVEL SPLIT (THEOREM): the assembled block, the hinge block,
 368and the recorded stencil-only residual are tied in the kernel at the
 369reported TT witness with the report's sign convention.**
 370`assembled(E_w) = hinge(E_w) - stencilOnlyConstantWitnessResidual`: the
 371sympy report records the SAME value `-pi*(sqrt 2 + 4)/8` for the hinge
 372block and the `Sigma_Gcc` residual, and the assembled quadratic vanishes,
 373so the assembly combines them with a relative minus sign.  This theorem
 374pins that convention: no silent sign change is possible, because all
 375three objects appear together in one kernel identity. -/
 376theorem assembled_witness_split :
 377    assembledConstantBlock ttWitnessPolarization =
 378      hingeEdgeDiagonalBlock ttWitnessPolarization -
 379        stencilOnlyConstantWitnessResidual := by
 380  rw [assembledConstantBlock_eq_zero, hinge_cancels_recorded_residual,
 381    sub_self]
 382
 383/-! ## §5. Zero momentum kills the canonical finite value, every `N` -/
 384
 385/-- Zero integer wave vector gives the zero commensurate momentum. -/
 386theorem commensurateMomentum_zero (N : ℕ) [NeZero N] :
 387    commensurateMomentum N (fun _ => (0 : ℤ)) = fun _ => (0 : ℝ) := by
 388  funext i
 389  simp [commensurateMomentum]
 390
 391/-- At zero momentum every midpoint phase vanishes, so every plane-wave
 392velocity is the bare edge-class coefficient of its displacement class. -/
 393theorem planeWaveTetVelocity_zeroMomentum (N : ℕ) [NeZero N]
 394    (E : Fin 3 → Fin 3 → ℝ) (τ : PeriodicTet N N N) (f : Fin 6) :
 395    ReggeTTLocalSymbolExistence.planeWaveTetVelocity N E
 396        (fun _ => (0 : ℝ)) τ f =
 397      polEdgeCoeff E (slotDispClass τ.2 f) := by
 398  unfold ReggeTTLocalSymbolExistence.planeWaveTetVelocity
 399  rw [show edgeMidpointPhase N (fun _ => (0 : ℝ))
 400        (localEdgeOf τ.1 τ.2 f) = 0 by
 401    unfold edgeMidpointPhase
 402    simp]
 403  rw [Real.cos_zero, mul_one, slotDispClass_grounded N τ.1 τ.2 f]
 404
 405/-- The `k = 0` raw cell stencil is `2` times the per-cell assembled
 406constant block: the cell sum contributes exactly `N ^ 3` identical
 407copies, and the `2 / N ^ 3` normalization leaves the factor `2`. -/
 408theorem rawCellStencil_zeroMomentum (N : ℕ) [NeZero N]
 409    (E : Fin 3 → Fin 3 → ℝ) :
 410    rawCellStencil N E (fun _ => (0 : ℤ)) = 2 * assembledConstantBlock E := by
 411  unfold rawCellStencil
 412  have hterm : ∀ (τ : PeriodicTet N N N) (f g : Fin 6),
 413      rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g =
 414        rawJacobianCoefficient f g *
 415          polEdgeCoeff E (slotDispClass τ.2 f) *
 416          polEdgeCoeff E (slotDispClass τ.2 g) := by
 417    intro τ f g
 418    unfold rawCellStencilTerm rawJacobianCoefficient
 419    rw [commensurateMomentum_zero N,
 420      planeWaveTetVelocity_zeroMomentum N E τ f,
 421      planeWaveTetVelocity_zeroMomentum N E τ g]
 422    ring
 423  have hsum : (∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
 424      rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g) =
 425      (N : ℝ) ^ (3 : ℕ) *
 426        ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 427          rawJacobianCoefficient f g *
 428            polEdgeCoeff E (slotDispClass t f) *
 429            polEdgeCoeff E (slotDispClass t g) := by
 430    calc
 431      (∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
 432          rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g)
 433          = ∑ cell : Vertex N N N, ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 434              rawJacobianCoefficient f g *
 435                polEdgeCoeff E (slotDispClass t f) *
 436                polEdgeCoeff E (slotDispClass t g) := by
 437            rw [Fintype.sum_prod_type]
 438            refine Finset.sum_congr rfl fun cell _ => ?_
 439            refine Finset.sum_congr rfl fun t _ => ?_
 440            refine Finset.sum_congr rfl fun f _ => ?_
 441            refine Finset.sum_congr rfl fun g _ => ?_
 442            exact hterm (cell, t) f g
 443      _ = (Fintype.card (Vertex N N N) : ℝ) *
 444            ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 445              rawJacobianCoefficient f g *
 446                polEdgeCoeff E (slotDispClass t f) *
 447                polEdgeCoeff E (slotDispClass t g) := by
 448            rw [Finset.sum_const, nsmul_eq_mul, Finset.card_univ]
 449      _ = (N : ℝ) ^ (3 : ℕ) *
 450            ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
 451              rawJacobianCoefficient f g *
 452                polEdgeCoeff E (slotDispClass t f) *
 453                polEdgeCoeff E (slotDispClass t g) := by
 454            congr 1
 455            rw [show Fintype.card (Vertex N N N) = N * (N * N) by
 456              simp [Fintype.card_prod]]
 457            push_cast
 458            ring
 459  rw [hsum]
 460  unfold assembledConstantBlock
 461  have hN : ((N : ℝ)) ^ (3 : ℕ) ≠ 0 := by
 462    have hcast : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_of_neZero N).ne'
 463    positivity
 464  have hkey : ∀ (A S : ℝ), A ≠ 0 → (2 / A) * -(A * S) = 2 * -S := by
 465    intro A S hA
 466    field_simp
 467  exact hkey _ _ hN
 468
 469/-- The A2 canonical finite value at zero integer wave vector vanishes
 470for every torus side `N` and every polarization matrix (pure algebra:
 471Gate A1 regrouping + the zero-mode headline). -/
 472theorem canonicalFiniteH_zeroMomentum_eq_zero (N : ℕ) [NeZero N]
 473    (E : Fin 3 → Fin 3 → ℝ) :
 474    canonicalFiniteH N E (fun _ => (0 : ℤ)) = 0 := by
 475  rw [a2_reduced_eq_rawCellStencil, rawCellStencil_zeroMomentum,
 476    assembledConstantBlock_eq_zero, mul_zero]
 477
 478/-- **ZERO-MODE SYMBOL COROLLARY (THEOREM): the fixed-`N` TT Bloch symbol
 479of the TRUE nonlinear Regge action at ZERO wave vector exists and equals
 480`0`, for every `N` and every polarization matrix.**  This is the lattice
 481flat zero mode as a statement about the actual second variation, through
 482the Gate A1 existence chain and the Gate A2 reduction.  AXIOM
 483DISCLOSURE: this corollary (alone in this file) rides the certified
 484flat-deficit chain and therefore inherits `Lean.ofReduceBool` /
 485`Lean.trustCompiler` in addition to the standard trio. -/
 486theorem zeroMomentum_symbol_is_zero (N : ℕ) [NeZero N]
 487    (E : Fin 3 → Fin 3 → ℝ) :
 488    TTBlochSymbolIs N E (fun _ => (0 : ℤ)) 0 := by
 489  have h := ReggeTTFlatSecondVariation.planeWave_TTBlochSymbolIs_reduced
 490    N E (fun _ => (0 : ℤ))
 491  have hval : canonicalFiniteH N E (fun _ => (0 : ℤ)) =
 492      (2 / (N : ℝ) ^ (3 : ℕ)) *
 493        (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
 494          ReggeTTFlatSecondVariation.flatSlotSqrtDeriv N E
 495              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f *
 496            ReggeTTFlatSecondVariation.flatSlotAngleDeriv N E
 497              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f) := rfl
 498  rw [← hval, canonicalFiniteH_zeroMomentum_eq_zero N E] at h
 499  exact h
 500
 501end
 502
 503end ReggeTTHingeAwareZeroMode
 504end Analysis
 505end Gravity
 506end IndisputableMonolith
 507
 508#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.ttWitness_isTT
 509#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.hinge_cancels_recorded_residual
 510#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.slotDispClass_grounded
 511#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.zeroMode_free_coefficients
 512#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.polEdgeCoeff_alternatingSum
 513#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.assembledConstantBlock_eq_zero
 514#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.assembled_witness_split
 515#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.canonicalFiniteH_zeroMomentum_eq_zero
 516#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode.zeroMomentum_symbol_is_zero
 517