addFin5_zero_left
plain-language theorem explainer
Left unit law for addition on the cyclic group of order 5: adding the zero residue leaves any index unchanged. Gravity and discrete-geometry proofs that translate 5-periodic stencil vertices cite it. The proof is a one-line extensionality-plus-simp reduction of modular addition.
Claim. For every residue $i \in \{0,1,2,3,4\}$, the sum $0 + i$ taken modulo $5$ equals $i$.
background
The module certifies rational coefficients in the corrected $N=5$ mixed explicit-fiber Freudenthal axis-stencil residual, matching an exact Python audit without floating point. Coordinates live in $\mathrm{Fin},5$, the standard five-element type of residues modulo 5.
Modular addition on those residues is defined by reducing the ordinary sum of representatives: $\mathrm{add}(i,j)=\langle(i+j)\bmod 5\rangle$. The zero element is the residue of $0$. This left-unit fact is the elementary group law needed before one can talk about translating vertices of the periodic stencil.
proof idea
Apply extensionality on the underlying natural representative of the $\mathrm{Fin},5$ value, then simplify with the definition of modular addition. The congruence $(0+i)\bmod 5=i$ is immediate, so the constructed residue equals $i$.
why it matters
The parent result is the left-origin translation identity for five-periodic stencil vertices: translating any vertex by the origin vertex is the identity map. That identity unfolds componentwise into three applications of this left-unit law. The stencil certificate itself sits in the gravity layer that audits Freudenthal axis residuals used in Recognition Science discrete gravity constructions; clean $\mathbb{Z}/5\mathbb{Z}$ arithmetic keeps the monomial coefficient audit exact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.