Track1Disp0StationaryReductionEndpoint
plain-language theorem explainer
Packages Fork A's Agent A stationarity endpoint: on the canonical N=5 periodic Freudenthal torus, stationarity of the partial disp0 weighted deficit-derivative sum implies the base-vertex disp0 Schläfli leaf. Integration-lane consumers cite it as one Track 1.B reduction interface, not a closed discovery claim. The body is a pure Prop abbreviation of that implication.
Claim. The proposition asserting that stationarity of the partial $\mathrm{disp}_0$ weighted deficit-derivative sum (for every vertex potential on the canonical $N=5$ periodic Freudenthal torus) implies the matching base-vertex form of the $\mathrm{disp}_0$ Schläfli stationarity leaf at $N=5$.
background
Track 7 is the fork-handoff integration lane for gravity. It records exactly what parallel endpoints prove and does not upgrade the discovery claim. Fork A is the Track 1.B Schläfli-to-stationarity reduction package at $N=5$ on the canonical encoded periodic Freudenthal torus.
The antecedent is stationarity of the partial $\mathrm{disp}_0$ weighted deficit-derivative sum: for every vertex potential $\xi$, the sum has derivative zero at the origin. The consequent is the base-vertex $\mathrm{disp}_0$ Schläfli target: a finite sum over the 125 base vertices of typed edge summands vanishes, with no filtered periodic-edge bookkeeping. Upstream docs call the antecedent "the precise remaining analytic/combinatorial content for the $\mathrm{disp}_0$ leaf" and the consequent the "base-vertex form of the canonical $N=5$, $\mathrm{disp}_0$ Schläfli stationarity leaf."
proof idea
No proof: this is a definitional Prop packaging an implication between two named targets. The left-hand side is the stationarity target for the partial $\mathrm{disp}_0$ weighted deficit-derivative base sum at $N=5$; the right-hand side is the base-vertex second-Schläfli typed-edge $\mathrm{disp}_0$ target at $N=5$. Discharge is deferred to the companion theorem that applies the existing reduction lemma from stationarity to the base-vertex leaf.
why it matters
This is one of the seven Track 1 reduction interfaces that Fork A's handoff feeds into the Track 7 integration certificate. Downstream, it appears in the fork A/B/C/D/E/F one-statement and in ForkHandoffIntegrationCert as a required field of the integration package. The companion holds-theorem witnesses the implication via the existing stationarity-to-base-vertex reduction.
Module docs stress that Track 7 "does not upgrade the discovery claim" and keeps remaining Track 1 displacement-class leaves as the next dependency. The endpoint therefore narrows the $\mathrm{disp}_0$ leaf to a stationarity statement without closing the open Schläfli analysis. In the broader RS gravity stack this is bookkeeping for the discrete Regge/Schläfli sector on the $N=5$ torus, not a continuum GR derivation or a mass-ladder step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.