High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.TriadicPhysicalBlockRowTransport

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

Triadic transport of a physical block row

The physical block row is transported before the normalized-response all-depth sum is formed. Its activation scale becomes one, while the lost fraction of the original activation is retained in the row amplitude.

noncomputable def HCPolySupport.HighContrast.RowSupply.triadicallyScaledRowAmplitude (delta x : ℝ) (N : ℕ) (kappa : ℝ) : ℝ

The amplitude of the row after a triadic rescaling which places its activation below the unit generation.

Equations

• HCPolySupport.HighContrast.RowSupply.triadicallyScaledRowAmplitude delta x N kappa = delta * (x / 3 ^ N) ^ kappa

theorem HCPolySupport.HighContrast.RowSupply.hasAllLaterPhysicalBlockRow_physicalScaleCoeff {d : ℕ} (rho kappa delta : ℝ) (Abar : BlockMat d) (S X : CoeffSpace d → ℝ) (a : CoeffSpace d) (N : ℕ) (hrow : Quenched.HasAllLaterPhysicalBlockRow rho kappa delta Abar S X a) (hXone : 1 ≤ X a) (hburn : S a ≤ X a) (hactive : X a ≤ 3 ^ N) : Quenched.HasAllLaterPhysicalBlockRow rho kappa (triadicallyScaledRowAmplitude delta (X a) N kappa) Abar (fun (x : CoeffSpace d) => 1) (fun (x : CoeffSpace d) => 1) (Quenched.physicalScaleCoefficient N a)

An all-later physical row transports to the restored coefficient sample. The new row starts at one, and its amplitude records the exact activation ratio x / 3^N.