track1_mixed_axis_stencil_reduction_endpoint_holds
plain-language theorem explainer
The corrected N=5 mixed axis-stencil target for the canonical periodic hinge-deficit follows from the global explicit-fiber axis-stencil identity. Gravity Track 7 cites this as the Session 204 Track 1.B reduction endpoint inside the fork handoff certificate. The proof is a one-line term applying the N=5 canonical periodic mixed-hinge identity from the six-tet cubic Dirichlet instance.
Claim. If the canonical periodic mixed hinge-deficit satisfies the explicit-fiber axis-stencil target at $N=5$, then it satisfies the corrected mixed axis-stencil target at $N=5$.
background
Track 7 is the integration-lane receipt for parallel gravity fork handoffs. It records what each new endpoint proves without upgrading the discovery claim, and keeps remaining Track 1 displacement-class leaves as open dependencies. Fork A covers Track 1.B stationarity reduction at $N=5$.
The endpoint proposition is an implication: from the explicit-fiber form of the canonical periodic mixed hinge-deficit axis-stencil target at $N=5$, conclude the corrected mixed axis-stencil target at the same $N$. In the Regge/hinge setting, the axis stencil encodes translation-normalized residual structure on the periodic six-tet cubic geometry; the mixed target is the corrected Session 204 form of that residual condition.
Upstream, the PhysicalSixTetCubicDirichletInstance supplies the identity that the corrected target follows from the global explicit-fiber axis-stencil statement. Sibling endpoints in this module package Schläfli, displacement-zero, and seven-stationarity reductions in the same handoff style.
proof idea
One-line term proof. The goal is exactly the implication defining the endpoint proposition. It is discharged by applying canonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5_of_explicitFiberAxis, the Session 204 identity that the corrected $N=5$ axis-stencil mixed target is a consequence of the global explicit-fiber axis-stencil form on the canonical periodic mixed hinge-deficit.
why it matters
This declaration is the Session 204 corrected-target reduction theorem consumed by Track 7. It is wired into forkHandoffIntegrationCert as one of the Track 1.B handoff fields, alongside Schläfli reduction, displacement-class reductions, and the many-body amplitude-linear lift.
In the Recognition gravity stack, $N=5$ axis-stencil control is part of closing the discrete hinge-deficit residual path before Bianchi and physical-residual interfaces (Fork B). The module doc is explicit that this lane does not upgrade the discovery claim: it only certifies what the parallel forks already prove. Remaining Track 1 displacement-class leaves stay as the next dependency after this mixed-axis endpoint is recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.