Track1MixedAxisTranslationReductionEndpoint
plain-language theorem explainer
Defines the Track 1.B Session 209 reduction endpoint: translation invariance of the mixed-axis residual coefficients implies the full N=5 coefficient-vanishing certificate on all 125×125 vertex pairs. Gravity auditors and Track 7 handoff consumers cite it as the interface between the origin-row audit and the full table. The body is a one-line Prop abbreviation of that implication.
Claim. If the mixed-axis residual coefficient model is translation-invariant on the $N=5$ vertex set (every pair $(u,v)$ has the same coefficient as the origin paired with the relative vertex of $u$ and $v$), then the full residual coefficient certificate holds: $\mathrm{mixedAxisResidualCoeff}(u,v)=0$ for all vertices $u,v$.
background
Track 7 is the fork-handoff integration lane for gravity. It records what parallel endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; the remaining displacement-class leaves stay open.
The corrected axis-stencil residual at $N=5$ lives on a $5^3=125$ vertex set. The full coefficient-vanishing statement asserts that the mixed-axis residual coefficient vanishes on every ordered pair of vertices. Compiling all $125\times 125$ rows naively is heavy; the intended bridge is translation invariance of the rational residual model.
Upstream, translation invariance means every coefficient equals the origin-row value at the relative vertex. The full certificate is exactly universal vanishing of those coefficients, and is the finite gate before converting the audit into the canonical periodic mixed-hinge deficit target at $N=5$.
proof idea
Pure definitional abbreviation: the endpoint is the implication from the translation-invariance bridge proposition to the full residual coefficient-vanishing proposition. No tactics or lemmas run here. The companion theorem discharges it by applying the existing reduction fullResidualCoeffCert_of_translationInvariant.
why it matters
Session 209 packages the Track 1.B full-table reduction so Track 7 can consume a clean interface: once translation invariance is available, the origin-row certificate upgrades to the full $125\times 125$ vanishing certificate without row-by-row compilation.
Downstream, ForkHandoffIntegrationCert records Track 1 material as a reduction/interface package (not closure of the open Schläfli leaves), alongside Track 2 many-body and Track 6 sensitivity handoffs. The companion track1_mixed_axis_translation_reduction_endpoint_holds asserts this endpoint is inhabited.
In the gravity master-theorem lane this is scaffolding for the axis-stencil coefficient audit on the discrete recognition geometry, not a claim about continuum GR or the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.