IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridgeCore

   1import Mathlib.Algebra.BigOperators.Fin
   2import Mathlib.Data.Fintype.BigOperators
   3import Mathlib.Tactic.Push
   4import IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCertificateSpike
   5
   6/-!
   7# Regge TT Gate B bridge core (leaf algebra module for Gate C-B)
   8
   9Support module for `ReggeTTGateBBridge` (Gate C-B of the Lane C
  10finishing charter).  This file carries the HEAVY polynomial algebra of
  11the spike convention bridge in a LEAF import context: it imports ONLY
  12the committed spike transcription (which itself imports only basic real
  13arithmetic and the `ring`/`linear_combination` tactics), because the
  14full symbol-program import chain plus a 216-term `ring` normalization
  15exceeds the laptop build memory guard when combined in one file.
  16
  17Everything here is defined over literal tables and scalars:
  18
  19* `coreWeight`: the literal rational raw-coefficient table (the same 36
  20  values the independent `rationalStencilWeight` table of Gate C-A2f
  21  carries; the MAIN module kernel-identifies this table with the actual
  22  `rawJacobianCoefficient` through the Gate C-A2f theorem, so no
  23  transcription is trusted).
  24* `slotDispCore`: the literal slot displacement-class table (the main
  25  module grounds it against the actual periodic geometry).
  26* `slotMidTwice`: the literal doubled-midpoint table (the main module
  27  grounds it against the actual `edgeMidpointPhase`).
  28* `corePolEdgeCoeff`: the literal seven edge-class linear forms (the
  29  main module kernel-identifies them with the actual `polEdgeCoeff`).
  30* `coreTripleTerm`: one signed raw moment term
  31  `-(phase^2)/2 * -(w_fg * c_f * c_g)`.
  32
  33`coreTripleSum_eq_spikeSum` is the core identity: the 216-term raw
  34moment sum equals `tetBlock0 + ... + tetBlock5` with COMPLETELY FREE
  35`s2 s3 p`, identically in `E` and `x`.  The spike blocks enter as data
  36only; `tt_continuum_certificate` is never used.
  37
  38Expected axiom footprint: standard trio.  No `sorry`, no `admit`, no
  39new axioms, no `native_decide`.
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Gravity
  44namespace Analysis
  45namespace ReggeTTGateBBridgeCore
  46
  47open ReggeTTContinuumCertificateSpike
  48
  49noncomputable section
  50
  51set_option maxHeartbeats 3200000
  52
  53/-- Literal rational raw-coefficient table (see Gate C-A2f for the
  54kernel identification with `rawJacobianCoefficient`). -/
  55def coreWeight : Fin 6 → Fin 6 → ℝ
  56  | 0, 0 => 0        | 0, 1 => 0        | 0, 2 => 0
  57  | 0, 3 => 0        | 0, 4 => -(1 / 8) | 0, 5 => 1 / 4
  58  | 1, 0 => 0        | 1, 1 => 1 / 8    | 1, 2 => -(1 / 8)
  59  | 1, 3 => -(1 / 4) | 1, 4 => 1 / 4    | 1, 5 => -(1 / 8)
  60  | 2, 0 => 0        | 2, 1 => -(1 / 8) | 2, 2 => 1 / 12
  61  | 2, 3 => 1 / 4    | 2, 4 => -(1 / 8) | 2, 5 => 0
  62  | 3, 0 => 0        | 3, 1 => -(1 / 4) | 3, 2 => 1 / 4
  63  | 3, 3 => 1 / 4    | 3, 4 => -(1 / 4) | 3, 5 => 0
  64  | 4, 0 => -(1 / 8) | 4, 1 => 1 / 4    | 4, 2 => -(1 / 8)
  65  | 4, 3 => -(1 / 4) | 4, 4 => 1 / 8    | 4, 5 => 0
  66  | 5, 0 => 1 / 4    | 5, 1 => -(1 / 8) | 5, 2 => 0
  67  | 5, 3 => 0        | 5, 4 => 0        | 5, 5 => 0
  68
  69/-- Literal slot displacement-class table. -/
  70def slotDispCore : Fin 6 → Fin 6 → Fin 7
  71  | 0, 0 => 0 | 0, 1 => 3 | 0, 2 => 6 | 0, 3 => 1 | 0, 4 => 5 | 0, 5 => 2
  72  | 1, 0 => 0 | 1, 1 => 4 | 1, 2 => 6 | 1, 3 => 2 | 1, 4 => 5 | 1, 5 => 1
  73  | 2, 0 => 1 | 2, 1 => 3 | 2, 2 => 6 | 2, 3 => 0 | 2, 4 => 4 | 2, 5 => 2
  74  | 3, 0 => 1 | 3, 1 => 5 | 3, 2 => 6 | 3, 3 => 2 | 3, 4 => 4 | 3, 5 => 0
  75  | 4, 0 => 2 | 4, 1 => 4 | 4, 2 => 6 | 4, 3 => 0 | 4, 4 => 3 | 4, 5 => 1
  76  | 5, 0 => 2 | 5, 1 => 5 | 5, 2 => 6 | 5, 3 => 1 | 5, 4 => 3 | 5, 5 => 0
  77
  78/-- Literal doubled-midpoint table (`2 * (base offset + displacement/2)`
  79per coordinate). -/
  80def slotMidTwice : Fin 6 → Fin 6 → Fin 3 → ℤ
  81  | 0, 0, 0 => 1 | 0, 0, 1 => 0 | 0, 0, 2 => 0
  82  | 0, 1, 0 => 1 | 0, 1, 1 => 1 | 0, 1, 2 => 0
  83  | 0, 2, 0 => 1 | 0, 2, 1 => 1 | 0, 2, 2 => 1
  84  | 0, 3, 0 => 2 | 0, 3, 1 => 1 | 0, 3, 2 => 0
  85  | 0, 4, 0 => 2 | 0, 4, 1 => 1 | 0, 4, 2 => 1
  86  | 0, 5, 0 => 2 | 0, 5, 1 => 2 | 0, 5, 2 => 1
  87  | 1, 0, 0 => 1 | 1, 0, 1 => 0 | 1, 0, 2 => 0
  88  | 1, 1, 0 => 1 | 1, 1, 1 => 0 | 1, 1, 2 => 1
  89  | 1, 2, 0 => 1 | 1, 2, 1 => 1 | 1, 2, 2 => 1
  90  | 1, 3, 0 => 2 | 1, 3, 1 => 0 | 1, 3, 2 => 1
  91  | 1, 4, 0 => 2 | 1, 4, 1 => 1 | 1, 4, 2 => 1
  92  | 1, 5, 0 => 2 | 1, 5, 1 => 1 | 1, 5, 2 => 2
  93  | 2, 0, 0 => 0 | 2, 0, 1 => 1 | 2, 0, 2 => 0
  94  | 2, 1, 0 => 1 | 2, 1, 1 => 1 | 2, 1, 2 => 0
  95  | 2, 2, 0 => 1 | 2, 2, 1 => 1 | 2, 2, 2 => 1
  96  | 2, 3, 0 => 1 | 2, 3, 1 => 2 | 2, 3, 2 => 0
  97  | 2, 4, 0 => 1 | 2, 4, 1 => 2 | 2, 4, 2 => 1
  98  | 2, 5, 0 => 2 | 2, 5, 1 => 2 | 2, 5, 2 => 1
  99  | 3, 0, 0 => 0 | 3, 0, 1 => 1 | 3, 0, 2 => 0
 100  | 3, 1, 0 => 0 | 3, 1, 1 => 1 | 3, 1, 2 => 1
 101  | 3, 2, 0 => 1 | 3, 2, 1 => 1 | 3, 2, 2 => 1
 102  | 3, 3, 0 => 0 | 3, 3, 1 => 2 | 3, 3, 2 => 1
 103  | 3, 4, 0 => 1 | 3, 4, 1 => 2 | 3, 4, 2 => 1
 104  | 3, 5, 0 => 1 | 3, 5, 1 => 2 | 3, 5, 2 => 2
 105  | 4, 0, 0 => 0 | 4, 0, 1 => 0 | 4, 0, 2 => 1
 106  | 4, 1, 0 => 1 | 4, 1, 1 => 0 | 4, 1, 2 => 1
 107  | 4, 2, 0 => 1 | 4, 2, 1 => 1 | 4, 2, 2 => 1
 108  | 4, 3, 0 => 1 | 4, 3, 1 => 0 | 4, 3, 2 => 2
 109  | 4, 4, 0 => 1 | 4, 4, 1 => 1 | 4, 4, 2 => 2
 110  | 4, 5, 0 => 2 | 4, 5, 1 => 1 | 4, 5, 2 => 2
 111  | 5, 0, 0 => 0 | 5, 0, 1 => 0 | 5, 0, 2 => 1
 112  | 5, 1, 0 => 0 | 5, 1, 1 => 1 | 5, 1, 2 => 1
 113  | 5, 2, 0 => 1 | 5, 2, 1 => 1 | 5, 2, 2 => 1
 114  | 5, 3, 0 => 0 | 5, 3, 1 => 1 | 5, 3, 2 => 2
 115  | 5, 4, 0 => 1 | 5, 4, 1 => 1 | 5, 4, 2 => 2
 116  | 5, 5, 0 => 1 | 5, 5, 1 => 2 | 5, 5, 2 => 2
 117
 118/-- Literal edge-class linear forms (`c_d = sum_ij E_ij D_d^i D_d^j`). -/
 119def corePolEdgeCoeff (E : Fin 3 → Fin 3 → ℝ) : Fin 7 → ℝ
 120  | 0 => E 0 0
 121  | 1 => E 1 1
 122  | 2 => E 2 2
 123  | 3 => E 0 0 + E 0 1 + E 1 0 + E 1 1
 124  | 4 => E 0 0 + E 0 2 + E 2 0 + E 2 2
 125  | 5 => E 1 1 + E 1 2 + E 2 1 + E 2 2
 126  | 6 => E 0 0 + E 0 1 + E 0 2 + E 1 0 + E 1 1 + E 1 2 + E 2 0 + E 2 1 + E 2 2
 127
 128/-- One signed raw moment term of triple `q = (t, f, g)`:
 129`-(midpoint phase)^2/2 * -(w_fg * c_{d(t,f)} * c_{d(t,g)})`. -/
 130def coreTripleTerm (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 131    (q : Fin 6 × Fin 6 × Fin 6) : ℝ :=
 132  -((∑ i : Fin 3,
 133      x i * (((slotMidTwice q.1 q.2.2 i - slotMidTwice q.1 q.2.1 i : ℤ) : ℝ) /
 134        2)) ^ 2) / 2 *
 135    -(coreWeight q.2.1 q.2.2 *
 136      corePolEdgeCoeff E (slotDispCore q.1 q.2.1) *
 137      corePolEdgeCoeff E (slotDispCore q.1 q.2.2))
 138
 139private theorem coreBlock0_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 140    (s2 s3 p : ℝ) :
 141    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (0, f, g)) =
 142      tetBlock0 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 143        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 144  rw [tetBlock0_eq]
 145  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 146    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 147  push_cast
 148  ring
 149
 150private theorem coreBlock1_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 151    (s2 s3 p : ℝ) :
 152    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (1, f, g)) =
 153      tetBlock1 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 154        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 155  rw [tetBlock1_eq]
 156  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 157    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 158  push_cast
 159  ring
 160
 161private theorem coreBlock2_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 162    (s2 s3 p : ℝ) :
 163    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (2, f, g)) =
 164      tetBlock2 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 165        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 166  rw [tetBlock2_eq]
 167  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 168    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 169  push_cast
 170  ring
 171
 172private theorem coreBlock3_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 173    (s2 s3 p : ℝ) :
 174    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (3, f, g)) =
 175      tetBlock3 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 176        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 177  rw [tetBlock3_eq]
 178  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 179    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 180  push_cast
 181  ring
 182
 183private theorem coreBlock4_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 184    (s2 s3 p : ℝ) :
 185    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (4, f, g)) =
 186      tetBlock4 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 187        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 188  rw [tetBlock4_eq]
 189  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 190    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 191  push_cast
 192  ring
 193
 194private theorem coreBlock5_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 195    (s2 s3 p : ℝ) :
 196    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (5, f, g)) =
 197      tetBlock5 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 198        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 199  rw [tetBlock5_eq]
 200  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
 201    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
 202  push_cast
 203  ring
 204
 205/-- THE CORE IDENTITY (THEOREM): the 216-term raw moment sum equals the
 206sum of the six committed spike blocks, for COMPLETELY FREE `s2 s3 p` and
 207IDENTICALLY in `E` and `x`.  Only the block data is used; the spike's TT
 208conclusion is never invoked. -/
 209theorem coreTripleSum_eq_spikeSum (E : Fin 3 → Fin 3 → ℝ)
 210    (x : Fin 3 → ℝ) (s2 s3 p : ℝ) :
 211    (∑ q : Fin 6 × Fin 6 × Fin 6, coreTripleTerm E x q) =
 212      tetBlock0 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 213          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p
 214        + tetBlock1 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 215          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p
 216        + tetBlock2 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 217          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p
 218        + tetBlock3 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 219          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p
 220        + tetBlock4 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 221          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p
 222        + tetBlock5 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
 223          (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
 224  simp only [Fintype.sum_prod_type]
 225  rw [Fin.sum_univ_six]
 226  rw [coreBlock0_eq E x s2 s3 p, coreBlock1_eq E x s2 s3 p,
 227    coreBlock2_eq E x s2 s3 p, coreBlock3_eq E x s2 s3 p,
 228    coreBlock4_eq E x s2 s3 p, coreBlock5_eq E x s2 s3 p]
 229
 230end
 231
 232end ReggeTTGateBBridgeCore
 233end Analysis
 234end Gravity
 235end IndisputableMonolith
 236
 237#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridgeCore.coreTripleSum_eq_spikeSum
 238