Track1TotalSymmetryStationarityEndpoint
plain-language theorem explainer
Total stationarity of the seven displacement-class weighted deficit-derivative sums, together with their mutual equality as one-variable functions, implies the canonical N=5 weighted-deficit stationarity target. Gravity Track 7 and Fork A handoff consumers cite this Prop as the direct total-plus-symmetry endpoint. It is a pure implication interface; the discharging theorem is a one-line application of the named reduction lemma.
Claim. If the sum over all seven displacement-class partial weighted deficit-derivative sums is stationary at the flat point on the canonical periodic Freudenthal torus of scale $N=5$, and if those seven partial sums are identical as functions of the real parameter $t$, then the canonical $N=5$ weighted-deficit derivative stationarity target holds.
background
Track 7 is the fork-handoff integration lane for gravity. It records what parallel endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B Schläfli-to-stationarity reduction at $N=5$ on the canonical encoded periodic Freudenthal torus.
The weighted-deficit stationarity target is the $N=5$ typed-edge Schläfli condition rephrased for the nonlinear Hessian route: the derivative of the weighted hinge-deficit functional vanishes at the flat vertex potential. Upstream, Session 567 splits this into two intermediate targets. Total stationarity asserts that the sum of the seven displacement-class base-sum derivatives has derivative zero at the flat point. Displacement symmetry asserts that all seven class-wise base-sum maps equal one common one-variable function (finite translation/cube symmetry after total stationarity).
This definition packages those two antecedents as the direct implication into the full $N=5$ stationarity target.
proof idea
No proof body: the declaration is a Prop abbreviation whose value is the nested implication
(total stationarity at $N=5$) $\to$ (displacement-class base-sum symmetry at $N=5$) $\to$ (weighted-deficit stationarity at $N=5$).
The companion theorem track1_total_symmetry_stationarity_endpoint_holds discharges it in one line by applying canonicalPeriodicWeightedDeficitDerivativeStationaryTargetAtN5_of_totalStationary_and_dispSymmetry.
why it matters
This is the Session 572 Track 7 endpoint for the direct total-plus-symmetry route on Track 1.B-SCH. It feeds the Fork A/B/C/D/E/F integration certificate and the integrated one-statement, both of which project it via dedicated accessors so Track 7 can consume total stationarity plus displacement symmetry without reopening the seven-leaf Schläfli reduction.
Downstream, fork_A_B_C_D_E_F_handoffs_integrated_one_statement deliberately stops short of the unconditional discovery theorem; this endpoint is one of the stronger handoff facts recorded there. Remaining Track 1 displacement-class leaves stay as open dependencies. In the broader RS gravity stack it tightens the discrete stationarity side of the master structural certificate at the $N=5$ certificate scale, without claiming continuum GR or full mass-ladder closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.