module module moderate

`IndisputableMonolith.Gravity.D2DampedScheduleClosure`

Damped-schedule closure for the D2 Regge-to-Einstein-Hilbert reduction: local radius and constant, residual coefficients, and probe-sum nonnegativity that discharge the uniform-residual analytic input. Downstream D2 quadrature and Track 1.B modules import it. Argument is elementary positivity, scaling, and bound lemmas on the graph Dirichlet energy.

claimThe module packages damped-schedule data for D2 classical recovery: a positive local radius $R$, a nonnegative local constant $C$, residual-coefficient bounds, nonnegative probe norm and cube sums, and quadratic homogeneity $E(\lambda u)=\lambda^2 E(u)$ of the canonical graph-Dirichlet energy under scalar rescaling of the vertex potential.

background

D2 is the classical-recovery track that takes a discrete Regge/J-cost witness toward continuum Einstein-Hilbert structure. The upstream scoping audit (D2ScopingAudit) pins what is proved versus what remains open on that path, and names the classical-recovery witness consumed by the master theorem.

This module supplies the damped-schedule layer of that witness. Sibling objects introduce a local radius (strictly positive), a local constant (nonnegative), a residual coefficient with nonnegativity, and probe norm/cube sums used to control residuals. The DOC_COMMENT on the energy scaling lemma records that the canonical graph-Dirichlet energy is quadratically homogeneous under scalar rescaling of the vertex potential.

Notation is graph-analytic rather than continuum: potentials live on vertices; energy is a discrete Dirichlet form; the schedule damps residuals uniformly so later quadrature and stencil arguments can close without ad-hoc cutoffs.

proof idea

Not a single theorem: a small library of definitions and elementary lemmas. Local radius and constant are introduced, then positivity/nonnegativity (localRadius_pos, localConstant_nonneg) and a local bound. Probe norm and cube sums are defined and shown nonnegative. The residual coefficient is defined and proved nonnegative. The energy identity is the scaling lemma: Dirichlet energy pulls out $\lambda^2$ under $u\mapsto\lambda u$. No deep analysis; algebraic homogeneity plus nonnegativity of the schedule data.

why it matters in Recognition Science

Closes the uniform-residual input of the D2 reduction. Downstream D2QuadratureInstances states explicitly that damped-schedule closure discharged that input, leaving cross-cardinality quadrature as the remaining analytic piece (flat sector closes; curved sector reduces). Track1BCorrectedQuadratic sits on the Track 1.B route to the local Regge/J-cost correspondence and imports this schedule layer as part of the axis-stencil setup. In the broader RS gravity stack this is infrastructure, not a forcing-chain landmark (T0-T8), but it is required before continuum-facing D2 claims can be stated without residual gaps.

scope and limits

Does not prove continuum Einstein-Hilbert recovery or the full D2 master theorem.
Does not discharge cross-cardinality quadrature (that is D2QuadratureInstances).
Does not assert the corrected Track 1.B gate; that gate remains named open downstream.
Does not introduce new RS axioms; schedule data are definitions plus elementary bounds.
Does not treat curved-sector geometry beyond residual schedule inputs.

used by (2)

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

IndisputableMonolith.Gravity.D2QuadratureInstances module_import
IndisputableMonolith.Gravity.Track1BCorrectedQuadratic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.D2ScopingAudit module_import

declarations in this module (31)

theorem canonicalDirichletEnergy_smul L75
def localRadius L105
def localConstant L114
theorem localRadius_pos L122
theorem localConstant_nonneg L131
theorem local_bound L142
def probeNormSum L172
def probeCubeSum L182
theorem probeNormSum_nonneg L191
theorem probeCubeSum_nonneg L200
def residualCoefficient L211
theorem residualCoefficient_nonneg L219
def dampingFactor L230
theorem one_add_probeNormSum_pos L235
theorem one_add_residualCoefficient_pos L242
theorem dampingFactor_pos L249
theorem dampingFactor_le_radius_quotient L258
theorem dampingFactor_mul_residualCoefficient_le_one L264
def dampedSlice L284
theorem dampedSlice_quadratureIntegral L316
theorem normalized_regge_sub_limit_abs_le L330
theorem dampedSlice_residual_abs_le L434
def dampedFamily L551
theorem dampedFamily_uniformResidual L565
theorem dampedFamily_quadrature_target L588
def dampedProductFilterData L608
theorem dampedFamily_fullReggeProduct_tendsto_continuum L632
theorem dampedProductFilterData_satisfies_master_target L652
theorem d2_residual_vanishing_target_damped L674
theorem d2_reduction_to_quadrature_only L689
theorem d2_damped_schedule_closure_one_statement L709