High-contrast homogenization: Provider.Quenched.SmallContrastHoneAtIsotropy

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

The family's output is the fused core's hone slot

The last joint between's two halves, and it is free.

exists_one_step_family_at_isotropy_var_at_level_conv_family_min reports each generation's step with the excess written hatExcessAt P q ((N₀ : ℤ) + (n : ℤ)); the isotropic account core body's hone binder writes the same quantity expanded, as (d : ℝ) * (adaptedHattedContrast P q ((N₀ : ℤ) + (n : ℤ)) - 1). Those are the two sides of hatExcessAt's definition (HCPoly.Provider.Quenched.SmallContrastSmallnessPack), so the joint is definitional.

hone_of_one_step_family_isotropy below checks it: its proof is h, so its type-checking is the verification. With it, the endpoint's hone slot is filled by the family with no conversion layer at all — the generation-step conversion is gone entirely.

theorem HCPolySupport.HighContrast.Quenched.hone_of_one_step_family_isotropy {d : ℕ} {Cpre eta : ℝ} {H : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {N₀ ns : ℕ} {cRow kap : ℝ} {wv : ℕ → ℝ} (h : ∀ (n : ℕ), ns ≤ n → adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (hatExcessAt P q (↑N₀ + ↑n)) + wv n) + 2 * ((3 * ↑d + 4) * hatExcessAt P q (↑N₀ + ↑n) ^ 2)) (n : ℕ) : ns ≤ n → adaptedHattedContrast P q (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q (↑N₀ + ↑(n - H)) - adaptedHattedContrast P q (↑N₀ + ↑n))) + rowValue2Isotropy d cRow kap (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) + wv n) + 2 * ((3 * ↑d + 4) * (↑d * (adaptedHattedContrast P q (↑N₀ + ↑n) - 1)) ^ 2)

The joint. The one-step family's report, at the isotropy row carrier, is the fused core's hone hypothesis on the nose.