delta1
plain-language theorem explainer
Indicator (Kronecker) function on the two-site circle that equals 1 at site 1 and 0 at site 0. Gravity and HKT rigidity proofs cite it as the second test lapse or shift when evaluating Poisson brackets of Hamiltonian and momentum densities. The body is a one-line piecewise definition on ZMod 2.
Claim. Define $\delta_1:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ by $\delta_1(j)=1$ if $j=1$ and $\delta_1(j)=0$ otherwise. Equivalently, $\delta_1$ is the standard basis vector dual to the site labeled $1$ on the two-point lattice.
background
This module repairs the point-split Hojman–Kuchař–Teitelboim (HKT) dynamic target after the unsplit mom_ham field proved uninhabitable for nearest-neighbor local momentum against a frozen quadratic Hamiltonian at $n=2$. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so symmetric discrete derivatives vanish and the momentum sector is handled via smeared point-split densities rather than a pure abelian generator.
The two-site phase space carries configuration and momentum values at labels $0$ and $1$. Test lapses and shifts are real functions on $\mathbb{Z}/2\mathbb{Z}$. The companion $\delta_0$ is the indicator of site $0$; together $(\delta_0,\delta_1)$ form the standard dual basis used to probe Hamiltonian–Hamiltonian and momentum–momentum brackets cell by cell.
No rigidity is proved in this file. The definitions only supply the combinatorial probes that later modules instantiate inside CanonicalMom and Strong point-split targets.
proof idea
Pure definition: a single lambda that pattern-matches on equality with $(1:\mathrm{ZMod},2)$ and returns the real constants $1$ or $0$. No lemmas, no tactics.
why it matters
Downstream CanonicalMom rigidity uses $\delta_0$ and $\delta_1$ as the pair of lapses that extract the alternating functional equation forced by the ham_ham bracket at $n=2$ (profiled_ham_ham_alternating_FE, localHamHamCoefficient_delta01, structure_mom_delta01). The same pair witnesses load-bearing nonabelian momentum: quarticBalanced_mom_load_bearing_witness evaluates the balanced-momentum bracket on $(\delta_0,\delta_1)$ and shows it is nonzero, which is exactly the witness packed into quarticBalancedStrongTarget.mom_load_bearing. Kinetic-normalized rigidity reuses the pair inside alternating_FE_of_profile and the vacuum kinetic strong target. In the SevenGaps gravity campaign this is the concrete combinatorial dual basis that makes the repaired point-split HKT schema checkable rather than schematic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.