High-contrast homogenization: Provider.Quenched.SmallContrastInitialLedgerCap #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.Quenched.corrected_cadence_initial_ledger_power_cap
{ns cA : ℕ}
{A alpha S0 S2 d0 beta base Cns cns CX Ct1 Ct2u C7 ct2 : ℝ}
(hbase : 3 ≤ base)
(hA : 1 ≤ A)
(hd0 : 0 < d0)
(hd01 : d0 ≤ 1)
(hbeta : 0 < beta)
(hCns : 1 ≤ Cns)
(hct2 : 0 ≤ ct2)
(hCX : 1 ≤ CX)
(hS2 : 1 ≤ S2)
(hns : 3 ^ ns ≤ Cns * base.rpow cns)
(hsource : S2 / (A * d0 ^ 2) ≤ CX / d0 ^ 2 * ((3 ^ ns).rpow beta * base.rpow (beta * ct2)))
(hCt1 : Ct1 = 3 / d0 ^ 2)
(hCt2u : Ct2u = (CX / d0 ^ 2).rpow beta⁻¹)
(hC7 : C7 = Ct1 * 3 * Ct2u)
:
The two one-time source payments in the corrected cadence level schedule are absorbed by two copies of the generation cap and the fixed source cap.