Track1MixedAxisStencilRhsTranslationEndpoint
plain-language theorem explainer
Names the Track 1.B Session-209 endpoint asserting that the corrected three-axis stencil residual coefficients are translation-invariant on the N=5 periodic torus. Gravity Track 7 handoff integration cites it as the RHS-translation receipt before LHS-only reduction. The body is a pure Prop alias of the Freudenthal axis-stencil translation-invariance statement.
Claim. The Track 1 mixed-axis stencil right-hand-side translation endpoint is the proposition that the corrected three-axis stencil residual coefficient is translation invariant on the $N=5$ periodic torus: for all vertices $u,v$, the residual coefficient at $(u,v)$ equals the residual coefficient at the origin paired with the relative vertex of $u$ and $v$.
background
Track 7 (Fork Handoff Integration) records parallel fork receipts without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; this endpoint is the Session-209 RHS-translation piece of that package.
The underlying model is the corrected three-axis stencil residual coefficient on Vertex5 (the discrete $N=5$ torus). Upstream, translation invariance is stated directly: for all $u,v$, the residual coefficient at $(u,v)$ equals the coefficient evaluated from the origin against the relative vertex of $u$ and $v$. That side is small enough to certify in Lean and is the sole dependency here.
Sibling endpoints in the same module package Schläfli reduction, displacement-class leaves, seven-stationarity, and many-body amplitude-linear lifts; this definition only names the axis-stencil RHS translation fact.
proof idea
Definitional alias, not a proved theorem. The Prop is definitionally equal to the upstream translation-invariance statement for the corrected three-axis stencil residual coefficient. Discharge is deferred to the companion theorem, which applies the existing axis-stencil residual-coefficient translation-invariance proof in one line.
why it matters
Gives Track 7 a stable named receipt for Session 209's axis-stencil RHS translation fact so the fork handoff certificate can consume it without reopening the Freudenthal coefficient development. Downstream, the companion holds-theorem witnesses the endpoint, and the fork integration structure threads Track 1 reduction/interface facts alongside many-body, Page-capacity, dark-energy $w(z)$, and falsifier-sensitivity handoffs.
Per the module framing, this does not close open Schläfli or displacement-class leaves; it only records that the RHS is translation-invariant, after which the full coefficient certificate reduces to an LHS-only obligation. In the gravity lane this is bookkeeping for discrete stencil consistency on the $N=5$ torus, not a new continuum GR claim and not a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.