High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.RowCertificateRebase

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

Reading the row's certificate off the root certificate

The undelayed exact-gauge row Root.exists_printOrderUndelayedExactGaugeRow consumes a printed certificate whose amplitude is exactly correctorTargetAmplitude c kappa for a smallness c below its own law-free ceiling cMax (d, g, eta). The root certificate rootGoodScaleAt d g cStar κ carries its certificate at the source amplitude and at the source scale X a, together with the identity

x = commonQuantitativeAffineScale sourceAmplitude
      (correctorTargetAmplitude cStar κ) κ Caff overlinePi κ X a.

Which ceiling the large-scale C¹ slope approximation route imposes on cStar was not settled earlier. It imposes none. The PrintOrderQuantitativeNormalizedReferenceCertificate.commonAffineScale rebases the same certificate to any positive target amplitude, at the correspondingly enlarged common scale; lowering the target from correctorTargetAmplitude cStar κ to correctorTargetAmplitude c' κ enlarges the scale by at most (cStar / c') ^ κ⁻¹, a factor fixed before the matrix and the sample. The terminal's own free delay L absorbs exactly that factor, because triadicCeilingIndex of a bounded multiple of x exceeds triadicCeilingIndex x by at most triadicCeilingIndex of the multiple.

So the large-scale C¹ slope approximation clause smallness is chosen by the consumer, not reconciled against cStar: no sixth ceiling enters the five-ceiling reconciliation. That is the structural content of this module; everything in it is scale arithmetic.

Lowering the target amplitude costs one explicit factor

theorem HCPolySupport.HighContrast.CorrectorComposition.commonQuantitativeAffineScale_le_of_target_le {d : ℕ} {amplitude T T' kappaRate Caff overlinePi kappaCube : ℝ} {X : CoeffSpace d → ℝ} {a : CoeffSpace d} (hkappa : 0 < kappaRate) (hT' : 0 < T') (hT'T : T' ≤ T) (hX : 0 ≤ X a) : commonQuantitativeAffineScale amplitude T' kappaRate Caff overlinePi kappaCube X a ≤ (T / T') ^ kappaRate⁻¹ * commonQuantitativeAffineScale amplitude T kappaRate Caff overlinePi kappaCube X a

The common affine scale is Lipschitz in the target amplitude. Lowering the target from T to T' enlarges the scale by at most (T / T') ^ κ⁻¹.

theorem HCPolySupport.HighContrast.CorrectorComposition.correctorTargetAmplitude_le_of_le {c c' kappa : ℝ} (hkappa : 0 < kappa) (hcc : c' ≤ c) : correctorTargetAmplitude c' kappa ≤ correctorTargetAmplitude c kappa

The target amplitude is monotone in the corrector smallness.

theorem HCPolySupport.HighContrast.CorrectorComposition.correctorTargetAmplitude_div_eq {c c' kappa : ℝ} (hkappa : 0 < kappa) (hc' : 0 < c') : correctorTargetAmplitude c kappa / correctorTargetAmplitude c' kappa = c / c'

The ratio of two target amplitudes is the ratio of the smallnesses.

The row's certificate

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_rowCertificate_of_rootGoodScaleAt (d : ℕ) [NeZero d] {g cStarg c' kappa : ℝ} (hkappa : 0 < kappa) (hc' : 0 < c') (hc'le : c' ≤ cStarg) {abar : Mat d} {a : CoeffSpace d} {x : ℝ} (h : rootGoodScaleAt d g cStarg kappa abar a x) : ∃ (xRow : ℝ), 1 ≤ xRow ∧ xRow ≤ (cStarg / c') ^ kappa⁻¹ * x ∧ PrintOrderQuantitativeNormalizedReferenceCertificate abar g (correctorTargetAmplitude c' kappa) kappa xRow a

The row's certificate, read off the root certificate at the consumer's own smallness. No ceiling is imposed on cStar: the scale paid is the explicit factor (cStar / c') ^ κ⁻¹, which depends on (cStar, c', κ) alone and therefore may be absorbed by the large-scale C¹ slope approximation terminal's free delay.

The delay that absorbs the rebasing factor