zmod2_zero_add_one
plain-language theorem explainer
In the ring Z/2Z, the sum 0+1 equals 1. Local bookkeeping for two-site decoy configurations and lapse values in the dynamic structure-function bracket. Proof is a one-line decidability check on the finite ring.
Claim. In the ring $\mathbb{Z}/2\mathbb{Z}$, one has $0 + 1 = 1$.
background
The ambient module closes the first two typed residuals (R0 decoy, R1 honest Frechet) of the Wave C2 Gap5 residual DAG for a dynamic structure-function bracket on two sites. Configurations and lapses are evaluated at binary labels, so arithmetic in $\mathbb{Z}/2\mathbb{Z}$ appears when specializing decoy points and when matching Frechet summands to HasFDerivAt.const.add.
Sibling facts record the same ring at the other binary combination ($0-1$) and pin decoy lapse and configuration coordinates at $0$ and $1$. The dynamic Hamiltonian HamDyn is the honest candidate whose Frechet derivative includes the $\partial g/\partial q$ term that the naive frozen lookalike omits.
No continuum or HKT residual is settled here; the module explicitly leaves those open and does not flip gap5_constraint_recovery.
proof idea
One-line decide on the finite decidable ring $\mathbb{Z}/2\mathbb{Z}$. No lemmas are invoked; equality of concrete elements is discharged by the decidable instance.
why it matters
Purely local arithmetic scaffolding inside the R0/R1 closure for the two-site dynamic bracket. It lets later Frechet and decoy specializations rewrite binary sums without ad-hoc case splits. Downstream external uses are empty (private lemma); its value is internal hygiene for HamDyn / HamDynD and the decoy phase-point lemmas.
Framework-wise it sits under Gravity SevenGaps Wave C2, not under the T0–T8 forcing chain or the Recognition Composition Law. Continuum measure and HKT residuals remain open, as does full constraint recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.