dampingFactor
plain-language theorem explainer
Per-slice damping factor for the D2 damped schedule: the minimum of a local-radius quotient and a residual-coefficient reciprocal. It keeps every scaled probe inside the Track 1.B correspondence ball and forces the per-slice residual coefficient below one. Downstream residual bounds and the damped-slice constructor cite it. Pure definition as an explicit min of two real expressions from the slice witnesses.
Claim. For a cardinality slice $S$, the damping factor is $d_S = \min\bigl(r_S/(1+\sum_\tau\|\xi_\tau\|),\; 1/(1+K_S)\bigr)$, where $r_S$ is the local-correspondence radius of $S$, $\sum_\tau\|\xi_\tau\|$ is the sum of probe norms over the slice tetrahedra, and $K_S$ is the residual coefficient (limiting cell-volume weight times the local cubic constant times the cubed probe-norm sum).
background
The module closes D2 open item 2 of the scoping audit: the uniform residual-vanishing target that the product-filter datum previously carried as a supplied analytic field. Every cardinality slice already carries Track 1.B local correspondence, the cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$. That local bound alone forces the two-scale residual to vanish once the within-slice refinement schedule is damped per slice.
The three ingredients of the damping factor are slice-local. The local radius $r_S$ is the correspondence radius carried by the slice. The probe-norm sum aggregates $|\xi_\tau|$ over the slice tetrahedra. The residual coefficient is $K_S=(|V_S|/6)\cdot C_S\cdot\sum_\tau|\xi_\tau|^3$, the limiting cell-volume weight times the cubic constant times the cubed-norm sum. The damped family keeps the same cardinalities, probes, and limiting cell volumes (hence the same quadrature proxies) but replaces within-slice spacing by $\sigma(t)\cdot d_S$.
proof idea
Definition, not a proof. The body is the pointwise minimum of the two explicit real expressions localRadius S / (1 + probeNormSum S) and 1 / (1 + residualCoefficient S). No lemmas are applied; positivity and the two one-sided inequalities are proved separately as thin wrappers around lt_min and min_le_left/min_le_right.
why it matters
This is the scalar that turns the local cubic bound into a uniform residual envelope without any supplied analytic field. It is the damping weight inside dampedSlice, which freezes the cell-volume schedule at its limit and multiplies the universal schedule $\sigma$ by $d_S$. The residual theorem dampedSlice_residual_abs_le then bounds the full nonlinear Regge aggregate minus the quadrature proxy by $|\sigma t|$, uniformly in the slice, whenever $\sigma t\ne 0$ and $|\sigma t|\le 1$.
Sibling inequalities (dampingFactor_pos, dampingFactor_le_radius_quotient, dampingFactor_mul_residualCoefficient_le_one) package the two design constraints: probes stay inside the correspondence ball, and $d_S K_S\le 1$. Together they discharge D2 residual vanishing for the damped family, so full Regge-to-continuum product-filter convergence needs only the quadrature limit. That is the module's stated closure of open item 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.