Track1MixedAxisCoeffSoundnessToAxisStencilEndpoint
plain-language theorem explainer
Packages Track 1.B Session 213 as an implication endpoint: coefficient-soundness of the explicit-fiber residual at N=5 yields the corrected mixed hinge-deficit axis-stencil target. Gravity auditors and Track 7 handoff consumers cite it as the named Prop that the holds theorem discharges. The body is a pure implication of two upstream Props, not a proof.
Claim. The packaging endpoint asserts: if, for every $N=5$ vertex potential $\xi$, the explicit-fiber axis-stencil residual equals the unordered monomial expansion of the rational residual coefficients, then the corrected mixed hinge-deficit axis-stencil target holds at the canonical periodic $N=5$ certificate scale.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs (A–F). It records what new endpoints prove without upgrading the discovery claim; remaining Track 1 displacement-class leaves stay open dependencies.
The antecedent is the Session 212/213 coefficient-soundness bridge at $N=5$: the real explicit-fiber residual equals the unordered monomial expansion of the rational residual coefficients, for every vertex potential on the five-vertex certificate. That is the remaining algebraic packaging surface after every coefficient was closed.
The consequent is the corrected mixed hinge-deficit axis-stencil target specialized to the canonical periodic instance at scale parameters $(5,5,5)$. Upstream packaging treats global explicit-fiber coefficient-table closure as what proves that corrected mixed axis-stencil target.
proof idea
Definitional packaging only: the Prop is the bare implication from explicit-fiber coefficient-soundness at $N=5$ to the canonical periodic mixed hinge-deficit axis-stencil target at $N=5$. No tactics or lemmas run here. The companion theorem discharges it by applying the existing bridge canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_coeffSoundness, which routes coefficient-soundness through the Session 204 explicit-fiber wrapper into the corrected-axis target.
why it matters
Session 213 Track 1.B corrected-target packaging: the same coefficient-soundness bridge also proves the corrected mixed axis-stencil target via the Session 204 explicit-fiber wrapper. Downstream, the holds theorem asserts this Prop is inhabited, and ForkHandoffIntegrationCert consumes Track 1 reduction/interface packages among the Fork A–F handoffs.
Per the integration cert, the structural master theorem still uses structural witnesses where required; Track 1 here is a reduction/interface package, not closure of open Schläfli leaves. In the gravity lane this pins the mixed-axis coefficient path into the N=5 stencil endpoint that Track 7 records, while displacement-class leaves remain the next dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.