hasFDerivAt_vacuumKineticLocalCell
plain-language theorem explainer
On the two-mode phase space, the vacuum kinetic Hamiltonian density pulled back to cell coordinates (q_j, q_{j+1}, p_j) is Fréchet differentiable, with derivative the linear combination of the three coordinate covectors weighted by the profile partials Ha, Hb, Hp. Anyone building LocalHamSmooth instances for the kinetic-normalized vacuum sector cites this. The proof composes profile differentiability with the cell-coordinate chart derivative and matches the continuous-linear-map identity by evaluation on basis directions.
Claim. For each cell index $j \in \mathbb{Z}/2\mathbb{Z}$ and each point $x$ in the two-mode phase space, the map $y \mapsto H_{\mathrm{vac}}(q_j(y), q_{j+1}(y), p_j(y))$ is Fréchet differentiable at $x$, and its derivative is $\partial_a H_{\mathrm{vac}}\, dq_j + \partial_b H_{\mathrm{vac}}\, dq_{j+1} + \partial_p H_{\mathrm{vac}}\, dp_j$ evaluated at the cell coordinates of $x$.
background
The module closes Wave C4/C5 gap5 on HKT mod-vacuum kill and kinetic-normalized rigidity. The vacuum kinetic local profile is a smooth scalar Hamiltonian density on three real arguments (two neighboring configuration coordinates and one momentum). Phase space for two modes is the product of configuration and momentum maps indexed by $\mathbb{Z}/2\mathbb{Z}$.
profileMap packages a local profile $h$ as the map $(a,b,p)\mapsto h(a,b,p)$ on $\mathbb{R}\times\mathbb{R}\times\mathbb{R}$. Cell coordinates extract $(q_j, q_{j+1}, p_j)$ from a phase-space point; their derivative is the continuous linear map assembling the three coordinate projections. The partials Ha, Hb, Hp are the classical first derivatives of the vacuum kinetic profile in those three slots.
The local setting is the kinetic-normalized CanonicalMom intensivity field: FTC recovery is theorem-derived rather than an assumed class field, and this differentiability fact is the analytic half of packaging the vacuum kinetic density as a smooth local Hamiltonian.
proof idea
Start from continuous differentiability of the vacuum kinetic profile (ContDiff of order 2 implies Differentiable), evaluate at the cell coordinates of $x$, and obtain HasFDerivAt for the profile map. Compose with the already-proved HasFDerivAt of the cell-coordinate chart.
Rewrite the target scalar function as profileMap composed with cell coordinates (definitional equality). It remains to identify the composed continuous linear map with the claimed combination of coordQ and coordP. Extensionality on an arbitrary tangent vector $v$, expand the triple $(v_j^q, v_{j+1}^q, v_j^p)$ in the standard basis of $\mathbb{R}^3$, apply linearity of the Fréchet derivative, and simplify with the definitions of Ha, Hb, Hp and the coordinate functionals. The resulting identity discharges the composition.
why it matters
This lemma is the sole analytic obligation inside vacuumKineticLocalSmooth, which packages Ha, Hb, Hp together with cellwise Fréchet differentiability into a LocalHamSmooth instance for the vacuum kinetic profile. That instance is the kinetic-normalized half of the gap5 ledger: after both ledger halves bind green, Gap5ConstraintCloseStatus owns the flip of gap5_constraint_recovery.
In the broader SevenGaps gravity program, smooth local Hamiltonian structure is what lets the kinetic-normalized CanonicalMom PDE and the mod-vacuum kill talk to the same phase-space calculus. Without an explicit derivative formula in the coordinate basis, later mean-value and FTC recovery steps cannot fire. The result is pure analysis on the two-mode vacuum sector; it does not itself settle the rigidity statement, but it is the terminal smoothness brick that statement rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.