High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedGenerationCap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The corrected generation cap #
This file packages the three finite generation delays used by the endpoint. The burn-in, deep-cap, and reverse-transfer delays are combined at the printed base, with the coefficient and exponent table used by the corrected cadence.
theorem
HCPolySupport.HighContrast.Quenched.max_reverseAdapterFactor_le_corrected_generation_scale
{d : ℕ}
{g K base cW Cd Cdz C5 CB CF cF : ℝ}
{E : BlockMat d}
{mAl : Mat d}
{G D : ℕ}
(hg : g ∈ Set.Ico 0 1)
(hK : 1 ≤ K)
(hbase : 3 ≤ base)
(hcW : 0 ≤ cW)
(hCd : 1 ≤ Cd)
(hzeta : 1 ≤ zetaG g)
(hecc : witnessEccentricity mAl ≤ base)
(hkappa1 : 1 ≤ kappaRef E)
(hkappa : kappaRef E ≤ 9 / 8)
(hgrowth : growthBar K ≤ 2 * base.rpow cW)
(hGD : G + 1 = D)
(hdepth : 3 ^ D ≤ C5 * base)
(hCB : 0 ≤ CB)
(hCdz : Cdz = Cd * zetaG g)
(hCF : CF = max 1 (CB * (45 / 2) * Cdz * C5))
(hcF : cF = 4 + 3 * cW)
:
The reverse-adapter factor is absorbed by the transfer coefficient and
the exponent 4 + 3*cW appearing in the corrected generation table.
theorem
HCPolySupport.HighContrast.Quenched.corrected_generation_power_cap
(d : ℕ)
(hd : 2 ≤ d)
{H D G ns nB nE nF : ℕ}
{g K Pi base cW rate Cd Cdz C5 CE CB CF cF Cns cns : ℝ}
{E : BlockMat d}
{mAl : Mat d}
(hg : g ∈ Set.Ico 0 1)
(hK : 1 ≤ K)
(hPi : 1 ≤ Pi)
(hPiBase : Pi ≤ base)
(hbase : 3 ≤ base)
(hcW : 0 ≤ cW)
(hrate : 0 < rate)
(hCd : 1 ≤ Cd)
(hzeta : 1 ≤ zetaG g)
(hecc : witnessEccentricity mAl ≤ base)
(hkappa1 : 1 ≤ kappaRef E)
(hkappa : kappaRef E ≤ 9 / 8)
(hgrowth : growthBar K ≤ 2 * base.rpow cW)
(hD : D = burnSplitDepth d Cd g Pi)
(hGD : G + 1 = D)
(hCB : 0 ≤ CB)
(hCdz : Cdz = Cd * zetaG g)
(hC5 : C5 = 3 * (100 / 99 * Cd * zetaG g * √↑d))
(hCE : CE = 8100 * 3 ^ (3 * H) * C5 ^ 4)
(hCF : CF = max 1 (CB * (45 / 2) * Cdz * C5))
(hcF : cF = 4 + 3 * cW)
(hCns : Cns = 3 ^ (H + 1) * 624 * CE * (3 * CF.rpow rate⁻¹) * 3)
(hcns : cns = 4 * cW + 4 + cF / rate)
(hnsSum : ns ≤ H + 1 + nB + nE + nF)
(hB : 3 ^ nB ≤ 3 * (13 * growthBar K ^ 4))
(hE : 3 ^ nE ≤ 8100 * 3 ^ (3 * H) * 3 ^ (4 * D))
(hF : 3 ^ nF ≤ 3 * (max 1 (CB * reverseAdapterFactor Cd g K E mAl G)).rpow rate⁻¹)
:
The maximum of the three finite delay components obeys the generation coefficient and exponent table used by the initial cadence level schedule.