differentiable_quarticHam2
plain-language theorem explainer
For any site weights N on the two-point lattice, the quartic Hamiltonian built from fourth powers of momentum coordinates is differentiable as a real map on two-site phase space. Gravity and continuum-limit workers cite it when assembling weak HKT point-split inhabitants that need kinetic regularity. The proof is a one-line pointwise lift from the already-established Fréchet derivative.
Claim. For every weight function $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the map $x\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\,p_j(x)^4$ on two-site phase space is differentiable over $\mathbb{R}$.
background
The module repairs the weak point-split Hamilton–Kirchhoff–Toda (HKT) target after an adversarial pass showed the original dynamical schema is decoy-inhabitable by a quartic zero-momentum configuration. The strong class adds load-bearing momentum, Mom–Ham advection, and kinetic regularity; the weak class remains the place where decoys are exhibited formally.
Here quarticHam2 N is the global Hamiltonian obtained by summing site densities $N(j),p_j^4$ over the two-point lattice $\mathbb{Z}/2\mathbb{Z}$. Phase space is the product of configuration and momentum coordinates at each site. Differentiability of this Hamiltonian is the minimal regularity needed before one can talk about Hamiltonian vector fields, brackets, or advection identities in either the weak or strong target.
Upstream, hasFDerivAt_quarticHam2 already constructs the Fréchet derivative at every point by summing constant multiples of fourth powers of the momentum coordinate projections.
proof idea
One-line term proof. At each phase-space point $x$, apply hasFDerivAt_quarticHam2 N x and convert the Fréchet derivative witness into a DifferentiableAt fact via .differentiableAt. Pointwise differentiability yields global Differentiable ℝ (quarticHam2 N).
why it matters
This lemma supplies the kinetic-regularity obligation for quartic Hamiltonians used as decoy and balanced weak inhabitants. Downstream, quarticZeroMomTarget builds the formal witness that the weak point-split schema is decoy-inhabitable (zero momentum, decorative structure, vanishing advection), and quarticBalancedWeakTarget in the CanonicalMom module builds the balanced-quartic falsifier of strong-class rigidity.
In the Wave C2 repair narrative, strong-class rigidity over point-split dynamics is already marked false; binding rigidity moves to CanonicalMom. Differentiability of the quartic Hamiltonian is a small but load-bearing brick: without it the weak inhabitants cannot even state their Hamiltonian data cleanly. It does not restore rigidity; it makes the decoy and falsifier constructions honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.