track1_mixed_axis_translation_reduction_endpoint_holds
plain-language theorem explainer
Translation invariance of the mixed-axis residual coefficients upgrades the origin-row vanishing certificate to the full 125×125 coefficient table on the N=5 periodic torus. Track 7 handoff integration cites this as the Session 209 Track 1.B translation-reduction endpoint. The proof is a one-line packaging of the existing Freudenthal-axis stencil coefficient theorem.
Claim. If the mixed-axis residual coefficients are translation invariant on the $N=5$ periodic torus, then the full residual-coefficient certificate holds: every entry of the $125 \times 125$ coefficient table vanishes. Translation invariance therefore upgrades the origin-row certificate to the full table without enumerating all rows.
background
Track 7 is the integration-lane receipt for parallel fork handoffs in the gravity master-theorem stack. It records what each fork endpoint proves and does not upgrade the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; the remaining displacement-class leaves stay as open dependencies.
The mixed-axis residual is the exact rational coefficient model for the corrected three-axis stencil on the $N=5$ periodic torus (125 vertices). An origin-row certificate already shows vanishing at a fixed base vertex. Translation invariance of those coefficients means every other row is a translate of the origin row, so the full $125 \times 125$ vanishing table follows without compiling each entry.
Upstream, fullResidualCoeffCert_of_translationInvariant implements that reduction: rewrite by the translation hypothesis, then apply the origin-row certificate at the relative vertex on the five-point lattice.
proof idea
One-line term wrapper. The endpoint proposition is definitionally the implication from mixed-axis residual translation invariance to the full residual-coefficient certificate. The proof names the existing theorem fullResidualCoeffCert_of_translationInvariant, which already has that type: for arbitrary vertices $u,v$, rewrite the residual coefficient by translation invariance and invoke the origin-row certificate at the relative vertex relativeVertex5 u v.
why it matters
This is the Session 209 Track 1.B translation-reduction endpoint consumed by Track 7. It feeds forkHandoffIntegrationCert, the integration-lane certificate that bundles Fork A–F handoffs (Schläfli reduction, disp0 base-vertex and stationary reductions, many-body amplitude-linear lift, Page-capacity transfer, dark-energy $w(z)$ band, and falsifier-sensitivity packaging).
In the gravity stack the point is computational: proving one origin row plus translation invariance replaces a 15 625-entry compile. The module keeps remaining Track 1 displacement-class leaves as the next dependency; this endpoint closes only the mixed-axis translation-reduction leaf, not the full stationarity or physical-residual story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.