High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.RowRetainingGoodScaleInterface

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

Row-retaining root certificate interface

The normalized-reference certificate used by deterministic consumers is a lossy projection of the stochastic row which produced it. The response-rate consumer retains that row together with the projected good-scale certificate.

structure HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale (d : ℕ) [NeZero d] (g c kappaRate : ℝ) (abar : Mat d) (a : CoeffSpace d) (x : ℝ) : Type

Root good-scale data with the producing physical block row retained. The row rate is twice the response rate because the response converter takes a square root.

• good : PrintOrderRateBearingCommonAffineGoodScale d g c kappaRate abar a x
• delta : ℝ

  Nonnegative amplitude in the retained physical block-row estimate.

• sourceScale : CoeffSpace d → ℝ

  Coefficient-dependent source scale entering the retained physical block row.

• activationScale : CoeffSpace d → ℝ

  Coefficient-dependent scale above which the retained physical block-row estimate applies.

• delta_nonneg : 0 ≤ self.delta
• activation_one : 1 ≤ self.activationScale a
• source_le_activation : self.sourceScale a ≤ self.activationScale a
• activation_le_common : self.activationScale a ≤ x
• row : Quenched.HasAllLaterPhysicalBlockRow (Certificate.printRowOrder g) (2 * kappaRate) self.delta (Book.Ch02.constantBlockMatrix abar) self.sourceScale self.activationScale a

theorem HCPolySupport.HighContrast.RowSupply.sqrt_triadicallyScaledRowAmplitude_le_physicalFrameRate {delta activation epsilon x kappa : ℝ} {N : ℕ} (hdelta : 0 ≤ delta) (hactivation : 0 ≤ activation) (hepsilon : 0 < epsilon) (hkappa : 0 ≤ kappa) (hax : activation ≤ x) (hN : epsilon⁻¹ ≤ 3 ^ N) : √(triadicallyScaledRowAmplitude delta activation N (2 * kappa)) ≤ √delta * (epsilon * x) ^ kappa

The transported row amplitude contains the requested physical-frame power before any response aggregation is performed.