Track1MixedAxisEdgeLhsTranslationEndpoint
plain-language theorem explainer
Names the Track 1.B Session-212 endpoint asserting that each mixed explicit-fiber LHS edge summand is invariant under N=5 torus translation. Gravity auditors cite it when wiring Fork A into the Track 7 handoff certificate. The body is a pure Prop alias of the edge-summand translation bridge already proved upstream.
Claim. The mixed-axis left-hand-side edge coefficient is translation-invariant on the $N=5$ periodic complex: for every torus shift $a$, every periodic edge $e$, and every pair of vertices $u,v$, the coefficient of the translated edge and vertices equals the coefficient of $(e,u,v)$.
background
Module Gravity.MasterTheoremHandoffIntegration is the Track 7 integration-lane receipt for parallel fork handoffs. Fork A covers Track 1.B stationarity reduction at $N=5$; this declaration is one local endpoint in that package. It does not close the open Schläfli leaves; it only records what the new edge-summand fact proves.
The upstream proposition states the edge-summand form of the mixed LHS translation bridge: after factoring the mixed-axis LHS coefficient as a sum over periodic edges on the five-vertex torus, each summand must be invariant under simultaneous translation of the edge and its two endpoint vertices. That is the remaining local target once the global coefficient is decomposed edgewise.
Notation: Vertex5 and PeriodicEdge5 are the discrete $N=5$ torus vertices and edges; translateVertex5 / translateEdge5 are the torus action; the mixed-axis edge LHS coefficient is the explicit-fiber contribution appearing in the Track 1.B stencil.
proof idea
One-line definitional alias. The Prop is definitionally equal to the upstream edge-summand translation invariance statement; no extra proof work lives here. The companion theorem discharges the endpoint by applying the already-proved mixed-axis edge-coefficient translation invariance lemma.
why it matters
Track 7 consumes this endpoint as part of the Fork A handoff into ForkHandoffIntegrationCert. The module doc is explicit: the structural master theorem still uses structural witnesses where the plan requires them; Track 1 contributions are reduction/interface packages, not closures of the open Schläfli displacement-class leaves.
Downstream, the holding theorem packages the Session-212 edge-summand fact for the integration certificate, and a sibling full-coefficient translation endpoint sits next to it. In the broader RS gravity lane this is discrete stencil bookkeeping on the eight-tick / $N=5$ complex, not a new continuum Einstein equation. It keeps the fork ledger honest: translation invariance of the mixed LHS edge terms is recorded and available, while remaining Track 1 displacement leaves stay the next dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.