zmod2_zero_add_one'
plain-language theorem explainer
In the two-site cyclic group Z/2Z, the sum of the zero class and the unit is the unit. The lemma is a tiny arithmetic fact used when evaluating momentum densities and brackets on the two-point lattice. The proof is a one-line decision procedure on the finite ring.
Claim. In the ring $\mathbb{Z}/2\mathbb{Z}$, one has $0 + 1 = 1$.
background
The module repairs the point-split Hamilton–Killing–Toda (HKT) target after an adversarial pass showed the weak dynamical class admits a quartic zero-momentum decoy. The strong class therefore demands load-bearing momentum, advection tied to the Mom–Ham bracket calculus, and kinetic regularity on a two-site lattice indexed by $\mathbb{Z}/2\mathbb{Z}$.
Site labels are elements of $\mathbb{Z}/2\mathbb{Z}$. Momentum and density profiles (e.g. $\delta_0$, $\delta_1$) are functions on that ring, so elementary identities such as $0+1=1$ appear when simplifying pointwise evaluations and when comparing a site to its neighbour under the successor map.
proof idea
One-line wrapper: decide discharges the equality by exhaustive evaluation in the finite ring $\mathbb{Z}/2\mathbb{Z}$. No external lemmas are invoked.
why it matters
Feeds hamDyn_mom_load_bearing_witness, which shows that the Mom–Mom bracket of the two site deltas on the load-bearing witness phase is nonzero, thereby excluding the quartic zero-momentum decoy from the strong HKT point-split class. That discrimination gate is the module’s main repair: honest inhabitants pass, the decoy fails. The arithmetic itself is not a physics claim; it is scaffolding for the two-site lattice bookkeeping that underpins the strong target and the later move of binding rigidity to the CanonicalMom line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.