Track1MixedAxisCorrectedAxisStencilTargetEndpoint
plain-language theorem explainer
Packages the Session 230 corrected mixed hinge-deficit axis-stencil target at the canonical N=5 scale as a Track 7 handoff endpoint. Gravity Track 7 integration and the corresponding holds theorem cite it as a named Track 1 leaf. The body is a one-line alias of the specialized canonical periodic mixed hinge-deficit target.
Claim. The corrected mixed hinge-deficit axis-stencil target holds at the canonical certificate scale $N = 5$ (periodic mixed hinge-deficit stencil with all three size parameters equal to 5).
background
Track 7 is the fork-handoff integration lane for gravity: it records what parallel forks prove without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; remaining Track 1 displacement-class leaves stay open.
The upstream object is the corrected mixed hinge-deficit axis-stencil target specialized to the canonical $N=5$ certificate scale: all three discrete size parameters are 5, with decidable side conditions. That Prop is the global explicit-fiber coefficient-table target whose closure proves the corrected mixed axis-stencil statement at $N=5$.
This definition simply names that specialized Prop as a Track 1 mixed-axis endpoint for the handoff certificate bundle.
proof idea
Definitional one-line alias. The body is exactly the upstream abbreviation CanonicalPeriodicMixedHingeDeficitAxisStencilTargetAtN5, itself the mixed hinge-deficit axis-stencil target applied at parameters $(5,5,5)$ with decide proofs of the side conditions. No extra proof work occurs here.
why it matters
Gives Track 7 a stable name for the Session 230 corrected axis-stencil leaf so the fork integration certificate can consume it without inlining the $N=5$ specialization. Downstream, track1_mixed_axis_corrected_axis_stencil_target_endpoint_holds asserts this Prop by the corresponding canonical $N=5$ theorem, and ForkHandoffIntegrationCert bundles Track 1 reduction/interface packages (Schläfli reduction, disp0 base-vertex and stationary reductions, etc.) alongside Track 2 many-body and Track 6 sensitivity facts.
Per the module doc, this is a reduction/interface package, not closure of the open Schläfli leaves. It sits in the gravity master-theorem handoff path that feeds structural witnesses where the master plan still requires them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.