quarticHam2
plain-language theorem explainer
Smeared quartic Hamiltonian on the two-site lattice: H_N(q,π) = Σ_j N(j) π_j^4. Gravity and HKT workers cite it as the model Hamiltonian for point-split bracket identities and as the balanced-quartic witness that kills strong-class rigidity. The body is a direct weighted sum of the site densities π_j^4.
Claim. For a smearing $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)$ on the two-site lattice, the quartic Hamiltonian is $H_N(x)=\sum_{j\in\mathbb{Z}/2\mathbb{Z}} N(j)\,\pi_j^4$.
background
The ambient setting is the Wave C2 repair of the point-split HKT target on a two-site periodic lattice. Phase space is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The site density used here is the pure quartic kinetic model $h_j=\pi_j^4$ (no potential, no spatial coupling in the density itself).
Smearing against a test function $N$ turns the local density into a global Hamiltonian functional on phase space. That is the standard ADM-style pairing used throughout the SevenGaps hypersurface-deformation calculus: brackets of smeared generators encode the hypersurface deformation algebra.
The module exists because the weak point-split schema admitted a quartic zero-momentum decoy. The strong class adds load-bearing momentum and kinetic regularity; this quartic Hamiltonian is the concrete model object against which those gates and the later balanced-quartic falsifier are checked.
proof idea
Pure definition: evaluate the site density $\pi_j^4$ at each lattice point and sum against the smearing weights $N(j)$. No lemmas, no tactics.
why it matters
This is the workhorse Hamiltonian for the point-split strong module and for the CanonicalMom falsifier path. Downstream it feeds the vanishing self-bracket bracket_quarticHam2_quarticHam2, Fréchet differentiability and partials (differentiable_quarticHam2, hasFDerivAt_quarticHam2, pderivQ_quarticHam2), and the balanced-quartic package in HKTCanonicalMomTarget (Mom–Ham bracket, Ham–Ham bracket zero, kinetic-regularity witness, and the weak-schema inhabitant).
In framework terms it is a model generator inside the gravity SevenGaps HKT grind, not a forcing-chain landmark. Its role is diagnostic: the balanced quartic (definitionally equal to this smeared form) inhabits the weak schema and supplies the explicit counterexample that makes strong-class rigidity false, pushing binding rigidity to the CanonicalMom target. No ledger flag flips; the discrimination gate is that honest inhabitants pass while zero-momentum decoys fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.