High-contrast homogenization: Provider.Quenched.SmallContrastMetricFactorAccount

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

The two metric factors of the sharp weak value, at the recentered reference

weakValueBoundSharpIsotropyAt carries two metric factors, both at the recentering skew h_0 = h_rsp(K_t) of the terminal adapted mean:

• K_{M,F_2} at the inflated reference F_2 = c_F 𝐄;
• K_{M,E_t} at the terminal adapted mean itself.

This file bounds both by reference data only — no generation, no source moment — once the reference has been recentered so that its canonical shear vanishes (SmallContrastCanonRecenter.canonicalShear_recentered_eq_zero, the normalization of Section 2.5 of HC) and the terminal mean is two-sidedly comparable with the reference:

E_t ≤ c_F 𝐄 (the entry envelope) and 𝐄 ≤ κ E_t (the entry comparability).

Under the recentering the canonical metric block of the reference is the split metric M_0 = diag(m(𝐄), m(𝐄)^{-1}), so the balance chain M(𝐄) ≤ 𝐄 ≤ 𝔡(𝐄)^{1/2} M(𝐄) turns the two comparabilities into a two-sided comparison of E_t with M_0, which is exactly the input of responseSkew_quad_le_of_sandwich.

theorem HCPolySupport.HighContrast.Quenched.skewBlockCongr_zero {d : ℕ} (A : BlockMat d) : Response.skewBlockCongr 0 A = A

The trivial shear congruence is the identity.

noncomputable def HCPolySupport.HighContrast.Quenched.metricFactorValue {d : ℕ} (E : BlockMat d) (cF kap : ℝ) : ℝ

The metric-factor value: the reference imbalance times the shear distortion of the response skew, all under the square root.

Equations

• HCPolySupport.HighContrast.Quenched.metricFactorValue E cF kap = √(cF * √(HCPolySupport.HighContrast.kappaRef E) * (2 + 2 * (kap * (cF * √(HCPolySupport.HighContrast.kappaRef E)))))

theorem HCPolySupport.HighContrast.Quenched.metricFactorValue_nonneg {d : ℕ} (E : BlockMat d) (cF kap : ℝ) : 0 ≤ metricFactorValue E cF kap

theorem HCPolySupport.HighContrast.Quenched.diagonalWeakMetricFactor_recentered_le {d : ℕ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) (hrec : canonicalShear E = 0) {A : BlockMat d} {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hform : toFullBlockMat A = schurBlock S SStar K) {cF kap : ℝ} (hcF : 0 ≤ cF) (hkap : 0 ≤ kap) (henv : BlockMatLoewnerLE A (blockScale cF E)) (hcomp : BlockMatLoewnerLE E (blockScale kap A)) : Response.diagonalWeakMetricFactor (canonicalMetric E) (Response.skewBlockCongr (Response.responseSkew K) (blockScale cF E)) ≤ metricFactorValue E cF kap ∧ Response.diagonalWeakMetricFactor (canonicalMetric E) (Response.skewBlockCongr (Response.responseSkew K) A) ≤ metricFactorValue E cF kap

Both metric factors of the sharp weak value, at the recentered reference. The bound depends only on the reference 𝐄 (through its imbalance κ_𝐄), the envelope constant c_F, and the comparability constant κ — never on the generation.