High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.FormulaicShiftedNormalizedReferencePowerTail

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

Formulaically shifted power tails for an exactly normalized reference coefficient

One global affine-pullback coefficient family supplies every reference cube. A fixed enclosure of the exact normalized root controls every physical row, and a further natural generation shift absorbs the resulting geometric and exponent-gap factor. The shift is the ceiling of an explicit logarithmic expression, so the same witness used by the tail proof has a deterministic upper bound.

noncomputable def HCPolySupport.HighContrast.Certificate.shiftedTailAbsorptionPrefactor (d : ℕ) (s rho : ℝ) (G : ℕ) : ℝ

The deterministic prefactor absorbed by the generation shift.

Equations

• HCPolySupport.HighContrast.Certificate.shiftedTailAbsorptionPrefactor d s rho G = 6 * ↑d * √↑d * (3 ^ (rho * ↑G) * (1 / (1 - 3 ^ (-(2 * s - rho)))))

noncomputable def HCPolySupport.HighContrast.Certificate.formulaicNormalizedReferenceTailShift (d : ℕ) (s rho kappa : ℝ) (G : ℕ) : ℕ

The formulaic generation shift used in the normalized-reference tail.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Certificate.formulaicNormalizedReferenceTailShift_spec {d : ℕ} {s rho kappa : ℝ} {G : ℕ} (hkappa : 0 < kappa) (hC : 0 < shiftedTailAbsorptionPrefactor d s rho G) : shiftedTailAbsorptionPrefactor d s rho G ≤ 3 ^ (kappa * ↑(formulaicNormalizedReferenceTailShift d s rho kappa G)) ∧ ↑(formulaicNormalizedReferenceTailShift d s rho kappa G) < max 0 (Real.logb 3 (shiftedTailAbsorptionPrefactor d s rho G) / kappa) + 1

The formulaic shift absorbs its prefactor and lies strictly below the corresponding logarithmic threshold plus one.

theorem HCPolySupport.HighContrast.Certificate.exists_formulaicShiftedNormalizedReferencePowerTail_of_hasAllLaterPhysicalBlockRow {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (s rho kappa delta : ℝ) (S X : CoeffSpace d → ℝ) (hrho : 0 < rho) (hrho1 : rho ≤ 1) (hrhoGap : rho < 2 * s) (hkappa : 0 < kappa) (hdelta : 0 ≤ delta) (hrow : Quenched.HasAllLaterPhysicalBlockRow rho 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 = formulaicNormalizedReferenceTailShift d s rho kappa G ∧ ↑L < max 0 (Real.logb 3 (shiftedTailAbsorptionPrefactor d s rho G) / kappa) + 1 ∧ (∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) ∧ ScalarIdentityPowerTail aRef s (√delta) (kappa / 2) (3 ^ ↑(Quenched.triadicCeilingIndex (X a) + L))

A physical block row produces one global exactly normalized reference family whose identity weak errors retain the square-root amplitude and the halved row-decay rate above the shifted triadic scale.