zmod2_zero_add_two
plain-language theorem explainer
In the ring Z/2Z, adding 2 to the zero class returns zero. Gravity and HKT rigidity proofs cite it when phase-space indices live in ZMod 2 and a double step must collapse. The proof is a one-line kernel decision on finite-ring arithmetic.
Claim. In the ring $\mathbb{Z}/2\mathbb{Z}$, the equality $0 + 2 = 0$ holds.
background
The ambient module is the Wave C2 gap5 CanonicalMom rigidity session: it extracts the alternating functional equation forced by the ham_ham Poisson-bracket identity under local, structure, and canonical-momentum profiles at spatial dimension parameter $n = 2$.
Phase-space coordinates are indexed by $j \in \mathbb{Z}/2\mathbb{Z}$. Neighboring cells appear as $j+1$ and double steps as $j+2$. The same arithmetic fact is already present in the sibling KineticNormalized rigidity module; this file re-states it privately for local use.
No Recognition-Science cost functional or forcing-chain landmark is involved: the lemma is pure modular arithmetic supporting index bookkeeping in the alternating FE.
proof idea
One-line tactic proof: by decide. Lean’s decision procedure evaluates the concrete finite-ring equation $(0 : \mathrm{ZMod}, 2) + 2 = 0$ and closes the goal. No lemmas are invoked.
why it matters
Parent consumers are profiled_ham_ham_alternating_FE (the alternating FE forced by CanonicalMom ham_ham at $n=2$) and alternating_FE_of_profile (the same identity for an explicit local-profile witness). Both unpack Hamiltonian densities and structure functions on PhaseSpace 2 with indices in ZMod 2; collapsing $0+2$ to $0$ keeps the alternating difference well-typed when the phase cell is stepped twice.
The lemma is scaffolding arithmetic inside the gap5 rigidity route. It does not itself advance the PDE core or flip gap5_constraint_recovery; it only keeps the index algebra honest so later sessions can assemble canonicalMom_rigidity_of_FE_solution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.