HKTPointSplitTargetDyn
plain-language theorem explainer
Schema-only Hojman-Kuchar-Teitelboim target on cyclic phase space: local Hamiltonian and momentum densities, a dynamic structure function, and point-split source/target advection densities, with Poisson-bracket identities for mom-mom, mom-ham, and ham-ham. Gravity workers cite it as the weak repaired Dyn interface after unsplit advection failed at n=2. It is a structure definition, not a theorem; free advection slots and weak nondegeneracy admit decoy inhabitants.
Claim. For $n \ge 1$, a point-split dynamic HKT target is a tuple of real densities on phase space $X_n \times \mathbb{Z}/n\mathbb{Z}$: Hamiltonian density $h$, momentum density $p$, structure function $S$, source/target advection densities $A_{\mathrm{from}}, A_{\mathrm{to}}$, and Wronskian density $W$, such that smeared $h$ and $p$ are differentiable; $S$ is nonconstant; $h$ is nearest-neighbour local and cyclically covariant; $S$ is ultralocal in the configuration; $\{p_v,p_w\}=\sum_j(v_j w_{j+1}-w_j v_{j+1})W_j$; $\{p_w,H_N\}=\sum_j w_j(N_{j+1}A_{\mathrm{to},j}-N_j A_{\mathrm{from},j})$; $\{H_N,H_M\}=\sum_j(N_j M_{j+1}-M_j N_{j+1})S_j p_j$; and $h$ is not identically zero.
background
The module repairs the widened dynamic HKT target whose unsplit momentum-Hamiltonian bracket is uninhabitable for honest nearest-neighbour local momentum against a frozen quadratic Hamiltonian: at $n=2$, unsplit advection forces a singular identity on $p_0+p_1=0$. The unsplit Dyn record stays as a falsification-adjacent witness; this structure is the repaired sibling.
Phase space carries configuration and momentum fields indexed by $\mathbb{Z}/n\mathbb{Z}$. Smeared observables are linear combinations $\sum_j N_j h_j$ and $\sum_j w_j p_j$. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the DgenSym packaging of advection vanishes identically; the API therefore states point-split source/target densities against the same smeared momentum sector already used in the ham-ham bracket.
Upstream cost algebra supplies the shifted cost $H=J+1$ and the Recognition Composition Law in d'Alembert form, but this declaration is pure discrete Poisson-structure bookkeeping on the cyclic lattice, not a derivation of $J$ or $\phi$.
proof idea
No proof body: the declaration is a Lean structure (record type). Fields package densities, differentiability, locality/covariance, three bracket identities (mom-mom Wronskian, point-split mom-ham advection, ham-ham with dynamic structure times momentum), and a weak nondegeneracy existential. Inhabitants are supplied downstream by explicit density assignments (for example balanced quartic or vacuum kinetic), not by a constructive argument here.
why it matters
This is the weak Wave C2 R5 point-split Dyn schema after the unsplit mom-ham failure. Downstream, the Strong refinement and the computed advection recoveries (with equality theorems under the split identity at $n=2$) treat free advection slots as determined by brackets. Explicit weak inhabitants include the balanced quartic and vacuum kinetic targets.
Critic adjudication demoted the type to schema-only: a quartic zero-momentum decoy ($h_j=\pi_j^4$, $p=0$, decorative $S$, vanishing advection/bracket densities) still inhabits it. Load-bearing rigidity and gravity claims must use the Strong refinement. No ledger flag flips here; no link is claimed to T5-T8, RCL uniqueness, or the $\alpha$ band. The open unsplit claim against campaign HamDyn remains a separate proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.