siteDelta_self
plain-language theorem explainer
On the cyclic lattice Z/nZ the Kronecker site weight is 1 when source and target indices coincide. Anyone reducing Mom–Ham advection identities at fixed sites cites this. The proof is a one-line simp unfolding of the piecewise definition.
Claim. For every $n \ge 1$ and every site $k \in \mathbb{Z}/n\mathbb{Z}$, the Kronecker site weight $\delta_k(k)$ equals $1$ in $\mathbb{R}$.
background
The module repairs the Wave C2 point-split HKT target after an adversarial pass showed the weak dynamical class is decoy-inhabitable by quartic zero-momentum data. The strong class adds load-bearing momentum, Mom–Ham bracket advection, and kinetic regularity; discrimination is that the honest inhabitant passes and the quartic decoy fails.
siteDelta is the Kronecker lapse/shift weight on $\mathbb{Z}/n\mathbb{Z}$: at fixed source $k$ it sends $j \mapsto 1$ if $j=k$ and $0$ otherwise. It is the standard test function that isolates a single lattice site when the Mom–Ham split identity is specialized.
The local setting is discrete Hamiltonian kinetics on a cyclic phase space of period $n$, with advection slots hamAdvFrom/hamAdvTo constrained by the bracket calculus rather than by free functional choice.
proof idea
One-line wrapper: simp [siteDelta] unfolds the definition and discharges the true branch of the if j = k guard when both arguments are the same site $k$, yielding the real unit $1$.
why it matters
Feeds the two equalities that pin advection slots to the bracket calculus at $n=2$: hamAdvFrom_eq_computed (source slots) and hamAdvTo_eq_computed (target slots). Both apply the Mom–Ham split identity to pairs of Kronecker weights; the diagonal case needs $\delta_k(k)=1$ so the summed test collapses to the computed advection value.
In the SevenGaps gravity stack this is bookkeeping, not a new physical law: it lets the strong point-split target talk honestly about site-local advection while the weak class remains decoy-inhabitable. Binding rigidity has already moved to CanonicalMom; this lemma only keeps the strong-class witness algebraically clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.