HomSeamCompositionCcg

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

The composition target, at a MODEL-DEPENDENT clause constant

What this file does

The composition of HomSeamComposition reduced the frozen root to ONE object, but at the lane's NUMERAL clause constant recutPinnedCcgFlux d p — which the producing route cannot meet (CA ≍ |log γ|^{1-1/(4d)}). This file re-states the reduction at a model-dependent constant CcgF: ABKModel d → ℝ, subject to exactly the two things the lane actually needs of it:

  C(p,d) ≤ ofReal (CcgF M)                             -- the duality-leg pin
  CcgF M · GEOM(M) ≤ C_bud · |log γ|                    -- the budget

The second is exactly the shape of the two-factor budget HomSeamBudgetArith.recut_geomBudget_le_absLog (GEOM · (1 + (s·p')⁻¹)^{1/p'} ≤ 2|log γ|), so a producer whose constant is ≲ (1 + (s·p')⁻¹)^{1/p'} — which is what the unconditional sup-form multiscale clause of HomSpineDepthBandInput delivers at x₀ = s·p' — meets it.

The re-thread is a genuine widening: the pinned producer still drives the composition (its constant is model-free, and GEOM ≤ 2|log γ| is available), so it only enlarges the class of admissible producers.

1. The provider at a model-dependent clause constant

theorem Algsuperdiff.Section4.Provider.Homogenization.generator_renormalization_provider_final_of_supClauseAt (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) {gamma0 Cgap Cbud : ℝ} {CcgF : Section3.ABKModel d → ℝ} (hg0 : 0 < gamma0) (hCgap : 0 < Cgap) (hCbud : 0 ≤ Cbud) (hCcg0 : ∀ (M : Section3.ABKModel d), 0 ≤ CcgF M) (hCcgDom : ∀ (hd : 2 ≤ d) (M : Section3.ABKModel d), cgDualBoundConstFlux d (recutExponent d ⋯) ≤ ENNReal.ofReal (CcgF M)) (hbud : ∀ (hd : 2 ≤ d) (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → CcgF M * coarseGrainingGeomFactor (recutExponent d ⋯).exponent.toReal (homS M / 4) ≤ Cbud * |Real.log M.gamma|) (hclause : ∀ (hd : 2 ≤ d), NeZero d → SeamMultiscaleSupClauseSupplyAt d ⋯ cstar gamma0 CcgF) : GeneratorRenormalizationShape d cstar

THE FROZEN generator_renormalization BODY FROM A BUDGETED CLAUSE.

The provider at the sup-form clause, with the numeral Ccg pin freed. The hypothesis list is {0 < cstar, 0 < gamma0, 0 < Cgap, 0 ≤ Cbud} plus the three properties of CcgF and the clause supply — and NOTHING else. C_en⁰, C_top and the geometric factor are still closed terms pinned inside; K_abs is now the closed term seamKabsAt d hd1 C_gap (CcgF M) (C_en⁰(M)).

2. THE ONE REMAINING INPUT, at a budgeted constant

def Algsuperdiff.Section4.Provider.Homogenization.SupClauseProducerAtBudgeted (d : ℕ) (cstar : ℝ) : Prop

THE ONE REMAINING INPUT, RE-CUT.

An a.e. producer of the sup-form multiscale clause at SOME positive γ₀ and at SOME model-dependent constant meeting the duality pin and the budget. This is the composition's one remaining input with the Ccg slot freed.

Equations

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

3. THE COMPOSITION

theorem Algsuperdiff.Section4.Provider.Homogenization.generatorRenormalizationShape_of_supClauseProducerAtBudgeted (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) (h : SupClauseProducerAtBudgeted d cstar) : GeneratorRenormalizationShape d cstar

THE COMPOSITION, AT A BUDGETED CLAUSE CONSTANT.

The frozen conclusion, at every dimension and every cstar > 0, from the budgeted sup-form clause producer ALONE. C_gap is pinned to the numeral 1; C_en⁰, C_top and the geometric factor are closed terms pinned inside; K_abs is seamKabsAt d hd1 1 (CcgF M) (C_en⁰(M)).