HomSpineInstallArith

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The §4.5 level arithmetic of the re-cut bundle, reduced to its residues

What this file supplies

The re-cut bundle carries two arithmetic conditions, hlevel and hlevelDual, on the printed right-hand side coarseGrainingFinitePRHS. This file EXPANDS both at the display's own data and reduces them to the smallest set of residues, proving every model-side piece outright:

• the σ-bookkeeping σ · dataBracket = 3^{m/2}K_g + σ(K_h^∞ + 3^{m/2}K_h) and √σ · energyBracket = σ · dataBracket;
• the 3-power split 3^{s₂n} · 3^{(1/2-s₂)m} = 3^{s₂(n-m)} · 3^{m/2} (the printed display's 3^{\frac12(n-m)} 3^{\frac12 m}, at general s₂);
• the dual-order cancellation: K_test(□_m, s, s′, p′) · 3^{s′m} = d(1 + C_rad^{1/p′}) · 3^{sm} — the 3^{sm} on the two sides of hlevelDual cancel EXACTLY, so the dual condition is the SAME arithmetic read at s′ with one extra dimensional constant.

The residues that survive

coarseGrainingFinitePRHS_le_of_energyBound is the reduction. Its three content-bearing hypotheses are:

1. hSbound: S ≤ C_en · energyBracket σ 3^{m/2} K_g K_h^∞ K_h — the Theorem-C residue: the Step-2 energy-density datum ( the mesoscale energy bound), whose C_en carries 3^{(1-α)X_m(α)};
2. hDgbound: D_g ≤ C_data · K_g · 3^{(1/2-s₂)m} — the data slot; PROVED for the pinned carrier in HomSpineInstallData;
3. hA, hB — the E_B pairing: the two summands of the printed constant against the two summands of EthmB(m) ("comparing to the definition of EthmB(m)").

Everything else in the two conditions is discharged here.

1. The σ bookkeeping of the printed level

theorem Algsuperdiff.Section4.Provider.Homogenization.sigma_mul_dataBracket (sigma pow Kg KhInf Kh : ℝ) (hsig : 0 < sigma) : sigma * dataBracket sigma pow Kg KhInf Kh = pow * Kg + sigma * (KhInf + pow * Kh)

The printed level, expanded. σ · D = 3^{m/2}K_g + σ(K_h^∞ + 3^{m/2}K_h): the σ^{-1} of the introduction's homogenization estimate's bracket is cancelled by the σ weight of the coarse-graining display's right-hand side. No inequality is spent.

theorem Algsuperdiff.Section4.Provider.Homogenization.sigma_mul_dataBracket_nonneg {sigma pow Kg KhInf Kh : ℝ} (hsig : 0 < sigma) (hpow : 0 ≤ pow) (hKg : 0 ≤ Kg) (hKhInf : 0 ≤ KhInf) (hKh : 0 ≤ Kh) : 0 ≤ sigma * dataBracket sigma pow Kg KhInf Kh

The expanded level is nonnegative on the printed data.

theorem Algsuperdiff.Section4.Provider.Homogenization.dataLeg_le_sigma_mul_dataBracket {sigma pow Kg KhInf Kh : ℝ} (hsig : 0 < sigma) (hpow : 0 ≤ pow) (hKhInf : 0 ≤ KhInf) (hKh : 0 ≤ Kh) : pow * Kg ≤ sigma * dataBracket sigma pow Kg KhInf Kh

The data leg alone is below the expanded level.

theorem Algsuperdiff.Section4.Provider.Homogenization.sqrt_mul_energyBracket (sigma pow Kg KhInf Kh : ℝ) (hsig : 0 < sigma) : √sigma * energyBracket sigma pow Kg KhInf Kh = sigma * dataBracket sigma pow Kg KhInf Kh

The √σ half of the same bookkeeping: the display's σ^{1/2} weight turns the Step-2 the introduction's energy display bracket into the printed level.

2. The 3-power split of the forcing leg

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_mesoscale_split (s2 : ℝ) (m n : ℤ) : 3 ^ (s2 * ↑n) * 3 ^ ((1 / 2 - s2) * ↑m) = 3 ^ (s2 * (↑n - ↑m)) * 3 ^ (↑m / 2)

The mesoscale 3-power split at general s₂: 3^{s₂n} · 3^{(1/2-s₂)m} = 3^{s₂(n-m)} · 3^{m/2}. Exact.

3. THE REDUCTION

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingFinitePRHS_le_of_energyBound {Ccg s s2 sigma E1 E2 Dg S Cen Cdata Kg KhInf Kh A B : ℝ} {m n : ℤ} (hsig : 0 < sigma) (hs0 : 0 < s) (hss2 : s < s2) (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hKg0 : 0 ≤ Kg) (hKhInf0 : 0 ≤ KhInf) (hKh0 : 0 ≤ Kh) (hCen0 : 0 ≤ Cen) (hCdata0 : 0 ≤ Cdata) (hSbound : S ≤ Cen * energyBracket sigma (3 ^ (↑m / 2)) Kg KhInf Kh) (hDgbound : Dg ≤ Cdata * Kg * 3 ^ ((1 / 2 - s2) * ↑m)) (hA : Ccg * s⁻¹ * E1 * Cen ≤ A) (hB : Ccg * s ^ (-(9 / 2)) * (s2 - s)⁻¹ * (1 + E2 ^ 2) * Cdata * 3 ^ (s2 * (↑n - ↑m)) ≤ B) : coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S n ≤ (A + B) * (sigma * dataBracket sigma (3 ^ (↑m / 2)) Kg KhInf Kh)

The printed right-hand side, reduced to its three residues.

Every model-side piece of the §4.5 level arithmetic is discharged; what remains on the right is the single product (A + B) · (σ · dataBracket), i.e. the printed level with the two constants left abstract.

• hSbound is the Theorem-C residue (the Step-2 energy-density datum);
• hDgbound is the data slot (proved for the pinned carrier elsewhere);
• hA, hB are the two EthmB(m) pairings.

4. hlevel, from the residues

theorem Algsuperdiff.Section4.Provider.Homogenization.hlevel_of_energyBound {Ccg s s2 sigma E1 E2 Dg S Cen Cdata Cw EB Kg KhInf Kh A B : ℝ} {m n : ℤ} (hsig : 0 < sigma) (hs0 : 0 < s) (hss2 : s < s2) (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hKg0 : 0 ≤ Kg) (hKhInf0 : 0 ≤ KhInf) (hKh0 : 0 ≤ Kh) (hCen0 : 0 ≤ Cen) (hCdata0 : 0 ≤ Cdata) (hSbound : S ≤ Cen * energyBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh) (hDgbound : Dg ≤ Cdata * Kg * 3 ^ ((1 / 2 - s2) * ↑m)) (hA : Ccg * s⁻¹ * E1 * Cen ≤ A) (hB : Ccg * s ^ (-(9 / 2)) * (s2 - s)⁻¹ * (1 + E2 ^ 2) * Cdata * 3 ^ (s2 * (↑n - ↑m)) ≤ B) (hsplit : A + B ≤ Cw * EB) : coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S n ≤ sigma * (Cw * EB * dataBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh)

THE BUNDLE'S hlevel, from the named residues alone.

The conclusion is byte-identical to the hlevel conjunct of the re-cut bundle.

5. The dual-order cancellation, and hlevelDual

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.cgTestConstBase (d : ℕ) (alpha s' t : ℝ) : ℝ

The scale-free half of the test-class constant, d(1 + C_rad^{1/t}). cgTestConst is this times the single scale power L^{α-s′}.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.cgTestConstBase_nonneg (d : ℕ) {alpha s' t : ℝ} (hlo : 0 < (alpha - s') * t) : 0 ≤ cgTestConstBase d alpha s' t

theorem Algsuperdiff.Section4.Provider.Homogenization.cgTestConst_mul_rpow_originCube (d : ℕ) (m : ℤ) (alpha s' t : ℝ) : cgTestConst d (HCPolySupport.originCube d m) alpha s' t * Real.rpow 3 (s' * ↑m) = cgTestConstBase d alpha s' t * Real.rpow 3 (alpha * ↑m)

THE DUAL-ORDER CANCELLATION.

K_test(□_m, α, s′, t) · 3^{s′m} = d(1 + C_rad^{1/t}) · 3^{αm}. The single scale power the order-losing test-class comparison carries is EXACTLY the one that turns the display's own 3^{s′m} into the consumption site's 3^{αm}, so the 3^{αm} factors on the two sides of hlevelDual cancel and the dual condition is the plain level condition read at the dual order.

theorem Algsuperdiff.Section4.Provider.Homogenization.hlevelDual_of_energyBound {d : ℕ} {Ccg s s' s2 sigma E1 E2 Dg S Cen Cdata Cw EB Kg KhInf Kh A B t : ℝ} {m n : ℤ} (hsig : 0 < sigma) (hs'0 : 0 < s') (hs's2 : s' < s2) (hlo : 0 < (s - s') * t) (hCcg0 : 0 ≤ Ccg) (hE10 : 0 ≤ E1) (hE20 : 0 ≤ E2) (hKg0 : 0 ≤ Kg) (hKhInf0 : 0 ≤ KhInf) (hKh0 : 0 ≤ Kh) (hCen0 : 0 ≤ Cen) (hCdata0 : 0 ≤ Cdata) (hSbound : S ≤ Cen * energyBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh) (hDgbound : Dg ≤ Cdata * Kg * 3 ^ ((1 / 2 - s2) * ↑m)) (hA : cgTestConstBase d s s' t * (Ccg * s'⁻¹ * E1 * Cen) ≤ A) (hB : cgTestConstBase d s s' t * (Ccg * s' ^ (-(9 / 2)) * (s2 - s')⁻¹ * (1 + E2 ^ 2) * Cdata * 3 ^ (s2 * (↑n - ↑m))) ≤ B) (hsplit : A + B ≤ Cw * EB) : cgTestConst d (HCPolySupport.originCube d m) s s' t * (Real.rpow 3 (s' * ↑m) * coarseGrainingFinitePRHS Ccg s' s2 sigma E1 E2 Dg S n) ≤ Real.rpow 3 (s * ↑m) * (sigma * (Cw * EB * dataBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh))

THE BUNDLE'S hlevelDual, from the named residues alone.

The conclusion is byte-identical to the hlevelDual conjunct of the re-cut bundle. The residues are the SAME three as hlevel's, read at the dual order s′ and carrying the one extra factor cgTestConstBase d s s′ p′.