High-contrast homogenization: Provider.PolynomialHomogenization.Root.Dirichlet.AmplitudeRate

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

The amplitude rate, re-derived from the provider's exports

The formulaic anchored provider transports the physical block row through an exact triadic dilation before the response aggregation, and the transported amplitude already contains the requested physical-frame power. That step is performed inside the provider's proof but is not exported, so a parallel provider that consumes the exported package rather than the internal proof has to re-derive it. It is re-derived here from exactly three exported conjuncts — the dilation identity for the microscopic parameter, its residual window, and the definition of the transported amplitude — together with the certificate's own structure fields.

No hypothesis beyond the provider's own binder surface is introduced.

theorem HCPolySupport.HighContrast.RowSupply.sqrt_deltaScaled_le_physicalFrameRate {d : ℕ} [NeZero d] {g c kappaRate : ℝ} {abar : Mat d} {a : CoeffSpace d} {x epsilon lambda deltaScaled : ℝ} {N : ℕ} (h : RowRetainingPrintOrderGoodScale d g c kappaRate abar a x) (hkappa : 0 < kappaRate) (hepsilon : 0 < epsilon) (hlambda : lambda = epsilon * 3 ^ N) (hlambdaRange : lambda ∈ Set.Icc 1 3) (hdeltaScaled : deltaScaled = triadicallyScaledRowAmplitude h.delta (h.activationScale a) N (2 * kappaRate)) : √deltaScaled ≤ √h.delta * (epsilon * x) ^ kappaRate

The transported amplitude carries the physical frame rate. From the exported dilation identity lambda = epsilon * 3 ^ N, its residual window and the exported definition of the transported amplitude, the square root of the transported amplitude is below the certificate's own amplitude times the physical frame rate at the unfolded length.