zmod2_one_add_one
plain-language theorem explainer
In the ring of integers mod 2, one plus one is zero. Gravity lemmas that index two-site phase space by Z/2Z cite this constantly when simplifying neighbor shifts j ↦ j+1. The proof is a one-line kernel decision procedure on a finite ring.
Claim. In the ring $\mathbb{Z}/2\mathbb{Z}$, one has $1+1=0$.
background
The module sits in Wave C2 gap5 of the SevenGaps gravity stack: kill strong rigidity for the point-split dynamical target at $n=2$, then repair a CanonicalMom class that still admits an honest Hamiltonian density. Phase space is two configuration/momentum cells, so lattice sites are elements of $\mathbb{Z}/2\mathbb{Z}$. Neighbor shifts appear as $j\mapsto j+1$ in Poisson brackets, alternating sums, and balanced quartic densities.
The same arithmetic fact is re-proved privately in several sibling rigidity modules (CanonicalMom, KineticNormalized, PointSplit, VacuumSectorKill). It is pure finite-ring arithmetic, not a physics hypothesis: addition in $\mathbb{Z}/2\mathbb{Z}$ is XOR, so the unique nonzero element is its own additive inverse.
proof idea
One-line wrapper: decide evaluates the closed equality in the decidable finite ring $\mathrm{ZMod},2$ and closes the goal. No lemmas are invoked.
why it matters
Parent uses include the CanonicalMom rigidity package: localHamHamCoefficient_delta01, structure_mom_delta01, and the alternating functional equation profiled_ham_ham_alternating_FE forced by CanonicalMom ham_ham at $n=2$. In this module it feeds bracket identities for the balanced momentum density (bracket_MomBalanced_MomBalanced, bracket_MomBalanced_quarticHam) and the balance/closure lemmas for the quartic falsifier.
Those identities separate the balanced quartic decoy from the honest HamDyn inhabitant of HKTPointSplitTargetDynCanonicalMom, which is the Session B design of the D-qg-hkt-rigidity route. The lemma itself is bookkeeping; without $1+1=0$ the two-site alternating sums do not collapse to the $(0)-(1)$ difference that the rigidity statements need. No ledger flag is flipped here (gap5_constraint_recovery stays false).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.