High-contrast homogenization: Provider.Quenched.SmallContrastValueClauseAtCarriers

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

The value clause at the design carriers

The released one-step family reports its weak value at the isotropy reference, the scalar load and the generation's own window; the fused core asks for that value below the parametrized base at the pinned group coefficients. This file joins the two at the exact spelling the family produces, so the assembly has nothing left to reconcile on the value side.

The window is read at the generation's own height by instantiating the fixed-window statement once per generation — the value clause is universally quantified over the height, so no restatement is needed for a growing window.

The released window-tail coefficient is above the pinned one because the split level is at least one, which is the printed range's left endpoint.

theorem HCPolySupport.HighContrast.Quenched.sqrt_two_le_energyGoodConstantAtLevel {lev : ℝ} (hlev : 1 ≤ lev) : √2 ≤ Response.energyGoodConstantAtLevel lev

The pinned window tail is below the released one on the printed range.

noncomputable def HCPolySupport.HighContrast.Quenched.designNormalizer (lev M : ℝ) : ℝ

The normalizer the value clause hands the fused core.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.designNormalizer_nonneg {lev M : ℝ} (hlev : 1 ≤ lev) (hM : 0 ≤ M) : 0 ≤ designNormalizer lev M

theorem HCPolySupport.HighContrast.Quenched.hmaj_at_design_carriers_at_level {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) (hrec : canonicalShear E = 0) {cIso rho : ℝ} (hcIso : 0 ≤ cIso) (hcsmall : cIso < 1) (hrho1 : rho < 1) {lAl : ℤ} {N₀ : ℕ} {S0 SStar0 K0 : ℕ → Mat d} (hS0 : ∀ (n : ℕ), Matrix.PosDef (S0 n)) (hStar0 : ∀ (n : ℕ), Matrix.PosDef (SStar0 n)) (hform : ∀ (n : ℕ), toFullBlockMat (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) = schurBlock (S0 n) (SStar0 n) (K0 n)) (henv : ∀ (n : ℕ), BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) (isotropyReference cIso E)) (hcomp : ∀ (n : ℕ), BlockMatLoewnerLE E (blockScale (isotropyKap2 cIso) (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)))) {V : ℕ → ℕ → ℝ} {V0 : ℕ → ℝ} {Dr : ℕ → ℕ → ℝ} {Vmean bmaj : ℕ → ℝ} {beta lev : ℝ} {Hw : ℕ → ℕ} (hV : ∀ (n j : ℕ), 0 ≤ V n j) (hV0 : ∀ (n : ℕ), 0 ≤ V0 n) (hDr : ∀ (n j : ℕ), 0 ≤ Dr n j) (hVmean : ∀ (n : ℕ), 0 ≤ Vmean n) (hbmaj : ∀ (n : ℕ), 0 ≤ bmaj n) (hbeta : 0 ≤ beta) (hlev : 1 ≤ lev) {M : ℝ} (hM : metricFactorValue E (1 + cIso) (isotropyKap2 cIso) ≤ M) (n : ℕ) : weakValueBoundSharpIsotropyAt (Response.recentConstantAtLevel lev) (Response.maxGroupConstantAtLevel lev) (Response.energyGoodConstantAtLevel lev) P (canonicalMetric E) (Response.responseSkew (K0 n)) (isotropyReference cIso E) (loadScaleOfScalar (1 + cIso) (isotropyKap2 cIso)) (canonicalMetric E) rho (Hw n) (bmaj n) beta lev (↑N₀ + ↑n) lAl (V n) (V0 n) (Dr n) (Vmean n) ≤ weakValueBaseIsotropyAtPar 16 16 (designNormalizer lev M) (isotropyLoadScale cIso (isotropyKap2 cIso)) rho (Hw n) (bmaj n) beta lev (V n) (V0 n) (Dr n) (Vmean n) ^ 2

The value clause at the design carriers, at the pinned coefficients. This is the fused core's value hypothesis, produced from the released chain at the spelling the released one-step family reports.