Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastEchoWitness

High-contrast homogenization: Provider.Quenched.SmallContrastEchoWitness #

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

The echo witness: the construction recursion admits a staircase solution #

gate branch (c). The two-component scheduler's below-range echo re-excites, and the certificate is stronger than an envelope-class kill: the construction's hypothesis set — the recursion at the preserved-lag anchor shiftedBaseIndex ns available from ns, the a-priori floor, the origin initial datum (the stated condition), antitonicity, and a source that still exceeds the floor on the pre-base block — admits an explicit solution, the echo witness, whose value on the j-th octave of the inverse anchor orbit is the tower echoTower (j+1) = A^(2^(j+1)-1)·δ₀^(2^(j+1)).

The octaves stretch geometrically (echoBoundary (j+1) − ns is at least (4/3)^(j+1) times the burn-in m₀+1−ns), so at the fixed octave j₀ with (D+1)·3^(j₀) ≤ 4^(j₀) the witness value is a law-free positive constant while any target M·3^(−mu·(n−T₀)) with T₀ ≤ ns + D·(m₀+1−ns) is smaller once the burn-in is large, with the smallness threshold made explicit by the logarithmic echo gap. Hence NO method consuming only the construction hypotheses — the late-start/original- anchor two-component scheduler included — can conclude a law-free rate at a linear threshold. The first echo damps in magnitude (δ₀ → A·δ₀²), exactly as the scheduler's design intuited; the tower records that the demand at the octaves outruns the damping against any geometric target.

The tower of levels: each octave squares the previous level.

Equations
Instances For

    Boundary arithmetic #

    Index computation #

    Tower facts #

    theorem HCPolySupport.HighContrast.Quenched.echoTower_pos {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (k : ℕ) :
    0 < echoTower A d0 k
    theorem HCPolySupport.HighContrast.Quenched.echoTower_le_floor {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hAd : A * d0 ≤ 1) (k : ℕ) :
    echoTower A d0 k ≤ d0

    The witness satisfies every construction hypothesis #

    The kill #