hasDerivAt_vacuumKinetic_b
plain-language theorem explainer
The vacuum kinetic local Hamiltonian profile is differentiable in the second field slot, and its derivative at b equals the closed-form expression (1/2)(1+a²)(b-a)(1+b²), independent of momentum p. Gravity/HKT rigidity arguments cite this to identify the b-partial with an explicit algebraic formula. The proof splits the profile into a p-dependent constant plus the W potential and adds the known W derivative.
Claim. For all real $a,b,p$, the map $s \mapsto A(a)\,p^2 + W(a,s)$ is differentiable at $s=b$, and its derivative equals $\tfrac12(1+a^2)(b-a)(1+b^2)$, where $A(a)=(1+a^2)^{-1}$ and $W$ is the vacuum kinetic potential polynomial.
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 remaining work is to make the kinetic-normalized intensity field and its FTC recovery theorem-derived rather than assumed.
The local Hamiltonian profile under study is $$\mathrm{profile}(a,b,p)=A(a),p^2+W(a,b),$$ with $A(a)=(1+a^2)^{-1}$ and $W$ a fixed bivariate polynomial (the vacuum kinetic potential). The closed candidate for the $b$-partial is $$H_b^{\mathrm{cl}}(a,b)=\tfrac12(1+a^2)(b-a)(1+b^2).$$
Upstream, hasDerivAt_vacuumKineticW_b already shows that $s\mapsto W(a,s)$ has derivative $H_b^{\mathrm{cl}}(a,b)$ at $s=b$, by rewriting $W$ as a constant multiple of the design kernel $K$ and differentiating. The present result lifts that fact from $W$ alone to the full local profile.
proof idea
Three short steps. First, the summand $A(a),p^2$ is independent of the differentiation variable, so hasDerivAt_const gives derivative $0$ at $b$. Second, definitional equality identifies the local profile with $A(a),p^2+W(a,\cdot)$. Third, add the two derivatives via HasDerivAt.add, feeding in the upstream theorem that $W$ differentiates to $H_b^{\mathrm{cl}}(a,b)$; a one-line ring rewrite clears the $0+$ summand. No mean-value or Frechet machinery is needed here; that appears only in the downstream identification of the named partial.
why it matters
Feeds directly into vacuumKineticLocalHb_eq_closed, which equates the profile's named $b$-partial (extracted via ContDiff/fderiv) with the closed algebraic formula $H_b^{\mathrm{cl}}$. That equality is the analytic half of kinetic-normalized rigidity: once partials match closed forms, FTC recovery of the normalized CanonicalMom intensity becomes a theorem rather than a class field assumption.
In the SevenGaps ledger this sits under gap5 (HKT mod-vacuum / kinetic-normalized rigidity). The module binding flips gap5_constraint_recovery only after both ledger halves bind green. The result is pure real analysis on the vacuum kinetic ansatz; it does not itself invoke the Recognition forcing chain (T5–T8) or the RCL, but it is the calculus step that lets the gravity-side rigidity statement close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.