Track1MixedAxisOriginPropCoeffCertEndpoint
plain-language theorem explainer
Defines the origin-row vanishing statement for mixed-axis residual stencil coefficients on the N=5 Freudenthal lattice: every coefficient from the origin vertex is zero. Gravity Track 1.B and the Track 7 fork-handoff layer cite it as the Prop-shaped certificate behind translation invariance of the residual table. The body is a pure Prop abbreviation, not a proof.
Claim. For every vertex $v$ in the $5\times 5\times 5$ discrete lattice, the mixed-axis residual stencil coefficient from the origin $(0,0,0)$ to $v$ vanishes: $c_{\mathrm{mix}}((0,0,0),v)=0$.
background
The module is the Track 7 fork-handoff integration lane for gravity. It records parallel endpoints (Track 1.B stationarity reduction at $N=5$, physical residual/Bianchi interface, many-body amplitude lift, Page-capacity transfer, dark-energy $w(z)$ band, and falsifier sensitivity) without upgrading the discovery claim.
Vertex5 is the discrete $5\times 5\times 5$ vertex set used by the Freudenthal-axis stencil certificates. The origin vertex is the lattice point $(0,0,0)$. The mixed-axis residual coefficient of a pair of vertices is the sum of the mixed-axis left-hand-side coefficient and the axis-stencil residual coefficient (exact rationals).
Session 209 exposes the former boolean origin-row certificate as this theorem-shaped vanishing statement so the translation-invariance bridge can consume a Prop rather than an ad-hoc flag.
proof idea
No proof: this is a definitional Prop. It packages the universal quantification that every mixed-axis residual coefficient with first argument the origin vertex equals zero. The companion theorem track1_mixed_axis_origin_prop_coeff_cert_endpoint_holds discharges it by applying the existing origin residual coefficient certificate.
why it matters
Track 1.B needs an origin-row coefficient vanishing fact before translation invariance can promote a single-row certificate to the full residual table. This Prop is that endpoint. Downstream, the holds-theorem feeds the Track 7 integration certificate structure, which assembles Fork A–F handoffs for the structural master theorem. The module doc is explicit that Track 1 remains a reduction/interface package: open Schläfli and displacement-class leaves are not closed here. In the broader RS gravity program this is bookkeeping on the discrete stencil side of the master theorem, not a new dynamical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.