Track1Disp0BaseVertexReductionEndpoint
plain-language theorem explainer
The zero-displacement Schläfli leaf on the N=5 periodic Freudenthal torus is packaged as an implication: the finite base-vertex cancellation target yields the filtered periodic-edge target for displacement class 0. Track 7 gravity integration cites this as Agent A's disp0 handoff endpoint. The declaration is a Prop alias of that implication; a companion theorem discharges it via a named base-vertex reduction lemma.
Claim. If the base-vertex form of the canonical $N=5$ second-order Schläfli stationarity leaf for displacement class $0$ holds (a finite sum over the $125$ base vertices of the $5\times5\times5$ periodic Freudenthal torus, with no filtered periodic-edge bookkeeping), then the fixed-displacement-class form of that typed Schläfli edge target holds for displacement index $d=0$.
background
Track 7 is the fork-handoff integration lane for the gravity master theorem. It records what parallel endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B Schläfli stationarity reduction at $N=5$; the remaining open work is a family of displacement-class leaves.
The typed second-order Schläfli target at fixed displacement $d\in\mathrm{Fin},7$ asserts that a weighted edge sum over the filtered periodic edges of class $d$ vanishes for every vertex potential on the canonical encoded periodic Freudenthal torus. The disp0 base-vertex target is the same leaf rewritten as a sum over the $125$ base vertices only, stripping filtered PeriodicEdge bookkeeping from the caller.
Upstream, the base-vertex target at $N=5$ is the finite periodic axis-edge cancellation statement; the fixed-displacement form is the general typed Schläfli target specialized to $d=0$. Active-edge count $A=1$ appears only as ambient RS scaffolding, not in the Prop body.
proof idea
Definitional packaging, not a tactic proof. The body is the single implication from the $N=5$ disp0 base-vertex target to the typed edge-displacement target at parameters $(5,5,5)$ and displacement index $0:\mathrm{Fin},7$, with the three $2<N$ side conditions discharged by decide.
The companion theorem track1_disp0_base_vertex_reduction_endpoint_holds is a one-line wrapper applying canonicalPeriodicSecondSchlaefliTypedEdgeDisp0TargetAtN5_of_baseVertexTarget, which is the actual reduction lemma that turns base-vertex cancellation into the filtered-edge form.
why it matters
This is the Agent A disp0 endpoint consumed by the integration lane. It feeds three downstream objects: the holds theorem that asserts the Prop, the ForkHandoffIntegrationCert structure field for Track 1 disp0 base-vertex reduction, and the one-statement conjunction fork_A_B_C_D_E_F_handoffs_integrated_one_statement that bundles Forks A–F for Track 7.
Per the module doc, Track 7 deliberately does not assert the unconditional discovery theorem. It records that the axis displacement-class leaf is reduced to finite base-vertex cancellation, with remaining Track 1 displacement-class leaves still open. In the RS gravity stack this sits inside the Schläfli-to-stationarity reduction chain on the six-tet cubic Dirichlet instance, not in the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.