zmod2_zero_add_one
plain-language theorem explainer
In the ring $\mathbb{Z}/2\mathbb{Z}$, the sum $0+1$ equals $1$. Anyone working the $n=2$ point-split HKT lattice cites this as a one-line arithmetic fact. The proof is a pure `decide` on the finite ring.
Claim. In $\mathbb{Z}/2\mathbb{Z}$, one has $0 + 1 = 1$.
background
The ambient module repairs the Hojman–Kuchař–Teitelboim dynamic target by point-splitting the momentum–Hamiltonian sector. At lattice size $n=2$ the spatial index lives in $\mathbb{Z}/2\mathbb{Z}$, where $-1=1$, so several generator-symmetry identities collapse and the unsplit $mom_ham$ field is uninhabitable for smooth nearest-neighbour profiles against the frozen quadratic Hamiltonian.
Local momentum profiles, smeared densities, and cell differences are therefore indexed by elements of $\mathbb{Z}/2\mathbb{Z}$. The four elementary addition and subtraction identities on ${0,1}$ are the arithmetic substrate for those constructions; this lemma is the first of them.
proof idea
One-line kernel decision: by decide evaluates the finite equality in the computable ring $\mathbb{Z}/2\mathbb{Z}$ and closes the goal. No lemmas are invoked.
why it matters
The lemma is private scaffolding inside the point-split HKT repair. It does not flip any ledger flag and proves no rigidity. It only supplies the $0+1=1$ case needed when rewriting source/target advection densities and cell differences on the two-site lattice that replaces the unsplit Dyn target. Downstream siblings (sum_zmod2, momFromProfile, localMomCellD) sit on the same arithmetic base; the load-bearing class remains HKTPointSplitTargetDynStrong.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.