AssemblyArith

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

1. The two σ square-root moves

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_mul_inv_eq_sqrt_inv {a : ℝ} (ha : 0 < a) : √a * a⁻¹ = √a⁻¹

√a · a⁻¹ = √(a⁻¹): the move that turns the boundary Caccioppoli prefactor's σ^{1/2} against the datum pricing's λ^{-1} ≤ K σ^{-1} into the force leg's σ^{-1/2}.

2. Two numerals

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_two_two_eq_four : Real.rpow 2 2 = 4

2^2 = 4, read on Real.rpow.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_two_three_eq_eight : Real.rpow 2 3 = 8

2^3 = 8, read on Real.rpow.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_two_threeHalves_le_three : Real.rpow 2 (3 / 2) ≤ 3

2^{3/2} ≤ 3. Proved by squaring, with the transcendental atom made opaque before the nonlinear step.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_two_half_le_two : Real.rpow 2 (1 / 2) ≤ 2

2^{1/2} ≤ 2. Same pattern.

3. The pin's canonical s-powers

theorem Algsuperdiff.Section4.Provider.ExcessDecay.pin_force_sq {s : ℝ} (hs : 0 < s) : (s / 2).rpow (-(3 / 2)) * (s / 2).rpow (-(3 / 2)) = 8 * s.rpow (-3)

Rows 4/5, canonical form. (s/2)^{-3/2} · (s/2)^{-3/2} = 8 s^{-3}; against the envelope's s^{-4} this is the frozen force leg s^{-7}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.pin_gradh_prod {s : ℝ} (hs : 0 < s) : (s / 2).rpow (-(3 / 2)) * (s / 2).rpow (-(1 / 2)) = 4 * s.rpow (-2)

Row 6, canonical form — the leg that fits the frozen display at equality. (s/2)^{-3/2} · (s/2)^{-1/2} = 4 s^{-2}; against the envelope's s^{-4} this is exactly 4 s^{-6}, the frozen display's legs 4 and 5, with no slack in the exponent.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.pin_force_cube {s : ℝ} (hs : 0 < s) : (s / 2).rpow (-3) = 8 * s.rpow (-3)

Row 4, canonical form. (s/2)^{-3} = 8 s^{-3}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.pin_force_half_le {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : (s / 2).rpow (-(3 / 2)) ≤ 3 * s.rpow (-3)

Row 2, canonical form (with slack). (s/2)^{-3/2} ≤ 3 s^{-3} on s ∈ (0,1].

theorem Algsuperdiff.Section4.Provider.ExcessDecay.pin_gradh_half_le {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : (s / 2).rpow (-(1 / 2)) ≤ 2 * s.rpow (-2)

Row 1, canonical form (with slack). (s/2)^{-1/2} ≤ 2 s^{-2} on s ∈ (0,1].

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_half_le_neg_two {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : s.rpow (-(1 / 2)) ≤ s.rpow (-2)

Row 3, canonical form (with slack). s^{-1/2} ≤ s^{-2}: the datum pricing's crude datum leg proves inside the frozen display's fifth leg.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.one_le_rpow_neg_two {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : 1 ≤ s.rpow (-2)

1 ≤ s^{-2} on s ∈ (0,1]: the s-power-free data Poincaré leg proves inside the frozen display's fifth leg.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_four_mul_neg_two {s : ℝ} (hs : 0 < s) : s.rpow (-4) * s.rpow (-2) = s.rpow (-6)

The envelope's s^{-4} against the canonical s^{-2}: the frozen display's legs 4 and 5.

4. The boundary energy assembly, on abstract letters

theorem Algsuperdiff.Section4.Provider.ExcessDecay.five_leg_bound {K c1 c2 c3 c4 c5 L1 L2 L3 L4 L5 T : ℝ} (hT : T ≤ c1 * L1 + c2 * L2 + c3 * L3 + c4 * L4 + c5 * L5) (h1 : c1 ≤ K) (h2 : c2 ≤ K) (h3 : c3 ≤ K) (h4 : c4 ≤ K) (h5 : c5 ≤ K) (hL1 : 0 ≤ L1) (hL2 : 0 ≤ L2) (hL3 : 0 ≤ L3) (hL4 : 0 ≤ L4) (hL5 : 0 ≤ L5) : T ≤ K * (L1 + L2 + L3 + L4 + L5)

Raising a five-leg bound to a joint constant.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.five_leg_bound_errorWeighted {K C E L1 L2 L3 L4 L5 T : ℝ} (hK : 0 ≤ K) (hE : E ≤ C) (hL1 : 0 ≤ L1) (hL2 : 0 ≤ L2) (hL3 : 0 ≤ L3) (hL4 : 0 ≤ L4) (hL5 : 0 ≤ L5) (hT : T ≤ K * (L1 + L2 + L3 + E * L4 + L5)) : T ≤ K * max 1 C * (L1 + L2 + L3 + L4 + L5)

Cap one error-weighted leg and enlarge a joint five-leg constant.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_energy_arith {T alpha beta rs ri sig sK KR CG1 CG2 CB2 gP dd D3 sd negC Cbg Cgw P2 Q3s Sm3 Sm2 X S H Gs Hs p32 p12 p3 low lamInv Bg Hn negf DirG DirB : ℝ} (halpha : 0 ≤ alpha) (hbeta : 0 ≤ beta) (hrs : 0 ≤ rs) (hri : 0 ≤ ri) (hsK : 0 ≤ sK) (hKR : 0 ≤ KR) (hCG1 : 0 ≤ CG1) (hCB2 : 0 ≤ CB2) (hgP : 0 ≤ gP) (hdd : 0 ≤ dd) (hD3 : 0 ≤ D3) (hsd : 0 ≤ sd) (hCbg : 0 ≤ Cbg) (hCgw : 0 ≤ Cgw) (hQ3s : 0 ≤ Q3s) (hSm2 : 0 ≤ Sm2) (hH : 0 ≤ H) (hGs : 0 ≤ Gs) (hHs : 0 ≤ Hs) (hp32 : 0 ≤ p32) (hp3 : 0 ≤ p3) (hBg0 : 0 ≤ Bg) (hHn0 : 0 ≤ Hn) (hDirG0 : 0 ≤ DirG) (hsig : 0 < sig) (hrsri : rs * ri = 1) (hrssig : rs * sig⁻¹ = ri) (hsKsq : sK * sK = KR) (hpp3 : p32 * p32 = 8 * Sm3) (hpp2 : p32 * p12 = 4 * Sm2) (hp3eq : p3 = 8 * Sm3) (hp32le : p32 ≤ 3 * Sm3) (hp12le : p12 ≤ 2 * Sm2) (hone : 1 ≤ Sm2) (hlowle : low ≤ sK * ri) (hlamInvle : lamInv ≤ KR * sig⁻¹) (hBgle : Bg ≤ Cbg * Q3s * (Cgw * Gs)) (hHnle : Hn ≤ sd * D3 * H) (hnegfle : negf ≤ negC * Sm2) (hnegC : 0 ≤ negC) (hDirGle : DirG ≤ CG2 * p32 * (sK * ri) * (Cbg * Q3s * (Cgw * Gs)) + CG2 * p12 * (sK * rs) * (sd * D3 * H + Cbg * Q3s * (Cgw * Hs))) (hDirBle : DirB ≤ CB2 * p32 * (sK * ri) * (Cbg * Q3s * (Cgw * Gs)) + CB2 * p12 * (sK * rs) * (sd * D3 * H + Cbg * Q3s * (Cgw * Hs))) (hmain : T ≤ alpha * rs * (P2 * (D3 * X) + P2 * S + gP * (dd * (D3 * H)) + CG1 * (p32 * low * DirG + p3 * lamInv * Bg + negf * Hn)) + beta * DirB) : T ≤ alpha * D3 * (rs * P2 * X) + alpha * (rs * P2 * S) + (8 * alpha * CG1 * CG2 * KR * Cbg * Cgw + 8 * alpha * CG1 * KR * Cbg * Cgw + 3 * beta * CB2 * sK * Cbg * Cgw) * (Sm3 * ri * Q3s * Gs) + (4 * alpha * CG1 * CG2 * KR * Cbg * Cgw + 2 * beta * CB2 * sK * Cbg * Cgw) * (Sm2 * rs * Q3s * Hs) + (alpha * gP * dd * D3 + 4 * alpha * CG1 * CG2 * KR * sd * D3 + negC * alpha * CG1 * sd * D3 + 2 * beta * CB2 * sK * sd * D3) * (Sm2 * rs * H)

The boundary energy assembly's arithmetic.

T is the square root of the boundary Caccioppoli's left-hand side, alpha rs its prefactor after the two coarse caps, beta the direct Dirichlet-energy prefactor, and the remaining letters are the atoms of the parent-L² pricing, the composed datum pricing and the two Dirichlet-energy legs (all of them nonnegative reals). The conclusion prices T onto the five canonical legs

  rs P2 X ,   rs P2 S ,   Sm3 ri Q3s Gs ,   Sm2 rs Q3s Hs ,   Sm2 rs H ,

which are exactly the shapes the σ-frame division turns into the frozen display's first, scalar, force, [∇h] and ‖∇h‖ legs.

5. The five-summand absorption of the boundary composition

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_absorb {Cf C A A' B B' T3 T4 T5 : ℝ} (hAA' : A ≤ A') (hA' : 0 ≤ A') (hBB' : B ≤ 4 * B') (hB' : 0 ≤ B') (hT3 : 0 ≤ T3) (hT4 : 0 ≤ T4) (hT5 : 0 ≤ T5) (hCf : 0 ≤ Cf) (h1 : Cf ≤ C) (h4 : 4 * Cf ≤ C) : Cf * (A + B + T3 + T4 + T5) ≤ C * (A' + B' + T3 + T4) + C * T5

The boundary re-cut absorption.

The composed boundary bound carries five legs: the flux-weighted L² leg A, the force leg B (at the σ_{n+3} index), the two ∇h legs T3, T4, and the open scalar's leg T5. The frozen display takes A inside its first bracket (A ≤ A', the bracket's companion being nonnegative), pays the σ gap-3 factor 4 on the force leg, and carries T3, T4 unchanged; T5 is the successor leg.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_five_term_bound_errorWeighted (CE KE kappa cg A1 : ℝ) : A1 = cg * 216 * (kappa * KE) → 0 ≤ A1 → ∀ (s : ℝ), 0 < s → ∀ (S Erep : ℝ), Erep ≤ CE * (1 / 2) → 0 ≤ Erep → ∀ (sig X Gs Hs Hn P2 Q3s Q1s R3n S4 S7 S6 Sm3 Sm2 : ℝ), 0 ≤ X → 0 ≤ Gs → 0 ≤ Hs → 0 ≤ S → 0 ≤ Q3s → 0 ≤ R3n → 0 ≤ Sm3 → 0 ≤ Sm2 → 0 ≤ sig⁻¹ → sig⁻¹ * sig = 1 → s⁻¹ ^ 4 = S4 → S4 * Sm3 = S7 → S4 * Sm2 = S6 → R3n * P2 ≤ 1 → R3n * Q3s ≤ 9 * Q1s → sig⁻¹ * R3n * (cg * (216 * s⁻¹ ^ 4 * (kappa * KE * Erep * (sig * (P2 * X) + sig * (P2 * S) + Sm3 * (Q3s * Gs) + Sm2 * (sig * (Q3s * Hs)) + Sm2 * (sig * Hn))))) ≤ A1 * (S4 * Erep * X) + 9 * (CE * (1 / 2)) * A1 * (S7 * sig⁻¹ * Q1s * Gs) + 9 * (CE * (1 / 2)) * A1 * (S6 * Q1s * Hs) + A1 * (S6 * Erep * R3n * Hn) + A1 * (S4 * Erep * S)

Five-term frame estimate retaining the representative error in the flat leg.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_five_term_bound (CE KE kappa cg A1 : ℝ) : A1 = cg * 216 * (kappa * KE) → 0 ≤ A1 → ∀ (s : ℝ), 0 < s → ∀ (S Erep : ℝ), Erep ≤ CE * (1 / 2) → 0 ≤ Erep → ∀ (sig X Gs Hs Hn P2 Q3s Q1s R3n S4 S7 S6 Sm3 Sm2 : ℝ), 0 ≤ X → 0 ≤ Gs → 0 ≤ Hs → 0 ≤ Hn → 0 ≤ S → 0 ≤ Q3s → 0 ≤ R3n → 0 ≤ Sm3 → 0 ≤ Sm2 → 0 ≤ sig⁻¹ → sig⁻¹ * sig = 1 → s⁻¹ ^ 4 = S4 → S4 * Sm3 = S7 → S4 * Sm2 = S6 → R3n * P2 ≤ 1 → R3n * Q3s ≤ 9 * Q1s → sig⁻¹ * R3n * (cg * (216 * s⁻¹ ^ 4 * (kappa * KE * Erep * (sig * (P2 * X) + sig * (P2 * S) + Sm3 * (Q3s * Gs) + Sm2 * (sig * (Q3s * Hs)) + Sm2 * (sig * Hn))))) ≤ A1 * (S4 * Erep * X) + 9 * (CE * (1 / 2)) * A1 * (S7 * sig⁻¹ * Q1s * Gs) + 9 * (CE * (1 / 2)) * A1 * (S6 * Q1s * Hs) + CE * (1 / 2) * A1 * (S6 * R3n * Hn) + A1 * (S4 * Erep * S)

Capped specialization of the error-weighted five-term frame estimate.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_comparison_bounds_errorWeighted (CE KE kappa cg A1 : ℝ) : A1 = cg * 216 * (kappa * KE) → 0 ≤ A1 → ∀ (s : ℝ), 0 < s → ∀ (n : ℤ), s ≤ 1 → ∀ (S Erep : ℝ), Erep ≤ CE * (1 / 2) → 0 ≤ Erep → ∀ (sig X Gs Hs Hn P2 : ℝ), P2 = Real.rpow 3 (-↑(n + 2)) → ∀ (Q3s : ℝ), Q3s = Real.rpow 3 (s * ↑(n + 2)) → ∀ (Q3sn : ℝ), Q3sn = Real.rpow 3 (s * ↑n) → ∀ (Q1s : ℝ), Q1s = Real.rpow 3 ((1 + s) * ↑n) → ∀ (R3n : ℝ), R3n = Real.rpow 3 ↑n → ∀ (S4 S7 S6 Sm3 Sm2 : ℝ), 0 ≤ X → 0 ≤ Gs → 0 ≤ Hs → 0 ≤ S → 0 ≤ Q3s → 0 ≤ R3n → 0 ≤ Sm3 → 0 ≤ Sm2 → 0 ≤ sig⁻¹ → sig⁻¹ * sig = 1 → s⁻¹ ^ 4 = S4 → S4 * Sm3 = S7 → S4 * Sm2 = S6 → R3n * Q3sn = Q1s ∧ sig⁻¹ * R3n * (cg * (216 * s⁻¹ ^ 4 * (kappa * KE * Erep * (sig * (P2 * X) + sig * (P2 * S) + Sm3 * (Q3s * Gs) + Sm2 * (sig * (Q3s * Hs)) + Sm2 * (sig * Hn))))) ≤ A1 * (S4 * Erep * X) + 9 * (CE * (1 / 2)) * A1 * (S7 * sig⁻¹ * Q1s * Gs) + 9 * (CE * (1 / 2)) * A1 * (S6 * Q1s * Hs) + A1 * (S6 * Erep * R3n * Hn) + A1 * (S4 * Erep * S)

The five-term boundary estimate with its triadic frame weights exposed.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_force_correction_bounds (B correction window b0 cg A2 : ℝ) : A2 = cg * 1944 * (b0 * (B * window)) → 0 ≤ A2 → ∀ (A3 : ℝ), A3 = correction * window → 0 ≤ A3 → ∀ (s S Erep : ℝ), 0 ≤ Erep → ∀ (sig X Gs Hs Hn Q3sn Q1s R3n S4 S7 S6 : ℝ), 0 ≤ X → 0 ≤ Gs → 0 ≤ Hs → 0 ≤ Hn → 0 ≤ S → 0 ≤ Q1s → 0 ≤ R3n → 0 ≤ S4 → 0 ≤ S7 → 0 ≤ S6 → 0 ≤ sig⁻¹ → s⁻¹ ^ 6 = S6 → S6 ≤ S7 → s.rpow (-(1 / 2)) ≤ S7 → R3n * Q3sn = Q1s → sig⁻¹ * R3n * (cg * (1944 * s⁻¹ ^ 6 * (b0 * (B * Q3sn * (window * Gs))))) ≤ A2 * (S7 * sig⁻¹ * Q1s * Gs) ∧ sig⁻¹ * R3n * (correction * s.rpow (-(1 / 2)) * Q3sn * (window * Gs)) ≤ A3 * (S7 * sig⁻¹ * Q1s * Gs) ∧ 0 ≤ S4 * Erep * X ∧ 0 ≤ S4 * Erep * S ∧ 0 ≤ S7 * sig⁻¹ * Q1s * Gs ∧ 0 ≤ S6 * Q1s * Hs ∧ 0 ≤ S6 * Erep * R3n * Hn

Force and correction estimates for an arbitrary boundary window coefficient.

Complete weighted boundary assembly

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_composed_comparison_bounds_errorWeighted (besov correction window CE KE kappa b0 cg A1 : ℝ) : 0 ≤ A1 → A1 = cg * 216 * (kappa * KE) → ∀ (A2 : ℝ), 0 ≤ A2 → A2 = cg * 1944 * (b0 * (besov * window)) → ∀ (A3 : ℝ), 0 ≤ A3 → A3 = correction * window → ∀ (s : ℝ), 0 < s → ∀ (n : ℤ), s ≤ 1 → ∀ (S : ℝ), 0 ≤ S → ∀ Erep ≤ CE * (1 / 2), 0 ≤ Erep → ∀ (sig : ℝ), 0 ≤ sig⁻¹ → ∀ (X : ℝ), 0 ≤ X → ∀ (Gs : ℝ), 0 ≤ Gs → ∀ (Hs : ℝ), 0 ≤ Hs → ∀ (Hn : ℝ), 0 ≤ Hn → ∀ (P2 : ℝ), P2 = Real.rpow 3 (-↑(n + 2)) → ∀ (Q3s : ℝ), 0 ≤ Q3s → Q3s = Real.rpow 3 (s * ↑(n + 2)) → ∀ (Q3sn : ℝ), Q3sn = Real.rpow 3 (s * ↑n) → ∀ (Q1s : ℝ), 0 ≤ Q1s → Q1s = Real.rpow 3 ((1 + s) * ↑n) → ∀ (R3n : ℝ), 0 ≤ R3n → R3n = Real.rpow 3 ↑n → ∀ (S4 : ℝ), 0 ≤ S4 → S4 = s.rpow (-4) → ∀ (S7 : ℝ), 0 ≤ S7 → S7 = s.rpow (-7) → ∀ (S6 : ℝ), 0 ≤ S6 → S6 = s.rpow (-6) → ∀ (Sm3 : ℝ), 0 ≤ Sm3 → ⋯

Composite comparison and nonnegativity bounds for arbitrary Besov, correction and window coefficients, with the triadic and exponent conversions shared.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_composed_absorption_errorWeighted {prefactor coarse energy force correction CE A1 A2 A3 L1 L2 L3 L4 L5 : ℝ} (hA1 : 0 ≤ A1) (hA2 : 0 ≤ A2) (hA3 : 0 ≤ A3) (hCE2 : 0 ≤ 9 * (CE * (1 / 2)) * A1) (hCE3 : 0 ≤ CE * (1 / 2) * A1) (hL1 : 0 ≤ L1) (hL2 : 0 ≤ L2) (hL3 : 0 ≤ L3) (hL4 : 0 ≤ L4) (hL5 : 0 ≤ L5) (hEnergy : prefactor * (coarse * energy) ≤ A1 * L1 + 9 * (CE * (1 / 2)) * A1 * L2 + 9 * (CE * (1 / 2)) * A1 * L3 + A1 * L4 + A1 * L5) (hForce : prefactor * (coarse * force) ≤ A2 * L2) (hCorrection : prefactor * correction ≤ A3 * L2) : prefactor * (coarse * (energy + force) + correction) ≤ (A1 + 9 * (CE * (1 / 2)) * A1 + CE * (1 / 2) * A1 + A2 + A3 + 1) * (L1 + L2 + L3 + L4 + L5)

Combine the energy, force and correction bounds and absorb their five nonnegative legs into the original joint coefficient. All scalar inputs are arbitrary.