zmod2_zero_add_two
plain-language theorem explainer
In the ring Z/2Z, adding the integer 2 to the zero class returns zero. Gravity and HKT rigidity proofs cite it when stepping a two-site phase index by a full period. The proof is a one-line kernel decision procedure on finite modular arithmetic.
Claim. In $\mathbb{Z}/2\mathbb{Z}$, the equality $0 + 2 = 0$ holds (equivalently, the residue class of $2$ is the zero class).
background
The ambient module closes Wave C4/C5 gap5: a mod-vacuum kill plus kinetic-normalized rigidity for HKT (Hamilton–Killing-type) point-split targets. Phase space is two-site, so lattice indices live in $\mathbb{Z}/2\mathbb{Z}$. Neighbor steps are written $j+1$ and full-period steps $j+2$; the latter must collapse to the identity on the index set.
Sibling facts record the full addition table on $\mathbb{Z}/2\mathbb{Z}$ ($0+1=1$, $1+1=0$, $0+2=0$, $1+2=1$). Downstream alternating functional equations for the local Hamiltonian density and structure function evaluate fields at $j$ and $j+1$, so period-two reindexing must be definitionally clean.
The same lemma is duplicated (or re-exported) in the CanonicalMom rigidity module; the kinetic-normalized terminal imports that arithmetic glue when it specializes the profiled Hamiltonian identity.
proof idea
One-line proof by decide: Lean’s kernel decision procedure for closed equalities in the finite ring $\mathbb{Z}/2\mathbb{Z}$. No lemmas are invoked; the statement is pure modular arithmetic.
why it matters
Feeds profiled_ham_ham_alternating_FE (CanonicalMom route) and alternating_FE_of_profile (kinetic-normalized terminal). Those theorems force the alternating functional equation on the local Hamiltonian profile at $n=2$: the Poisson-bracket field identity after unpacking local_ham_profile, structure_profile, and canonical_mom.
Without $0+2=0$ on the index ring, period-two reindexing of phase cells $(a,b,p,r)$ and lapses would not reduce, blocking the honest $n=2$ shape note that the identity only partially determines the profile. In the SevenGaps ledger this is arithmetic scaffolding for gap5 constraint recovery after both mod-vacuum and kinetic-normalized halves bind green. It is not itself a physics claim; it is the finite-index bookkeeping forced by the two-tick (period $2$) cell structure used throughout the HKT rigidity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.