High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedSourceCap

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

The normalized corrected source cap

The released bad-source constant has polynomial degree eight in the growth bar. Squaring it gives the degree-sixteen payment recorded in ct2; this file packages that calculation in the exact normalized form consumed by the initial cadence level schedule.

theorem HCPolySupport.HighContrast.Quenched.badSourceConstant_le_three_mul_growthBar_pow_eight (K : ℝ) : badSourceConstant K ≤ 3 * growthBar K ^ 8

The released bad-source scalar grows at most like the eighth power of the source growth bar.

theorem HCPolySupport.HighContrast.Quenched.badSourceLegConstantAtLevel_le_corrected_source_scale {L K R base cW : ℝ} (hR : 1 ≤ R) (hbase : 3 ≤ base) (hcW : 0 ≤ cW) (hgrowth : growthBar K ≤ 2 * base.rpow cW) : badSourceLegConstantAtLevel L K R ≤ √2 * √(L + 1) * R * 6 * 256 * base.rpow (8 * cW)

The released bad-source constant at the endpoint is absorbed by a fixed coefficient, that module, and base^(8*cW).

theorem HCPolySupport.HighContrast.Quenched.corrected_normalized_source_cap {d ns : ℕ} {A delta beta base cW Cpre M L rho K R CX S2 ct2 : ℝ} (hA : 1 ≤ A) (hdelta : 0 < delta) (hbeta : 0 < beta) (hbase : 3 ≤ base) (hcW : 0 ≤ cW) (hCpre : 1 ≤ Cpre) (hM : 0 ≤ M) (hrho : rho < 1) (hR : 1 ≤ R) (hgrowth : growthBar K ≤ 2 * base.rpow cW) (hCX : CX = 1 + 6 * weakCoefficient d Cpre * (16 * M / (1 - rho) * (√2 * √(L + 1) * R * 6)) ^ 2 * 65536) (hS2 : S2 = 1 + 6 * weakCoefficient d Cpre * weakSourceGroupSummed M L rho 0 0 (badSourceLegConstantAtLevel L K R) ^ 2 * Real.rpow 3 (beta * ↑ns)) (hct2 : ct2 = 16 * cW / beta) : S2 / (A * delta ^ 2) ≤ CX / delta ^ 2 * ((3 ^ ns).rpow beta * base.rpow (beta * ct2))

The fixed source coefficient has the normalized cap required by the initial corrected cadence level schedule.