siteDelta
plain-language theorem explainer
The Kronecker site weight on the cyclic lattice Z/nZ picks out a single site k by returning 1 there and 0 elsewhere. Gravity and HKT point-split arguments cite it as the discrete lapse/shift probe that localizes momentum and Hamiltonian densities. The body is the standard indicator definition, not a derived identity.
Claim. For $n \ge 1$ and fixed $k \in \mathbb{Z}/n\mathbb{Z}$, the site weight $\delta_k : \mathbb{Z}/n\mathbb{Z} \to \mathbb{R}$ is $\delta_k(j) = 1$ if $j = k$ and $\delta_k(j) = 0$ otherwise.
background
This module strengthens the Hamilton–Killing–transport (HKT) point-split target after an adversarial pass showed the weak dynamical class is decoy-inhabitable by quartic zero-momentum data. The strong class ties advection to the momentum–Hamiltonian Poisson bracket and demands load-bearing momentum plus kinetic regularity.
On a cyclic lattice of $n$ sites, densities (momentum, Hamiltonian) are functions of phase space valued in $\mathbb{R}$ at each site. To probe a single site, one multiplies by a discrete weight and sums. The natural weight is the Kronecker indicator at a chosen site $k$: the classical discrete delta on $\mathbb{Z}/n\mathbb{Z}$.
Downstream, source and target advection are recovered by evaluating brackets of the form ${ \mathrm{Mom},\delta_j,, \mathrm{Ham},\delta_j }$ and ${ \mathrm{Mom},\delta_j,, \mathrm{Ham},\delta_{j+1} }$. Those constructions insert this weight as the coefficient of each density before summing over sites.
proof idea
Pure definition: the map sends each lattice index $j$ to the real $1$ when $j$ equals the fixed site $k$, and to $0$ otherwise. No lemmas or tactics; it is the indicator of ${k}$ as a real-valued function on $\mathbb{Z}/n\mathbb{Z}$.
why it matters
Every load-bearing advection identity in the strong point-split repair routes through this weight. Computed source and target advection (computedHamAdvFrom, computedHamAdvTo) are defined by bracketing momentum and Hamiltonian densities against $\delta_j$ and $\delta_{j+1}$. Equality theorems then match the target's declared advection slots to those bracket values under the Mom–Ham split hypothesis at $n=2$.
The same weight appears in the vacuum-kinetic normalized rigidity stream: vacuum kinetic advection-from/to and the Mom–Ham split for vacuum kinetic density are written as brackets against $\sum_i \delta_j(i),\rho_i$. Non-vanishing of the weight off the diagonal (siteDelta_ne) supports discrimination between honest inhabitants and the quartic zero-momentum decoy.
Within Recognition gravity, this is scaffolding for discrete HKT calculus on the eight-tick / cyclic lattice side of the Seven Gaps program, not a forcing-chain (T0–T8) step. Strong-class rigidity itself is already marked dead; binding rigidity moves to CanonicalMom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.