siteDelta_ne
plain-language theorem explainer
When two sites on the cyclic lattice differ, the Kronecker lapse weight is zero. Point-split HKT and smeared-constraint arguments cite this to drop off-support terms in single-site Mom–Ham brackets. The proof is a one-line simplification of the piecewise definition under the inequality hypothesis.
Claim. For $n \ge 1$ and $k,j \in \mathbb{Z}/n\mathbb{Z}$, if $j \neq k$ then the Kronecker lapse weight at source $k$ evaluated at $j$ equals $0 \in \mathbb{R}$.
background
This module strengthens the point-split HKT dynamical target after an adversarial pass showed the weak class is decoy-inhabitable by quartic zero-momentum configurations. The strong class demands load-bearing momentum, advection tied to the Mom–Ham bracket calculus, and kinetic regularity; the quartic decoy is excluded by the momentum load-bearing gate.
The Kronecker lapse weight on $\mathbb{Z}/n\mathbb{Z}$ is the indicator that equals $1$ at a chosen site $k$ and $0$ elsewhere. It smears the linearized Hamiltonian constraint $H[N]=\sum_i N_i(\pi_i^2+(q_{i+1}-q_i)^2)/2$ (and the companion momentum functional) so that single-site contributions can be isolated in the point-split calculus.
proof idea
One-line term proof: simp unfolds the Kronecker weight definition and rewrites with the hypothesis $j\neq k$, selecting the zero branch of the piecewise indicator.
why it matters
Local bookkeeping for the strengthened point-split HKT infrastructure: off-diagonal vanishing lets single-site smearing isolate diagonal kinetic and gradient terms when recovering source advection from ${Mom,\delta_j, Ham,\delta_j}$. Sibling lemmas in the same module (computed advection from/to, equality of advected Hamiltonians with those computations, and the strong dynamical target) rely on this clean support property. No recorded downstream edges yet; the lemma does not touch the T0–T8 forcing chain, RCL, or the alpha band. It is pure discrete GR index arithmetic on the cyclic lattice supporting the Wave C2 repair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.