Gravity Analysis Regge Ttgate Bbridge Core Pol Edge Coeff Eq

The edge coefficient bridge

In numerical work on quantum gravity, a calculation is often split across modules, each written by a different person or at a different time. A recurring danger is that two modules encode the same physical quantity with different conventions, and the mismatch is found only after long computations disagree. The declaration corePolEdgeCoeff_eq is a machine-checked proof that closes exactly such a gap for a set of edge coefficients used in a Regge calculus calculation.

The classical setting is Regge calculus, a discrete approximation to general relativity where spacetime is built from flat tetrahedral blocks. The calculation in question concerns the second moment of a certain momentum distribution on the edges of these blocks. Two modules in the framework's library each define a table of coefficients, one called corePolEdgeCoeff, the other polEdgeCoeff. The theorem proves, by checking all seven possible displacement classes, that for every input the two tables produce identical real numbers. It is an equality of definitions, not a statement about physics.

The proof is a finite case check: the declaration splits on the seven displacement classes and simplifies both sides to the same polynomial expression. It relies on the fact that both tables were built from the same underlying stencil data. The practical consequence is that the rest of the calculation can use either table interchangeably, and the bridge between the two conventions is certified rather than assumed.

In Recognition Science, this theorem is one link in a chain that connects a raw stencil of 216 tetrahedral triples to a committed spike form used in a broader analysis. The chain includes other identifications, such as the core weight table matching the raw Jacobian coefficient, and the slot displacement table matching the grounded displacement class. Together they show that a large polynomial normalization, which could have been a transcription error, is in fact faithful to the raw data.

The declaration does not claim that the edge coefficients are physically meaningful on their own, nor that the spike form is the correct description of quantum gravity. It only certifies an equality between two tables. The broader question of whether the spike convention itself is justified remains a separate matter, addressed by other theorems in the library.

/-- The core edge-class linear forms ARE the actual `polEdgeCoeff`. -/
theorem corePolEdgeCoeff_eq (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
    corePolEdgeCoeff E d = polEdgeCoeff E d := by
  fin_cases d <;>
    · simp only [corePolEdgeCoeff, polEdgeCoeff, Fin.sum_univ_three,
        FreudenthalStencilPreflight.dispReal]
      ring

/-- The core edge-class linear forms ARE the actual `polEdgeCoeff`. -/
theorem corePolEdgeCoeff_eq (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
    corePolEdgeCoeff E d = polEdgeCoeff E d := by
  fin_cases d <;>
    · simp only [corePolEdgeCoeff, polEdgeCoeff, Fin.sum_univ_three,
        FreudenthalStencilPreflight.dispReal]
      ring

What this page does not claim

The declaration does not establish that the spike convention is physically correct. It does not prove any property of the edge coefficients beyond their equality across the two tables. It does not address the seven TT hypotheses that appear as antecedents in the locked headline theorem.

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: