IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode
   2import IndisputableMonolith.Gravity.Analysis.ReggeTTBlochConventionAudit
   3import IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridgeCore
   4
   5/-!
   6# Regge TT Gate B: the spike convention bridge (Gate C-B)
   7
   8QG full-theory campaign, Paper C / Pillar 1, Lane C of the finishing
   9charter.  This module closes the panel-locked Gate B target
  10`GateBConventionTarget` of `ReggeTTBlochConventionAudit`: the interface
  11moment fold `reggeTTMoment`, instantiated on support / phase quadratic /
  12amplitude built FROM THE ACTUAL RAW STENCIL, equals the committed spike
  13LHS `tetBlock0 + ... + tetBlock5` under the seven TT hypotheses.
  14
  15## Instantiation (all from the raw stencil, none from the spike)
  16
  17* `bucketKeyOf (t, f, g)` sends a raw stencil triple (tetrahedron type,
  18  ordered slot pair) to the bucket `(f, g, u)` whose integer phase key
  19  `u = 2*(mid_g - mid_f)` is the doubled midpoint displacement of the
  20  slot pair, from the literal `slotMidTwice` table of the core module.
  21  The table is GROUNDED against the actual periodic geometry:
  22  `edgeMidpointPhase_grounded` proves that the preregistered midpoint
  23  Bloch phase of `localEdgeOf` at the base cell is exactly
  24  `sum_i k_i * (slotMidTwice t f i) / 2`.
  25* `rawMomentSupport` is the image of all 216 raw triples under
  26  `bucketKeyOf`: the support IS the raw cell stencil's bucket set.
  27* `rawPhaseQuadratic x b = (sum_i x_i * u_i / 2)^2` is the squared
  28  midpoint-displacement phase of the bucket: the campaign's frozen
  29  cosine two-jet convention (`cos z ~ 1 - z^2/2`; `reggeTTMoment`
  30  supplies the `-z^2/2` evaluator itself).
  31* `rawBucketAmplitude E b` is the honest BUCKET-FIBER AGGREGATION: the
  32  sum over the raw triples in the fiber of `b` of
  33  `-(J_fg/(2 sqrt a*_f)) * c_{d(t,f)} * c_{d(t,g)}`, with
  34  `rawJacobianCoefficient` and `polEdgeCoeff` the actual interface-audit
  35  objects and `slotDispClass` the grounded displacement-class table.
  36  The minus sign is the raw cell stencil's own sign
  37  (`rawCellStencil = (2/N^3) * (-sum ...)`).
  38
  39## Proof architecture (memory-guard split)
  40
  41The 216-term polynomial normalization lives in the LEAF module
  42`ReggeTTGateBBridgeCore` (import-light so the local build memory guard
  43is respected); every literal table it uses is kernel-identified here
  44with the corresponding ACTUAL raw-stencil object
  45(`coreWeight_eq_raw`, `corePolEdgeCoeff_eq`, `slotDispCore_eq`,
  46`tripleTerm_ident`), so nothing rests on a transcription:
  47
  481. `reggeTTMoment_eq_rawTripleSum`: the bucket fold with the
  49   fiber-aggregated amplitude equals the plain 216-triple sum
  50   (`Finset.sum_image'`; nothing dropped or double counted).
  512. `tripleTerm_ident`: each signed raw term equals the core term.
  523. `coreTripleSum_eq_spikeSum` (core): the triple sum equals
  53   `tetBlock0 + .. + tetBlock5` with free `s2 s3 p`, identically.
  544. `rawMoment_eq_committedSpikeLHS`: chained at
  55   `s2 = sqrt 2, s3 = sqrt 3, p = pi`.
  565. `gateB_convention_bridge`, THE LOCKED HEADLINE:
  57   `GateBConventionTarget rawMomentSupport (rawPhaseQuadratic x)
  58   (rawBucketAmplitude E) E x` for every `E, x`.
  59
  60`tt_continuum_certificate` and the spike's `-1/4` conclusion are NEVER
  61invoked; only the spike LHS blocks `tetBlock0..5` are used, as data.
  62
  63## Disclosure: the seven TT hypotheses are not consumed
  64
  65The bridge equality turned out to hold IDENTICALLY in `(E, x)`: the raw
  66J-weighted moment and the full-Hessian spike moment agree per
  67tetrahedron type BEFORE any TT reduction (the theta-second-derivative
  68part of the spike's Hessian weights drops out of the second-moment
  69layer per tet).  The locked target Prop takes the seven TT equations as
  70antecedents; they are introduced and the consequent is closed a
  71fortiori by the unconditional identity.  The stronger unconditional
  72statement is exported as `rawMoment_eq_committedSpikeLHS` so no
  73hypothesis strength is hidden.
  74
  75## Inherited axiom footprint (disclosure)
  76
  77Everything here is finite algebra over the Gate C-A2f table; the
  78expected footprint of every theorem is the standard trio
  79`[propext, Classical.choice, Quot.sound]`.  Receipts at end of file.
  80
  81No `sorry`, no `admit`, no new axioms, no `native_decide`, no `: True`
  82or `Nonempty`-only headline in this file.
  83-/
  84
  85namespace IndisputableMonolith
  86namespace Gravity
  87namespace Analysis
  88namespace ReggeTTGateBBridge
  89
  90open Geometry.PeriodicFreudenthalTorus
  91open ReggeTTSymbolPreflight
  92open ReggeTTBlochInterfaceAudit
  93open ReggeTTBlochConventionAudit
  94open ReggeTTGateBBridgeCore (coreWeight slotDispCore slotMidTwice
  95  corePolEdgeCoeff coreTripleTerm coreTripleSum_eq_spikeSum)
  96open ReggeTTBucketAggregation (rawJacobianCoefficient_eval)
  97open ReggeTTHingeAwareZeroMode (slotDispClass slotDispClass_grounded)
  98
  99noncomputable section
 100
 101set_option maxHeartbeats 1600000
 102
 103/-! ## §1. Grounding the literal tables against the actual objects -/
 104
 105/-- GROUNDING (THEOREM): the literal doubled-midpoint table reproduces
 106the ACTUAL preregistered midpoint Bloch phase of the periodic geometry:
 107for every momentum `k` and slot, the midpoint phase of the local edge at
 108the base cell is `sum_i k_i * (slotMidTwice t f i) / 2` (stated at the
 109smallest campaign torus `N = 4` with the base cell; the offsets are
 110cell-relative by construction). -/
 111theorem edgeMidpointPhase_grounded (k : Fin 3 → ℝ) (t f : Fin 6) :
 112    edgeMidpointPhase 4 k
 113        (localEdgeOf (((0 : Fin 4), (0 : Fin 4), (0 : Fin 4)) :
 114          Vertex 4 4 4) t f) =
 115      ∑ i : Fin 3, k i * (((slotMidTwice t f i : ℤ) : ℝ) / 2) := by
 116  fin_cases t <;> fin_cases f <;>
 117    · simp only [edgeMidpointPhase, Fin.sum_univ_three, vertCoord,
 118        localEdgeOf, addVertexBits, addBits, addBit, bit, vertexBits,
 119        cubeEdgeBase, cubeEdgeDisp,
 120        Geometry.FreudenthalCubeTriangulation.localEdgeOf,
 121        FreudenthalStencilPreflight.dispReal, slotMidTwice]
 122      push_cast
 123      norm_num
 124
 125/-- The core weight table IS the actual raw Jacobian coefficient (via
 126the Gate C-A2f kernel evaluation; nothing is transcribed on trust). -/
 127theorem coreWeight_eq_raw (f g : Fin 6) :
 128    coreWeight f g = rawJacobianCoefficient f g := by
 129  rw [rawJacobianCoefficient_eval f g]
 130  fin_cases f <;> fin_cases g <;>
 131    norm_num [coreWeight, ReggeTTBucketAggregation.rationalStencilWeight]
 132
 133/-- The core edge-class linear forms ARE the actual `polEdgeCoeff`. -/
 134theorem corePolEdgeCoeff_eq (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
 135    corePolEdgeCoeff E d = polEdgeCoeff E d := by
 136  fin_cases d <;>
 137    · simp only [corePolEdgeCoeff, polEdgeCoeff, Fin.sum_univ_three,
 138        FreudenthalStencilPreflight.dispReal]
 139      ring
 140
 141/-- The core slot displacement table IS the grounded `slotDispClass`. -/
 142theorem slotDispCore_eq (t f : Fin 6) :
 143    slotDispCore t f = slotDispClass t f := by
 144  fin_cases t <;> fin_cases f <;> rfl
 145
 146/-! ## §2. The raw-stencil instantiation of the moment fold -/
 147
 148/-- The bucket key of one raw stencil triple `(t, f, g)`: slot pair
 149`(f, g)` with integer phase key the doubled midpoint displacement
 150`2*(mid_g - mid_f)`. -/
 151def bucketKeyOf (p : Fin 6 × Fin 6 × Fin 6) : Bucket :=
 152  ⟨p.2.1, p.2.2,
 153    fun i => slotMidTwice p.1 p.2.2 i - slotMidTwice p.1 p.2.1 i⟩
 154
 155/-- The support: the bucket set of the raw cell stencil (image of all
 156216 raw triples). -/
 157def rawMomentSupport : Finset Bucket :=
 158  Finset.univ.image bucketKeyOf
 159
 160/-- The phase quadratic of a bucket: the squared midpoint-displacement
 161phase `(sum_i x_i * u_i/2)^2` in direction `x` (the halving undoes the
 162doubling of the integer key). -/
 163def rawPhaseQuadratic (x : Fin 3 → ℝ) (b : Bucket) : ℝ :=
 164  (∑ i : Fin 3, x i * (((b.phase i : ℤ) : ℝ) / 2)) ^ 2
 165
 166/-- One signed raw stencil moment weight: `-(J_fg / (2 sqrt a*_f)) *
 167c_{d(t,f)} * c_{d(t,g)}` (the raw cell stencil's own minus sign). -/
 168def rawTripleWeight (E : Fin 3 → Fin 3 → ℝ)
 169    (p : Fin 6 × Fin 6 × Fin 6) : ℝ :=
 170  -(rawJacobianCoefficient p.2.1 p.2.2 *
 171    polEdgeCoeff E (slotDispClass p.1 p.2.1) *
 172    polEdgeCoeff E (slotDispClass p.1 p.2.2))
 173
 174/-- The amplitude: the honest BUCKET-FIBER AGGREGATION of the signed raw
 175stencil weights over the triples landing in the bucket. -/
 176def rawBucketAmplitude (E : Fin 3 → Fin 3 → ℝ) (b : Bucket) : ℝ :=
 177  ∑ p ∈ Finset.univ.filter (fun p => bucketKeyOf p = b),
 178    rawTripleWeight E p
 179
 180/-! ## §3. The fold equals the plain raw triple sum -/
 181
 182/-- The bucket fold with fiber-aggregated amplitudes equals the plain
 183sum over all 216 raw triples: no collision of bucket keys is dropped or
 184double counted (`Finset.sum_image'` on the key map). -/
 185theorem reggeTTMoment_eq_rawTripleSum (E : Fin 3 → Fin 3 → ℝ)
 186    (x : Fin 3 → ℝ) :
 187    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
 188        (rawBucketAmplitude E) =
 189      ∑ p : Fin 6 × Fin 6 × Fin 6,
 190        -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p := by
 191  unfold reggeTTMoment reggeTTBlochFold rawMomentSupport
 192  rw [Finset.sum_image' (fun p : Fin 6 × Fin 6 × Fin 6 =>
 193    -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p)]
 194  intro p _
 195  unfold rawBucketAmplitude
 196  rw [Finset.mul_sum]
 197  refine Finset.sum_congr rfl fun q hq => ?_
 198  have hkey : bucketKeyOf q = bucketKeyOf p := (Finset.mem_filter.mp hq).2
 199  rw [hkey]
 200
 201/-- Each signed raw moment term equals the core module's literal term
 202(pointwise identification of every table with its actual object; no
 203case split on the triple is needed). -/
 204theorem tripleTerm_ident (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
 205    (p : Fin 6 × Fin 6 × Fin 6) :
 206    -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p =
 207      coreTripleTerm E x p := by
 208  unfold rawPhaseQuadratic bucketKeyOf rawTripleWeight
 209  unfold ReggeTTGateBBridgeCore.coreTripleTerm
 210  rw [coreWeight_eq_raw, corePolEdgeCoeff_eq, corePolEdgeCoeff_eq,
 211    slotDispCore_eq, slotDispCore_eq]
 212
 213/-! ## §4. The bridge and the locked headline -/
 214
 215/-- **THE UNCONDITIONAL BRIDGE (THEOREM): the raw-stencil moment fold
 216equals the committed spike LHS IDENTICALLY in `(E, x)`.**  Chains the
 217fiber-aggregation fold, the pointwise identification, and the core
 218216-term identity at `s2 = sqrt 2`, `s3 = sqrt 3`, `p = pi` (the
 219sidecar's committed instantiation; the core identity holds for free
 220values).  The spike's `tt_continuum_certificate` and its `-1/4`
 221conclusion are never invoked: only the block data `tetBlock0..5`. -/
 222theorem rawMoment_eq_committedSpikeLHS (E : Fin 3 → Fin 3 → ℝ)
 223    (x : Fin 3 → ℝ) :
 224    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
 225        (rawBucketAmplitude E) =
 226      committedSpikeLHS (spikeInput E x) := by
 227  rw [reggeTTMoment_eq_rawTripleSum]
 228  rw [Finset.sum_congr rfl fun p _ => tripleTerm_ident E x p]
 229  rw [coreTripleSum_eq_spikeSum E x (Real.sqrt 2) (Real.sqrt 3) Real.pi]
 230  rfl
 231
 232/-- **GATE C-B HEADLINE (THEOREM): the panel-locked Gate B target is
 233closed on the raw-stencil instantiation.**  `GateBConventionTarget`
 234(exactly the sidecar's Prop) holds for the raw-stencil support, the
 235midpoint-displacement phase quadratic, and the bucket-fiber-aggregated
 236amplitude, for every `E` and `x`.  DISCLOSURE: the seven TT antecedents
 237of the locked Prop are introduced but not consumed, because the bridge
 238equality holds identically in `(E, x)`
 239(`rawMoment_eq_committedSpikeLHS`); the locked statement shape is closed
 240a fortiori and the stronger unconditional theorem is exported above. -/
 241theorem gateB_convention_bridge (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ) :
 242    GateBConventionTarget rawMomentSupport (rawPhaseQuadratic x)
 243      (rawBucketAmplitude E) E x := by
 244  intro _ _ _ _ _ _ _
 245  exact rawMoment_eq_committedSpikeLHS E x
 246
 247end
 248
 249end ReggeTTGateBBridge
 250end Analysis
 251end Gravity
 252end IndisputableMonolith
 253
 254#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.edgeMidpointPhase_grounded
 255#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.coreWeight_eq_raw
 256#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.corePolEdgeCoeff_eq
 257#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.slotDispCore_eq
 258#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.reggeTTMoment_eq_rawTripleSum
 259#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.tripleTerm_ident
 260#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.rawMoment_eq_committedSpikeLHS
 261#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge.gateB_convention_bridge
 262