Track1TotalSymmetryStationarityReductionEndpoint
plain-language theorem explainer
Named proposition packaging the Track 1.B reduction: total stationarity of the seven-class weighted deficit-derivative sum plus displacement-class symmetry implies stationarity of each individual displacement leaf at N=5. Track 7 fork-integration certificates and the one-statement handoff cite it as the Session 568 endpoint. The body is a pure Prop abbreviation, not a proved implication.
Claim. The proposition that if the sum over all seven displacement-class partial weighted deficit-derivative sums is stationary at the flat point, and if those seven partial sums coincide as one-variable real functions, then for every displacement index $d\in\{0,\ldots,6\}$ the partial sum for class $d$ is stationary at the flat point, on the canonical periodic Freudenthal torus at $N=5$.
background
Module setting is Gravity Track 7 fork-handoff integration: a receipt lane that records what parallel forks prove without upgrading the discovery claim. Fork A is the Track 1.B Schläfli-to-stationarity reduction at $N=5$ on the canonical encoded periodic Freudenthal torus.
Three upstream targets supply the content. Total stationarity says the sum over all seven displacement-class partial weighted deficit-derivative sums has derivative zero at the flat vertex potential. Displacement symmetry says those seven partial sums are the same one-variable function (finite translation/cube symmetry after the total claim). Each leaf target asks stationarity of the partial sum for a fixed displacement $d:\mathrm{Fin},7$.
The remaining analytic work per leaf is exactly that leaf stationarity; this endpoint packages the reduction that total stationarity plus symmetry discharges all seven leaves at once.
proof idea
Definition-only packaging: the declaration is a Prop abbreviation whose body is the implication
total-stationarity target $\to$ displacement-symmetry target $\to$ $\forall d$, leaf-stationarity target $d$.
No tactics or lemmas run here. The actual discharge is the sibling theorem that applies canonicalPeriodicDispWeightedDeficitDerivativeBaseStationaryTargetAtN5_of_totalStationary_and_dispSymmetry to inhabit this proposition.
why it matters
Session 568 Track 7 endpoint for the total-plus-symmetry stationarity reduction on Track 1.B-SCH. Downstream, track1_total_symmetry_stationarity_reduction_endpoint_holds proves it; ForkHandoffIntegrationCert and both integrated one-statement theorems expose it as a projection field so Track 7 can consume the reduction without claiming unconditional discovery.
It sits among sibling Track 1 endpoints (Schläfli reduction, disp0 base-vertex and stationary reductions, seven-stationarity). Module doc is explicit: remaining Track 1 displacement-class leaves stay the next dependency; this only records the total-plus-symmetry closure path for the seven-leaf stationarity target at $N=5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.