High-contrast homogenization: Provider.Quenched.SmallContrastEntryEstimates

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

The bootstrap entry is polynomial

The hentry clause of the endpoint asks for the entry generation to be bounded by a fixed power of the law parameter Π = 2 + aspectRatio 𝐄 · K. With

N₁ = entryGeneration (s_K + 1 + gap) (entryDelay c_w C_src δ) n₀

the assembly is the entry-generation power bound; the per-constant core is below.

The core is that every delay in the chain is a ceiling of a base-3 logarithm, and 3^{⌈log₃ x⌉₊} ≤ 3·max 1 x: a delay defined that way is automatically polynomial in whatever bounds x. This applies unchanged to entryDelay c_w C_src δ = ⌈log₃(3 c_w C_src / δ)⌉₊ and, in the bootstrap module's form, to gap. The third estimate, 3^{n₀} ≤ Π^{C_delay}, is the account's own first clause and needs nothing.

theorem HCPolySupport.HighContrast.Quenched.three_pow_ceil_logb_le {x : ℝ} (hx : 0 < x) : 3 ^ ⌈Real.logb 3 x⌉₊ ≤ 3 * max 1 x

The delay core. A delay defined as a ceiling of a base-3 logarithm is below 3·max 1 x after exponentiation.