structureDyn_eq_concrete
plain-language theorem explainer
On the two-site lattice phase space, the point-split HKT structure function at site j equals the concrete positive inverse-metric candidate 1 + q_j². Gravity workers assembling the strong point-split HKT dynamic target cite this to identify the two presentations. The proof is a one-line simp that unfolds both definitions and rewrites a·a as a².
Claim. Let $x=(q,\pi)$ be a point of the two-site canonical phase space $(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})\times(\mathbb{Z}/2\mathbb{Z}\to\mathbb{R})$, and let $j\in\mathbb{Z}/2\mathbb{Z}$. Then the structure function $1+q_j\cdot q_j$ equals the concrete dynamic inverse metric $1+q_j^2$.
background
The ambient setting is the Wave C2 R5 repair of the Hojman–Kuchař–Teitelboim (HKT) dynamic target on a periodic lattice. The unsplit Dyn momentum–Hamiltonian field is uninhabitable for honest nearest-neighbor momentum profiles against the frozen quadratic Hamiltonian at $n=2$; this module supplies the point-split sibling, with load-bearing class the strong point-split Dyn target.
Phase space is the product of configuration and conjugate momentum maps on $\mathbb{Z}/n\mathbb{Z}$. Here $n=2$, so sites are $\mathbb{Z}/2\mathbb{Z}$. The structure function used by the point-split target is $1+q_j q_j$. Independently, the dynamic-structure blocker package defines a MODEL positive inverse-metric candidate $1+(q_j)^2$ that depends only on the configuration coordinate at each site.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generic symmetric deformation generator is definitionally zero as a functional; the repaired momentum sector therefore uses smeared point-split advection densities rather than that generator.
proof idea
One-line wrapper. Unfold both sides (structureDyn and concreteDynamicInverseMetric) and apply pow_two, which rewrites the product $q_j\cdot q_j$ as the square $q_j^2$. No arithmetic beyond that identity is required; the two expressions are definitionally the same real after that rewrite.
why it matters
Pins the structure function of the repaired point-split HKT Dyn target to the concrete positive inverse-metric MODEL already used in the dynamic-structure blocker layer. Without this identification, the strong point-split class and the inverse-metric candidate would be only informally the same object.
The module is explicitly non-rigid: no rigidity theorem is proved, and no ledger flag is flipped. Downstream use is presently empty in the graph; the lemma is infrastructure for anyone discharging metric-variation or structure-function side conditions inside HKTPointSplitTargetDynStrong or related $n=2$ bracket identities (bracket_HamDyn_HamDyn, smeared momentum densities). It sits in the gravity SevenGaps campaign, not in the T0–T8 forcing chain, and does not touch $\phi$, the eight-tick octave, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.