High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedSourcePricing

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

The corrected three-channel pricing of the entry-slot source

The corrected source model (the strengthened free-threshold estimate) at the design carriers: the entry-slot source 3·wC·(weakSourceGroupSummed …)² splits additively into its lag part (the two variance legs, decaying in the window depth n−m with a coefficient carrying only the supply value) and its absolute part (the bad-event leg, decaying in the generation past the threshold), each priced by the proved leg lemmas at its own rate — no common-rate coupling. The result is exactly the three-channel model of hcore_body_of_corrected_family: bA = b0 = 1 and b2 = 2β₂, with the threshold shift paid once in the third coefficient.

theorem HCPolySupport.HighContrast.Quenched.corrected_source_pricing (d : ℕ) (hd : 2 ≤ d) {Cpre Mabs L Csub Msc delta conv K R : ℝ} (hCpre : 0 ≤ Cpre) (hM0 : 0 ≤ Mabs) (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (hconv : 0 ≤ conv) (hR : 1 ≤ R) {g : ℝ} (hg1 : g < 1) {beta2 : ℝ} (hb2A : beta2 ≤ contrastAlpha g) {ns n m : ℕ} (hm : ns ≤ m) (hmn : m ≤ n) {Delta : ℤ} (hD0 : 0 ≤ Delta) (hDrate : beta2 * ↑(n - ns) ≤ 1 / 2 * ↑Delta) : 3 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) (slotVsumSharp d Csub Msc delta (n - m)) (conv * slotSourceSeq d Csub Msc delta (n - m) 0) (√2 * √(L + 1) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K Delta) (R / 2) R + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(n - ns)) * √(L + 1)) ^ 2 ≤ 1 * 3 ^ (-(1 * ↑m)) + (1 + 6 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) (vsumSourceConstant d Csub Msc delta) (conv * vsumSourceConstant d Csub Msc delta) 0 ^ 2) * 3 ^ (-(1 * ↑(n - m))) + (1 + 6 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) 0 0 (badSourceLegConstantAtLevel L K R) ^ 2 * 3 ^ (2 * beta2 * ↑ns)) * 3 ^ (-(2 * beta2 * ↑n))

The corrected three-channel pricing of the entry-slot source.

theorem HCPolySupport.HighContrast.Quenched.corrected_source_pricing_min (d : ℕ) (hd : 2 ≤ d) {Cpre Mabs L Csub Msc delta conv K R : ℝ} (hCpre : 0 ≤ Cpre) (hM0 : 0 ≤ Mabs) (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (hconv : 0 ≤ conv) (hR : 1 ≤ R) {g : ℝ} (hg1 : g < 1) {beta2 : ℝ} (hb2A : beta2 ≤ contrastAlpha g) {ns n m : ℕ} (hm : ns ≤ m) (hmn : m ≤ n) {Delta : ℤ} (hD0 : 0 ≤ Delta) (hDrate : beta2 * ↑(n - ns) ≤ 1 / 2 * ↑Delta) : 3 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) (slotVsumSharp d Csub Msc delta (n - min n m)) (conv * slotSourceSeq d Csub Msc delta (n - min n m) 0) (√2 * √(L + 1) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K Delta) (R / 2) R + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(n - ns)) * √(L + 1)) ^ 2 ≤ 1 * 3 ^ (-(1 * ↑m)) + (1 + 6 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) (vsumSourceConstant d Csub Msc delta) (conv * vsumSourceConstant d Csub Msc delta) 0 ^ 2) * 3 ^ (-(1 * ↑(n - m))) + (1 + 6 * weakCoefficient d Cpre * weakSourceGroupSummed Mabs L (contrastRho g) 0 0 (badSourceLegConstantAtLevel L K R) ^ 2 * 3 ^ (2 * beta2 * ↑ns)) * 3 ^ (-(2 * beta2 * ↑n))

The corrected source pricing with the entry-slot depth written in the min-normalized form consumed by the corrected cadence design.