Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing

show as:
view Lean formalization →

Models the continuum shape of the dynamic inverse metric along the field profile $G(x)=1+(qx)^2$. Proves continuity of that profile, equates it to the concrete dynamic sample, and shows fixed background weights miss the full dynamic family. Supplies the typed Gap-5 residual for dynamic continuum smearing. Argument is definitional profile plus reach/miss lemmas, not a full Dirac-algebra closure.

claimAlong a field profile the continuum shape of the concrete dynamic inverse metric is $G(x)=1+(q x)^2$. That profile is continuous; sampling it recovers the discrete dynamic inverse metric. No single fixed background weight reproduces every member of the dynamic family under continuum smearing, so the background-weighted reach misses the dynamic family.

background

Part of the QG Seven-Gaps campaign (Pillar 1, constraint algebra). Upstream, the background-weighted hypersurface bracket puts a fixed site weight $w$ in the stiffness slot and proves the exact lattice bracket; its continuum smearing keeps that weight frozen as the phase-space point moves. Full ADM gravity instead needs the inverse spatial metric in the structure-function slot to vary with the canonical metric data.

The dynamic structure-function blocker records that gap: bracket_HamW_HamW and the weighted continuum limit both freeze the weight. The two-site dynamic bracket module closes the first decoy residual (naive substitution of $g x$ into the frozen Hamiltonian density leaves an uncompensated $\partial g/\partial q$).

This module supplies the continuum model of that missing dynamic shape: the profile $G(x)=1+(q x)^2$ as the continuum avatar of the concrete dynamic inverse metric.

proof idea

Definitional core: introduce the continuum profile $G(x)=1+(q x)^2$ and prove it is continuous on the relevant domain. Equate the concrete dynamic inverse metric to this profile and to its discrete sample.

Reach layer: package a dynamic weighted continuum-reach predicate, then show the background-weighted reach misses the dynamic family and that no single fixed profile equals all dynamic profiles. Close by naming the typed Gap-5 residual for dynamic continuum smearing from those miss lemmas. No full Dirac-algebra identity is proved here; the module stops at shape, continuity, and residual typing.

why it matters in Recognition Science

Fills Wave C2 residual R3 (dynamic structure continuum smearing) in the Gap-5 constraint-recovery DAG. Downstream, DiracAlgebraContinuum packages this R3 profile with the R2 lattice RHS shape and the sampled-lapse Wronskian rate-$h$ residual into dynamic_bracket_shape_continuum_limit. The companion audit module demands headline theorems print inside [propext, Classical.choice, Quot.sound].

In the broader RS gravity stack this is the continuum witness that frozen background weights cannot stand in for a metric-dependent structure function, the obstruction that separates the weighted hypersurface bracket from full ADM constraint algebra. It does not yet close HKT rigidity or the full dynamic Dirac algebra; those remain named open residuals in the same DAG.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)