High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FluxConstantSlotSplit

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

(α) part two: the flux constant's three-slot split

The restated the negative-Sobolev Dirichlet error clause hole fixes C₀ : ℝ → ℝ → ℝ → ℝ before ∀ g, and Lg after g, κ but before abar, s₀, ρ, Rad, U, ε. So every factor of the flux constant must be routed to exactly one of

slot	may depend on
C₀ s₀ ρ Rad	d, s₀, ρ, Rad
Lg	d, g, κ
eccentricityFoldFactor abar pEcc	abar only

The explicit foldedAnchoredFrameConstant mixes the two non-fold classes: (2 Rad) ^ (s₀ − b) carries g through b and Rad; frameFoldConstant's bracket factor carries g, κ and J; and responseOneFromTwoGapFactor b s₀ carries g and s₀ at once. A factor in two classes fits no slot.

Each of the three is separated here by the same device the energy collapse uses for the geometric factor — trim the order dependence against the window's own endpoints:

• 0 ≤ s₀ − b ≤ 1/2 turns (2 Rad) ^ (s₀ − b) into max 1 ((2 Rad) ^ (1/2)), which is Rad-level;
• b − κ ≤ 1/2 together with the bracket 3 ^ J ≤ 1 + 3 (2 Rad) turns max 1 (3 ^ ((b − κ)(J + 2))) into 3 · max 1 ((1 + 3 (2 Rad)) ^ (1/2)), which is Rad-level — this is the resolution of the J-versus-Rad ambiguity flagged earlier;
• the frozen window s₀ ≥ (1 + g)/4 and b = (3 + 5 g)/16 give s₀ − b ≥ (1 − g)/16, which trims the gap factor's s₀-dependence away and leaves it g-level. Its remaining s₀-factor geometricDiscount s₀ 1 is below 1 and is simply dropped.

The certificate amplitude leaves through √δ ≤ 1. What remains is exactly

3 ^ b · foldedAnchoredFrameConstant …  ≤  fluxC0Factor d s₀ Rad cnorm · fluxLgFactor d g κ

with fluxC0Factor a function of (d, s₀, Rad, cnorm) and fluxLgFactor a function of (d, g, κ) — no abar, and no crossing between the slots. At the frozen normalization radius cnorm = 1/(3√d) the first is (d, s₀, Rad)-level, which is inside C₀ s₀ ρ Rad's permitted dependence.

Two order-trimming lemmas

theorem HCPolySupport.HighContrast.RowSupply.rpow_le_max_one_rpow_half {t e : ℝ} (ht : 0 < t) (he : 0 ≤ e) (he2 : e ≤ 1 / 2) : t ^ e ≤ max 1 (t ^ (1 / 2))

The order trim. A positive base raised to an order in [0, 1/2] is below the truncated square root of that base — a quantity free of the order.

theorem HCPolySupport.HighContrast.RowSupply.max_one_rpow_three_bracket_le {e Jr B : ℝ} (he2 : e ≤ 1 / 2) (hJr : 0 ≤ Jr) (hB1 : 1 ≤ B) (hJB : 3 ^ Jr ≤ B) : max 1 (3 ^ (e * (Jr + 2))) ≤ 3 * max 1 (B ^ (1 / 2))

The J-to-Rad trade. The bracket factor of frameFoldConstant is below a Rad-level quantity: the generation J enters only through 3 ^ J ≤ 1 + 3 (2 Rad), and the order b − κ is trimmed at 1/2.

theorem HCPolySupport.HighContrast.RowSupply.geometricDiscount_mono_order {s₁ s₂ q : ℝ} (hq : 0 ≤ q) (h : s₁ ≤ s₂) : Book.Ch02.geometricDiscount s₁ q ≤ Book.Ch02.geometricDiscount s₂ q

The geometric discount is monotone in its order.

The two slot classes

noncomputable def HCPolySupport.HighContrast.RowSupply.fluxC0Factor (d : ℕ) (s₀ Rad cnorm : ℝ) : ℝ

The C₀ class of the flux constant: a function of (d, s₀, Rad, cnorm), and at the frozen cnorm = 1/(3√d) a function of (d, s₀, Rad) — inside C₀ s₀ ρ Rad's permitted dependence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.RowSupply.fluxLgFactor (d : ℕ) (g kappaRate : ℝ) : ℝ

The Lg class of the flux constant: a function of (d, g, κ) — inside the per-g length factor's permitted dependence.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.activationFoldConstant_nonneg (d : ℕ) (g kappaRate c : ℝ) : 0 ≤ activationFoldConstant d g kappaRate c

The split

theorem HCPolySupport.HighContrast.RowSupply.three_rpow_mul_foldedAnchoredFrameConstant_le {d : ℕ} {g kappaRate s₀ Rad cnorm delta Jr : ℝ} (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappaRate) (hs₀ : s₀ ∈ Set.Ico ((1 + g) / 4) (1 / 2)) (hRad : 0 < Rad) (hJr : 0 ≤ Jr) (hJB : 3 ^ Jr ≤ 1 + 3 * (2 * Rad)) (hdelta1 : √delta ≤ 1) : Real.rpow 3 (responseWindowOrder g) * foldedAnchoredFrameConstant d g kappaRate s₀ (coarseFluxResponseConstant d) Rad cnorm delta Jr ≤ fluxC0Factor d s₀ Rad cnorm * fluxLgFactor d g kappaRate

(α), part two. The explicit flux frame constant splits into a (d, s₀, Rad, cnorm)-level factor and a (d, g, κ)-level factor, with no factor left in two classes and no dependence on abar.