Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket

show as:
view Lean formalization →

Defines the dynamic Hamiltonian density that substitutes a phase-space-dependent inverse metric into the background-weighted HamW form pointwise. Lattice ADM and Dirac-algebra workers cite it as the n=2 model of a structure bracket with genuine metric dependence. The module installs HamDyn, its equality to the naive substitution, decoy phase/lapse fixtures, and Frechet bookkeeping hooks used downstream.

claimDefine the dynamic Hamiltonian density by pointwise substitution of the phase-space-dependent inverse metric into the weighted density: $\mathrm{ham}(N,x) := \mathrm{HamW}(G(x),N,x)$, where $G(x)$ is the concrete dynamic inverse metric at phase-space point $x$. The principal object is the two-site dynamic structure bracket of this density against itself, with supporting decoy lapse/phase data and the Frechet derivative $D\mathrm{HamDyn}$.

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 as the phase-space point varies. Full ADM gravity needs the inverse spatial metric in that slot to depend on the canonical metric data.

This module is the lookalike model that performs the substitution: $\mathrm{ham},N,x := \mathrm{HamW}(\mathrm{concreteDynamicInverseMetric},x),N,x$. Sibling objects include the naive dynamic density, HamDyn and its equality to that naive form, decoy phase points and lapses (including the zero/one cases), $\mathbb{Z}/2\mathbb{Z}$ wraparound identities, and the Frechet derivative object used in bracket differentiation.

proof idea

Definition-and-identity module for the n=2 dynamic bracket, not a deep existence proof. It introduces the dynamic density as pointwise substitution of the concrete dynamic inverse metric into HamW, proves equality with the naive substitution form, and installs decoy phase/lapse fixtures plus ZMod arithmetic lemmas needed when differentiating the bracket. Frechet bookkeeping (derivative of HamDyn, metric-response correction, Kronecker collapse under periodic reindex) is prepared here for the two-site case; the bracket identity and its n-generalization live downstream.

why it matters in Recognition Science

Wave C2 infrastructure that replaces fixed background weights by ADM-style metric dependence in the Dirac algebra. Downstream, DynamicStructureBracketN generalizes HamDyn and the dynamic self-bracket from n=2 to arbitrary n with NeZero; DynamicStructureContinuumSmearing extends the banked fixed-background continuum reach so the structure profile is induced by a continuum field q via G(x)=1+(qx)^2; DiracAlgebraContinuum packages the sampled-lapse Wronskian rate-h residual with the R2 lattice RHS shape and R3 dynamic profile as the dynamic bracket-shape continuum limit. Gap5ConstraintResidualDAG and Gap5MomentumMagnitudeBridge name residuals for dynamic Dirac structure functions and HKT rigidity; DynamicStructureBracketAudit constrains the axiom surface of the R0+R1 theorems; HKTPointSplitTarget also imports the model.

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)