RootClauseAEndpointC1Floor

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

1. The parametric clause-(B) lane in the RootDisplayClauseBAe slot

theorem Algsuperdiff.Section4.Provider.Regularity.clauseB_endpoint_as_clauseBAe_floor (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar Crg : ℝ) (hcstar : 0 < cstar) (hCrg : 0 < Crg) : ∃ (Cfl : ℝ) (Citer : ℝ) (Cest : ℝ) (k : ℕ), 1 ≤ Cfl ∧ 0 ≤ Cest ∧ 11 ≤ k ∧ ∀ (Cedos : ℝ), Cfl ≤ Cedos → ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - Crg * √M.gamma → RootDisplayClauseBAe M (stepOneC1 d Cedos 1 Citer k) Cest alpha

The parametric clause-(B) endpoint, restated in RootDisplayClauseBAe.

rootClauseB_display_offGrid_final_floor with its ∀ n L, n ≤ m → m ≤ L → payload → … prefix reordered into the slot's ∀ n, n ≤ m → payload → ∀ L, m ≤ L → …. A pure binder move.

2. The re-cut endpoint

theorem Algsuperdiff.Section4.Provider.Regularity.anomalous_regularity_provider_of_boundaryClauseAC1Floor (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar Crg : ℝ) (hcstar : 0 < cstar) (hCrg : 0 < Crg) (hbdry : ∀ (Citer : ℝ) (k : ℕ), 11 ≤ k → ∃ (CflA : ℝ), 1 ≤ CflA ∧ ∀ (Cedos : ℝ), CflA ≤ Cedos → ∃ (CestA : ℝ) (gamma0A : ℝ) (CrgA : ℝ), 0 ≤ CestA ∧ 0 < gamma0A ∧ 0 < CrgA ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0A → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - CrgA * √M.gamma → RootDisplayClauseABoundaryC1Ae M (stepOneC1 d Cedos 1 Citer k) CestA alpha) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ n ≤ m, X omega ≤ ↑(m - n).toNat → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg) + ENNReal.ofReal (√↑(Section3.Annealed.sigmaBar M m) * Real.rpow 3 (↑m / 2) * Kh)) ∧ (x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg)))

t.regularity from clause (B) and the boundary clause (A).

anomalous_regularity_provider_of_boundaryClauseAC1 with the ONE named conditional asked at its own parameters: the boundary producer receives (C_iter, k), answers with a C_edos-floor, and the endpoint runs both lanes at the max of the two floors, at C_annp = 1. Everything else — the minimal scale, its measurability and tail, the γ₀ min-merge, the α-range max-merge, the off-grid transfer — is verbatim.

hbdry is a carried mathematical obligation, NOT a source premise: it is the printed estimate itself at the centres offGridCentre n x ∉ □_{m-1}.