module module moderate

`IndisputableMonolith.Gravity.D2DampedScheduleClosure`

Closes the damped-schedule residual bound used by the D2 Regge-to-Einstein-Hilbert reduction on the recognition graph. It packages quadratic homogeneity of the canonical graph-Dirichlet energy, local radius/constant controls, and nonnegative residual coefficients built from probe norm and cube sums. Downstream quadrature and Track 1.B modules import it to discharge the uniform-residual hypothesis. Arguments are elementary scaling and positivity identities on finite graphs.

claimOn a finite recognition graph, the canonical Dirichlet energy $E$ is quadratically homogeneous: $E(c u)=c^{2} E(u)$ under scalar rescaling of the vertex potential. Local radius and local constant quantities are nonnegative (radius strictly positive) and bound a residual coefficient assembled from nonnegative probe norm and cube sums, yielding a damped schedule with controlled uniform residual for the D2 reduction.

background

D2 is the classical-recovery track that takes discrete Regge-type data on the recognition graph toward an Einstein-Hilbert continuum limit. The upstream scoping audit (D2ScopingAudit) fixes what is proved versus named-open for that witness: theorem status for claimed content, with the open frontier stated rather than asserted.

This module works inside that audit. The canonical graph-Dirichlet energy is the discrete quadratic form on vertex potentials that plays the role of a kinetic/action density. A damped schedule is a residual-control scheme: local geometric scales (radius, constant) and probe sums (norm and cube) assemble a residual coefficient whose nonnegativity and size bound the error term fed to continuum recovery.

Sibling content therefore splits into scaling of the energy, positivity of local and probe quantities, and the residual coefficient itself. Units and continuum constants from the broader RS stack are not re-derived here; the module is pure discrete analysis on the graph.

proof idea

Definition-and-lemma module, not a single master theorem. It introduces local radius and local constant, proves radius positivity and constant nonnegativity, then a local bound relating them. Probe norm and cube sums are defined and shown nonnegative. The residual coefficient is assembled from those pieces and proved nonnegative. Separately, a short scaling identity records quadratic homogeneity of the canonical Dirichlet energy under scalar multiplication of the vertex potential. No heavy analysis: algebraic identities and nonnegativity on finite sums.

why it matters in Recognition Science

Parent consumers are explicit. D2QuadratureInstances states that damped-schedule closure discharged the uniform-residual input of the D2 reduction, leaving cross-cardinality quadrature as the remaining analytic obligation; the flat sector then closes and the curved sector reduces. Track1BCorrectedQuadratic factors the Track 1.B local Regge/J-cost correspondence through this residual control on the axis-stencil side.

In the gravity domain this is infrastructure, not a new continuum theorem: it turns the residual hypothesis of the D2 witness into a named, proved package so later modules can cite a closed schedule rather than re-prove positivity and scaling. It does not itself finish Einstein-Hilbert recovery or close the corrected Track 1.B gate (still named open downstream).

scope and limits

Does not prove continuum Einstein-Hilbert recovery or full D2 master theorem.
Does not close cross-cardinality quadrature (handled downstream).
Does not assert the corrected Track 1.B gate; that remains named open.
Does not introduce new RS constants, mass ladders, or forcing-chain steps T0–T8.
Does not treat curved-sector geometry beyond residual coefficient 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