High-contrast homogenization: Frozen.PolynomialEntryBridge

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

From the printed form of t.polynomial.entry to the calibrated form

The theorem t.polynomial.entry is printed as a statement about every scale beyond the entry scale: for a tolerance σ ∈ (0, 1] there is a constant C with Θ_m ≤ 1 + σ for every m ≥ ⌈C log₃(2 + Π K)⌉. The consumers of the theorem in the proofs of t.algebraic.convergence and t.random.homogenization use it in a calibrated form instead: a tolerance c_* below both members of a calibration pair (c_sc, c_end), and a single entry generation m_ent exhibited as a natural number, bounded by the printed ceiling and with 3^{m_ent} polynomial in 2 + Π K.

This module derives the second from the first. Three steps are involved.

• The tolerance. c_* := min 1 (min c_sc c_end) is positive, lies below both members of the calibration pair, and is admissible as a tolerance in the printed statement, which requires σ ≤ 1.
• The entry generation. The printed statement quantifies over all scales above ⌈C log₃(2 + Π K)⌉. That ceiling is positive, because Π ≥ 0 and K > 1 make 2 + Π K exceed one and C is positive, so m_ent := ⌈C log₃(2 + Π K)⌉ is a natural number and is itself an admissible scale.
• The length bound. ⌈x⌉ < x + 1 turns the ceiling into the printed polynomial bound: 3^{m_ent} ≤ 3^{x+1} = 3 · 3^{C log₃(2 + Π K)} = 3 (2 + Π K)^C.

The assumptions e.stationarity, e.unit.range and e.coarse.ellipticity are the ones the printed statement carries: HCPoly.Frozen.IsStationaryLaw, HCPoly.Frozen.IsUnitRangeLaw and HCPoly.Frozen.CoarseEllipticityDagger, read by the proofs of the propositions under their project-namespace names. Nothing is converted here.

theorem HCPoly.Frozen.one_lt_two_add_aspectRatio_mul {d : ℕ} (E : HCPolySupport.BlockMat d) {K : ℝ} (hK : 1 < K) : 1 < 2 + HCPolySupport.HighContrast.aspectRatio E * K

The positivity of the printed entry scale: 2 + Π K > 1 whenever the reference aspect ratio is nonnegative and the growth witness exceeds one, so a positive multiple of its base-three logarithm has a positive ceiling.

theorem HCPoly.Frozen.exists_entry_generation {C b : ℝ} (hC : 0 < C) (hb : 1 < b) : ∃ (mEnt : ℕ), ↑mEnt = ⌈C * Real.logb 3 b⌉ ∧ 3 ^ mEnt ≤ 3 * b ^ C

The printed entry generation as a natural number, with the two printed readings of the entry scale: it is the ceiling itself, and its triadic exponential is bounded by the printed polynomial.

theorem HCPoly.Frozen.polynomial_entry_random_source_of_printed (d : ℕ) (hd : 2 ≤ d) (cSc _δ₀ cEnd : ℝ) (hcSc : 0 < cSc) (_hδ₀ : _δ₀ ∈ Set.Ioo 0 1) (hcEnd : 0 < cEnd) (_hcal : (1 + _δ₀) ^ 2 * (1 + cEnd) ≤ 1 + cSc) : ∃ cStar ∈ Set.Ioc 0 (min cSc cEnd), ∀ g ∈ Set.Ico 0 1, ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (HCPolySupport.HighContrast.CoeffSpace d)) (E : HCPolySupport.BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : HCPolySupport.HighContrast.CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∃ (mEnt : ℕ), ↑mEnt ≤ ⌈C * Real.logb 3 (2 + HCPolySupport.HighContrast.aspectRatio E * K)⌉ ∧ HCPolySupport.HighContrast.annealedContrast P ↑mEnt - 1 ≤ cStar ∧ 3 ^ mEnt ≤ 3 * (2 + HCPolySupport.HighContrast.aspectRatio E * K) ^ C

The bridge. The calibrated form of t.polynomial.entry used by ss.algebraic.convergence and ss.random.dirichlet, derived from the printed form. The calibration pair (c_sc, c_end) is carried by the statement; the intermediate δ₀ and the calibration inequality are carried for the consumers and are not used here.