Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN

show as:
view Lean formalization →

Generalizes the two-site dynamic Hamiltonian to n lattice sites: kinetic term unweighted, stiffness weighted by g_j(q)=1+q_j^2. Supplies Fréchet derivatives, configuration and momentum partials, and the exact self-bracket identity needed for the continuum Dirac-algebra limit. Cited by the Wave C2 R4 continuum-binding argument. Proofs are mostly equality rewrites against the two-site model plus direct differentiation.

claimOn phase space $(\mathbb{R}^n\times\mathbb{R}^n)$, the dynamic Hamiltonian is $H_n(q,p)=\frac12\sum_j p_j^2+\frac12\sum_j(1+q_j^2)(\Delta q)_j^2$ (kinetic slot unweighted; stiffness $g_j(q)=1+q_j^2$). It is $C^1$, its partials are explicit, and the lattice Dirac bracket satisfies $\{H_n,H_n\}=2$ (up to the standard normalization of the structure sum).

background

Wave C2 of the Seven Gaps program builds a lattice Dirac algebra whose continuum limit recovers the ADM hypersurface-deformation algebra. The frozen weighted Hamiltonian $H_W$ keeps the inverse-metric weight fixed in phase space; full gravity needs that weight to move with the canonical metric data.

The upstream two-site module DynamicStructureBracket closes residuals R0–R1: the decoy that plugs a dynamic $g$ into frozen partials fails because $\partial_q$ picks up an uncompensated $\partial g/\partial q$ term. The companion blocker module records why background-weighted brackets cannot be reused once the weight depends on configuration.

This module lifts that two-site dynamic model to general $n$. Notation: phase point $x=(q,p)\in\mathbb{R}^n\times\mathbb{R}^n$; stiffness $g(x)_j=1+(q_j)^2$; $H_n$ has unweighted kinetic slot and $g$-weighted stiffness. Sibling lemmas give the inverse-metric reading, Fréchet derivative, and $p$- and $q$-partials of $H_n$.

proof idea

Definition module plus comparison and calculus lemmas, not a single deep theorem. HamDynN is the n-site formula; HamDynN_eq_HamDyn specializes to the two-site dynamic Hamiltonian. dynamicInverseMetricN packages the stiffness weight as a diagonal inverse metric, with an equality lemma tying it to $g$.

Differentiability is proved by exhibiting the Fréchet derivative (hasFDerivAt_HamDynN) and reading off momentum and configuration partials. The self-bracket identities (bracket_HamDynN_HamDynN, primed variant, and the normalized ..._eq_two) reduce the n-site structure sum to the two-site calculation by sitewise algebra, then assemble the global factor.

why it matters in Recognition Science

Feeds DiracAlgebraContinuumBinding, which binds the freestanding Riemann shape sampledDynamicBracketSum to the genuine lattice bracket of $H_n$ after periodic wrap treatment, and lands the ledger terminal dirac_algebra_continuum_limit for 1-periodic $C^1$ data.

Without the n-site dynamic Hamiltonian and its exact self-bracket, the continuum smearing argument has nothing lattice-exact to pass to the limit. This is the discrete carrier for the dynamic structure-function slot demanded by ADM: inverse spatial metric varying with canonical data, not a frozen background weight. Closes the modeling gap flagged by the structure-function blocker and extends the R0–R1 two-site repair to the lattice size used in the continuum binding.

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)