Track1MixedAxisStencilReductionEndpoint
plain-language theorem explainer
Defines the Track 1.B corrected-target reduction endpoint: if the global explicit-fiber axis-stencil identity holds at the canonical N=5 scale, then the corrected mixed hinge-deficit axis-stencil target holds. Gravity Track 7 integration cites this as the Session 204 handoff fact. The body is a pure implication packaging two N=5 abbreviations; the companion theorem discharges it by the explicit-fiber reduction lemma.
Claim. The Track 1.B mixed axis-stencil reduction endpoint is the implication: if the global explicit-fiber coefficient-table identity for the mixed hinge deficit holds at the canonical certificate scale $N=5$, then the corrected mixed hinge-deficit axis-stencil target at $N=5$ holds.
background
This module is the Gravity Track 7 fork-handoff integration lane. It records what parallel forks prove without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; the remaining Track 1 displacement-class leaves stay open.
The two sides of the implication are $N=5$ specializations of mixed hinge-deficit targets on the physical six-tet cubic Dirichlet instance. The consequent is the corrected mixed hinge-deficit axis-stencil target at the canonical certificate scale. The antecedent is the global explicit-fiber coefficient-table target whose closure is designed to prove that corrected target.
In the Recognition gravity stack these targets encode discrete curvature (hinge deficit) constraints along mixed axes, with stencil coefficients fixed by the explicit fiber table rather than by an uncorrected residual.
proof idea
No proof body: this is a definitional abbreviation of a Prop. It is literally the implication from the explicit-fiber axis-stencil target at $N=5$ to the corrected mixed axis-stencil target at $N=5$. Discharge is deferred to the companion theorem track1_mixed_axis_stencil_reduction_endpoint_holds, which applies the existing reduction lemma that the corrected target follows from the explicit-fiber identity.
why it matters
Session 204 corrected-target endpoint for Track 1.B, consumed by Track 7. It feeds ForkHandoffIntegrationCert as part of the Track 1 reduction/interface package (not a closure of the open Schläfli leaves) and is witnessed by track1_mixed_axis_stencil_reduction_endpoint_holds.
In the fork map this sits under Fork A (1B-SCH stationarity reduction at $N=5$). The module doc is explicit: the structural master theorem still uses structural witnesses where required; this endpoint only records the corrected-target reduction, leaving displacement-class leaves as the next dependency. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is a discrete-geometry handoff inside the gravity master-theorem stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.