Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.HKTLocalFunctionalEquation

show as:
view Lean formalization →

Defines the local Hamiltonian density on a finite lattice cell and packages the general-n local functional equation as a Prop, with the n=2 case already theorem-grade. Supplies Fréchet derivatives of the cell Hamiltonian in the (p,q) directions and smoothness lemmas. Downstream HKT canonical-momentum and groundwork-audit modules import this layer to state rigidity and constraint targets.

claimOn a periodic lattice cell, a local Hamiltonian density $H$ is built from a smooth profile of conjugate pairs $(p,q)$. The module records the Fréchet derivatives $\partial_p H$ and $\partial_q H$, smoothness of $H$, and a general-$n$ packaging proposition for the local functional equation (the proved form is the $n=2$ theorem).

background

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

Here the focus narrows to a single lattice cell. A local Hamiltonian profile assigns an energy density to the cell's conjugate data $(p,q)$. From that profile one constructs the cell Hamiltonian $H$, then its Fréchet derivative in the ambient phase-space normed space. Partials along the $p$- and $q$-directions are extracted as specializations of that derivative.

The "local functional equation" is the discrete stand-in for the continuum statement that the Hamiltonian density depends only on local canonical data and transforms correctly under hypersurface deformations. The module packages the general-$n$ claim as a Prop; the $n=2$ instance is the proved form referenced above the packaging.

proof idea

Definition-and-calculus layer, not a single end-to-end theorem. LocalHamProfile and LocalHamFromProfile introduce the cell density; LocalHamSmooth and the hasFDerivAt_* lemmas establish Fréchet differentiability via Mathlib's fderiv API on the finite-dimensional phase space. cellD_pdir and cellD_qdir specialize the total derivative to the $p$ and $q$ coordinate directions; pderivP_* and pderivQ_* name those partials. The general-$n$ packaging is a Prop wrapper around the already-proved $n=2$ local functional equation, ready for later discharge at higher $n$.

why it matters in Recognition Science

Feeds two Wave C2 consumers. HKTCanonicalMomTarget imports it to "kill strong rigidity" and repair the CanonicalMom class: Session A inhabits the point-split dynamical target at $n=2$ by a balanced quartic falsifier and proves the negation of the strong rigidity statement; Session B defines the honest CanonicalMom target. HKTGroundworkAudit imports it for the R5/R6 axiom audit of the HKT groundwork.

In the broader RS gravity program this is the local analytic substrate under discrete ADM/Dirac constraint closure: without a differentiable cell Hamiltonian and a stated local functional equation, Poisson brackets of constraints cannot be formed honestly on the lattice. It does not yet close the full constraint algebra; it supplies the density and derivative facts those closure theorems need.

scope and limits

used by (2)

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 (17)