Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample

show as:
view Lean formalization →

One-site model with quartic kinetic density $h=\pi^4$ that falsifies HKT rigidity for non-quadratic kinetics in the discrete constraint algebra. Gap-5 gravity readers cite it when checking that hypersurface-deformation closure fails off the quadratic kinetic sector. The file defines the density and zero-momentum companion, proves Fréchet differentiability, and evaluates the Poisson self-bracket on a single lattice site.

claimOn one lattice site, take the quartic kinetic Hamiltonian density $h=\pi^4$ and the zero momentum density $p\equiv 0$. The module records Fréchet differentiability of $h$ and $p$, the partials $\partial_q h$, $\partial_q p$, $\partial_\pi p$, and the Poisson self-bracket $\{h,h\}$ in the discrete canonical phase space of the hypersurface-deformation setup.

background

This file sits inside the QG Seven-Gaps campaign, Lane 5 (constraint closure). The upstream hypersurface-deformation module supplies a finite-dimensional canonical phase space on a periodic 1D lattice, an fderiv-based Poisson bracket, and kernel-checked closure relations for discrete constraint generators in the linearized regime.

HKT (Hojman–Kuchař–Teitelboim) rigidity asks whether the hypersurface-deformation algebra forces the kinetic term to be the standard quadratic supermetric form. The model here is deliberately non-quadratic: a single-site quartic density $h_j=\pi_j^4$, paired with a vanishing momentum density, so that derivatives and brackets can be computed exactly without continuum or multi-site clutter.

Sibling objects cover the integrated quartic Hamiltonian, its Fréchet derivative and differentiability, configuration partials, the self-bracket, and the corresponding facts for the zero-momentum density.

proof idea

Definition-and-computation module, not a single theorem. It introduces the quartic density and zero-momentum density as concrete phase-space functions, then proves Fréchet differentiability and evaluates partial derivatives by direct calculus on $\pi^4$ and on the zero map. The Poisson self-bracket of the quartic Hamiltonian is reduced via the ambient fderiv bracket from the hypersurface-deformation layer; the zero-momentum side collapses by the identity that the density is identically zero. No continuum limit or multi-site coupling is attempted here.

why it matters in Recognition Science

Supplies the concrete one-site counterexample that the Gap-5 residual DAG and close-status ledger need for HKT rigidity. Downstream, Gap5ConstraintCloseStatus binds ledger flags so that gap5 constraint recovery is marked true while the continuum-algebra HKT-open bit and the residual DAG hktRigidityOpen bit flip false. Gap5ConstraintResidualDAG names residuals for dynamic Dirac structure functions and HKT rigidity; this module is the explicit falsifying model those residuals point at. HKTGroundworkAudit and HKTOneSiteCounterexampleAudit import it as the audited witness that non-quadratic kinetics break the expected deformation algebra on even a single site.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (23)