Research proof index

PDE-facing De Giorgi pre-iteration theorem on concentric balls. This now factors through the explicit cutoff-Sobolev bridge deGiorgi_cutoffSobolev_on_concentricBalls_of_ballPosPart instead of keeping the local Sobolev argument bundled into one monolithic proof.

Approximation-based version of the PDE-facing De Giorgi pre-iteration theorem. This is the approximation-driven counterpart of deGiorgi_preiter_on_concentricBalls_of_ballPosPart: instead of taking a pre-built witness for (u - θ)_+ or a generic positive-part closure axiom, it uses the outer-ball smooth approximation package for u - θ. The analytic pr...

Rewrite the one-step estimate on canonical radii and levels into the standard nonlinear recurrence.

The canonical De Giorgi recurrence tends to zero under the standard smallness threshold. This is the non-PDE closeout for the De Giorgi iteration.

General cutoff admissibility theorem, parameterized by a positive-part witness theorem. This packages the reusable cutoff argument while keeping the localization argument in memW01p_of_memW1p_of_tsupport_subset.

Concrete cutoff admissibility theorem using the Chapter 02 positive-part witness constructor and an explicit smooth-approximation package for u - k.