HomSeamSupClauseCcgFree

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

Seam supply at a model-dependent clause constant

The clause constant is explicit at each model. This module supplies three interfaces:

• RecutCoreSupplyFluxSupClauseAt: the sup-form clause at a constant Ccg;
• SeamMultiscaleSupClauseSupplyAt: its almost-sure supply at CcgF M;
• SeamSupplyFluxAtSupGradBudget: the energy and clause supply, together with the flux-corrected parent identification, at that same model-dependent constant.

seamSupplyFluxAtSupGradBudget_of_supClauseAt combines a clause supply with the regularity display. The downstream core in HomSeamSupClauseChain already carries Ccg freely, so seamBundleOfRegularityHalfSupGradBudget_of_supplyAt produces the budgeted seam bundle without fixing a numeral for this constant.

The pairing envelope is linear in Ccg and affine in C_en⁰, as proved by recutCwHalfEnvelope_affine. For positive exponents, one_le_coarseGrainingGeomFactor bounds the energy factor below by one. With this hypothesis, seamKabsAt_le_budget bounds the full constant from the product budget Ccg * GEOM ≤ C_bud * L.

1. The clause carrier and the supply, at a FREE Ccg

def Algsuperdiff.Section4.Provider.Homogenization.RecutCoreSupplyFluxSupClauseAt {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (hd1 : 1 ≤ d) (hlog : 4 ≤ |Real.log M.gamma|) (Ccg : ℝ) (omega : Section3.Cutoff.CutoffSample d) : Prop

THE SUP-FORM CLAUSE CARRIER AT A FREE Ccg.

The sup-form clause carrier of HomSeamSupClauseProvider with the numeral pin recutPinnedCcgFlux d p replaced by a parameter. NOTHING else changes — not a binder, not an order, not a constant.

Equations

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

def Algsuperdiff.Section4.Provider.Homogenization.SeamMultiscaleSupClauseSupplyAt (d : ℕ) (hd1 : 1 ≤ d) (cstar gamma0 : ℝ) (CcgF : Section3.ABKModel d → ℝ) : Prop

The sup-form clause, asked almost surely at every admissible model and scale, at a MODEL-DEPENDENT constant CcgF M.

Equations

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

2. The supply layer at CcgF

def Algsuperdiff.Section4.Provider.Homogenization.SeamSupplyFluxAtSupGradBudget (d : ℕ) (hd1 : 1 ≤ d) (cstar gamma0 : ℝ) (Cen0F CcgF : Section3.ABKModel d → ℝ) (Ctop Creg : ℝ) : Prop

The energy and clause supply at a model-dependent constant CcgF M, with the flux-corrected parent identification included in RecutCoreSupplyFluxAtSupGrad.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.seamSupplyFluxAtSupGradBudget_of_supClauseAt (d : ℕ) [NeZero d] (hd1 : 1 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) {gamma0in : ℝ} {CcgF : Section3.ABKModel d → ℝ} (hg0in : 0 < gamma0in) (hclause : SeamMultiscaleSupClauseSupplyAt d hd1 cstar gamma0in CcgF) : ∃ (gamma0 : ℝ) (Ctop : ℝ), 0 < gamma0 ∧ 0 ≤ Ctop ∧ ∀ (Creg : ℝ), 0 < Creg → SeamSupplyFluxAtSupGradBudget d hd1 cstar gamma0 (fun (M : Section3.ABKModel d) => Creg * 729 * coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (homS M / 4)) CcgF Ctop Creg

THE SUPPLY LAYER, FROM THE CLAUSE ALONE.

The supply layer of HomSeamSupClauseProvider at a free Ccg, with the flux-corrected parent identification (already unconditional) appended so that the output is the Ccg-free carrier RecutCoreSupplyFluxAtSupGrad.

3. K_abs at a free Ccg, and its budget

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.seamCwCen0Slope (d : ℕ) (hd1 : 1 ≤ d) : ℝ

The C_en⁰ slope of the pairing envelope: the envelope is AFFINE in C_en⁰ with this slope, at every Ccg.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.seamCwCen0Slope d hd1 = 2 * (1 + Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalfBound d hd1 * (7 / 8)⁻¹)

theorem Algsuperdiff.Section4.Provider.Homogenization.seamCwCen0Slope_nonneg (d : ℕ) (hd1 : 1 ≤ d) : 0 ≤ seamCwCen0Slope d hd1

theorem Algsuperdiff.Section4.Provider.Homogenization.recutCwHalfEnvelope_affine (d : ℕ) (hd1 : 1 ≤ d) (Ccg Cgap Cen0 : ℝ) : recutCwHalfEnvelope d hd1 Ccg Cgap Cen0 = Ccg * (Cen0 * seamCwCen0Slope d hd1 + recutCwHalfEnvelope d hd1 1 Cgap 0)

THE ENVELOPE IS LINEAR IN Ccg AND AFFINE IN C_en⁰. Every one of the four legs of recutCwHalfEnvelope carries Ccg exactly once, and only the two C_en⁰ legs carry C_en⁰.

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.seamKabsAt (d : ℕ) (hd1 : 1 ≤ d) (Cgap Ccg Cen0 : ℝ) : ℝ

K_abs AT A FREE Ccg. The half-gauge K_abs with the numeral pin freed; at the pin it IS that term.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.seamKabsAt_nonneg (d : ℕ) (hd1 : 1 ≤ d) {Cgap Ccg Cen0 : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) : 0 ≤ seamKabsAt d hd1 Cgap Ccg Cen0

theorem Algsuperdiff.Section4.Provider.Homogenization.seamKabsAt_le_budget (d : ℕ) (hd1 : 1 ≤ d) {Cgap : ℝ} (hCgap : 0 < Cgap) {Creg Ccg GEOM Cbud L : ℝ} (hCreg : 0 < Creg) (hCcg0 : 0 ≤ Ccg) (hGEOM1 : 1 ≤ GEOM) (hbud : Ccg * GEOM ≤ Cbud * L) : seamKabsAt d hd1 Cgap Ccg (Creg * 729 * GEOM) ≤ (2 * stepFourSchauderConstU d + 288 * ↑d ^ 2) * (Creg * 729 * seamCwCen0Slope d hd1 + recutCwHalfEnvelope d hd1 1 Cgap 0) * Cbud * L

THE BUDGET AT A FREE Ccg.

K_abs is inside C_abs·L as soon as the PRODUCT Ccg·GEOM is inside C_bud·L. The energy factor is at least 1, so the same input also controls the Ccg-only leg: no second budget hypothesis is needed.

4. The bundle, at CcgF

theorem Algsuperdiff.Section4.Provider.Homogenization.seamBundleOfRegularityHalfSupGradBudget_of_supplyAt (d : ℕ) [NeZero d] (hd : 2 ≤ d) {cstar gamma0 Cgap Ctop Creg : ℝ} {Cen0F CcgF : Section3.ABKModel d → ℝ} (hCgap : 0 < Cgap) (hCen0 : ∀ (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → 0 ≤ Cen0F M) (hCcg0 : ∀ (M : Section3.ABKModel d), 0 ≤ CcgF M) (hCcgDom : ∀ (M : Section3.ABKModel d), cgDualBoundConstFlux d (recutExponent d ⋯) ≤ ENNReal.ofReal (CcgF M)) (hsupply : SeamSupplyFluxAtSupGradBudget d ⋯ cstar gamma0 Cen0F CcgF Ctop Creg) : SeamBundleOfRegularityHalfSupGradBudget d cstar (min gamma0 (1 / 81)) Cgap (fun (M : Section3.ABKModel d) => seamKabsAt d ⋯ Cgap (CcgF M) (Cen0F M)) Ctop Creg

THE BUNDLE, AT A MODEL-DEPENDENT CLAUSE CONSTANT.

The budgeted bundle of HomSeamSupClauseSpine with the numeral pin replaced by CcgF M. The two facts the pin used to supply — 0 ≤ Ccg and C(p,d) ≤ ofReal Ccg — become hypotheses; every other step is unchanged, because the whole chain above RecutCoreSupplyFluxAtSupGrad already carries Ccg free.

5. The energy factor is at least one

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_coarseGrainingGeomFactor {p w : ℝ} (hp : 0 < p) (hw : 0 < w) : 1 ≤ coarseGrainingGeomFactor p w

The ℓ^p depth-aggregation energy factor (1-3^{-wp})^{-1/p} is at least 1: the base of the power is at least 1. This is what lets the ONE budget hypothesis Ccg·GEOM ≤ C_bud·L also control Ccg alone.