High-contrast homogenization: Provider.Quenched.SmallContrastSharpLine

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

The per-generation recursion at the sharp constant

The theorem per_generation_hrec_at_recursionAlpha_sharp_at_jb_src specializes the drop-history recursion to the ratio 3 ^ (-recursionAlpha g). Its hA1 hypothesis contains geometric factor

a * (((3 ^ (-recursionAlpha g)) ^ H)⁻¹ * (1 - 3 ^ (-recursionAlpha g))⁻¹) + 3 * cw * cdrop ≤ A .

The specialization built from hrec_final_sharp_at_jb_src instead uses

a * ((3 ^ (-recursionAlpha g)) ^ H)⁻¹ + 3 * cw * cdrop ≤ A ,

which deletes (1 - r)⁻¹. The constant fusionRecursionConstantIsotropySharp supplies this sharper hypothesis.

theorem HCPolySupport.HighContrast.Quenched.hA1_of_fusionRecursionConstantIsotropySharp (d : ℕ) (Cpre eta : ℝ) (H : ℕ) (M L g cRow kap cD delta cVsum cVm : ℝ) : dropCoefficient d Cpre eta * ((3 ^ (-recursionAlpha g)) ^ H)⁻¹ + 3 * weakCoefficient d Cpre * weakDropConstant M L (contrastAlpha g) cD delta ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm

The drop branch of the sharp constant satisfies the sharp hA1 hypothesis by le_max.

theorem HCPolySupport.HighContrast.Quenched.hA2_of_fusionRecursionConstantIsotropySharp (d : ℕ) (Cpre eta : ℝ) (H : ℕ) (M L g cRow kap cD delta cVsum cVm : ℝ) : quadCoefficient d Cpre (rowCoefficientIsotropy d cRow kap) + 3 * weakCoefficient d Cpre * weakBaseCoefficientSummed M L cVsum cVm ^ 2 ≤ fusionRecursionConstantIsotropySharp d Cpre eta H M L g cRow kap cD delta cVsum cVm

The quadratic branch of the sharp constant, for the hA2 slot.