CanonicalPeriodicMixedHingeDeficitLengthChainTargetAtN5
plain-language theorem explainer
Specializes the mixed hinge-deficit length-chain identity to the canonical N=5 certificate scale on the periodic Freudenthal torus. Gravity packaging theorems cite it as the remaining Track 1.B endpoint after Schläfli closure. The body is a one-line abbreviation of the general target at lattice size 5 with decidable side conditions. Session 202 audits flag the present edge-stencil weighting as incorrect, so the name is retained only for packaging continuity.
Claim. The mixed hinge-deficit length-chain target on the canonical periodic Freudenthal instance holds at certificate scale $N=5$ (three lattice extents equal to $5$, with the standard decidable side conditions).
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it only names the residual theorem-shaped targets needed for that instantiation.
The mixed hinge-deficit length-chain target is the residual identity linking Regge hinge deficits (angle defects at hinges of the six-tet cubic decomposition) to a length-chain quadratic form on edge stencils. At the canonical certificate scale $N=5$, finite audits compare a single-vertex mixed left-hand side against an edge-stencil right-hand side built from axis, face-diagonal, and space-diagonal contributions.
Upstream geometry supplies the periodic Freudenthal torus scaffold and the Regge-action nonlinear correspondence; the length-chain endpoint certificates and cubic-lattice limit modules fix the discrete-to-continuum packaging into which this $N=5$ specialization plugs.
proof idea
Pure abbreviation: apply the general mixed hinge-deficit length-chain target at parameters $(5,5,5)$ and discharge the three side conditions by decide. No algebraic content is proved here; the name is a fixed certificate-scale Prop alias for downstream packaging.
why it matters
Track 1.B packaging reduces the canonical $N=5$ local Regge/J-cost correspondence to this single mixed length-chain identity: the handoff definition states that the edge-stencil local correspondence at $N=5$ follows once this target is assumed. The companion theorem canonicalPeriodicEdgeStencilLocalCorrespondenceAtN5_of_mixedLengthChain is exactly that implication, feeding the stationary weighted-deficit target from the near-zero Schläfli lane.
In the Recognition gravity stack this sits on the discrete Regge side of the continuum Dirichlet limit for the six-tet cubic model (the physical route toward the continuum action used with RS constants and the $D=3$ forcing). Session 202's exact finite audit exposes a scalar obstruction (mixed LHS $12$ versus edge-stencil RHS $6+6\sqrt{2}+2\sqrt{3}$), so the abbreviation is kept only so existing packaging theorems compile while a corrected mixed/Hessian target is named. Closing or replacing this surface is the next finite-lane task before the local correspondence can be unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.