HomSpineDepthBandBudget

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

The produced clause constant, inside the frozen budget

What this file settles

HomSpineDepthBandInput produces the sup-form multiscale clause unconditionally at CA = (1 + C(d)·(near + 2·x₀⁻¹))^{1/p'}; HomSpineSupFormClauseAt displays the resulting clause constant as (√d · CA · C(p,d)).toReal. The frozen budget (HomSeamCompositionCcg) asks for exactly one inequality:

  Ccg(M) · GEOM(M) ≤ C_bud · |log γ|.

This file proves it, at the realization's own pin x₀ = s·p' with s = homS M = |log γ|⁻¹:

• gridDepthConverseConst_toReal_le — CA ≤ K(d,p) · (1 + x₀⁻¹)^{1/p'}, with K(d,p) = 1 + C(d)·near + 2·C(d) a MODEL-FREE numeral: the whole model dependence of CA is the far-band factor, and nothing else;
• recutDepthBandPin — the two-sided pin holds at s = homS M, x₀ = s·p' (the lower half by equality, the upper half by s ≤ 1/4 and p' ≤ 4/3);
• seamProducedCcg_le_budget — the product with the energy factor, closed by the two-factor inequality HomSeamBudgetArith.recut_geomBudget_le_absLog (GEOM · far ≤ 2|log γ|).

So the frozen display's one extra |log γ| pays for BOTH machine-pinned costs of realizing Step 3 at p = 4d, with the budget constant √d·K·C(p,d)·2.

1. The dimensional Gagliardo constant, as a real

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConstReal (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : ℝ

The real behind HomSpineDepthBandInput.gridDepthGagliardoConst.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConstReal d p = 2 ^ p.conjugate.exponent.toReal * (2 ^ (d + 3) * (↑d + 1) * 3 ^ d)

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConstReal_nonneg (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : 0 ≤ gridDepthGagliardoConstReal d p

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthGagliardoConst_eq_ofReal (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : gridDepthGagliardoConst d p = ENNReal.ofReal (gridDepthGagliardoConstReal d p)

2. CA is the far-band factor times a MODEL-FREE numeral

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.gridDepthPinConst (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : ℝ

The model-free part of the dual-converse constant: K(d,p) = 1 + C(d)·near + 2·C(d).

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_gridDepthPinConst (d : ℕ) (p : HCPolySupport.FiniteLpExponent) : 1 ≤ gridDepthPinConst d p

theorem Algsuperdiff.Section4.Provider.Homogenization.gridDepthConverseConst_toReal_le (d : ℕ) (p : HCPolySupport.FiniteLpExponent) {x₀ : ℝ} (hx₀ : 0 < x₀) : (gridDepthConverseConst p (gridDepthGagliardoConst d p) x₀).toReal ≤ gridDepthPinConst d p * (1 + x₀⁻¹) ^ p.conjugate.exponent.toReal⁻¹

CA IS THE FAR-BAND FACTOR, UP TO A MODEL-FREE NUMERAL.

(1 + C(d)(near + 2x₀⁻¹))^{1/p'} ≤ K(d,p) · (1 + x₀⁻¹)^{1/p'}. All of the model dependence of the dual-converse constant sits in (1 + x₀⁻¹)^{1/p'}, which is EXACTLY the factor the two-factor budget controls.

3. The conjugate exponent at the §4.5 pin, and the two-sided pin

theorem Algsuperdiff.Section4.Provider.Homogenization.recutConjugate_le (d : ℕ) (hd1 : 1 ≤ d) : (recutExponent d hd1).conjugate.exponent.toReal ≤ 4 / 3

At p = 4d the conjugate exponent is at most 4/3.

theorem Algsuperdiff.Section4.Provider.Homogenization.recutDepthBandPin {d : ℕ} (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : DepthBandPin (recutExponent d hd1) (homS M * (recutExponent d hd1).conjugate.exponent.toReal) (recutOrderBase M hlog)

The two-sided pin holds at the realization's own order s = homS M, with x₀ = s·p': the lower half is an equality and the upper half is s·p' ≤ (1/4)·(4/3) ≤ 1/2.

4. THE BUDGET

theorem Algsuperdiff.Section4.Provider.Homogenization.seamProducedCcg_le_budget (d : ℕ) (hd1 : 1 ≤ d) (C : ENNReal) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : (ENNReal.ofReal √↑d * gridDepthConverseConst (recutExponent d hd1) (gridDepthGagliardoConst d (recutExponent d hd1)) (homS M * (recutExponent d hd1).conjugate.exponent.toReal) * C).toReal * coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (homS M / 4) ≤ √↑d * gridDepthPinConst d (recutExponent d hd1) * C.toReal * 2 * |Real.log M.gamma|

The produced clause constant is inside the frozen budget.

At the realization's pin x₀ = s·p', s = homS M, the constant produced by HomSpineSupFormClauseAt times the ℓ^p energy factor is at most (√d·K(d,p)·C(p,d)·2)·|log γ|. This is precisely the hypothesis hbud of HomSeamCompositionCcg.generator_renormalization_provider_final_of_supClauseAt.