HomSeamGradProvider

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

The conditional provider, re-threaded: gradient binder, tail binder, Creg hoist

What this file supplies

The §4.5 energy supply has four obstructions. Three of them are ours; this file gives them:

• (α) the display's classical-gradient binder is threaded all the way to the top, where the frozen ROOT's OWN binder re-supplies it — the provider introduced it as _hgrad and discarded it;
• (β) the a.e. finiteness of the minimal scale becomes an explicit binder of the supply and is DISCHARGED here from the Theorem-C tail (ae_ne_top_of_regTail);
• (γ) the Theorem-C constant Creg is hoisted above the K_abs pin, so C_en⁰ — which is linear in Creg — may legally depend on it.

The source-facing hypothesis count is UNCHANGED: the threaded binder is the frozen root's own, and the tail binder is discharged, not assumed.

1. The minimal-scale tail kills the value ⊤

theorem Algsuperdiff.Section4.Provider.Homogenization.ae_ne_top_of_regTail {d : ℕ} (M : Section3.ABKModel d) {Cst : ℝ} (hCst : 1 ≤ Cst) (hs : 0 < homS M) {X : Section3.Cutoff.CutoffSample d → ℕ∞} (htail : ∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-((1 - homAlpha M) ^ 2 * (↑N - Cst)) / (Cst * M.gamma)))) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), X omega ≠ ⊤

THE X-TAIL BINDER, DISCHARGED.

HomProviderBAssembly.exists_regularity_minimalScale supplies, at every admissible model, the Theorem-C tail bound

  ∀ N, P[N ≤ X] ≤ C_st exp(-(1-α)²(N - C_st)/(C_st γ)).

Since 1 - α = s/2 > 0 and C_st γ > 0 the right-hand side is a geometric sequence with ratio exp(-(1-α)²/(C_st γ)) < 1, so it tends to 0 and the event {X = ⊤}, which sits inside every {N ≤ X}, is null. This is the binder the per-ω energy slot needs: off it the enlarged Y degenerates to ⊤ and the printed factor carries no information.