Gravity Analysis Regge Ttgate Bbridge

The spike convention bridge

Regge calculus is a way of doing general relativity without smooth geometry: spacetime is chopped into flat tetrahedral blocks, and gravity lives on the edges and faces where those blocks meet. The framework's quantum-gravity program works in this discrete setting, and it needs to compare two distinct ways of writing down a certain moment, a weighted sum over the tetrahedra that encodes how the geometry responds to a probe direction. The first way starts from the raw stencil, the literal list of 216 tetrahedron configurations with their signed weights. The second way is the committed spike, a condensed expression built from six blocks, each a sum over tetrahedra of a particular type. The module ReggeTTGateBBridge proves, in the machine-checked library of formal theorems, that these two sums are the same number for every choice of external field and probe direction.

The proof is a chain of identifications. It first shows that the bucket fold, the version of the moment that groups the 216 raw terms by their phase key, is exactly equal to the plain sum over all 216 triples, with nothing dropped and nothing counted twice. Then it shows that each signed raw term is pointwise equal to the corresponding term in the core module, the leaf file that carries the heavy 216-term polynomial normalization. The core identity then matches that triple sum to the six spike blocks at the committed values of the square roots of 2 and 3 and pi. Chaining these three equalities gives the headline theorem: the raw-stencil moment equals the committed spike left-hand side, for every E and x.

The surprising part is what the proof does not use. The bridge equality holds identically in the external field and probe direction, before any of the seven TT hypotheses, the theory's transverse-traceless conditions, are applied. The locked target proposition takes those seven equations as antecedents, but the proof introduces them and then closes the consequent a fortiori, because the unconditional identity already holds. The stronger statement is exported separately, so no hypothesis strength is hidden. The spike's own continuum certificate and its minus one quarter conclusion are never invoked; only the six block expressions are used, as data.

What this establishes in plain language is a consistency guarantee. Two independent-looking ways of assembling the same physical quantity, one from the raw geometric stencil and one from the condensed spike blocks, agree exactly. That agreement closes a panel-locked gate in the framework's campaign, the Gate B convention target, and it does so with the standard axiom footprint of the machine-checked library: the usual trio of choice, quotient, and propositional extensionality, with no new axioms and no admitted proofs. The reader can now treat the spike convention and the raw stencil convention as interchangeable in this layer of the calculation, which is what the gate was asking for.

/-- **THE UNCONDITIONAL BRIDGE (THEOREM): the raw-stencil moment fold
equals the committed spike LHS IDENTICALLY in `(E, x)`.**  Chains the
fiber-aggregation fold, the pointwise identification, and the core
216-term identity at `s2 = sqrt 2`, `s3 = sqrt 3`, `p = pi` (the
sidecar's committed instantiation; the core identity holds for free
values).  The spike's `tt_continuum_certificate` and its `-1/4`
conclusion are never invoked: only the block data `tetBlock0..5`. -/
theorem rawMoment_eq_committedSpikeLHS (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
        (rawBucketAmplitude E) =
      committedSpikeLHS (spikeInput E x) := by
  rw [reggeTTMoment_eq_rawTripleSum]
  rw [Finset.sum_congr rfl fun p _ => tripleTerm_ident E x p]
  rw [coreTripleSum_eq_spikeSum E x (Real.sqrt 2) (Real.sqrt 3) Real.pi]
  rfl

/-- The bucket fold with fiber-aggregated amplitudes equals the plain
sum over all 216 raw triples: no collision of bucket keys is dropped or
double counted (`Finset.sum_image'` on the key map). -/
theorem reggeTTMoment_eq_rawTripleSum (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
        (rawBucketAmplitude E) =
      ∑ p : Fin 6 × Fin 6 × Fin 6,
        -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p := by
  unfold reggeTTMoment reggeTTBlochFold rawMomentSupport
  rw [Finset.sum_image' (fun p : Fin 6 × Fin 6 × Fin 6 =>
    -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p)]
  intro p _
  unfold rawBucketAmplitude
  rw [Finset.mul_sum]
  refine Finset.sum_congr rfl fun q hq => ?_
  have hkey : bucketKeyOf q = bucketKeyOf p := (Finset.mem_filter.mp hq).2
  rw [hkey]

/-- Each signed raw moment term equals the core module's literal term
(pointwise identification of every table with its actual object; no
case split on the triple is needed). -/
theorem tripleTerm_ident (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (p : Fin 6 × Fin 6 × Fin 6) :
    -(rawPhaseQuadratic x (bucketKeyOf p)) / 2 * rawTripleWeight E p =
      coreTripleTerm E x p := by
  unfold rawPhaseQuadratic bucketKeyOf rawTripleWeight
  unfold ReggeTTGateBBridgeCore.coreTripleTerm
  rw [coreWeight_eq_raw, corePolEdgeCoeff_eq, corePolEdgeCoeff_eq,
    slotDispCore_eq, slotDispCore_eq]

/-- **THE UNCONDITIONAL BRIDGE (THEOREM): the raw-stencil moment fold
equals the committed spike LHS IDENTICALLY in `(E, x)`.**  Chains the
fiber-aggregation fold, the pointwise identification, and the core
216-term identity at `s2 = sqrt 2`, `s3 = sqrt 3`, `p = pi` (the
sidecar's committed instantiation; the core identity holds for free
values).  The spike's `tt_continuum_certificate` and its `-1/4`
conclusion are never invoked: only the block data `tetBlock0..5`. -/
theorem rawMoment_eq_committedSpikeLHS (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    reggeTTMoment rawMomentSupport (rawPhaseQuadratic x)
        (rawBucketAmplitude E) =
      committedSpikeLHS (spikeInput E x) := by
  rw [reggeTTMoment_eq_rawTripleSum]
  rw [Finset.sum_congr rfl fun p _ => tripleTerm_ident E x p]
  rw [coreTripleSum_eq_spikeSum E x (Real.sqrt 2) (Real.sqrt 3) Real.pi]
  rfl

What this page does not claim

This module does not derive the value of any physical constant or coupling. It does not prove that the spike convention is physically correct, only that it agrees with the raw stencil. It does not invoke the continuum certificate or the spike's minus one quarter conclusion.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTGateBBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: