HomSeamFluxFreeCcg

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

The ã core and its supply with the Ccg slot FREED

Why this file exists

The ã core, its supply and its producer were stated at the PINNED coarse-graining constant recutPinnedCcgFlux d p = (cgDualBoundConstFlux d p).toReal, and so were the two level lemmas they consume — even though HomSeamFluxLevelChain's own pairing chain (seamSplitOf_of_seam) is already stated at a FREE Ccg. A clause producer that delivers its own constant Ccg₀ therefore cannot enter the chain without a detour.

This file removes the detour: every statement below carries Ccg as a bare real, constrained only by

  0 ≤ Ccg                                  (the pairing chain's own use), and
  cgDualBoundConstFlux d p ≤ ofReal Ccg    (the bundle's own conjunct).

Both are monotone UP in Ccg, so a clause produced at any Ccg₀ composes at max Ccg₀ (recutPinnedCcgFlux d p); at Ccg = recutPinnedCcgFlux d p the statements are the pinned ones, with the second hypothesis discharged by cgDualBoundConstFlux_dominates_self.

NOTHING mathematical changes. The proofs use the pinned constant only through its nonnegativity and through that one domination; both are hypotheses here. In particular this file makes NO claim about which constant the multiscale clause can actually be produced at.

Disclosure

The lane's pairing constant is LINEAR in Ccg (both legs of pairCwOf are), so a Ccg that grows with the model grows C_w — and hence K_abs — by the same factor. Freeing the slot does not make a model-dependent Ccg free of charge; it only makes the entry point honest.

2. The two level conditions at a free Ccg

theorem Algsuperdiff.Section4.Provider.Homogenization.hlevelFluxAt_of_seam {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L : ℤ) (omega : Section3.Cutoff.CutoffSample d) (m : ℤ) (jn : ℕ) {sigmaBarM : ℝ} (hsig : 0 < sigmaBarM) {Cgap : ℝ} (Y : Section3.Cutoff.CutoffSample d → ENNReal) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Ccg Kg Kh KhInf S Cen0 Ktest : ℝ} (hCcg0 : 0 ≤ Ccg) (hs : 0 < homS M) (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (hCgap : 0 < Cgap) (hss2 : homS M < ↑s2) (hs2lt : ↑s2 < 1 / 2) (hs2gt : 1 / 2 - ↑d / p.exponent.toReal < ↑s2) (hs2gap : 5 < 10 * ↑s2 * Real.log 3) (hKtest0 : 0 ≤ Ktest) (hKg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g) (hKhInf0 : 0 ≤ KhInf) (hKh0 : 0 ≤ Kh) (hCen0 : 0 ≤ Cen0) (hjn : (HCPolySupport.originCube d m).scale - ↑jn = homN M m) (hSbound : S ≤ Cen0 * recutEnergyFactor M Y m omega * energyBracket sigmaBarM (Real.rpow 3 (↑m / 2)) Kg KhInf Kh) (hdom1 : ENNReal.ofReal (recutPinnedE1Flux M L omega m jn hsig (recutOrderBase M hlog)) ≤ Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homHalf (homSeamBase M hs)) omega) (hdom2 : ENNReal.ofReal (recutPinnedE2Flux M L omega m jn hsig (recutOrderBase M hlog)) ≤ ENNReal.ofReal √2 * Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homQuarterOf (homSeamBase M hs)) omega) (hfin : ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega ≠ ⊤) : coarseGrainingFinitePRHS Ccg (↑(recutOrderBase M hlog)) (↑s2) sigmaBarM (recutPinnedE1Flux M L omega m jn hsig (recutOrderBase M hlog)) (recutPinnedE2Flux M L omega m jn hsig (recutOrderBase M hlog)) (recutPinnedDg m s2 p g) S ((HCPolySupport.originCube d m).scale - ↑jn) ≤ sigmaBarM * (2 * pairCwOf d Ccg p s2 Cgap Cen0 (homS M) Ktest * (ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega).toReal * dataBracket sigmaBarM (Real.rpow 3 (↑m / 2)) Kg KhInf Kh)

hlevel AT A FREE Ccg, THE ã COEFFICIENT AND THE BASE s/8.

The seam's hlevel with the coarse-graining constant freed; the proof uses the pinned constant only through its nonnegativity.

3. The two monotonicity steps that make max compose

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingFinitePRHS_mono_ccg {Ccg Ccg' s s2 sigma E1 E2 Dg S : ℝ} (n : ℤ) (hCcg : Ccg ≤ Ccg') (hs : 0 < s) (hss2 : s < s2) (hE1 : 0 ≤ E1) (hDg : 0 ≤ Dg) (hS : 0 ≤ S) : coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S n ≤ coarseGrainingFinitePRHS Ccg' s s2 sigma E1 E2 Dg S n

The printed right-hand side is monotone UP in the coarse-graining constant, at the signs the bundle's own conjuncts carry.

theorem Algsuperdiff.Section4.Provider.Homogenization.cgDualBoundConstFlux_le_ofReal_of_pinned_le (d : ℕ) (hd : 2 ≤ d) (p : HCPolySupport.FiniteLpExponent) (hp2 : 2 ≤ p.exponent) {Ccg : ℝ} (hCcg : recutPinnedCcgFlux d p ≤ Ccg) : cgDualBoundConstFlux d p ≤ ENNReal.ofReal Ccg

The bundle's own Ccg conjunct at any constant above the pin: this is what makes max Ccg₀ (recutPinnedCcgFlux d p) an admissible entry point.