Track1DispStationaryReductionEndpoint
plain-language theorem explainer
For each of the seven displacement indices, stationarity of the partial weighted deficit-derivative sum implies the matching base-vertex Schläfli leaf on the canonical N=5 periodic Freudenthal torus. Gravity Track 1.B integration cites this as the parametric disp-d reduction endpoint. The declaration is a pure Prop alias packaging that implication over Fin 7.
Claim. For every displacement index $d \in \{0,\ldots,6\}$, if the partial $\mathrm{disp}\,d$ weighted deficit-derivative sum on the canonical $N=5$ periodic Freudenthal torus is stationary (derivative zero at the zero vertex potential), then the corresponding base-vertex typed-edge Schläfli stationarity leaf at $N=5$ holds.
background
Module Gravity.MasterTheoremHandoffIntegration is the Track 7 integration-lane receipt for parallel fork handoffs A–F. It records what the new endpoints prove without upgrading the discovery claim, and keeps remaining Track 1 displacement-class leaves as open dependencies.
The antecedent is stationarity of the partial $\mathrm{disp},d$ weighted deficit-derivative sum: for every vertex potential $\xi$ on the $N=5$ encoded periodic Freudenthal torus, the real function summing those weighted deficit derivatives has derivative zero at the origin. Upstream marks this as the precise remaining analytic/combinatorial content for each displacement leaf.
The consequent is the generic base-vertex form of the canonical $N=5$ displacement-class Schläfli stationarity leaf: a sum over base vertices of typed-edge Schläfli summands vanishes (or meets its target) for every vertex potential. Both sides are indexed by $d : \mathrm{Fin},7$, matching the seven displacement classes in the cubic six-tet Dirichlet instance.
proof idea
No proof body: this is a definitional Prop. It is the universal quantification over $d : \mathrm{Fin},7$ of the implication from the disp-$d$ weighted-deficit stationarity target to the matching base-vertex Schläfli target. The companion theorem track1_disp_stationary_reduction_endpoint_holds discharges it by applying, for each $d$, the existing reduction lemma that builds the Schläfli leaf from stationarity.
why it matters
Fork A in the Track 7 handoff is the Track 1.B stationarity reduction at $N=5$. This endpoint is the parametric $\mathrm{disp},d$ half of that package: it states that each displacement leaf’s Schläfli form follows from its partial weighted-deficit stationarity.
Downstream, track1_disp_stationary_reduction_endpoint_holds proves the Prop, and both ForkHandoffIntegrationCert and fork_A_B_C_D_E_F_handoffs_integrated_one_statement consume it alongside the Schläfli reduction, disp0 base-vertex/stationary endpoints, many-body lift, Page-capacity, $w(z)$ bands, and falsifier-sensitivity package. The integrated one-statement deliberately does not assert the fully unconditional discovery theorem; remaining displacement-class leaves stay open.
In RS gravity terms this is bookkeeping for the discrete curvature/stationarity side of the master theorem, not a new continuum GR derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.