High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.FormulaicMidpointNormalizedReferencePowerTail

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

Formulaically shifted midpoint normalized-reference tails

The midpoint specialization retains the exact old converter interface and also exports the enclosure generation, the formulaic shift, and its strict deterministic upper bound.

theorem HCPolySupport.HighContrast.RowSupply.exists_midpointNormalizedReferencePowerTail_with_formulaicShift {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {g kappa delta : ℝ} (S X : CoeffSpace d → ℝ) (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappa) (hdelta : 0 ≤ delta) (hrow : Quenched.HasAllLaterPhysicalBlockRow (Certificate.printRowOrder g) kappa delta (Book.Ch02.constantBlockMatrix abar) S X a) (hXone : 1 ≤ X a) (hburn : S a ≤ X a) : ∃ (G : ℕ) (aRef : Book.Ch03.CoeffFamily d) (L : ℕ), witnessEccentricity (symmPart abar) * √↑d ≤ 3 ^ ↑G ∧ 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d) ∧ L = Certificate.formulaicNormalizedReferenceTailShift d (midpointResponseOrder g) (Certificate.printRowOrder g) kappa G ∧ ↑L < max 0 (Real.logb 3 (Certificate.shiftedTailAbsorptionPrefactor d (midpointResponseOrder g) (Certificate.printRowOrder g) G) / kappa) + 1 ∧ (∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) ∧ ScalarIdentityPowerTail aRef (midpointResponseOrder g) (√delta) (kappa / 2) (3 ^ ↑(Quenched.triadicCeilingIndex (X a) + L))

The midpoint converter with the enclosure and formulaic shift data kept in its conclusion.