Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN

show as:
view Lean formalization →

General-n model of the dynamic Hamiltonian whose kinetic term is unweighted and whose stiffness slot carries the configuration-dependent factor g_j(q)=1+q_j^2. Extends the two-site dynamic structure-function bracket to an n-site lattice, with Fréchet derivatives, partials, and the self-bracket identity. Cited by continuum Dirac-algebra binding that lands the ledger terminal for 1-periodic C¹ data.

claimOn an $n$-site phase space, the dynamic Hamiltonian $H_n$ has unweighted kinetic slot and stiffness weights $g_j(q)=1+q_j^2$. The inverse-metric structure function is configuration-dependent. The module records Fréchet differentiability of $H_n$, explicit $p$- and $q$-partials, and the lattice self-bracket identity $\{H_n,H_n\}=2$ (up to the standard normalization of the dynamic bracket).

background

Wave C2 of the Seven Gaps gravity program closes typed residuals in the Dirac algebra continuum limit. The frozen weighted Hamiltonian keeps the structure-function weight fixed while the phase-space point varies; full ADM gravity instead needs the inverse spatial metric in that slot to depend on the canonical metric data.

The two-site module already shows that naively plugging a dynamic $g(x)$ into the frozen Hamiltonian and reusing frozen partials fails: the configuration partial picks up an uncompensated $\partial g/\partial q$ term. The correct dynamic Hamiltonian therefore rebuilds both the energy and its partials so the structure-function slot carries $g_j(q)=1+q_j^2$ with kinetic slot left unweighted.

This module lifts that two-site model to general $n$, supplying the $n$-site dynamic Hamiltonian, its identification with the two-site object when $n=2$, the dynamic inverse-metric data, and the differentiability package needed for lattice brackets.

proof idea

Definition-first module with supporting equalities and calculus lemmas. The $n$-site dynamic Hamiltonian is declared by the exact shape (unweighted kinetic slot, stiffness $g_j=1+q_j^2$), then identified with the two-site dynamic Hamiltonian on the overlap. Dynamic inverse-metric data are defined and matched to the two-site version. Fréchet derivative and $p$-/$q$-partial lemmas are proved by direct differentiation of the explicit formula; differentiability follows. Self-bracket theorems reduce the $n$-site dynamic bracket to the two-site identity already established upstream, yielding the normalized self-bracket value two.

why it matters in Recognition Science

Feeds the continuum binding module that attaches the freestanding Riemann shape of the sampled dynamic bracket sum to the genuine lattice bracket of the $n$-site dynamic Hamiltonian after periodic wrap treatment, then discharges the ledger terminal for the Dirac-algebra continuum limit on 1-periodic $C^1$ data. Without the general-$n$ dynamic Hamiltonian and its self-bracket, the sampled continuum object would remain disconnected from the lattice Dirac structure. Closes the modeling gap flagged by the dynamic structure-function blocker: weights must vary with canonical metric data, not stay frozen. Sits in the Gravity/SevenGaps chain toward a continuum ADM-compatible Dirac algebra.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)