High-contrast homogenization: Provider.Quenched.Prop211Arithmetic

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

Arithmetic for the one-time rebase

The constants in this file are selected before the coefficient law. The triadic bracket is selected afterwards from the law's polynomial base.

theorem HCPolySupport.HighContrast.Quenched.exists_rebase_enlargement {cSc cStar : ℝ} (hc : cStar ∈ Set.Ioo 0 cSc) : ∃ delta ∈ Set.Ioo 0 1, (1 + delta) ^ 2 * (1 + cStar) ≤ 1 + cSc

A positive enlargement below one that preserves a prescribed strict small-contrast margin.

theorem HCPolySupport.HighContrast.Quenched.three_le_rebaseBase {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Psi K S) : 3 ≤ 2 + aspectRatio E * K

The polynomial base of the rebase is uniformly at least three.

theorem HCPolySupport.HighContrast.Quenched.pow_three_bracket_sq_le_four {base : ℝ} {q : ℕ} (hbase : 3 ≤ base) (hlow : base ^ 2 ≤ 3 ^ ↑q) (hupp : 3 ^ ↑q ≤ 1 + 3 * base ^ 2) : 1 ≤ q ∧ 3 ^ ↑q ≤ base ^ 4

A bracket for the square of a base at least three costs at most four powers of that base.

theorem HCPolySupport.HighContrast.Quenched.T_le_renormBase_of_gain_bound {gamma nu mu delta Gain G0 T base : ℝ} {l0 h D q : ℕ} (hT : 1 ≤ T) (hdelta : 0 < delta) (hGain : 0 < Gain) (hGainBound : Gain ≤ G0 * base) (hpow : G0 * T / delta * base ≤ 3 ^ (mu * ↑(D * q) - mu)) (hexp : gamma - nu + mu * (↑l0 - ↑h) = mu * ↑(D * q) - mu) : T ≤ renormBase gamma nu mu delta Gain l0 h

The lower-floor parameter follows from the selected gain multiplier.

theorem HCPolySupport.HighContrast.Quenched.kappa_burn_of_multiplier {kappa delta diff base : ℝ} {A q : ℕ} (hdelta : 0 < delta) (hq : 1 ≤ q) (hcoef : 0 ≤ diff * ↑A - 1) (hfixed : 12 / (1 + delta) ≤ 3 ^ (diff * ↑A - 1)) (hbase0 : 0 ≤ base) (hbaseq : base ≤ 3 ^ q) (hkappa : kappa ≤ 6 * base) : 2 * kappa ≤ (1 + delta) * 3 ^ (diff * ↑(A * q))

The old-reference comparison is absorbed by the exponent gap across the selected recent window.