HomSeamClauseGeomProvider

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

The §4.5 conditional provider at the multiscale clause and the factor D3

What this file supplies

The §4.5 conditional provider reproduces the frozen root's conclusion verbatim from EXACTLY

  {0 < cstar, 0 < gamma0, 0 < Cgap, 0 ≤ GEOM}        -- numeral binders
  hclause: the multiscale coarse-graining clause, a.e., at the shape
  hgeom: one model-uniform bound for coarseGrainingGeomFactor (4d) (s/4)

and nothing else. C_en⁰, K_abs and C_top are no longer slots: they are the closed terms Creg · 729 · GEOM, recutKabsHalf d hd1 Cgap (Creg · 729 · GEOM) and seamTopScaleConst d C_step, pinned INSIDE the proof after exists_regularity_minimalScale has produced the model-free Creg.

hgeom is item D3 and nothing else: it is exhibited as a hypothesis, not assumed away. Nothing here asserts that it holds.

2. The Creg hoist: C_en⁰ split into Creg, a numeral, and D3

theorem Algsuperdiff.Section4.Provider.Homogenization.three_rpow_homAlpha_homK_le {d : ℕ} (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : 3 ^ ((1 - homAlpha M) * ↑(homK M)) ≤ 729

THE 3^{(1-α)k} FACTOR OF recutEnergySlotConst IS MODEL-FREE.

1 - α = s/2 = 1/(2|log γ|) and k = ⌈10|log γ|⌉ ≤ 10|log γ| + 1, so the exponent is at most 5 + 1/(2|log γ|) ≤ 41/8 ≤ 6 on the printed gate |log γ| ≥ 4. This is the half of C_en⁰ that carries no γ.

theorem Algsuperdiff.Section4.Provider.Homogenization.recutEnergySlotConst_le_of_geom {d : ℕ} {M : Section3.ABKModel d} (hd1 : 1 ≤ d) {Creg GEOM : ℝ} (hCreg : 0 ≤ Creg) (hlog : 4 ≤ |Real.log M.gamma|) (hgeom : coarseGrainingGeomFactor (recutExponent d hd1).exponent.toReal (homS M / 4) ≤ GEOM) : recutEnergySlotConst Creg (homAlpha M) (recutExponent d hd1).exponent.toReal (homS M) (homK M) ≤ Creg * 729 * GEOM

C_en⁰, SPLIT.

The energy-slot constant of the per-ω display is Creg · 3^{(1-α)k} · coarseGrainingGeomFactor (4d) (s/4). The middle factor is model-free (three_rpow_homAlpha_homK_le); the last factor is item D3, and it is the ONLY place a model-uniform input is needed.