Track1MixedAxisLhsRow100TranslationEndpoint
plain-language theorem explainer
The mixed-axis LHS stencil row at lattice vertex (1,0,0) is translation-normalized: its coefficients match the origin row after relative-vertex reduction. Track 1.B and Track 7 handoff consumers cite this as a Session 210 endpoint, independent of the already-proved RHS stencil translation. The declaration is a Prop alias for a Boolean decision certified upstream.
Claim. The mixed-axis left-hand-side stencil coefficient row at vertex $(1,0,0)$ is translation-invariant: for every vertex $v$ on the five-vertex domain, the coefficient pairing $((1,0,0), v)$ equals the coefficient pairing the origin with the translate of $v$ relative to $(1,0,0)$.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs (A through F). It records what new endpoints prove without upgrading the discovery claim, and keeps remaining Track 1 displacement-class leaves as open dependencies.
The upstream predicate checks translation invariance of the corrected three-axis mixed-fiber LHS stencil coefficient: for a fixed source vertex $u$, it decides whether for every target $v$ the coefficient at $(u,v)$ equals the coefficient at the origin paired with the relative vertex of $v$ with respect to $u$. Here $u$ is specialized to the non-origin cube direction $(1,0,0)$.
The probe is deliberately on the LHS itself, separate from any RHS stencil translation already established in the Freudenthal-axis coefficient certificates.
proof idea
Definitional alias, not a proved theorem. The Prop is definitionally the Boolean equality that the mixed-axis LHS coefficient translation-invariance decision returns true at source vertex $(1,0,0)$. No tactics; the companion holds theorem discharges it by citing the upstream Boolean certificate for that row.
why it matters
Session 210 Track 1.B LHS row-100 translation endpoint consumed by Track 7. It feeds the companion holds theorem and appears among the Track 1 reduction/interface facts packaged into the fork handoff integration certificate (alongside Schläfli reduction, disp0 base-vertex and stationary reductions, many-body amplitude-linear lift, and Track 6 sensitivity).
Per the integration certificate, the Track 1 result remains a reduction/interface package, not a closure of the open Schläfli leaves. The structural master theorem still uses structural witnesses where the master plan requires them. This endpoint narrows the mixed-axis LHS translation gap on one concrete non-origin row without claiming full displacement-class closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.