vertex5Code_injective
plain-language theorem explainer
The base-5 place-value code on vertices of the periodic 5³ lattice is injective. Gravity auditors of the corrected Freudenthal N=5 axis-stencil residual cite it when selecting a unique ordered representative of each unordered monomial pair. The proof destructures both vertices and finishes by omega on the digit expansion.
Claim. The encoding $(x,y,z)\mapsto x\cdot 25+y\cdot 5+z$ from vertices of $(\mathbb{Z}/5\mathbb{Z})^3$ into $\mathbb{N}$ is injective.
background
The module certifies, by exact rational arithmetic only, every coefficient of an unordered monomial $\xi(u)\xi(v)$ in the corrected $N=5$ mixed explicit-fiber axis-stencil residual (mirroring the Python audit script). Vertices live on the periodic cube $(\mathrm{Fin},5)^3$.
The product order on that cube is only partial, so incomparable pairs would be dropped if one tried to canonicalize unordered pairs by componentwise comparison. The code map therefore supplies a total-order key: write the three $\mathrm{Fin},5$ coordinates in base 5 as a single natural number. Upstream, that key is defined exactly as $v_1\cdot 25+v_2\cdot 5+v_3$; the present theorem is its injectivity.
proof idea
Term-mode proof. Introduce two vertices and the equality of their codes; destructure both as triples of $\mathrm{Fin},5$ coordinates. Componentwise extensionality, then simp with the code definition, reduces the goal to three arithmetic equalities on values in ${0,\ldots,4}$. Each is discharged by omega (unique base-5 digits).
why it matters
Feeds the cross-term half of the axis-stencil soundness calculation: unorderedCrossMonomialExpansionAtN5 expands the double sum over unordered pairs by selecting the canonical representative via the total-order key, and needs injectivity so that distinct vertices never collide under that key. Without it the coefficient audit of the corrected Freudenthal residual at $N=5$ would be incomplete. The result is local scaffolding for the gravity certificate, not a forcing-chain landmark (T0–T8), but it closes a concrete gap in the exact rational residual check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.