axisEdgeEndpointsComparable5
plain-language theorem explainer
On the N=5 periodic Freudenthal torus, the two endpoints of any axis-aligned periodic edge are comparable in the product order. Local geometry and stencil audits cite this when ordering unordered pairs along coordinate axes. The proof cases on the three axis directions and reduces each to single-coordinate bit-flip comparability on Fin 5.
Claim. Let $v$ be a vertex of the $N=5$ periodic Freudenthal torus and let $d\in\{0,1,2\}$ be an axis direction. Form the periodic edge $e$ with base $v$ and positive axis displacement along $d$. Writing $e_1,e_2$ for the two endpoints of $e$, one has $e_1\le e_2$ or $e_2\le e_1$ in the product order on vertices.
background
This module certifies corrected axis-stencil coefficients on the $N=5$ mixed explicit-fiber Freudenthal residual by exact rational arithmetic (no floats). It audits every unordered monomial $\xi(u)\xi(v)$ coefficient against the Python reference audit.
A Vertex5 is a triple in $(\mathrm{Fin},5)^3$. A PeriodicEdge5 is a positive-displacement periodic edge: a base vertex together with one of seven cube displacements. Axis edges use the three pure-axis displacements (one coordinate flipped by one bit, the others fixed). Endpoints are obtained by adding the displacement bits via addBits/dispBits; addBit_false leaves a coordinate unchanged.
Comparability is the product (componentwise) partial order on vertices. The doc-comment notes this lemma remains useful for local geometry audits even though the full coefficient expansion now routes through a canonical order covering every unordered pair.
proof idea
Destructure the base vertex into coordinates $(x,y,z)$ and case on the axis index $d:\mathrm{Fin},3$.
For each axis, unfold PeriodicEdge.endpoints, periodicAxisDisp, dispBits, and addBits, then simplify with addBit_false so only the active coordinate moves. Invoke the single-coordinate lemma addBitTrueComparable5 on that coordinate: either the base bit is $\le$ the flipped bit or the reverse. Rebuild the product-order inequality by placing that comparison in the active slot and rfl on the fixed coordinates. The three cases are symmetric.
why it matters
The module is the Lean mirror of the corrected Freudenthal axis-stencil coefficient certificate for the $N=5$ residual. Axis-edge endpoint order is a small geometric prerequisite for treating unordered pairs ${u,v}$ when expanding local stencil contributions (negative corrected Dirichlet atoms on non-loop axis edges).
No downstream theorem currently depends on this declaration in the graph; the doc-comment states the live coefficient path prefers vertex5CanonLE for full unordered-pair coverage. The result still anchors axis-only audits and documents that product-order comparability holds on pure axis edges of the periodic torus used in the gravity stencil work. It sits in the discrete geometry layer feeding RS gravity certificates, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.