HKTRigidityStatementPointSplitDynN2
plain-language theorem explainer
At two lattice sites, every point-split HKT dynamic target is asserted to have Hamiltonian density of frozen quadratic shape: kinetic p² term, structure-weighted nearest-neighbor gradient, and constant vacuum. Gravity/HKT auditors would cite it as the weak n=2 rigidity Prop. It is only a named proposition (no proof body); the module marks it demoted and likely false because the weak schema admits quartic zero-momentum decoys.
Claim. For every point-split HKT dynamic target $T$ on two sites, there exist real constants $c_{\mathrm{kin}}, c_{\mathrm{grad}}, c_{\mathrm{vac}}$ such that for all phase-space points $x$ and sites $j\in\mathbb{Z}/2\mathbb{Z}$, the Hamiltonian density equals $c_{\mathrm{kin}}\,p_j^2 + c_{\mathrm{grad}}\,S_T(x,j)\,(q_{j+1}-q_j)^2 + c_{\mathrm{vac}}$, where $S_T$ is $T$'s structure function.
background
This module repairs the unsplit Hojman–Kuchař–Teitelboim dynamic target. The widened Dyn target keeps an unsplit momentum–Hamiltonian field that is uninhabitable for honest nearest-neighbor local momentum against a frozen quadratic Hamiltonian: at $n=2$, unsplit advection forces a singular relation on $p_0+p_1=0$. The repaired sibling uses point-split source/target advection densities already present in the smeared Ham–Ham bracket.
HKTPointSplitTargetDyn is the weak schema: dynamic structure function, smeared momentum density, and point-split mom–ham advection. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric generator $D_{\mathrm{gen}}^{\mathrm{sym}}$ vanishes identically (DgenSym_eq_zero_two); a DgenSym-shaped split would be vacuous. The momentum sector is non-abelian: bracket_MomDyn_MomDyn carries a Wronskian density, and bracket_MomDyn_HamDyn records the split advection form.
The module states explicitly that no rigidity theorem is proved here and no ledger flag is flipped. The load-bearing class after adjudication is the Strong variant; this weak Prop is schema-only.
proof idea
There is no proof: the declaration is a bare Prop abbreviation packaging a universal quantification over weak two-site point-split targets and an existential claim that Hamiltonian density is frozen-quadratic (kinetic, structure-weighted gradient, vacuum). Supporting facts in the file (vanishing of $D_{\mathrm{gen}}^{\mathrm{sym}}$, mom–mom and mom–ham brackets, unsplit impossibility) motivate the shape of the statement but are not applied inside a proof term.
why it matters
In the SevenGaps gravity campaign this names the weak n=2 rigidity claim for point-split HKT dynamics after the unsplit Dyn target was shown uninhabitable. The doc-comment demotes it: critic finding D-qg-hkt-pointsplit-adjudication-20260722 shows the n=1 quartic disease reproduces at n=2 over this weak class (the quartic zero-momentum decoy inhabits it). Binding rigidity is the Strong sibling statement. Downstream use count is zero; the module records axiom receipts for the supporting bracket and impossibility lemmas but flips no ledger flag. Framework role is local to the HKT gap repair, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.