vacuumKineticStrongTarget
plain-language theorem explainer
Packages the variable-kinetic vacuum Hamiltonian density on two sites into a strong point-split dynamical target: momentum is load-bearing, advected Hamiltonian slots match bracket calculus, and the kinetic form is regular at a nondegenerate phase. Gravity/gap-5 workers cite it as the strong half of the CanonicalMom counterexample that kills mod-vacuum rigidity. The body is a structure instance: weak target plus four short witness lemmas.
Claim. There is a strong dynamical point-split target on $n=2$ sites whose underlying weak data are the vacuum-kinetic Hamiltonian density, dynamical momentum density, and dynamical structure function, such that (i) the Poisson bracket of two independent momentum observables is nonzero at a fixed witness phase, (ii) source and target advected Hamiltonian slots equal their bracket-calculus values, and (iii) the partial derivative of the summed Hamiltonian density in the first momentum coordinate is nonzero at a nondegenerate phase.
background
Module Wave C4/C5 gap5 closes the mod-vacuum half of HKT rigidity and the kinetic-normalized terminal. The local setting is discrete Hamiltonian dynamics on phase space $(\mathbb{R}^{\mathbb{Z}/2})^2$: configuration and momentum fields on two sites, with Hamiltonian density, momentum density, and a structure function that enter a point-split Poisson calculus.
The weak target already installs the vacuum-kinetic density (variable kinetic coefficient built from a local profile), dynamical momentum density, and structure function $1+q^2$. Strongening adds three dynamical constraints used throughout the SevenGaps stack: momentum load-bearing (the bracket of two independent momentum observables is nonzero), advected Hamiltonian slots tied to computed bracket values under the mom-ham split, and kinetic regularity (a nonzero partial of the summed density in a momentum direction at a nondegenerate phase).
Upstream, hamAdvFrom_eq_computed and hamAdvTo_eq_computed state that under mom-ham split at $n=2$, source and target slots equal bracket-calculus values. The load-bearing witness is the nonzero bracket of MomDyn delta0 against MomDyn delta1 at a fixed phase; kinetic regularity is witnessed by a nonzero partial of the vacuum-kinetic density sum at the phase with one unit of momentum on site 0.
proof idea
Structure instance on top of the weak vacuum-kinetic target. Momentum load-bearing is the triple of site deltas and the standard mom-load-bearing phase, discharged by hamDyn_mom_load_bearing_witness after a MomDyn simp. Advected-from and advected-to ties are pointwise applications of hamAdvFrom_eq_computed and hamAdvTo_eq_computed to the weak target. Kinetic regularity packages the nondegenerate phase (unit momentum on site 0), the zero site index, and vacuumKinetic_kinetic_regular_witness, which reduces the summed density to a local-profile Hamiltonian and evaluates the partial.
why it matters
This is the strong dynamical spine of the variable-kinetic CanonicalMom inhabitant used to refute mod-vacuum rigidity. Downstream, vacuumKineticCanonicalMomTarget extends it by a local Hamiltonian profile, structure profile, and canonical-momentum field; not_HKTRigidityModVacuumStatementN2 feeds that inhabitant into the mod-vacuum statement and obtains a contradiction. Companion lemmas record that the same density fails the mod-vacuum ham-shape ansatz and is excluded from the kinetic-normalized class (momentum conjugate not globally linear in $p$).
In the gap-5 ledger this is Part 1 of the C4/C5 binding: a concrete counterexample showing $\neg$ HKTRigidityModVacuum at $n=2$, so vacuum-sector kill cannot be replaced by a pure mod-vacuum shape constraint. It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is a gravity-side rigidity obstruction inside the SevenGaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.