track1_schlaefli_reduction_endpoint_holds
plain-language theorem explainer
Fork A records that seven N=5 displacement-class Schläfli leaves imply the canonical weighted-deficit stationarity target used by the nonlinear Hessian route. Integration certificates and the Track 7 one-statement handoffs cite this as the 1B-SCH reduction endpoint. The proof is a one-line term applying the existing seven-displacement stationarity theorem.
Claim. If the seven displacement-class second Schläfli typed-edge targets hold on the canonical periodic lattice at $N=5$, then the weighted-deficit derivative stationarity target at $N=5$ holds.
background
Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master theorem. Fork A is the Track 1.B stationarity reduction labeled 1B-SCH at lattice size $N=5$. It does not upgrade the discovery claim; it packages what the new endpoints already prove and leaves remaining displacement-class leaves as open dependencies.
On the periodic Freudenthal torus, a positive-displacement edge is a base vertex together with one of seven positive cube displacements. The Schläfli side of the argument supplies second-variation typed-edge targets for each of those seven classes. The weighted-deficit stationarity target is the object consumed by the local-correspondence and nonlinear Hessian machinery downstream of Track 1.B.
The endpoint proposition is the pure implication from the seven-leaf Schläfli package to that stationarity target. The concrete implication is already proved as the canonical seven-displacement stationarity theorem in the six-tet cubic Dirichlet instance.
proof idea
One-line term proof. The body is exactly the upstream theorem that seven displacement-class Schläfli leaves imply the canonical $N=5$ weighted-deficit stationarity target. That theorem reduces via the typed-edge iff for the weighted-deficit derivative at $(5,5,5)$, then applies the seven-disp-to-typed-edge Schläfli target lemma. No extra hypotheses or bookkeeping are introduced at this layer.
why it matters
This is the Fork A receipt consumed by the integration lane. It appears as a conjunct in the full A/B/C/D/E/F handoff one-statement and in the backward-compatible A/C/F receipt, and it is the track1_schlaefli_reduction field of the fork handoff integration certificate.
In the Recognition gravity stack it closes the 1B-SCH handoff into the Track 1.B local-correspondence and Hessian route: once the seven $N=5$ Schläfli leaves are granted, stationarity of the weighted deficit is on the table. The module doc is explicit that this does not assert the unconditional discovery theorem; remaining Track 1 displacement-class leaves stay as the next dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.