High-contrast homogenization: Provider.Quenched.SmallContrastLoadScalePiFree

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

The load scale, the kap2 value and the metric factor

Corrected interface. This file was first written on the assumption that the Euclidean boundary envelope could be eliminated by an inequality: each of weakLoadScalePiFree, kap2Value and metricFactorValue is monotone in the scalar boundaryConst C_d g m_Al · 3^{gG}, so any Π-free upper bound on that scalar would propagate. The near-reference comparison refutes that reading: the hypothesis boundaryConst C_d g m_Al · 3^{gG} ≤ cIso forces witnessEccentricity m_Al ≤ cIso (the row-envelope eccentricity bound), and at the fusion's binding m_Al = canonicalMetric 𝐄 the family has witnessEccentricity (canonicalMetric 𝐄) → ∞ at constant contrast. No Π-free cIso satisfies it, and the near-reference comparison — which bounds adaptedMean, not boundaryConst — cannot discharge it.

The correct interface is the near-reference comparison's, and it is a change of normalizing block, not a scalar inequality: the account is taken against isotropyReference rather than the inflated reference, so isotropyLoadScale replaces weakLoadScalePiFree and isotropyKap2 replaces kap2Value. There is no inequality between the old and new carriers, and none is needed.

What this file therefore supplies:

• the two monotonicity steps, retained but no longer part of the load-scale interface: they are sound, and they remain the arithmetic that the row-3 re-parametrization will use once an envelope is produced, but they are not dischargeable from the near-reference comparison.
• — the arithmetic the consumers need at the near-reference comparison's carriers.
• — the metric factor, which does close: its r slot is discharged by the near-reference comparison's sqrt_kappaRef_le_of_refContrast_le at r = √(1 + 6σ), dimension-only. This closes the residual that the previous version of this file named as missing (kappaRef 𝐄 has no upper bound in the tree) — the near-reference comparison supplied it.
• — the propagation into fusionRecursionConstantIsotropySharp's quadratic branch, at carriers with no boundaryConst, no witnessEccentricity, no 3^{gG} and no kappaRef.

1. The envelope monotonicity steps (outside the load-scale interface)

def HCPolySupport.HighContrast.Quenched.weakLoadScalePiFree (cIso kap : ℝ) : ℝ

The weak load scale at an abstract envelope scalar.

Not Π-free in practice: see the header. Retained as arithmetic.

Equations

• HCPolySupport.HighContrast.Quenched.weakLoadScalePiFree cIso kap = 2 * cIso * kap * 7

2. The arithmetic at the near-reference comparison's carriers

theorem HCPolySupport.HighContrast.Quenched.one_le_isotropyKap2 {cIso : ℝ} (hcIso : 0 ≤ cIso) (hsmall : cIso < 1) : 1 ≤ isotropyKap2 cIso

The entry comparability constant is at least one.

3. The metric factor, closed at the near-reference comparison's imbalance bound

noncomputable def HCPolySupport.HighContrast.Quenched.metricFactorValuePiFree (cF kap r : ℝ) : ℝ

The metric factor at an abstract reference ratio r ≥ √κ_𝐄.

Equations

• HCPolySupport.HighContrast.Quenched.metricFactorValuePiFree cF kap r = √(cF * r * (2 + 2 * (kap * (cF * r))))

theorem HCPolySupport.HighContrast.Quenched.metricFactorValue_eq_piFree {d : ℕ} (E : BlockMat d) (cF kap : ℝ) : metricFactorValue E cF kap = metricFactorValuePiFree cF kap √(kappaRef E)

theorem HCPolySupport.HighContrast.Quenched.metricFactorValuePiFree_mono {cF cF' kap kap' r r' : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hr0 : 0 ≤ r) (hcF : cF ≤ cF') (hkap : kap ≤ kap') (hr : r ≤ r') : metricFactorValuePiFree cF kap r ≤ metricFactorValuePiFree cF' kap' r'

The metric factor is monotone in all three carriers.

theorem HCPolySupport.HighContrast.Quenched.metricFactorValue_le_piFree {d : ℕ} {E : BlockMat d} {cF cF' kap kap' r : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hcF : cF ≤ cF') (hkap : kap ≤ kap') (hr : √(kappaRef E) ≤ r) : metricFactorValue E cF kap ≤ metricFactorValuePiFree cF' kap' r

The metric factor at an abstract imbalance bound.

theorem HCPolySupport.HighContrast.Quenched.metricFactorValue_le_isotropy {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sigma : ℝ} (hsigma : refContrast E - 1 ≤ sigma) {cF cF' kap kap' : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hcF : cF ≤ cF') (hkap : kap ≤ kap') : metricFactorValue E cF kap ≤ metricFactorValuePiFree cF' kap' √(1 + 6 * sigma)

The metric factor closed at a dimension-only ratio. the near-reference comparison's sqrt_kappaRef_le_of_refContrast_le discharges the r slot at √(1 + 6σ), which carries no Π.

noncomputable def HCPolySupport.HighContrast.Quenched.isotropyMetricFactor (cIso sigma : ℝ) : ℝ

The metric factor at the near-reference comparison's carriers. Every argument is Π-free.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.metricFactorValue_le_isotropyMetricFactor {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sigma : ℝ} (hsigma : refContrast E - 1 ≤ sigma) {cIso cF kap : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hcF : cF ≤ 1 + cIso) (hkap : kap ≤ isotropyKap2 cIso) : metricFactorValue E cF kap ≤ isotropyMetricFactor cIso sigma

4. Propagation into the quadratic branch