module module moderate

`IndisputableMonolith.Gravity.FreudenthalAxisStencilCoeffCert`

Module packaging the full coefficient-vanishing certificate for the corrected N=5 axis-stencil residual on the periodic Freudenthal torus. Gravity auditors cite it as the finite algebraic gate before the residual audit becomes the explicit fiber axis-stencil target at N=5. Structure is a certificate assembly over Fin-5 vertex/edge translation lemmas imported from the physical six-tet cubic Dirichlet instance.

claimFor the corrected axis-stencil residual at lattice size $N=5$ on the periodic Freudenthal torus, every coefficient in the residual expansion vanishes, yielding the finite certificate required to identify the residual with the canonical periodic mixed-hinge deficit explicit fiber axis-stencil target at $N=5$.

background

Recognition Science gravity work tracks a local Regge/J-cost correspondence on discrete scaffolds. The Freudenthal torus supplies a periodic cubic lattice geometry; the physical six-tet cubic Dirichlet model is the continuum-facing target that the discrete residual must match. The upstream module does not give the Dirichlet equality for free: it packages the exact theorem obligations needed to instantiate that physical model on the periodic scaffold.

This module sits at the N=5 axis-stencil station. Sibling material introduces Fin-5 vertices and periodic edges, translation and negation on the five-point index set, and relative-edge maps. Those are the combinatorial substrate for expanding the corrected residual and reading off coefficients. The doc-comment frames the deliverable as the full coefficient-vanishing statement still required before the coefficient audit can be rewritten as the named explicit fiber axis-stencil target at N=5.

proof idea

Certificate module rather than a single theorem narrative. It assembles the finite N=5 coefficient-vanishing claim for the corrected axis-stencil residual, using the Fin-5 translation/negation algebra and the packaged obligations from the physical six-tet cubic Dirichlet instance. Expect explicit residual expansion, coefficient extraction on the periodic scaffold, and discharge that each coefficient is zero, closing the gate to the canonical target identification. Not a one-line wrapper; a structured finite audit.

why it matters in Recognition Science

Closes the finite algebraic step between coefficient audit and the canonical periodic mixed-hinge deficit explicit fiber axis-stencil target at N=5. Downstream, Track 1.B Corrected Quadratic consumes this lane as the axis-stencil local correspondence (Track 1.B route to Regge/J-cost, with the corrected gate itself still named open rather than asserted). Master Theorem Handoff Integration imports it into the Fork A / Track 1.B 1B-SCH stationarity reduction at N=5 among the parallel gravity fork receipts. Without the vanishing certificate, the residual cannot be promoted to the explicit N=5 target used by those handoffs.

scope and limits

Does not assert the physical Dirichlet equality on the continuum model.
Does not close the corrected Track 1.B gate; that gate remains named open downstream.
Does not treat N other than 5 or non-axis stencil residuals.
Does not prove Bianchi, many-body, or Page-capacity forks (B–D).
Does not replace the upstream obligation packaging for the six-tet instance.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import
IndisputableMonolith.Gravity.Track1BCorrectedQuadratic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import

declarations in this module (115)

abbrev Vertex5 L23
abbrev PeriodicEdge5 L24
def addFin5 L26
def negFin5 L29
theorem addFin5_zero_left L32
theorem addFin5_neg_self L37
theorem addFin5_neg_add_self L42
theorem addFin5_self_add_neg L48
def translateVertex5 L54
def negVertex5 L57
def relativeVertex5 L60
def translateEdge5 L63
theorem translateVertex5_neg_left L66
theorem translateVertex5_neg_right L72
def translateVertex5Equiv L78
def translateEdge5Equiv L84
def subOneMod5 L96
def subBit5 L99
theorem subBit5_addFin5 L102
def matchingBaseCell5 L107
theorem matchingBaseCell5_spec L111
def selectedCell5 L116
theorem selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell L119
theorem matchingBaseCell5_translate L128
theorem selectedCell5_translate L137
theorem addVertexBits_translate5 L143
theorem translateEdge5_endpoints L153
def sqEdgeRat L165
def snormRat L173
theorem sqEdgeRat_cast_eq_freudenthalTetSqEdges L211
theorem snormRat_cast_eq_freudenthalSchlaefliTable L217
theorem freudenthalLocalPairDisp_eq_of_mem L223
theorem periodicDispSqEdge_eq_freudenthalTetSqEdges_of_mem L231
def sameUnordered L245
theorem sameUnordered_translate L248
def scaledPairLocalVertexCoeff L256
theorem scaledPairLocalVertexCoeff_translate L267
def mixedAxisEdgeLhsCoeff L276
theorem mixedAxisEdgeLhsCoeff_translate L283
def mixedAxisLhsCoeff L297
theorem mixedAxisLhsCoeff_eq_sum_edge L300
def axisStencilResidualCoeff L303
def mixedAxisResidualCoeff L311
def originVertex L314
theorem translateVertex5_origin_left L317
theorem relativeVertex5_origin_eq_self L322
theorem relativeVertex5_self_eq_origin L329
def FullResidualCoeffCert L337
def MixedAxisLhsCoeffTranslationInvariant L343
def MixedAxisEdgeLhsCoeffTranslationInvariant L351
theorem mixedAxisLhsCoeff_translationInvariant_of_edge L357
def rowMixedAxisLhsCoeffTranslationInvariant L381
def AxisStencilResidualCoeffTranslationInvariant L388
def MixedAxisResidualCoeffTranslationInvariant L396
def axisStencilResidualCoeffTranslationInvariantCheck L401
theorem axisStencilResidualCoeffTranslationInvariantCheck_eq_true L406
theorem axisStencilResidualCoeff_translationInvariant L410
theorem mixedAxisResidualCoeff_translationInvariant_of_lhs L420
def originResidualCoeffsZero L431
theorem originResidualCoeffsZero_eq_true L434
theorem originResidualCoeffCert L438
theorem fullResidualCoeffCert_of_translationInvariant L442
theorem fullResidualCoeffCert_of_lhs_translationInvariant L449
theorem fullResidualCoeffCert_of_edge_lhs_translationInvariant L455
theorem mixedAxisEdgeLhsCoeff_translationInvariant L461
theorem mixedAxisLhsCoeff_translationInvariant L466
theorem fullResidualCoeffCert L470
abbrev P5 L477
abbrev VertexPotential5 L480
def potentialAtVertex5 L483
theorem freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_selectedCell5 L488
def vertex5Code L509
theorem vertex5Code_injective L512
def vertex5CanonLE L519
theorem unorderedDiagonalMonomialExpansionAtN5 L527
theorem unorderedCrossMonomialExpansionAtN5 L551
theorem unorderedSameUnorderedMonomialExpansionAtN5 L636
theorem scaledPairLocalVertexCoeffExpansionAtN5 L677
theorem scaledPairLocalVertexCoeffEndpointSumExpansionAtN5 L796
def scaledPairEndpointExpansionValueAtN5 L854

… and 35 more