hasDerivAt_vacuumKineticW_b
plain-language theorem explainer
The vacuum kinetic weight W(a,s), viewed as a function of the second slot, is differentiable at every real b, and its derivative equals the closed Hamiltonian density factor (1/2)(1+a²)(b−a)(1+b²). Gravity/HKT rigidity arguments cite this to pass from the design form of W to a usable pointwise derivative. The proof rewrites W as a constant-in-s multiple of the kinetic primitive K, applies the product rule, and rings the coefficients into the closed form.
Claim. For all real $a,b$, the map $s \mapsto W(a,s)$ is differentiable at $s=b$, and $$W_s(a,b)=\tfrac12(1+a^2)(b-a)(1+b^2),$$ where $W$ is the vacuum kinetic weight polynomial and the right-hand side is the closed $b$-derivative factor used in the kinetic-normalized Hamiltonian density.
background
This module closes Wave C4/C5 gap5 on HKT kinetic-normalized rigidity: after killing the mod-vacuum statement via a variable-kinetic CanonicalMom inhabitant, the kinetic-normalized sector must supply theorem-derived FTC recovery rather than an assumed class field.
The vacuum kinetic weight $W(a,b)$ is an explicit sextic/quartic polynomial in the pair $(a,b)$. A design identity equates it to a constant-in-$b$ prefactor times a primitive $$K(a,b)=\tfrac12(1+a^2)d^2+\tfrac{2a}{3}d^3+\tfrac14 d^4,\quad d=b-a.$$ The closed target derivative is $$H_b^{\mathrm{cl}}(a,b)=\tfrac12(1+a^2)(b-a)(1+b^2).$$
Upstream, differentiability of $s\mapsto K(a,s)$ at $b$ is already proved, with derivative $(1+a^2)(b-a)+(2a)(b-a)^2+(b-a)^3$, obtained from the chain rule on powers of $s-a$.
proof idea
Pointwise rewrite $s\mapsto W(a,s)$ as $s\mapsto \tfrac12(1+a^2),K(a,s)$ via the design identity, then funext and rewrite the goal under that equality.
The prefactor is constant in $s$, so its derivative at $b$ is $0$ by hasDerivAt_const. Multiply by the already-established derivative of $K$ (hasDerivAt_vacuumKineticK_b) via the product rule. A short ring identity shows
$$0\cdot K(a,b)+\tfrac12(1+a^2)\cdot\bigl((1+a^2)(b-a)+(2a)(b-a)^2+(b-a)^3\bigr)=H_b^{\mathrm{cl}}(a,b),$$
which discharges the goal.
why it matters
Feeds directly into hasDerivAt_vacuumKinetic_b, which differentiates the full local vacuum kinetic profile (weight plus the $A(a)p^2$ term) and recovers the same closed $H_b$ factor. That profile derivative is the analytic engine for kinetic-normalized CanonicalMom intensivity and for theorem-derived FTC recovery (ftc_recovery_of_normalized) in the gap5 close path.
In the SevenGaps gravity ledger this is part of the C5 upgrade that flips gap5_constraint_recovery once both ledger halves bind green. It is pure real analysis scaffolding for HKT rigidity, not a forcing-chain (T0–T8) step, but it is required infrastructure for the mod-vacuum kill and the kinetic-normalized rigidity terminal named in the module binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.