Track1SevenStationarityEndpoint
plain-language theorem explainer
The seven-displacement stationarity endpoint is the typed implication from the full seven-class displacement stationarity bundle to the single canonical N=5 weighted-deficit stationarity target. Track 1.B Hessian/local-correspondence work and Track 7 fork-handoff certificates cite it as the interface between the parametric seven-leaf bundle and the nonlinear stationarity target. It is a pure Prop abbreviation encoding that implication, not a proved closure of the leaves.
Claim. If every displacement class $d \in \{0,\ldots,6\}$ satisfies the base stationarity claim that the partial weighted deficit-derivative sum has vanishing derivative at zero, then the canonical $N=5$ weighted-deficit stationarity target (the typed-edge Schläfli target re-expressed for the nonlinear Hessian route) holds.
background
Track 7 is the Gravity fork-handoff integration lane. It records what parallel forks deliver without upgrading the discovery claim: Fork A is the Track 1.B stationarity reduction at $N=5$; remaining Track 1 displacement-class leaves stay open dependencies.
The seven-base bundle packages one HasDerivAt _ _ 0 claim per displacement class $d : \mathrm{Fin},7$ for the partial weighted deficit-derivative sum over that class. It supersedes the older disp0-only stationarity target. The consequent is the canonical $N=5$ weighted-deficit stationarity target: the typed-edge Schläfli target rewritten as the stationarity predicate consumed by the nonlinear Hessian route at certificate scale $(5,5,5)$.
Local setting is structural handoff bookkeeping, not unconditional GR recovery. Upstream docs stress that the bundle is parametric over all seven displacement classes and that the $N=5$ target is exactly what Track 1.B local-correspondence/Hessian machinery consumes.
proof idea
Definitional abbreviation only: the Prop is the bare implication from the seven-field stationarity structure to the single $N=5$ weighted-deficit stationarity abbrev. No tactics, no algebraic reduction. The companion theorem track1_seven_stationarity_endpoint_holds discharges it by applying the existing lemma that builds the canonical target from the seven-stationarity bundle.
why it matters
Fork A handoff needs a single named endpoint saying the seven-leaf stationarity package implies the Hessian-facing $N=5$ target. This definition is that endpoint. Downstream, track1_seven_stationarity_endpoint_holds proves it; ForkHandoffIntegrationCert and fork_A_B_C_D_E_F_handoffs_integrated_one_statement consume the sibling Track 1 reduction endpoints so Track 7 can cite Fork A's seven-leaf Schläfli-to-stationarity reduction alongside many-body, residual/Bianchi, Page-capacity, $w(z)$, and falsifier-sensitivity packages.
It does not close open Schläfli leaves. Module doc is explicit: integration records what endpoints prove and keeps remaining Track 1 displacement-class leaves as the next dependency. In RS gravity terms this is bookkeeping on the discrete recognition stencil at the eight-tick / $D=3$ cubic complex, not a new forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.