Pith. sign in
theorem

w11

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode
domain
Gravity
line
242 · github
papers citing
none yet

plain-language theorem explainer

The raw Jacobian coefficient at edge-slot pair (1,1) equals the rational 1/8. Anyone expanding the Regge TT constant-block contraction or the free-coefficient perfect-square identity cites this table entry. The proof is a one-line rewrite through the 36-entry evaluation lemma, then rational arithmetic on the literal stencil table.

Claim. For edge-slot indices $f=1$ and $g=1$, the raw Jacobian coefficient $\frac{J_{1,1}}{2\sqrt{a^*_1}}$ equals $\frac{1}{8}$ as a real number.

background

In the Regge TT hinge-aware zero-mode campaign (Gate C-A3, Paper C / Pillar 1, Lane C), the assembled O(1) constant block of the Bloch symbol is built from per-tetrahedron Hessian data. Each raw Jacobian coefficient is a single-entry weight: the flat-angle Jacobian divided by twice the square root of the Freudenthal squared edge length at the left slot. These are radical-free numbers used before any fiber aggregation.

Upstream, the full literal rational table records all 36 slot-pair values as a bare match, phase-independent and never defined through a fiber sum. The evaluation theorem states that every raw coefficient equals the corresponding table entry cast from $\mathbb{Q}$ to $\mathbb{R}$; the (1,1) clause of that table is exactly $1/8$.

The module's larger goal is the assembled zero mode: the stencil-only residual at the reported TT witness is cancelled by the hinge term under the pinned convention assembled = hinge minus the recorded stencil residual.

proof idea

One-line wrapper. Rewrite via the evaluation theorem at indices $(1,1)$, which replaces the raw coefficient by the rational stencil weight of bucket $\langle 1,1\rangle$ cast to $\mathbb{R}$. Then norm_num discharges the match on the full literal table, whose $(1,1)$ clause is the rational $1/8$.

why it matters

This is one of the thirty-six concrete rationals expanded by the free-coefficient identity: the raw-table contraction over six tetrahedron types in seven free coefficients equals the perfect square $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$. That identity is the exact algebraic shape of the assembled constant block; it vanishes on the alternating-sum hyperplane where geometric edge-class coefficient vectors live, and nowhere else among free coefficients.

The same table feeds the full-star homothety stationarity theorems in the ReggeHinge4DStarKernel family (base and variants 12, 13, 22), which show the directional full-star sum against class weights is zero. Within Gate C-A3 the entry is local scaffolding for the zero-mode headline that the Schlaefli-reduced assembled constant block vanishes at the TT witness.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.