vertex5Code
plain-language theorem explainer
Encodes an N=5 periodic lattice vertex (three coordinates in Fin 5) as a single natural number via base-5 place values. Anyone auditing the Freudenthal axis-stencil residual uses it to totally order vertices so unordered monomials get a unique representative. The body is a one-line arithmetic encoding: 25·x + 5·y + z.
Claim. For a vertex $v = (x,y,z)$ with $x,y,z \in \{0,1,2,3,4\}$, define the code $\mathrm{code}(v) := 25x + 5y + z \in \mathbb{N}$.
background
The module certifies every coefficient of unordered monomials $\xi(u)\xi(v)$ in the corrected $N=5$ mixed explicit-fiber axis-stencil residual, matching an exact rational Python audit with no floating point.
A vertex at period 5 is a triple in $\mathrm{Fin},5 \times \mathrm{Fin},5 \times \mathrm{Fin},5$ (abbreviated Vertex5). The product (componentwise) order on that cube is only partial: incomparable pairs would be dropped if one tried to pick a canonical unordered pair by that order alone.
This code supplies a total key on the finite set of vertices so that every unordered pair can be oriented by comparing two naturals.
proof idea
Pure definition: unpack the triple and form the base-5 place-value polynomial $x\cdot 5^2 + y\cdot 5^1 + z\cdot 5^0$. No lemmas are invoked; injectivity is proved separately by omega on the three coordinates.
why it matters
Local plumbing for the Freudenthal axis-stencil coefficient certificate. Downstream, vertex5CanonLE defines the total preorder $u \le_{\mathrm{can}} v$ by comparing codes, and vertex5Code_injective shows the map is one-to-one, so the order is a genuine total order on vertices (not merely a preorder with collisions). That canonical orientation is what lets the residual audit treat each unordered monomial $\xi(u)\xi(v)$ once. The work sits in the gravity domain of the RS mirror; it does not itself invoke the T0–T8 forcing chain or the mass ladder, but it hardens the discrete geometric side of the stencil residual that those continuum claims eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.