quarticBalancedStructure2
plain-language theorem explainer
Structure factor $1+q_j^2$ on the two-site lattice phase space, matching the shape of the dynamical structure weight. HKT gap-5 work cites it when assembling the balanced-quartic momentum density and the strong-rigidity counterexample. The body is a one-line algebraic expression in the configuration coordinate.
Claim. For a phase-space point $x=(q,\pi)$ on the two-site periodic lattice and a site index $j\in\mathbb{Z}/2\mathbb{Z}$, the balanced quartic structure factor equals $1+q_j^2$.
background
The ambient phase space is the product of configuration and conjugate momentum maps on a periodic lattice with $n$ sites: $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$, so each field is a pair of real values indexed by $\mathbb{Z}/2\mathbb{Z}$. The first factor $x.1$ is the configuration $q$.
This module closes Wave C2 gap 5 on the HKT point-split route: Session A builds a balanced quartic falsifier that kills the strong rigidity statement at $n=2$; Session B repairs the CanonicalMom class and banks a DEFINED-only rigidity claim for later sessions. No ledger flag is flipped.
The structure weight is deliberately the same shape as the dynamical structure factor used elsewhere in the hypersurface-deformation stack: a quadratic boost of the local configuration, $1+q_j^2$, rather than a pure constant.
proof idea
Pure definition: evaluate $1$ plus the square of the configuration coordinate at site $j$. No lemmas, no tactics; the body is the term $1 + x.1,j\cdot x.1,j$.
why it matters
Local building block for the balanced-quartic model that separates strong rigidity from the repaired CanonicalMom class. Downstream, the closed form of the balanced momentum functional writes the structure factor explicitly against the opposite-site weight; the $p$-derivative of that functional collapses to a linear combination of the two structure values; the Poisson bracket of two balanced momenta factors through a density built from the same weight; and the balance identity equates opposite-site products of structure and momentum density.
Those identities feed the strong-class counterexample: the balanced quartic forces $p^4=c_{\mathrm{Kin}}p^2+c_{\mathrm{Vac}}$ at three momenta, contradicting strong point-split rigidity at $n=2$. The definition therefore sits on the falsifier side of gap 5, not on the positive CanonicalMom rigidity claim that later sessions prove.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.