delta0
plain-language theorem explainer
The site-0 indicator on $\mathbb{Z}/2\mathbb{Z}$: value 1 at the zero cell and 0 at the one cell. Gravity workers cite it as the canonical test lapse $N=\delta_0$ when probing point-split HKT brackets and alternating functional equations at $n=2$. The body is a one-line piecewise definition.
Claim. Define $\delta_0:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ by $\delta_0(0)=1$ and $\delta_0(j)=0$ for $j\neq 0$ (equivalently $\delta_0(1)=0$).
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target. The unsplit mom_ham field is uninhabitable for honest nearest-neighbor local momentum profiles against a frozen quadratic Hamiltonian at $n=2$: unsplit advection forces a singular identity on $p_0+p_1=0$. The repaired API uses smeared point-split momentum densities with source/target advection slots.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generic symmetric difference operator vanishes and cannot carry the split. Test lapses are therefore the two site indicators $\delta_0$ and $\delta_1$. Instantiating Poisson-bracket fields at $(N,M)=(\delta_0,\delta_1)$ isolates single-cell coefficients and produces the alternating functional equations that feed CanonicalMom and KineticNormalized rigidity.
proof idea
Pure definition: the map sends the zero class of $\mathbb{Z}/2\mathbb{Z}$ to $1\in\mathbb{R}$ and every other class to $0$. No lemmas, no tactics.
why it matters
Load-bearing test lapse for the point-split HKT stack. Downstream, localHamHamCoefficient_delta01 and structure_mom_delta01 collapse $\sum_j(\delta_0(j)\delta_1(j+1)-\delta_1(j)\delta_0(j+1)),c_j$ to the single difference $c_0-c_1$. The same pair drives profiled_ham_ham_alternating_FE and alternating_FE_of_profile, which force the CanonicalMom ham–ham alternating equation at $n=2$.
It also witnesses non-abelian momentum: quarticBalanced_mom_load_bearing_witness shows the balanced-quartic Mom bracket at $(\delta_0,\delta_1)$ is nonzero, and quarticBalancedStrongTarget packages that witness into the strengthened point-split class. No rigidity is proved in this module; the definition only supplies the standard probe that later rigidity and strong-target constructions reuse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.