vacuumKineticWeakTarget
plain-language theorem explainer
Packages the vacuum-kinetic Hamiltonian density into a weak 2-site dynamical point-split target (HKT point-split dynamics). Anyone proving that mod-vacuum CanonicalMom rigidity fails, or that variable-kinetic models lie outside the kinetic-normalized class, cites this inhabitant. The body is a structure instance: fields are prior densities and bracket lemmas, with short locality and covariance tactics.
Claim. The vacuum-kinetic model supplies a weak dynamical point-split target on the $2$-site phase space: Hamiltonian density is the local vacuum-kinetic profile in $(q_j,q_{j+1},p_j)$, momentum density and structure function are the standard dynamical ones, advected Hamiltonian densities are the corresponding Poisson brackets, and the locality, covariance, mom-mom, mom-ham split, ham-ham, differentiability, and nondegeneracy axioms all hold.
background
Module setting is Wave C4/C5 gap5: kill mod-vacuum CanonicalMom rigidity and close kinetic-normalized rigidity. Binding notes name the cross-family verdict and the C5 acceptance adjudication. Part 1 builds a variable-kinetic CanonicalMom counterexample; Part 2 isolates the kinetic-normalized intensivity field so FTC recovery is theorem-derived rather than an assumed class field.
The Hamiltonian density is the local vacuum-kinetic profile evaluated on neighbouring configuration coordinates and the on-site momentum: $\mathrm{ham}(x,j)=\mathrm{profile}(q_j,q_{j+1},p_j)$. Advected densities are Poisson brackets of site-projected momentum against that ham density (from/to neighbouring sites). Differentiability of linear combinations of the ham density reduces to smoothness of the local profile. Bracket identities (mom-mom, mom-ham split, ham-ham) are already proved for this density against the dynamical momentum and structure fields.
Nondegeneracy is witnessed by a fixed phase and the vacuum-kinetic nondegeneracy lemma on $\mathbb{Z}/2\mathbb{Z}$.
proof idea
Structure instance for the weak dynamical target at $N=2$. Ham density, advected ham densities, and the three bracket theorems are plugged in by name. Differentiability of ham combinations is differentiable_vacuumKineticHam; mom differentiability and structure nonconstancy come from the shared dynamical fields. Locality of ham is dsimp plus rewriting the three coordinate hypotheses; covariance rewrites the $\mathbb{Z}/2$ index by a one-line ring identity then simp. Structure locality is the same pattern on structureDyn. Mom-mom and mom-ham split are simpa reductions to bracket_MomDyn_MomDyn and mom_ham_split_vacuumKinetic. Ham-ham is the prior theorem ham_ham_vacuumKinetic. Nondegeneracy is the pair of the vacuum-kinetic nondeg phase, site $0$, and vacuumKinetic_nondeg.
why it matters
This is the weak half of the variable-kinetic counterexample that kills mod-vacuum rigidity. Downstream, not_HKTRigidityModVacuumStatementN2 obtains a contradiction by feeding the related CanonicalMom target into the claimed rigidity statement (doc: "Mod-vacuum CanonicalMom rigidity is false"). Companion lemmas show the same density fails the mod-vacuum ham-shape ansatz and is not kinetic-normalized (load-bearing: the momentum factor is not globally of the form $2 c_{\mathrm{Kin}} p$). The strong target extends this weak package by mom load-bearing and advFrom-tied fields.
In the SevenGaps ledger this is Part 1 of gap5: a concrete inhabitant proving $\neg$ of the mod-vacuum rigidity statement at $N=2$, so the constraint-recovery flip can be owned by the gap5 close status once both ledger halves bind green. It does not itself touch T0-T8 or the RCL; it is gravity-side scaffolding closure for the HKT/CanonicalMom branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.