Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket

show as:
view Lean formalization →

Lattice model for a fully dynamical Dirac structure function: the Hamiltonian density that inserts a phase-space-dependent inverse metric into the background-weighted HamW density pointwise. Gravity workers closing the ADM algebra gap (Wave C2) cite HamDyn and its decoy fixtures as the n=2 base case. The module is definitional scaffolding plus elementary identities, not a continuum theorem.

claimDefine the dynamic Hamiltonian density by substituting the concrete phase-space-dependent inverse metric $G(x)$ into the background-weighted density: $\mathrm{ham}(N,x):=\mathrm{HamW}(G(x),N,x)$. The module packages this lookalike (and its naive form), decoy phase/lapse data, and the Fréchet bookkeeping object used in later bracket identities.

background

Upstream, the dynamic structure-function blocker records that bracket_HamW_HamW places a site-dependent weight in the Dirac structure-function slot and that weightedStructureSum_tendsto carries the smeared shape to the continuum, yet both keep that 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.

This module supplies the MODEL named in its header: the lookalike density obtained by pointwise substitution of a concrete dynamic inverse metric into HamW. Sibling objects include the naive dynamic density, the equality relating HamDyn to that naive form, decoy phase points and lapses (including the zero/one cases), ZMod 2 wraparound identities, and the Fréchet derivative bookkeeping object HamDynD used when differentiating through the metric dependence.

proof idea

Definition-and-identity module, not a deep existence proof. It introduces the dynamic density as pointwise substitution of the concrete dynamic inverse metric into HamW, records the equality to the naive form, and installs decoy phase/lapse fixtures plus elementary ZMod 2 arithmetic lemmas that later bracket calculations consume. Continuum smearing and general-$n$ bracket identities are left to importers.

why it matters in Recognition Science

Base lattice model for Wave C2 dynamic structure work. DynamicStructureBracketN generalizes HamDyn and the dynamic bracket from $n=2$ to arbitrary $n$ with the same Fréchet pattern. DynamicStructureContinuumSmearing extends fixed-background continuum reach so the structure profile is induced by a continuum field $q$ via $G(x)=1+(qx)^2$. DiracAlgebraContinuum lands the sampled-lapse dynamic bracket-shape continuum limit. Audit, Gap5 residual DAG, momentum-magnitude bridge, and HKT point-split modules import the same model. Closes the fixed-weight gap flagged by the structure-function blocker toward ADM-style metric dependence.

scope and limits

used by (7)

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