vacuumKineticLocalSmooth
plain-language theorem explainer
Packages the vacuum-kinetic local density $h(a,b,p)=A(a)p^2+W(a,b)$ as a smooth local Hamiltonian: partial profiles and the two-site cell Fréchet derivative. Anyone building the variable-kinetic CanonicalMom target or the gap-5 non-normalized counterexample cites it. Pure structure inhabitant wiring four prior lemmas.
Claim. The local Hamiltonian profile $h(a,b,p)=A(a)\,p^{2}+W(a,b)$ is smooth in the local-Hamiltonian sense: there exist partial profiles $h_a$, $h_b$, $h_p$ such that for every site $j\in\mathbb{Z}/2\mathbb{Z}$ and phase point $x$, the map $y\mapsto h(q_j(y),q_{j+1}(y),p_j(y))$ is Fréchet differentiable at $x$ with derivative $h_a\,dq_j+h_b\,dq_{j+1}+h_p\,dp_j$.
background
Module closes gap 5 of the HKT seven-gap ledger: a variable-kinetic density that inhabits CanonicalMom yet fails kinetic-normalized form, so the mod-vacuum rigidity statement is killed and the normalized class is forced separately.
A LocalHamProfile is a real function of three scalars (two neighboring configuration values and one momentum). LocalHamSmooth packages three partial profiles together with a cellwise Fréchet-derivative identity on two-site phase space PhaseSpace 2.
The vacuum-kinetic profile is $h(a,b,p)=A(a)p^{2}+W(a,b)$. Its partials vacuumKineticLocalHa/Hb/Hp are defined by directional Fréchet derivatives of the profile map; hasFDerivAt_vacuumKineticLocalCell proves the matching linear combination of coordinate covectors coordQ j, coordQ (j+1), coordP j.
proof idea
Definitional structure inhabitant, not a tactic proof. The four fields of LocalHamSmooth are filled by name: ha, hb, hp point at the three partial-profile defs (each an fderiv of the profile map along a standard basis vector), and hasFDerivCell is the already-proved lemma hasFDerivAt_vacuumKineticLocalCell. No further algebra.
why it matters
Load-bearing smoothness witness for the variable-kinetic side of gap 5. Downstream, differentiable_vacuumKineticHam lifts it to full Hamiltonian differentiability; ham_ham_vacuumKinetic computes the Poisson bracket; vacuumKineticCanonicalMomTarget installs the density as a CanonicalMom inhabitant; vacuumKinetic_kinetic_regular_witness checks nondegeneracy of $\partial_p H$; and vacuumKinetic_not_kineticNormalized uses the same package to show $h_p$ is not globally of the form $2 c_{\mathrm{Kin}} p$. That exclusion is the C5 half of the mod-vacuum kill: CanonicalMom alone does not force kinetic-normalized form, so the normalized class must be imposed separately before FTC recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.