Pith. sign in
theorem

w22

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

plain-language theorem explainer

The raw Jacobian coefficient at edge-pair indices (2,2) equals the exact rational 1/12. Anyone expanding the six-tetrahedron constant-block contraction into free edge-class coefficients cites this entry. The proof is a one-line wrapper: rewrite by the full 36-entry evaluation lemma, then norm_num on the literal rational stencil table.

Claim. The single-entry radical coefficient of the flat-angle Jacobian at slot pair $(2,2)$, divided by twice the square root of the corresponding Freudenthal squared edge length, equals $1/12$ in $\mathbb{R}$.

background

This module sits in the QG full-theory campaign (Paper C / Pillar 1, Lane C): it closes the hinge-aware zero-mode gate for the assembled Regge TT constant block. The raw Jacobian coefficient is the single-entry radical form $J_{fg}/(2\sqrt{a^*_f})$ used by the early bucket falsifier; it is not yet a fiber sum.

Upstream, rawJacobianCoefficient_eval states that every one of the 36 raw coefficients equals the corresponding entry of an independent literal rational table (rationalStencilWeight), obtained offline from the closed forms of the flat-angle Jacobian and Freudenthal squared edges and then kernel-checked entry by entry. That table is phase-independent and never defined through any fiber sum.

The local goal is the assembled $O(1)$ block at $k=0$: stencil-only residual plus hinge term, with the relative-minus assembly convention pinned by the witness-tie theorems.

proof idea

One-line wrapper. Rewrite the goal by the universal evaluation lemma rawJacobianCoefficient_eval at indices $(2,2)$, which replaces the radical coefficient by the cast of the literal rational stencil weight at bucket $\langle 2,2\rangle$. Then norm_num on that table entry discharges the equality to $1/12$.

why it matters

Feeds zeroMode_free_coefficients, the algebraic identity that the six-tetrahedron raw-table contraction in seven free coefficients is the perfect square $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$. That identity is the exact shape of the assembled constant block: it vanishes precisely on the alternating-sum hyperplane where geometric edge-class coefficient vectors live, and is the algebraic engine behind the zero-mode headline assembledConstantBlock_eq_zero.

In the Gate C-A3 story, the sympy diagnostic showed stencil-only residual nonzero under TT while the assembled quadratic vanishes; the kernel must therefore supply every rational entry that the free-coefficient expansion uses. This $(2,2)$ entry is one of those table pins. It does not itself invoke the Recognition forcing chain (T0–T8), but it is scaffolding for the Regge-TT gravity lane of the finishing charter.

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