contDiff_vacuumKineticA
plain-language theorem explainer
The vacuum kinetic amplitude map a ↦ (1+a²)⁻¹ is twice continuously differentiable on ℝ. Gravity and HKT-rigidity arguments cite it when they need C² control on the normalized kinetic prefactor before composing with product-space kinetic terms. The proof is a short term argument: C² of 1+a² plus inversion under the never-zero lemma.
Claim. The real function $a \mapsto (1+a^2)^{-1}$ is of class $C^2$ on $\mathbb{R}$.
background
In the kinetic-normalized HKT sector, the vacuum amplitude is defined by $A(a)=(1+a^2)^{-1}$. It is the scalar prefactor that multiplies squared momentum-like coordinates in the local kinetic density. The module sits in Wave C4/C5 gap5 work: mod-vacuum kill plus kinetic-normalized rigidity, with FTC recovery derived rather than assumed as a class field.
Twice continuous differentiability is the regularity needed before product-space compositions and multiplications that build the full kinetic term. The only nontrivial algebraic fact used upstream is that $1+a^2\neq 0$ for every real $a$, proved by nonnegativity of squares. The doc-comment notes that inversion is done first on $\mathbb{R}$; a product-space .inv at smoothness order $\top$ times out in the checker.
proof idea
Build $C^2$ for $a\mapsto 1+a\cdot a$ as the sum of a constant map and the product of the identity with itself. Rewrite the goal as $C^2$ of the pointwise inverse of that map. Apply Mathlib's ContDiff.inv with the lemma that $1+a^2$ never vanishes. No further calculus is required.
why it matters
Feeds the private theorem that the product-space kinetic term $t\mapsto A(t_1)\cdot(t_{2,2})^2$ is $C^2$, which is the regularity spine for kinetic-normalized CanonicalMom rigidity in this module. That chain supports the C5 upgrade of gap5 (constraint recovery owned by Gap5ConstraintCloseStatus after both ledger halves bind). In the broader SevenGaps gravity program this is bookkeeping calculus, not a new physical law: it licenses differentiation under the normalized kinetic profile used when ruling out or rigidifying HKT mod-vacuum inhabitants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.