High-contrast homogenization: Provider.Quenched.UnitRangeStoppingScaleDatum

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The stopping scale in its weak-Orlicz shape

The endgame states its stopping-scale estimate as a weak-Orlicz bound on the μ-th power of the generation-n scale,

R_n^μ = O_{Ψ_fr}(C 3^(nμ)),

against the finite-range gauge, and then converts it into the shifted tail the bad-tail engine consumes by choosing an integer buffer b large enough to absorb the constant C (e.random.quenched.tail, read as the shifted tail of the quenched radius).

This file performs that conversion. The buffer exists for every positive C, and once it is chosen the shifted tail holds at the dimensional constant c_fr(d), with no reference to any source scale, source gauge or window: the stopping scale is an arbitrary family here, exactly as it is in the engine. The composition with the engine is recorded at the end, so the whole route runs without the source window.

The datum

The buffer

theorem HCPolySupport.HighContrast.Quenched.exists_shift_of_pos {mu C : ℝ} (hmu : 0 < mu) (hC : 0 < C) : ∃ (b : ℕ), C ≤ 3 ^ (mu * ↑b)

A buffer absorbing the constant of the weak-Orlicz bound exists.

The shifted tail

The composition into the engine