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

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

The frame exponent, split into its two lengths

The response aggregation's frame exponent is (b - kappa) M + kappa L, where L is the certificate's activation generation and M is the enclosing parent generation, itself bounded by L + J + 2 with J the bracket of the outer sandwich radius. Splitting M separates the two lengths: the part carried by L collapses to the single power max b kappa of the activation length, and the part carried by J is a factor in the sandwich radius alone.

The split is uniform in the sign of b - kappa, which the response window's order data does not fix, so both cases are handled: the parent generation is at least one, so a negative exponent is already harmless, and a nonnegative one is carried by the upper bound on the parent.

Two elementary truncations

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_mul_le_max_one_of_le {e m n : ℝ} (hm : 1 ≤ m) (hmn : m ≤ n) : 3 ^ (e * m) ≤ max 1 (3 ^ (e * n))

A triadic power at an exponent between one and an upper bound is below the truncation of the power at that upper bound, whatever the sign of the rate.

theorem HCPolySupport.HighContrast.RowSupply.max_one_mul_le_mul_max_one {X Y : ℝ} (hY : 0 ≤ Y) : max 1 (X * Y) ≤ max 1 X * max 1 Y

Truncation at one is submultiplicative on nonnegative factors.

The activation half

theorem HCPolySupport.HighContrast.RowSupply.max_one_rpow_mul_rpow_le {b kappa L : ℝ} (hL : 0 ≤ L) : max 1 (3 ^ ((b - kappa) * L)) * 3 ^ (kappa * L) ≤ 3 ^ (max b kappa * L)

The activation half collapses. Truncating the parent's contribution at one and multiplying by the certificate's own contribution gives a single power of the activation length, at the larger of the two orders.

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_mul_eq_rpow_rpow (c L : ℝ) : 3 ^ (c * L) = (3 ^ L) ^ c

The triadic power at a scaled generation is the generation's power raised to the scale.

The split

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_frameExponent_le {b kappa M L J : ℝ} (hM1 : 1 ≤ M) (hMle : M ≤ L + J + 2) (hL : 0 ≤ L) : 3 ^ ((b - kappa) * M + kappa * L) ≤ (3 ^ L) ^ max b kappa * max 1 (3 ^ ((b - kappa) * (J + 2)))

The frame exponent splits. The activation length carries a single power at the larger of the two orders; the outer sandwich bracket carries the rest, truncated at one.