mixedAxisEdgeLhsCoeff
plain-language theorem explainer
Edge-local rational coefficient of the unordered monomial ξ(u)ξ(v) in the corrected N=5 mixed Freudenthal axis-stencil residual. Gravity auditors cite it when decomposing the global LHS stencil into per-edge summands before proving translation invariance or matching the Python rational audit. The body is a double sum: over the explicit Freudenthal local-pair fiber of the edge displacement, then over six tet edge-slots, adding the two endpoint contributions of the scaled pair-local vertex coefficient.
Claim. For a periodic edge $e$ on the $5\times5\times5$ torus and vertices $u,v$, the mixed-axis edge LHS coefficient is the rational $$\sum_{p\in F(\mathrm{disp}(e))}\sum_{k=0}^{5}\bigl(c_{\mathrm{scaled}}(e,p,k,e_1;u,v)+c_{\mathrm{scaled}}(e,p,k,e_2;u,v)\bigr),$$ where $e_1,e_2$ are the endpoints of $e$, $F$ is the explicit local Freudenthal $(\mathrm{tet},\mathrm{edge\text{-}slot})$ fiber of the displacement class, and $c_{\mathrm{scaled}}$ is the scaled pair-local vertex coefficient.
background
The module certifies the corrected Freudenthal axis-stencil residual on the $N=5$ periodic cubic torus by exact rational arithmetic, mirroring scripts/freudenthal_explicit_fiber_endpoint_analysis.py with no floating point. The object of study is the coefficient of every unordered monomial $\xi(u)\xi(v)$ in that residual.
Vertices and edges live on the $5\times5\times5$ periodic Freudenthal torus (Vertex 5 5 5, PeriodicEdge 5 5 5). Each edge carries a displacement class; the upstream fiber freudenthalLocalPairDispFiber lists the explicit local pairs (tetrahedron index, edge-slot) that realize that class. The sibling scaledPairLocalVertexCoeff evaluates the contribution of one such pair at one endpoint and one of the six tet edge-slots, after placing the selected cell and tet vertices on the torus.
This definition packages those atoms into a single edge-local rational: sum over the fiber and over slots, adding both endpoints of the given edge.
proof idea
Pure definitional construction, not a proof. Bind the two endpoints of the edge, then form the double finite sum over freudenthalLocalPairDispFiber edge.disp and k : Fin 6, adding the two calls to scaledPairLocalVertexCoeff at those endpoints. No lemmas are applied; the value is exactly that nested sum in Rat.
why it matters
This is the atomic edge summand from which the global mixed-axis LHS coefficient is built: mixedAxisLhsCoeff u v is literally the sum of mixedAxisEdgeLhsCoeff edge u v over all periodic edges. Downstream theorems expand the edge-local polynomial as a sum of checked endpoint/local-slot atoms (mixedAxisEdgeLhsCoeffExpansionAtN5), prove translation invariance of the edge coefficient under simultaneous translation of edge and vertices, and lift that invariance to the full LHS via the edge-sum factorization.
In the Recognition gravity track this sits inside the corrected Freudenthal axis-stencil certificate for Track 1.D on the $N=5$ torus: exact rational control of stencil coefficients before continuum or continuum-limit claims. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure for the discrete gravity residual audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.