forkHandoffIntegrationCert_track1_forall_disp_stationarity
plain-language theorem explainer
The Track 7 fork-handoff certificate reexports the direct uniform displacement-stationarity endpoint for Track 1.B-SCH: if every one of the seven displacement modes has stationary weighted-deficit derivative at N=5, the full canonical periodic target follows. Gravity auditors cite it as the integration-lane receipt that the forall-quantified stationarity reduction is wired in. Proof is a one-line term reexport of the Session 563 endpoint theorem.
Claim. If for every displacement index $d\in\{0,\ldots,6\}$ the canonical periodic weighted-deficit derivative base-stationarity target at $N=5$ holds in mode $d$, then the full canonical periodic weighted-deficit derivative stationarity target at $N=5$ holds.
background
Track 7 is the integration-lane receipt for parallel gravity fork handoffs. It does not upgrade discovery claims; it records exactly which endpoints the forks have closed. Fork A is the Track 1.B (1B-SCH) stationarity reduction at $N=5$ on the canonical periodic weighted-deficit action.
The endpoint proposition packaged here is the direct uniform stationarity form: a single implication quantified over $d:\mathrm{Fin},7$. The hypothesis is that each of the seven displacement modes separately meets the base stationarity target for the weighted-deficit derivative at $N=5$. The conclusion is the unbundled full stationarity target at the same $N$, so callers need not open the seven-field bundle.
Upstream, the Session 563 theorem already proves this implication by reducing the full target from the forall-over-displacements hypothesis. The present declaration is the Track 7 certificate face of that same endpoint.
proof idea
One-line term proof: the certificate is definitionally the Session 563 endpoint proposition, and the body is exactly the already-proved theorem track1_forall_disp_stationarity_endpoint_holds. That upstream theorem itself is a one-line application of the reduction lemma that builds the full $N=5$ weighted-deficit stationarity target from the forall-over-Fin 7 displacement-mode hypothesis. No new algebra is done at the certificate layer.
why it matters
In the Recognition gravity stack this is the Fork A handoff receipt inside Track 7: it exposes the direct uniform displacement-stationarity endpoint for Track 1.B-SCH so the master integration lane can cite a single named Prop rather than the internal reduction lemma. The module doc is explicit that remaining Track 1 displacement-class leaves stay as the next dependency; this certificate only locks the forall-quantified stationarity reduction already closed at Session 563/565.
No downstream consumers are wired yet (used_by is empty), so its role is archival and interface: auditors checking the fork-handoff board can see that the $N=5$ weighted-deficit stationarity target is available in the uniform forall form. It sits beside sibling certificates for Schläfli reduction, disp-0 base/stationary reductions, seven-stationarity, and the many-body Track 2 endpoint, keeping the parallel forks synchronized without claiming a full master-theorem close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.