Track1MixedAxisEdgeLhsTranslationReductionEndpoint
plain-language theorem explainer
Defines the Track 1.B Session-211 reduction endpoint: full vanishing of the corrected N=5 mixed-axis residual coefficients follows from translation invariance of a single edge-summand LHS coefficient. Gravity auditors cite it when packaging the axis-stencil coefficient audit into the fork handoff. It is a pure implication Prop, not a proved theorem.
Claim. The reduction endpoint asserts: if the mixed-axis edge LHS coefficient is invariant under $N=5$ torus translations of edges and vertices, then the full residual coefficient certificate holds, i.e. the corrected mixed-axis residual coefficient vanishes for every pair of vertices on the $N=5$ complex.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs in the gravity master plan. It records what each fork endpoint proves without upgrading the discovery claim; remaining Track 1 displacement-class leaves stay open.
The full residual coefficient certificate is the finite vanishing statement $\forall u,v,;\mathrm{mixedAxisResidualCoeff}(u,v)=0$ still needed before converting the coefficient audit into the canonical periodic mixed-hinge deficit target at $N=5$. After factoring the mixed LHS coefficient as a sum over periodic edges, the remaining local bridge is translation invariance of one edge summand: translating an edge and both vertices by the same $N=5$ lattice vector leaves the edge LHS coefficient unchanged.
That invariance is the only heavy finite reindexing step left in the corrected axis-stencil coefficient certificate; the outer finite edge sum is reindexed by the edge-translation equivalence.
proof idea
No proof body: this is a definitional Prop, the bare implication from edge-summand translation invariance to the full residual coefficient certificate. The companion theorem discharges it in one line by applying the existing bridge lemma that lifts edge-LHS translation invariance through the finite edge reindexing to full coefficient vanishing.
why it matters
Session 211 packages the Track 1.B edge-summand reduction so Track 7 can consume a clean handoff fact. Downstream, the companion holds-theorem witnesses the endpoint, and the fork handoff integration certificate includes the broader Track 1 reduction/interface package (Schläfli reduction, disp0 base-vertex and stationary reductions, etc.).
Per the integration cert doc, the Track 1 result remains a reduction/interface package, not a closure of the open Schläfli leaves; structural witnesses stay where the master plan requires them. In the Recognition gravity stack this sits on the discrete $N=5$ axis-stencil residual path toward the master theorem, not on the T0–T8 forcing chain or the mass ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.