Gravity Analysis Regge Ttgate Bbridge Core Core Pol Edge Coeff

The edge coefficient table

In numerical analysis, a linear form is a rule that takes a grid of numbers and returns a single weighted sum. The declaration corePolEdgeCoeff defines seven such forms on a 3 by 3 matrix E, where E holds the nine entries of a small symmetric array. The first three forms simply pick out the diagonal entries E 0 0, E 1 1, and E 2 2. The next three sum a 2 by 2 corner: for example, the fourth form adds E 0 0, E 0 1, E 1 0, and E 1 1. The seventh form adds all nine entries. Each form is a plain arithmetic recipe, nothing more.

The table matters because of what it feeds. The same seven forms appear inside a much larger sum: a 216-term expression built from products of these forms, weights, and midpoint phases. That expression is the raw moment sum of a Regge calculus calculation, a discrete approach to general relativity where spacetime is approximated by flat tetrahedra. The machine-checked library of formal theorems proves that this 216-term sum equals the sum of six simpler blocks, for any choice of three free parameters and identically in the matrix E and the coordinate vector x. The proof works by expanding both sides and simplifying with the ring tactic, a computational method that verifies polynomial identities by normalizing them.

The role of corePolEdgeCoeff is therefore architectural, not physical. It is one of several literal tables that keep the heavy algebra in a leaf module, a file that imports only basic arithmetic and avoids the full symbol-program import chain, which would exceed the laptop build memory guard when combined with a 216-term normalization. The main module kernel-identifies this table with the actual polEdgeCoeff, so no transcription is trusted. The core identity coreTripleSum_eq_spikeSum is the theorem that the 216-term raw moment sum equals the sum of the six spike blocks; the spike blocks enter as data only, and the spike's own conclusion is never invoked.

What the declaration does not claim is equally important. It does not assert that the seven forms have any physical meaning on their own. It does not claim that the 216-term identity holds for any particular geometry; it holds for all E and x, but the theorem says nothing about whether that identity corresponds to a valid gravitational configuration. The declaration also does not claim that the Regge calculus approximation is correct or that the spike convention bridge is physically justified. It only establishes that, given the literal tables and the definitions, the algebraic identity is true. The expected axiom footprint is the standard trio, with no sorry, no admit, no new axioms, and no native_decide.

/-- Literal edge-class linear forms (`c_d = sum_ij E_ij D_d^i D_d^j`). -/
def corePolEdgeCoeff (E : Fin 3 → Fin 3 → ℝ) : Fin 7 → ℝ
  | 0 => E 0 0
  | 1 => E 1 1
  | 2 => E 2 2
  | 3 => E 0 0 + E 0 1 + E 1 0 + E 1 1
  | 4 => E 0 0 + E 0 2 + E 2 0 + E 2 2
  | 5 => E 1 1 + E 1 2 + E 2 1 + E 2 2
  | 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

/-- THE CORE IDENTITY (THEOREM): the 216-term raw moment sum equals the
sum of the six committed spike blocks, for COMPLETELY FREE `s2 s3 p` and
IDENTICALLY in `E` and `x`.  Only the block data is used; the spike's TT
conclusion is never invoked. -/
theorem coreTripleSum_eq_spikeSum (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) (s2 s3 p : ℝ) :
    (∑ q : Fin 6 × Fin 6 × Fin 6, coreTripleTerm E x q) =
      tetBlock0 (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) (x 0) (x 1) (x 2) s2 s3 p
        + tetBlock1 (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) (x 0) (x 1) (x 2) s2 s3 p
        + tetBlock2 (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) (x 0) (x 1) (x 2) s2 s3 p
        + tetBlock3 (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) (x 0) (x 1) (x 2) s2 s3 p
        + tetBlock4 (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) (x 0) (x 1) (x 2) s2 s3 p
        + tetBlock5 (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) (x 0) (x 1) (x 2) s2 s3 p := by
  simp only [Fintype.sum_prod_type]
  rw [Fin.sum_univ_six]
  rw [coreBlock0_eq E x s2 s3 p, coreBlock1_eq E x s2 s3 p,
    coreBlock2_eq E x s2 s3 p, coreBlock3_eq E x s2 s3 p,
    coreBlock4_eq E x s2 s3 p, coreBlock5_eq E x s2 s3 p]

private theorem coreBlock0_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (s2 s3 p : ℝ) :
    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (0, f, g)) =
      tetBlock0 (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) (x 0) (x 1) (x 2) s2 s3 p := by
  rw [tetBlock0_eq]
  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
  push_cast
  ring

What this page does not claim

The seven linear forms have no physical meaning on their own. The 216-term identity holds for any E and x, but it does not assert anything about the physical validity of the Regge calculus approximation. The spike convention bridge is not claimed to be physically justified by this declaration alone.

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/ReggeTTGateBBridgeCore.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: