HKTPointSplitTargetDynStrong
plain-language theorem explainer
Strengthened point-split HKT dynamical target on n sites: the weak schema plus three critic fields (nontrivial momentum–momentum bracket, advection equal to Mom–Ham bracket extractions, and a nonzero kinetic π-partial). Gravity/HKT authors cite it to exclude quartic zero-momentum decoys while still admitting honest HamDyn. Pure structure extension; no proof body.
Claim. For $n\ge 1$, a strong point-split HKT dynamical target is a weak point-split HKT dynamical target on $n$ sites together with: (1) vectors $v,w$ and a phase-space point $x$ such that the Poisson bracket of the two smeared momentum densities $\sum_j v_j m_j$ and $\sum_j w_j m_j$ is nonzero at $x$; (2) source and target advection equal the bracket-calculus values extracted from the Hamiltonian and momentum densities; (3) some momentum partial of the unsmeared unit-lapse Hamiltonian $\sum_i h_i$ is nonzero at some phase-space point.
background
The local setting is Wave C2 repair of the point-split HKT target after an adversarial pass showed the weak dynamical schema is decoy-inhabitable (quartic zero-momentum densities pass every weak field). The weak class stays only as documentation of that decoy-inhabitable envelope.
Phase space is maps from $\mathbb{Z}/n\mathbb{Z}$ into configuration and momentum coordinates. Hamiltonian and momentum densities $h_j$, $m_j$ feed a discrete Poisson bracket. Source/target advection slots record how the Hamiltonian density is transported; the strong schema forces those slots to equal the explicit Mom–Ham bracket extractions computedHamAdvFrom / computedHamAdvTo, not free decorative data.
Kinetic regularity demands that the total Hamiltonian is not purely potential: some $\partial/\partial\pi_j$ of $\sum_i h_i$ is nonzero. Load-bearing momentum demands a nontrivial ${M,M}$ bracket among linear combinations of the $m_j$.
proof idea
Definitional structure only: extends the weak point-split dynamical target by three named fields (mom_load_bearing, advFrom_tied, advTo_tied, kinetic_regular). No tactics and no lemmas in the declaration body. Downstream inhabitants discharge the three fields by concrete witnesses (e.g. delta-supported test vectors and an explicit phase-space point for the momentum bracket; rfl/simp against the computed advection extractors; a nonzero $\pi$-partial of the honest HamDyn density).
why it matters
Closes the decoy hole that killed weak-class rigidity: the quartic zero-momentum model inhabits the weak schema but fails mom_load_bearing, while honest HamDyn inhabits the strong class (hamDynPointSplitTargetStrong), so the discrimination gate is formal. Downstream, CanonicalMom extends this strong class by local ham profile, structure profile, and canonical momentum shape $m_j = c,\pi_{j+1}(q_{j+1}-q_j)$ with $c\neq 0$; the balanced quartic still inhabits Strong but is excluded from CanonicalMom. Module doc records that strong-class rigidity itself is proven false (balanced-quartic falsifier), so binding grind targets move to CanonicalMom and kinetic-normalized variants. This is scaffolding hygiene inside the gravity SevenGaps HKT line, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.