High-contrast homogenization: Provider.Quenched.FixedGridWindowAccount

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

Fixed-grid response-window account

The canonical metric and its base rounded grid are fixed once and for all. For every sufficiently late terminal generation, a fresh source window begins H generations earlier and encloses every cell read by the response estimate. The first admissible terminal generation has a polynomial triadic bound in the reference aspect ratio and the source growth witness.

The lag H ≥ 4 is a parameter: the compact pre-Young absorption requires (3/2)·Cpre·3^{-H} ≤ 1/4 for the dimension-dependent response constant Cpre, so the printed lag four is admissible only after enlarging H to a dimension-dependent value, all before the law.

theorem HCPolySupport.HighContrast.Quenched.finite_adaptedMean_of_coarseEllipticityDagger {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) {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) : HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)

Coarse ellipticity makes every adapted mean on a positive grid finite and positive definite, independently of the source-window cutoff.