hamDynPointSplitTarget
plain-language theorem explainer
Concrete HamDyn package inhabiting the repaired point-split Hojman–Kuchař–Teitelboim dynamic target on the two-site phase space. Gravity workers cite it as the honest witness that the split-advection schema is non-vacuous for the dynamic quadratic Hamiltonian. The body wires known densities and structure data, then discharges locality, covariance, differentiability, and bracket fields by rewriting to existing HamDyn/MomDyn bracket lemmas.
Claim. There is an explicit package of Hamiltonian density $h$, momentum density $\pi$, structure function $S$, and source/target advection densities $A_{\mathrm{from}}$, $A_{\mathrm{to}}$ on the two-site phase space ($n=2$) such that the smeared Hamiltonian and momentum are differentiable, $S$ is non-constant, $h$ is local and covariant, $S$ is local, $\{\pi[v],\pi[w]\}$ equals the Wronskian-weighted structure density, $\{\pi[w],H[N]\}$ equals the point-split advection form $\sum_j w_j(N_{j+1}A_{\mathrm{to},j}-N_j A_{\mathrm{from},j})$, $\{H[N],H[M]\}$ matches the dynamic structure identity, and a nondegeneracy witness exists.
background
The module repairs the dynamic HKT target after the unsplit mom_ham field proved uninhabitable for honest nearest-neighbor momentum against a frozen quadratic Hamiltonian at $n=2$: unsplit advection forces a singular identity on $p_0+p_1=0$. The unsplit Dyn target stays as a falsification-adjacent record; this file supplies the repaired sibling with point-split momentum–Hamiltonian advection.
On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the generator-symmetric density vanishes and a DgenSym-shaped split would be empty. The schema therefore uses the smeared momentum density already present in the HamDyn–HamDyn bracket, with separate source and target advection densities. The momentum sector is not abelian: the momentum–momentum bracket carries a Wronskian density.
Upstream, bracket_HamDyn_HamDyn gives the exact dynamic structure-function identity for the two-site concrete inverse metric $1+(q_j)^2$. Parallel lemmas compute ${\mathrm{MomDyn},v,\mathrm{MomDyn},w}$ and ${\mathrm{MomDyn},w,\mathrm{HamDyn},N}$, and differentiability of both smeared generators is already on record.
proof idea
Structure inhabitant, not a deep proof. Fields are filled by the existing HamDyn density, MomDyn density, dynamic structure function, and the precomputed source/target advection densities.
Differentiability of the smeared Hamiltonian rewrites through the density-smear identity to differentiable_HamDyn; momentum differentiability is differentiable_MomDyn directly. Structure non-constancy is the existing dynamic witness. Locality of $h$ and of $S$ are short rewrites on the density definitions; covariance of $h$ is a $\mathbb{Z}/2$ index ring identity.
The three bracket obligations are one-line (or short) rewrites: mom_mom via bracket_MomDyn_MomDyn, mom_ham_split via bracket_MomDyn_HamDyn, and ham_ham via bracket_HamDyn_HamDyn after closing the density and inverse-metric forms. Nondegeneracy packages the known HamDyn phase witness.
why it matters
This is the honest HamDyn inhabitant of the repaired point-split Dyn target after the Wave C2 R5 adjudication: the unsplit Dyn target remains falsification-adjacent, while the load-bearing class is the strengthened point-split target. Downstream, hamDynPointSplitTargetStrong embeds this package and adds load-bearing momentum and advection-tie obligations; hktPointSplitTargetDyn_two_nonvacuous is the immediate Nonempty witness $\langle$ this package $\rangle$.
In the SevenGaps gravity line it shows that, once advection is point-split and the momentum density is the smeared sector already used by the Ham–Ham structure identity, the dynamic quadratic Hamiltonian with concrete inverse metric $1+q_j^2$ really does sit inside the HKT schema at two sites. No rigidity theorem is claimed here, and no ledger flag is flipped; the module is explicit that the weak target is schema-only and the strong class carries the weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.