High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.GenerationSelection

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

the large-scale C¹ slope approximation clause (b2), third step: the generation selection, log-free

What remains for ExactRootGaugeTerminal is to match the terminal's continuous radii r ∈ Icc rStart R to the cube row's generations q ∈ Finset.Icc n m, with Quenched.triadicCeilingIndex x ≤ n and n + 2 ≤ m.

This is bookkeeping, but carrying it out uncovers one structural fact worth recording, and it is not the one the rounded template suggests:

• the case split is on r against R / (108 √d), not on R against rStart. Above that threshold the canonical outer cube of r overshoots the inner cube of R — 3 ^ q(r) is only < 12 r, while 3 ^ m is only > R / (3 √d) — so the cube row does not apply there, at any R. That band is exactly what the near-terminal branch must cover, and r / R > 1 / (108 √d) is what makes that branch law-free;
• the row's n + 2 ≤ m is then automatic on the far branch, because 3 ^ m ≥ 36 · rStart > 3 ^ (n + 1).

Everything below is comparison of triadic powers: no logarithm monotonicity, no measure theory, and no estimate. outerTriadicGeneration is used only through its two scale bounds.

Comparing triadic powers

theorem HCPolySupport.HighContrast.CorrectorComposition.three_zpow_le_of_le {m n : ℤ} (h : m ≤ n) : 3 ^ m ≤ 3 ^ n

theorem HCPolySupport.HighContrast.CorrectorComposition.lt_of_three_zpow_lt {m n : ℤ} (h : 3 ^ m < 3 ^ n) : m < n

theorem HCPolySupport.HighContrast.CorrectorComposition.three_zpow_succ (m : ℤ) : 3 ^ (m + 1) = 3 * 3 ^ m

The inner generation: the largest triadic scale below R

noncomputable def HCPolySupport.HighContrast.CorrectorComposition.innerTriadicGeneration (R : ℝ) (_hR : 0 < R) : ℤ

The largest triadic generation whose scale does not exceed R.

Equations

• HCPolySupport.HighContrast.CorrectorComposition.innerTriadicGeneration R _hR = ⌊Real.logb 3 R⌋

theorem HCPolySupport.HighContrast.CorrectorComposition.innerTriadicGeneration_scale_le {R : ℝ} (hR : 0 < R) : 3 ^ innerTriadicGeneration R hR ≤ R

theorem HCPolySupport.HighContrast.CorrectorComposition.lt_three_mul_innerTriadicGeneration_scale {R : ℝ} (hR : 0 < R) : R < 3 * 3 ^ innerTriadicGeneration R hR

The far branch: the outer generation of r lands in Icc n m

theorem HCPolySupport.HighContrast.CorrectorComposition.outerTriadicGeneration_le_of_twelve_mul_le {r : ℝ} (hr : 0 < r) {m : ℤ} (h : 12 * r ≤ 3 ^ m) : outerTriadicGeneration (2 * (2 * r)) ⋯ ≤ m

The outer generation is bounded by a given inner one. If 12 r ≤ 3 ^ m then the canonical cube enclosing the ball of radius 2 r sits at a generation at most m.

theorem HCPolySupport.HighContrast.CorrectorComposition.outerTriadicGeneration_le_outerTriadicGeneration {rStart r : ℝ} (hrStart : 0 < rStart) (hr : rStart ≤ r) : outerTriadicGeneration (2 * (2 * rStart)) ⋯ ≤ outerTriadicGeneration (2 * (2 * r)) ⋯

The outer generation is monotone in the radius, log-free. The proof compares scales: 3 ^ n < 12 · rStart ≤ 12 · r = 3 · (4 r) ≤ 3 · 3 ^ q.

theorem HCPolySupport.HighContrast.CorrectorComposition.outerTriadicGeneration_add_two_le_of_thirtysix_mul_le {rStart : ℝ} (hrStart : 0 < rStart) {m : ℤ} (h : 36 * rStart ≤ 3 ^ m) : outerTriadicGeneration (2 * (2 * rStart)) ⋯ + 2 ≤ m

The row's gap n + 2 ≤ m is automatic on the far branch. If 36 · rStart ≤ 3 ^ m then the canonical outer generation of rStart is at least two below m.

The threshold, and the two bounds the far branch needs

theorem HCPolySupport.HighContrast.CorrectorComposition.farBranch_bounds {d : ℕ} [NeZero d] {rStart r R : ℝ} {m : ℤ} (hrStart : 0 < rStart) (hr : rStart ≤ r) (hmR : R ≤ 3 ^ m * (3 * √↑d)) (hthr : 108 * (√↑d * r) ≤ R) (hstart : 108 * (√↑d * rStart) ≤ R) : outerTriadicGeneration (2 * (2 * rStart)) ⋯ ≤ outerTriadicGeneration (2 * (2 * r)) ⋯ ∧ outerTriadicGeneration (2 * (2 * r)) ⋯ ≤ m ∧ outerTriadicGeneration (2 * (2 * rStart)) ⋯ + 2 ≤ m

The far/near threshold, discharged. With m an inner generation for R in the sense R ≤ 3 ^ m * (3 √d), every radius below R / (108 √d) has its canonical outer cube at a generation in Icc n m, and the gap n + 2 ≤ m holds as soon as rStart is below that threshold too.