quarticHam2D
plain-language theorem explainer
Explicit Fréchet derivative (as a continuous linear map on two-site phase space) of the weighted quartic momentum Hamiltonian. HKT point-split and canonical-momentum targets cite it when differentiating that Hamiltonian and when checking kinetic regularity or Mom–Ham brackets. The body is a two-term sum of scaled cubed-momentum multiples of the momentum coordinate functionals.
Claim. Fix weights $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and a phase-space point $x=(q,\pi)$ on the two-site lattice. Define the continuous linear map $DH_N(x):T_x\mathrm{PhaseSpace}_2\to\mathbb{R}$ by $$DH_N(x)=\sum_{i\in\mathbb{Z}/2\mathbb{Z}} N(i)\cdot\bigl(4\,\pi_i^3\bigr)\,\mathrm{d}\pi_i,$$ where $\mathrm{d}\pi_i$ is the $i$-th momentum coordinate functional.
background
The ambient setting is the Wave C2 repair of the point-split HKT target: the weak dynamical schema was decoy-inhabitable by a quartic zero-momentum example, so this module strengthens the target with load-bearing momentum, Mom–Ham advection, and kinetic regularity, and excludes that decoy.
Phase space on $n$ sites is the product of configuration and conjugate momentum maps $\mathrm{PhaseSpace},n=(q,\pi)$ with $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Here $n=2$. The upstream functional $\mathrm{coordP},i$ is the continuous linear map extracting the $i$-th momentum coordinate $\pi_i$.
The quartic Hamiltonian (sibling density sum) is built from fourth powers of the momenta, weighted by $N$. Its candidate derivative at a point is therefore proportional to cubed momenta times $\mathrm{d}\pi_i$, which is exactly what this definition packages.
proof idea
Definition, not a proved theorem. The body is the finite sum over $i:\mathbb{Z}/2\mathbb{Z}$ of the scalar $N(i)$ times $4\cdot(\pi_i)^3$ times the continuous linear map $\mathrm{coordP},i$. No tactics or lemmas are invoked; the formula is the chain-rule derivative of $\sum_i N(i),\pi_i^4$ with respect to phase space.
why it matters
Supplies the derivative object that the strong point-split calculus needs for the quartic Hamiltonian. Downstream, hasFDerivAt_quarticHam2 proves this map is the true Fréchet derivative of the quartic Hamiltonian, and pderivQ_quarticHam2 uses it to show all configuration partials vanish (purely kinetic quartic). In the canonical-momentum module it feeds the Mom–Ham bracket identity for the balanced quartic and the kinetic-regularity witness that kills zero-momentum decoys.
In the module narrative, strong-class rigidity over the point-split target is already dead (balanced-quartic falsifier); binding rigidity moves to CanonicalMom. This definition is infrastructure for that discrimination gate: honest inhabitants differentiate cleanly, while the weak quartic zero-momentum decoy fails load-bearing momentum checks. No ledger flag is flipped here; the object is pure differential scaffolding for the gravity SevenGaps HKT chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.