structureDyn
plain-language theorem explainer
On the two-site lattice phase space, the local structure density at site j is 1 + q_j^{2}. It is the geometric factor multiplying gradient-squared terms in the frozen quadratic Hamiltonian and the true source advection density in the point-split Poisson bracket {MomDyn w, HamDyn N}. Anyone checking HKT bracket identities or kinetic-normalized rigidity at n=2 cites it. The body is a one-line definitional expansion.
Claim. For a phase-space point $x=(q,\pi)$ on the periodic lattice with two sites and for each site index $j\in\mathbb{Z}/2\mathbb{Z}$, the structure density is $\mathrm{struct}(x,j):=1+q_j^2$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim (HKT) dynamic target on a two-site lattice. Phase space is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The unsplit Dyn target forces a singular advection identity against the frozen quadratic Hamiltonian; this module replaces that with a smeared point-split momentum sector.
The dynamic Hamiltonian density (unfolded for Fréchet calculus) is $$\mathrm{HamDyn}(N,x)=\sum_i\frac{N_i}{2}\Bigl(\pi_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\Bigr).$$ The factor $1+q_i^2$ is exactly the structure density defined here. Momentum is the smeared density $\mathrm{MomDyn}(w,x)=\sum_j w_j,m(x,j)$, and the Poisson bracket ${\mathrm{MomDyn},w,\mathrm{HamDyn},N}$ carries source/target advection built from this structure factor. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the usual generator-symmetric deformation vanishes identically and the point-split form is the honest replacement.
proof idea
Pure definition: expand the configuration coordinate of $x$ at site $j$ and return $1+q_j\cdot q_j$. No lemmas, no tactics. Downstream equalities such as structureDyn_eq_g are reflexivity after unfold.
why it matters
This density is the load-bearing geometric coefficient in the repaired point-split HKT algebra at $n=2$. It appears in the closed-form Ham–Ham bracket for vacuum-kinetic densities, $${H_N,H_M}=\sum_j(N_j M_{j+1}-M_j N_{j+1}),\mathrm{struct}(x,j),m(x,j),$$ and in the local-coefficient identity equating vacuum-kinetic $H_b H_p$ products to $\mathrm{struct}\cdot m$. Those identities feed the kinetic-normalized rigidity suite: the negative results that mod-vacuum CanonicalMom rigidity fails, that the variable-kinetic counterexample misses the mod-vacuum ham-density shape, and the strong point-split zero-momentum-density lemmas.
Within Recognition Science gravity, the declaration sits in the SevenGaps HKT campaign that tests whether hypersurface-deformation algebras close on the lattice without continuum crutches. No rigidity theorem is proved in this module; the definition only supplies the structure factor those later falsifiers and bracket computations need. It does not touch the T0–T8 forcing chain or the mass ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.