Track1SchlaefliReductionEndpoint
plain-language theorem explainer
Fork A endpoint: the seven N=5 displacement-class Schläfli typed-edge leaves imply the weighted-deficit stationarity target used by the nonlinear Hessian route. Integration certificates and the Track 7 handoff one-statements cite this Prop as the Track 1.B reduction interface. It is a pure definition packaging that implication, not a proof of the leaves.
Claim. The proposition asserting that if the seven named $N=5$ displacement-class Schläfli typed-edge obligations hold, then the weighted-deficit derivative stationarity target at the canonical periodic $N=5$ scale 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 at $N=5$ (label 1B-SCH): it does not close the open Schläfli leaves, but records the reduction interface those leaves feed.
Upstream, CanonicalPeriodicSecondSchlaefliTypedEdgeSevenDispTargetsAtN5 packages seven parallelizable displacement-class obligations (disp0 through disp6) under the typed-edge Schläfli target at lattice size $N=5$. The consequent, CanonicalPeriodicWeightedDeficitDerivativeStationaryTargetAtN5, re-expresses that typed-edge Schläfli target as the weighted-deficit stationarity condition consumed by the nonlinear Hessian route.
The module keeps remaining Track 1 displacement-class leaves as the next dependency and does not upgrade the discovery claim.
proof idea
Definition only: the Prop is the bare implication from the seven-leaf Schläfli package to the weighted-deficit stationarity target at $N=5$. No tactics. The companion theorem track1_schlaefli_reduction_endpoint_holds discharges it by applying the existing reduction lemma that turns the seven displacement targets into the stationary weighted-deficit target.
why it matters
This is the Fork A handoff fact consumed by Track 7. It appears in ForkHandoffIntegrationCert as track1_schlaefli_reduction, and in both fork_A_B_C_D_E_F_handoffs_integrated_one_statement and the backward-compatible fork_A_C_F_handoffs_integrated_one_statement.
Downstream docs stress the point: the Track 1 result is a reduction/interface package, not a closure of the open Schläfli leaves; the integration one-statement deliberately does not assert the fully unconditional discovery theorem. Sibling endpoints (disp0 base-vertex, disp0 stationary, seven-stationarity) sit alongside it as further Track 1 reduction interfaces. In the RS gravity stack this is the clean seam between discrete Schläfli edge work and the Hessian stationarity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.