Track1MixedAxisLhsTranslationEndpoint
plain-language theorem explainer
Session 212 Track 1.B endpoint: the mixed explicit-fiber LHS coefficient model on the five-vertex axis stencil is translation invariant after reindexing the periodic edge sum. Track 7 fork-handoff integration and the companion holds theorem cite it as a named receipt. The declaration is a one-line Prop alias of the upstream translation-invariance statement.
Claim. The mixed-axis left-hand-side coefficient model is translation invariant: for all vertices $u,v$ in the five-vertex set, the mixed-axis LHS coefficient at $(u,v)$ equals the coefficient evaluated at the origin paired with the relative vertex of $u$ and $v$.
background
This module is the Gravity Track 7 integration-lane receipt for parallel fork handoffs (Tracks 1.B stationarity, physical residual/Bianchi, many-body amplitude lift, Page capacity, dark-energy $w(z)$, and falsifier sensitivity). It records what the new endpoints prove without upgrading the discovery claim, and leaves remaining Track 1 displacement-class leaves open.
The upstream proposition asserts translation invariance of the mixed explicit-fiber LHS coefficient model: for every pair of vertices $u,v$ on the $N=5$ stencil, the mixed-axis LHS coefficient equals the same coefficient at the origin with the relative vertex of $u$ and $v$. That statement is described as the only heavy finite reindexing bridge left in the corrected axis-stencil coefficient certificate.
In this setting, "mixed" means the explicit-fiber form of the LHS coefficient on the Freudenthal/axis stencil; translation invariance after periodic edge-sum reindexing is the algebraic content packaged here as a Track 1.B endpoint.
proof idea
Definitional alias only: the endpoint Prop is definitionally equal to the upstream mixed-axis LHS coefficient translation-invariance proposition. No extra proof work lives at this declaration; the companion holds theorem discharges it by applying the proved translation-invariance lemma for the mixed-axis LHS coefficients.
why it matters
Named Session 212 Track 1.B receipt consumed by Track 7. It feeds the fork handoff integration certificate structure, which packages Forks A–F and treats the Track 1 material as a reduction/interface package rather than closure of the open Schläfli leaves. The companion holds theorem asserts the endpoint and is the fact integration code actually consumes.
Within the gravity master-theorem lane this pins the finite reindexing bridge for the corrected $N=5$ axis-stencil residual: once coefficients are translation-invariant under relative-vertex reindexing, residual and stationarity reductions can treat a single base-vertex representative. It does not finish the Schläfli or displacement-class leaves; those remain the next dependency called out by the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.