Pith. sign in
theorem

w55

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

plain-language theorem explainer

The (5,5) entry of the raw cell-stencil Jacobian coefficient table is exactly zero as a real. Anyone assembling the free-coefficient contraction of the Gate A1/A2 assembled constant block cites this entry identity. The proof rewrites to the closed-form evaluator and normalizes the rational stencil weight to zero.

Claim. The raw Jacobian coefficient of the Regge cell stencil at face-pair indices $(5,5)$ equals $0$ in $\mathbb{R}$.

background

This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the Schlaefli-reduced assembled constant block for Regge TT. The assembled block is the $k=0$ value of the raw cell stencil; by the Gate A2 Schlaefli reduction it already folds the hinge/edge-diagonal $2\pi L''$ piece together with the per-tet Hessian, with relative sign fixed by assembled = hinge - Sigma_Gcc at the TT witness.

The raw Jacobian coefficient table is the numerical $6\times 6$ face-pair kernel that multiplies edge-class coefficients inside each tetrahedron type. Downstream, the free-coefficient contraction sums rawJacobianCoefficient f g against products of seven free slot coefficients over six tet types. Individual diagonal and off-diagonal entries of that table are discharged one-by-one before the global algebraic identity is stated.

Local setting: stencil-only residual at the reported TT witness is nonzero, while the assembled quadratic vanishes once the hinge block cancels that residual. Entrywise identities such as this one are the arithmetic substrate of that cancellation algebra.

proof idea

One-shot tactic proof. Rewrite the left-hand side by the closed-form evaluator rawJacobianCoefficient_eval at indices $(5,5)$, then run norm_num against ReggeTTBucketAggregation.rationalStencilWeight to reduce the resulting rational expression to the real $0$. No case split and no geometric hypothesis: pure coefficient arithmetic.

why it matters

Feeds zeroMode_free_coefficients, the headline 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 every geometric edge-class coefficient vector lives, and does not vanish for free coefficients.

Within Gate C-A3 this is bookkeeping that makes the zero-mode headline (assembledConstantBlock_eq_zero) an algebraic consequence rather than a numeric accident. It sits downstream of the sympy diagnostic that found stencil-only residual $-\pi(\sqrt{2}+4)/8$ cancelled by the matching hinge value, and upstream of the TT witness checks that pin the assembly sign. No T0–T8 forcing step is invoked here; the link is gravity-side Regge calculus on the recognition lattice.

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