Track1ForallDispStationarityEndpoint
plain-language theorem explainer
Packages the Session 563 Track 1.B-SCH handoff as a single implication: stationarity of each of the seven partial displacement weighted-deficit derivatives at canonical N=5 yields the full N=5 weighted-deficit stationarity target. Track 7 fork-integration certificates and one-statements cite it so callers never see the seven-field bundle. Pure Prop definition; the discharging theorem is a one-line application of the forall-disp reduction lemma.
Claim. If for every displacement index $d \in \{0,\ldots,6\}$ the partial weighted deficit-derivative sum for displacement $d$ is stationary at the origin (for every vertex potential on the canonical periodic Freudenthal torus of size $N=5$), then the full canonical $N=5$ weighted-deficit stationarity target holds.
background
Track 7 is the Gravity fork-handoff integration lane. It records what parallel forks prove without upgrading the discovery claim. Fork A is the Track 1.B Schläfli-to-stationarity reduction at the canonical certificate scale $N=5$ on the periodic Freudenthal torus.
The full target is the $N=5$ typed-edge Schläfli condition rewritten as weighted-deficit stationarity of the mixed hinge-deficit length chain (the object consumed by the nonlinear Hessian route). Each leaf is the same stationarity statement restricted to one displacement direction $d$ among seven: for every vertex potential $\xi$, the partial weighted deficit-derivative sum in direction $d$ has derivative zero at the origin.
This definition hides that seven-field bundle behind a single quantified hypothesis so Track 7 can consume a uniform endpoint rather than seven separate leaf props.
proof idea
Definitional Prop, not a proved theorem. The body is the implication from the universal quantification over the seven displacement-leaf stationarity props to the full $N=5$ weighted-deficit stationarity abbrev. No tactics. The sibling theorem that asserts the endpoint holds is a one-line wrapper applying the upstream reduction canonicalPeriodicWeightedDeficitDerivativeStationaryTargetAtN5_of_forallDispStationarity.
why it matters
Session 563 direct uniform stationarity endpoint for Fork A (Track 1.B-SCH). It is the form Track 7 actually consumes: the integrated Fork A/B/C/D/E/F one-statement and ForkHandoffIntegrationCert both project this endpoint (Session 565 projections), and track1_forall_disp_stationarity_endpoint_holds discharges it.
In the Recognition gravity stack this is the clean handoff shape for the remaining displacement-class leaves at $N=5$: callers get one Prop instead of a seven-field bundle. It does not close those leaves; the module doc keeps the open Track 1 displacement-class work as the next dependency, and the integrated one-statement deliberately stops short of the unconditional discovery theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.