Track1MixedAxisCoeffCertEndpoint
plain-language theorem explainer
Session 207 Track 1.B endpoint: the translation-normalized origin-offset residual coefficients for the corrected N=5 axis-stencil all vanish in Lean. Gravity Track 7 cites it as a coefficient handoff fact inside the fork-integration certificate. The declaration is a one-line Prop alias equating the Boolean audit flag to true; the full unordered-pair table remains a Python exact check.
Claim. The proposition that the Lean Boolean audit of translation-normalized origin-offset residual coefficients for the corrected $N=5$ axis-stencil equals true: for every vertex $v$ in the five-cube vertex set, the mixed-axis residual coefficient of the pair $(\mathrm{origin}, v)$ is the rational $0$.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs (A through F). It records what the new endpoints prove without upgrading the discovery claim, and keeps remaining Track 1 displacement-class leaves as open dependencies.
The upstream Boolean originResidualCoeffsZero is the translation-normalized exact rational coefficient audit for the corrected $N=5$ axis-stencil target. Its doc states: the companion Python audit checks all unordered vertex pairs; Lean checks the 125 origin-offset representatives in the same rational coefficient model, via decide on $\forall v$, mixed-axis residual coeff at (origin, $v$) equals zero.
Sibling endpoints in the same file package Schläfli reduction, disp0 base-vertex and stationary reductions, seven-stationarity, and Track 2 many-body amplitude-linear lift. This coefficient endpoint is the Session 207 rational-vanishing receipt for Fork A / Track 1.B.
proof idea
Definitional alias, not a tactic proof. The Prop is literally the equality of the upstream Boolean audit flag to true. Discharge is deferred to the companion theorem that rewrites via originResidualCoeffsZero_eq_true (the decided universal quantification over the 125 origin-offset representatives).
why it matters
Track 7 consumes this as the Session 207 coefficient endpoint. The companion theorem track1_mixed_axis_coeff_cert_endpoint_holds proves the Prop holds. The integration structure ForkHandoffIntegrationCert packages Forks A–F; its doc stresses that the Track 1 result is a reduction/interface package, not closure of the open Schläfli leaves, while structural master-theorem witnesses remain where the master plan requires them.
In the Recognition gravity stack this pins the exact rational vanishing of origin-offset mixed-axis residuals for the corrected $N=5$ stencil, a concrete handoff fact on the path from Freudenthal axis-stencil certification toward master-theorem assembly. It does not finish the unordered-pair table (still Python) and does not close displacement-class leaves flagged as the next dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.