hktPointSplitTargetDyn_two_nonvacuous
plain-language theorem explainer
The repaired point-split dynamic HKT target on a two-site lattice is inhabited: Hamiltonian, momentum, structure, and split advection densities exist as a package. Gravity workers checking that the n=2 schema is not empty after the unsplit-advection failure cite this. The proof is a one-line term packing the HamDyn densities into the structure.
Claim. The type of point-split dynamic Hojman–Kuchař–Teitelboim targets on the two-site periodic lattice is nonempty: there exist a Hamiltonian density, a momentum density, a structure function, and source/target advection densities realizing the repaired schema at $n=2$.
background
The Hojman–Kuchař–Teitelboim (HKT) program asks which local Hamiltonian and momentum densities close under hypersurface-deformation brackets with a structure function. In this module the unsplit dynamic target keeps a single mom_ham field; against the frozen quadratic Hamiltonian that field is uninhabitable for honest nearest-neighbor momentum at $n=2$, because unsplit advection forces a singular identity on $p_0+p_1=0$.
The repair is a point-split schema: source and target advection densities replace the unsplit field, matching the smeared momentum already used in the Ham–Ham bracket. On $\mathbb{Z}/2\mathbb{Z}$ one has $-1=1$, so the symmetric-difference generator $D^{\mathrm{sym}}$ vanishes identically and any $D^{\mathrm{sym}}$-shaped split would be vacuous. The structure therefore records the true (non-abelian) momentum–momentum bracket via a Wronskian density.
Upstream, hamDynPointSplitTarget is the concrete HamDyn package (densities and split advectors) that fills every field of the schema at $n=2$.
proof idea
One-line term proof. Nonemptiness is witnessed by the existing definition hamDynPointSplitTarget, which supplies HamDyn Hamiltonian density, momentum density, structure function, and the two split advection densities. No algebraic work is done here; the declaration only packages that inhabitant as a Nonempty proof.
why it matters
Without a witness the repaired point-split Dyn schema would be an empty interface, and every universal claim over it would be vacuous. Downstream, HKTRigidityStatementPointSplitDynN2 quantifies over all such targets and asks whether the Hamiltonian density is forced into kinetic-plus-gradient-plus-vacuum form. That rigidity statement is itself demoted (likely false): the weak schema is also inhabited by a quartic zero-momentum decoy, so binding rigidity lives on the strong class instead.
In the SevenGaps gravity campaign this is the honest n=2 API adaptation after the Codex adjudication that killed unsplit advection. It does not flip any ledger flag and proves no rigidity; it only certifies that the repaired schema is nonvacuous so later strong-target work has a live baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.