vacuumKineticHpClosed
plain-language theorem explainer
Closed form for the momentum partial of the vacuum-kinetic local profile: twice A(a) times p, with A(a)=(1+a²)⁻¹. Gravity/HKT authors cite it when matching local Hp to an explicit algebraic expression and when proving the variable-kinetic vacuum sector is not kinetic-normalized. The body is a one-line product of the amplitude factor with p.
Claim. For real $a$ and $p$, set $H_p^{\mathrm{closed}}(a,p) := 2\,A(a)\,p$, where the amplitude is $A(a)=(1+a^2)^{-1}$.
background
Module Wave C4/C5 gap5 closes the mod-vacuum kill and kinetic-normalized rigidity terminal for HKT-style CanonicalMom targets. Part 1 builds a variable-kinetic inhabitant that falsifies mod-vacuum rigidity; Part 2 treats kinetic-normalized CanonicalMom as an intensivity field whose FTC recovery is theorem-derived rather than an assumed class field.
The sibling amplitude $A(a)=(1+a^2)^{-1}$ is the local prefactor of the vacuum-kinetic profile. The closed Hp is the explicit $p$-linear form expected if the Hamiltonian density were quadratic in momentum with that prefactor. Downstream, local Hp is identified with this closed expression after ContDiff/HasDerivAt work on the profile, so algebraic identities (FE, structure-mom matching, non-normalization) can avoid repeated differentiation.
proof idea
Definition, not a proof. Body is the product $2\cdot A(a)\cdot p$ with $A$ the sibling inverse-square amplitude. No lemmas are applied; later theorems unfold this name or rewrite local Hp to it.
why it matters
Load-bearing algebraic handle for the vacuum-kinetic counterexample half of gap5. Parents include: HasDerivAt of the local profile in the $p$ slot (derivative equals this closed form); equality of local Hp with the closed form; the vacuum-kinetic functional equation; structure-coefficient times mom-density matching; the kinetic-regular witness; and the terminal non-existence result that no KineticNormalizedCanonicalMom has this vacuum-kinetic target (hp is not globally of the form $2 c_{\mathrm{Kin}} p$).
In the Recognition gravity ledger this supplies the explicit Hp used to show variable kinetics escape the kinetic-normalized class, completing the mod-vacuum kill side of the C4/C5 binding before Gap5ConstraintCloseStatus flips constraint recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.