decorativeStructure2
plain-language theorem explainer
Quadratic structure function on the two-site lattice phase space: one plus the squared configuration coordinate at a chosen site. Serves as the structure piece of the quartic zero-momentum decoy that inhabits the weak point-split HKT schema. Anyone auditing the Wave C2 repair or decoy-exclusion gate cites it. The body is a one-line algebraic expression, not a derived identity.
Claim. On the two-site phase space $x=(q,\pi)$ with $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the decorative structure at site $j$ is the real number $1+q_j^2$.
background
The ambient phase space is the product of configuration and conjugate momentum maps on a periodic lattice of $n$ sites: pairs $(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 on the two sites.
This module is the Wave C2 repair of the point-split HKT target. An adversarial pass showed the weak dynamical target is decoy-inhabitable by a quartic zero-momentum example; the strong class adds load-bearing momentum, Mom–Ham advection, and kinetic regularity so that decoy fails and the honest inhabitant passes.
Structure functions of this shape appear in the weak schema as a free field. The present map is deliberately nonconstant and of the same algebraic shape as the dynamical structure used elsewhere, so it can be plugged into the decoy witness without extra hypotheses.
proof idea
Pure definition: project the phase-space pair to its configuration component, evaluate at the site index $j\in\mathbb{Z}/2\mathbb{Z}$, square that real, and add one. No lemmas, no tactics, no reduction.
why it matters
Supplies the structure field of the quartic zero-momentum decoy that formally witnesses decoy-inhabitability of the weak point-split schema (the Codex finding that motivated this module). Downstream, a short nonconstancy lemma shows the map is not a phase-space constant, which is the minimal sanity check before using it as a structure function. The same decoy is then excluded from the strong class by the load-bearing momentum gate, while the honest Hamiltonian inhabitant remains. Binding rigidity for the point-split story is thereby moved off the weak class and onto the CanonicalMom target; no ledger flag flips here. Framework role is local to the gravity SevenGaps HKT repair, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.