IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing
Continuum model of the dynamic inverse-metric structure function along the quadratic field profile G(x)=1+(q x)^2. Anyone tracking Wave C2 residual R3 in the Gap-5 constraint-algebra campaign cites this module. It defines the profile, proves continuity and sampling identities, and packages the typed residual that background-weighted smearing cannot hit the full dynamic family.
claimThe continuum shape of the concrete dynamic inverse metric along a field profile is the quadratic $G(x)=1+(q x)^2$. Continuum reach of any fixed background weight misses this dynamic family: no single fixed profile equals every dynamic profile at once. The module records that obstruction as the Gap-5 typed residual for dynamic continuum smearing.
background
Wave C2 of the QG Seven-Gaps campaign targets the Dirac constraint algebra with a dynamic structure function. Upstream, the background-weighted hypersurface bracket puts a fixed site-dependent weight $w$ in the stiffness slot and proves the exact lattice bracket; its continuum smearing (weightedStructureSum_tendsto) still keeps that weight frozen as the phase-space point varies.
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 the frozen-weight theorems do not cover this case. The two-site dynamic bracket (R0+R1) already shows that naively plugging a field-dependent $g$ into the frozen Hamiltonian density leaves an uncompensated $\partial g/\partial q$ term.
This module supplies the continuum model of that dynamic inverse metric: the concrete profile $G(x)=1+(q x)^2$, together with continuity, sampling equalities against the lattice inverse metric, and the reach statements that separate dynamic from background-weighted families.
proof idea
Definition-first module, not a single theorem. It introduces dynamicStructureProfile as $G(x)=1+(q x)^2$, proves it is continuous on the relevant domain, and identifies the concrete dynamic inverse metric with both this profile and its lattice samples.
Reach lemmas then compare continuum images: the dynamic weighted continuum reach is the set of profiles obtained by varying the field data; the background-weighted reach is shown to miss that family. A companion statement records that no single fixed profile can equal every dynamic profile simultaneously.
These facts are packaged as the typed residual TypedResidual_gap5_dynamic_continuum_smearing (and its inhabiting term), the R3 node in the Gap-5 residual DAG.
why it matters in Recognition Science
Closes Wave C2 residual R3 (dynamic structure continuum smearing) in the Gap-5 constraint-recovery DAG. Downstream, DiracAlgebraContinuum lands R4 by packaging this R3 dynamic structure profile with the R2 lattice RHS shape and the sampled-lapse Wronskian rate-$h$ residual into dynamic_bracket_shape_continuum_limit.
Gap5ConstraintResidualDAG names the residual in the typed DAG for dynamic Dirac structure functions and HKT rigidity. The companion audit module requires headline theorems here to print within [propext, Classical.choice, Quot.sound].
In the broader RS gravity stack this is the continuum witness that background weights (Pillar 1, bet C10) are strictly weaker than a field-dependent inverse metric in the Dirac structure slot, so the frozen-weight continuum limit cannot discharge full ADM constraint recovery.
scope and limits
- Does not prove the full dynamic Dirac bracket continuum limit (that is R4 in DiracAlgebraContinuum).
- Does not replace the lattice dynamic bracket; it only models the continuum profile shape G(x)=1+(q x)^2.
- Does not claim every admissible inverse-metric profile is quadratic; the quadratic is the concrete model used here.
- Does not discharge Gap-5 constraint recovery; it only records the R3 typed residual.
- Does not treat time-dependent or fully covariant smearing kernels beyond the stated continuum reach.
used by (3)
depends on (3)
declarations in this module (11)
-
def
dynamicStructureProfile -
theorem
continuousOn_dynamicStructureProfile -
structure
function -
theorem
concreteDynamicInverseMetric_eq_dynamicStructureProfile -
theorem
concreteDynamicInverseMetric_eq_sample -
def
DynamicWeightedContinuumReach -
theorem
dynamic_weighted_continuum_reach -
theorem
background_weighted_reach_misses_dynamic_family -
theorem
no_fixed_profile_equals_all_dynamic_profiles -
def
TypedResidual_gap5_dynamic_continuum_smearing -
theorem
typedResidual_gap5_dynamic_continuum_smearing