High-contrast homogenization: Provider.Quenched.SmallContrastSourceScaleMinimal

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

The source scale, chosen minimally

The one factor that was not already a named lemma.

exists_source_scale_minimal produces some sK with growthBar K ≤ 3 ^ sK above a prescribed floor, which is all the account needs. hentry needs more: it must know 3 ^ sK is not much larger than growthBar K, because 3 ^ sK enters the burn-in N1 = sK + 1 + gap and hentry must convert 3 ^ N1 into a law-free exponent on the base. An unconstrained sK gives nothing.

The fix is the same ⌈log₃ ·⌉ device as three_pow_ceil_logb_le, in its ℤ-ceiling form: taking sK := max floor ⌈log₃ (growthBar K)⌉ gives both bounds at once, and the floor costs only the factor 3 ^ floor, which is dimension-only because the endpoint's floor is kZero d.

theorem HCPolySupport.HighContrast.Quenched.exists_source_scale_minimal (K : ℝ) {floor : ℤ} (hfloor : 0 ≤ floor) : ∃ (sK : ℤ), floor ≤ sK ∧ growthBar K ≤ 3 ^ sK ∧ 3 ^ sK ≤ 3 ^ floor * (3 * growthBar K)

The source scale, minimally. Above any nonnegative floor there is a source scale that dominates the growth bar and is dominated by it, up to the floor's own factor and a single power of three.