sum_zmod2
plain-language theorem explainer
Any real-valued function on the two-site ring Z/2Z sums to the plain sum of its values at 0 and 1. Gravity and HKT calculations at lattice size n=2 cite this whenever a discrete site sum must expand into explicit terms. The proof decides that the universe equals {0,1} and rewrites via Finset.sum_pair.
Claim. For every function $g:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the finite sum over the ring equals the two-point evaluation: $\sum_{j\in\mathbb{Z}/2\mathbb{Z}} g(j)=g(0)+g(1)$.
background
The ambient module repairs the Hojman–Kuchař–Teitelboim dynamic target by point-splitting the momentum–Hamiltonian sector at lattice size $n=2$. Configurations and momenta live on $\mathbb{Z}/2\mathbb{Z}$, so every smeared density, bracket coefficient, and Hamiltonian is a sum over exactly two sites.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, which collapses several structure functionals and forces honest nearest-neighbor bookkeeping to expand site sums by hand. The same two-point identity already appears as a private lemma in the Gap5 momentum-magnitude bridge; this copy serves the point-split HKT API.
No cost-functional or smoothness hypothesis is involved: the statement is pure finite-sum algebra on a two-element type.
proof idea
Tactic proof in two steps. First, decide establishes that the Finset universe of $\mathbb{Z}/2\mathbb{Z}$ equals the literal pair ${0,1}$. Second, rewrite the sum with that equality and apply Finset.sum_pair, discharging the side condition $0\neq 1$ again by decide. No induction or analysis is used.
why it matters
This is the workhorse expansion for every $n=2$ HKT and Gap5 identity that begins with a sum over lattice sites. Downstream it feeds the HamDyn decoy evaluation, the local Ham–Ham coefficient identity localHamHamCoefficient_delta01, the structure-momentum pairing structure_mom_delta01, and the canonical momentum brackets bracket_MomBalanced_MomBalanced and bracket_MomBalanced_quarticHam.
In the Recognition gravity stack those brackets are the load-bearing witnesses that the point-split momentum sector is non-abelian (Wronskian density, not zero) and that the repaired strong point-split target is inhabited. The lemma itself carries no physics; it simply makes the two-site arithmetic transparent so the no-go for unsplit mom_ham and the positive results for the split target can be stated without Finset noise.
It does not flip any ledger flag and proves no rigidity theorem; those remain open or live in sibling modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.