contDiff_vacuumKinetic_kinTerm
plain-language theorem explainer
The vacuum kinetic term A(a)·p², with A the amplitude factor and p the third coordinate on ℝ³, is twice continuously differentiable. HKT kinetic-normalized rigidity arguments that differentiate the vacuum kinetic density twice rely on this smoothness. The proof multiplies the C² amplitude (after first-coordinate projection) by the square of the third-coordinate projection.
Claim. The map $(a,w,p)\mapsto A(a)\,p^{2}$ from $\mathbb{R}^{3}$ to $\mathbb{R}$ is of class $C^{2}$, where $A:\mathbb{R}\to\mathbb{R}$ is the vacuum kinetic amplitude factor.
background
The module closes Wave C4/C5 gap5 in the HKT gravity sector: mod-vacuum kill plus kinetic-normalized rigidity. The vacuum kinetic package splits into an amplitude factor A, a design weight W, and a kinetic density built from them; the Hamiltonian density is assembled from these pieces so that FTC recovery of the normalized canonical momentum is theorem-derived rather than an assumed class field.
Twice continuous differentiability is the calculus prerequisite for the rigidity PDE and mean-value arguments imported from Mathlib (ContDiff, FDeriv, MeanValue). The kinetic term singled out here is the product of A on the first coordinate with the square of the third coordinate (the momentum-like slot in the local profile).
proof idea
Term-mode assembly from Mathlib ContDiff combinators. First-coordinate projection is C² by contDiff_fst; third-coordinate projection is C² by contDiff_snd composed with itself. The amplitude A is already C², so its composition with the first projection is C². Multiply that by the product of the third projection with itself. No analytic estimates: pure structural closure under composition and multiplication.
why it matters
Private calculus lemma inside the kinetic-normalized rigidity terminal for gap5. It underwrites differentiation of the vacuum kinetic density used when the CanonicalMom intensivity field is normalized and when FTC recovery is derived rather than postulated. In the Recognition gravity stack this is bookkeeping for the HKT vacuum sector kill and the flip of gap5 constraint recovery once both ledger halves bind green. It does not itself state a physical law; it licenses the C² calculus steps those statements need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.