High-contrast homogenization: Provider.Regularity.FiniteAffineSlopeInverseFamily

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

Joint proof-gated finite affine inverse slope family

This module constructs a single total matrix family whose values on the good finite interval are the proof-gated inverses of the canonical best-fit slope maps. The arbitrary extension outside the interval is never characterized or used.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineSlopeInverseFamilyConstants (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ) (c : ℝ), 1 ≤ C ∧ c ∈ Set.Ioc 0 (2 * C)⁻¹ ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∃ (Q : ℤ → Mat d), (∀ (k : ℤ) (hk : k ∈ Finset.Icc n m), IsUnit (Matrix.det (Q k)) ∧ finiteAffineBestFitSlopeMatrix a k m ⋯ * Q k = 1 ∧ Q k * finiteAffineBestFitSlopeMatrix a k m ⋯ = 1) ∧ Book.Ch02.matrixNorm (Q m - 1) ≤ C * delta ∧ C * delta ≤ 1 / 2

A sufficiently small GoodMax row admits one joint family of proof-gated inverse best-fit slope matrices on all interval scales, with the source terminal operator bound.