correctedMixedTargetAtN5_of_gate
plain-language theorem explainer
The corrected Track 1.B gate at the N=5 certificate scale implies the corrected mixed hinge-deficit axis-stencil target at that scale. Gravity auditors closing the local Regge/J-cost endpoint cite this packaging step. The proof is a one-line application of the N=5 packaging theorem that reduces the axis-stencil target to the explicit-fiber coefficient identity named by the gate.
Claim. If the corrected Track 1.B gate holds at $N=5$ (equivalently: the explicit-fiber axis-stencil coefficient identity at that scale), then the corrected mixed hinge-deficit axis-stencil target holds at the canonical $N=5$ certificate scale.
background
Track 1.B aims at a local cubic-Taylor correspondence between Regge hinge deficit and a J-cost quadratic on the periodic cubic complex. Session 202's finite audit showed the legacy mixed identification was wrong-weighted: at the $N=5$ single-vertex bump the mixed quadratic evaluates to $12$, while the seven-class square-root edge stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$, and those scalars differ. The corrected identification equates the mixed quadratic to the rational axis stencil rather than the legacy edge stencil.
Second-order Schl"afli stationarity at $N=5$ is already a theorem, so corrected closure at the certificate scale reduces to one finite coefficient identity: the explicit-fiber axis-stencil target. The gate abbreviates exactly that identity. The conclusion is the packaged $N=5$ instance of the corrected mixed axis-stencil target (dimensions fixed at $5,5,5$). Upstream, a packaging theorem turns any proof of the explicit-fiber identity into the axis-stencil target at $N=5$.
proof idea
One-line term wrapper. The gate hypothesis is definitionally the explicit-fiber axis-stencil target at $N=5$. Feed it to the upstream packaging theorem canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_explicitFiberAxis, which specializes the general explicit-fiber-to-axis-stencil implication at dimensions $5,5,5$ (the decide side conditions discharge automatically). No further algebra.
why it matters
This module's job is the corrected Track 1.B endpoint: local correspondence with the axis stencil as quadratic, its homogeneity algebra, and rigidity explaining why the Session 202 correction is forced. The gate is the single remaining finite coefficient identity after Schl"afli stationarity; this theorem is the named bridge from that gate to the corrected mixed target used as the correspondence quadratic.
The gate itself is discharged externally by the Freudenthal axis-stencil coefficient certificate (finite native_decide over the $5^3=125$ vertex table). No downstream consumers are wired yet in the graph; the declaration exists so status records and later D2/damped-schedule hooks can assume the corrected $N=5$ target under the named gate rather than under a raw explicit-fiber hypothesis. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is pure gravity-side certificate packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.