High-contrast homogenization: Provider.Quenched.SmallContrastSplitAdapters

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

The two adapters of the closing pass records exactly one shape mismatch in the fusion's argument

table, and one identification that is definitional. Both are here.

• The rate adapter. weakValueSharpMajorant_le_three_group_summed_at_level produces its drop bound at the rooted-drop rate contrastAlpha g, while hrec_line_of_one_step_isotropy_sharp_at_jb_src consumes it at the recursion rate recursionAlpha g ≤ contrastAlpha g. Since iterationDropSum is increasing in its ratio, the move is iterationDropSum_mono_r — two lines, and neither side of the interface changes.

• The base identification. weakValueSharpMajorant_le_three_group_summed_at_level is the square of its base, so the hmaj position of hrec_line_of_one_step_isotropy_sharp_at_jb_src is stage 4's conclusion read through rfl at W := weakValueBase ….

theorem HCPolySupport.HighContrast.Quenched.iterationDropSum_alpha_adapter {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {g : ℝ} (hg1 : g ≤ 1) (n : ℕ) : iterationDropSum (3 ^ (-contrastAlpha g)) F n ≤ iterationDropSum (3 ^ (-recursionAlpha g)) F n

The rate adapter. A drop bound at the rooted-drop rate is a drop bound at the recursion rate.

theorem HCPolySupport.HighContrast.Quenched.weakDropConstant_nonneg (d : ℕ) {M L alpha cD delta : ℝ} (halpha0 : 0 < alpha) (hcD : 0 ≤ cD) (hdelta : 0 ≤ delta) : 0 ≤ weakDropConstant M L alpha cD delta

The drop constant of the summed split is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.hwsq_at_recursionAlpha {d : ℕ} {F : ℕ → ℝ} (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) {g : ℝ} (hg1 : g ≤ 1) {M L cD delta w : ℝ} {n : ℕ} (halpha0 : 0 < contrastAlpha g) (hcD : 0 ≤ cD) (hdelta : 0 ≤ delta) (hw : w ^ 2 ≤ weakDropConstant M L (contrastAlpha g) cD delta * iterationDropSum (3 ^ (-contrastAlpha g)) F n) : w ^ 2 ≤ weakDropConstant M L (contrastAlpha g) cD delta * iterationDropSum (3 ^ (-recursionAlpha g)) F n

The drop bound at the recursion rate. This is the hwsq position of hrec_line_of_one_step_isotropy_sharp_at_jb_src, from the summed split's output.