hasFDerivAt_quarticHam2
plain-language theorem explainer
The two-site quartic Hamiltonian H_N = Σ_j N_j π_j^4 is Fréchet differentiable on phase space, with explicit derivative Σ_i N_i · 4 π_i^3 dπ_i. Anyone building Poisson brackets or kinetic-regularity witnesses for the strong HKT point-split class cites this. The proof is a short term: sum of scaled fourth powers of the momentum coordinate maps.
Claim. For any weight $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and any point $x$ in the two-site phase space $(q,\pi)$, the map $H_N(x)=\sum_{j} N_j\,\pi_j^4$ is Fréchet differentiable at $x$, and its derivative is the continuous linear map $DH_N(x)=\sum_i N_i\cdot(4\pi_i^3)\,d\pi_i$.
background
Phase space on a periodic lattice with $n$ sites is the product of configuration and conjugate momentum: $(q,\pi)$ with both maps $\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$. The momentum coordinate functional $\mathrm{coordP},k$ extracts $\pi_k$; it is continuous linear, hence Fréchet differentiable everywhere (upstream hasFDerivAt_coord_snd).
The model density is the pure quartic kinetic term $h_j=\pi_j^4$. Weighted by a site-dependent $N$, one obtains the Hamiltonian $H_N=\sum_j N_j\pi_j^4$, with candidate derivative assembled as the corresponding sum of scaled cubics times $d\pi_i$.
This module strengthens the point-split HKT target after an adversarial pass showed the weak schema is decoy-inhabitable by a quartic zero-momentum model. Differentiability of $H_N$ is basic calculus infrastructure for the strong class (load-bearing momentum, advection tied to the Mom–Ham bracket, kinetic regularity).
proof idea
Unfold the three definitions ($H_N$, its candidate derivative, and the density $\pi_j^4$). The claim reduces to Fréchet differentiability of a finite sum of maps $x\mapsto N_i,(\pi_i(x))^4$. Apply HasFDerivAt.fun_sum, and for each summand chain: the momentum coordinate is differentiable by hasFDerivAt_coord_snd, raise that derivative to the fourth power via .pow 4, then scale by the constant $N_i$ with .const_mul. No further algebraic identities are needed.
why it matters
This lemma is the differentiability engine for the quartic Hamiltonian used as a model (and as a balanced falsifier) in the SevenGaps HKT repair. Downstream it feeds differentiable_quarticHam2 (global differentiability) and pderivQ_quarticHam2 (vanishing $q$-partials, as expected for a pure kinetic density). Those facts support the Mom–Ham bracket identity bracket_MomBalanced_quarticHam and the kinetic-regularity witness quarticBalanced_kinetic_regular_witness in HKTCanonicalMomTarget.
In framework terms this is gravity-side scaffolding for the HKT point-split program, not a T0–T8 forcing step. The module doc is explicit: strong-class rigidity is dead; binding rigidity moves to CanonicalMom, and the discrimination gate is that honest inhabitants pass while the quartic zero-momentum decoy fails. This derivative lemma keeps the honest and balanced quartic models analytically well-defined so those gates can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.