HomSchauderUniform

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

The s-UNIFORM Schauder constant, and the K_abs frame condition it closes

The trap

The §4.5 Step-4 Schauder constant C_S4(d,s) is a Classical.choose of an s-indexed existential. Its defining property is UPWARD CLOSED in the constant, so nothing in the tree bounds the chosen value: the frame condition

  spineClauseConst d s p C_w (C_S4 d s) ≤ K_abs

can be met at each fixed s, but NOT by one K_abs produced before the model — and at the §4.5 pin s = |log γ|⁻¹ the exponent is a function of the model. That is a genuine obstruction to Theorem B's constant scope, not a bookkeeping nuisance.

The s = 1/2 reduction

The underlying producer's constant does not depend on s at all (Section4.Provider.Schauder.cube_schauder_of_zeroDatumCubeSchauder returns 2·C₀ + 1 with C₀ the zero-datum constant), and the s-package is in any case a consequence of the s = 1/2 package on a triadic cube: on □_m the two points of a Hölder difference are at distance at most 3^m, so

  [f]_{C^{0,s}(□_m)} ≤ 3^{m(1/2 - s)} [f]_{C^{0,1/2}(□_m)},

and the target's own weight 3^{-sm} absorbs the factor EXACTLY: multiplying the s = 1/2 gauge estimate by 3^{m(1/2-s)} turns 3^{-m/2}K_sup + K_Höl ≤ C 3^{-m/2} ⟨data⟩ into 3^{-sm}K_sup + 3^{m(1/2-s)}K_Höl ≤ C 3^{-sm} ⟨data⟩, with the SAME C.

exists_comparator_schauder_package_uniform is that statement, and stepFourSchauderConstU d is its s-free constant. spineClauseConst_le_abs then closes the frame condition at a K_abs naming only d and an envelope for C_w — both available before the model.

Scope

The §4.5 bundle core refers to C_S4(d, s.1) inside its hKabs conjunct, so consuming the uniform constant requires a SIBLING of that bundle (and of the re-cut's two consumption sites, which spend hKabs through spineClauseConst) with C_S4(d, s.1) replaced by stepFourSchauderConstU d. That re-cut is NOT performed here; what is proved here is that the replacement is sound — the uniform constant satisfies the same package at every admissible s.

1. The Hölder order step

theorem Algsuperdiff.Section4.Provider.Homogenization.holderSeminormBoundOn_order_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {alpha beta K D : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hle : beta ≤ alpha) (hK : 0 ≤ K) (hD : 0 < D) (hdiam : ∀ x ∈ U, ∀ y ∈ U, ‖x - y‖ ≤ D) (h : Support.HolderSeminormBoundOn U alpha K f) : Support.HolderSeminormBoundOn U beta (K * D ^ (alpha - beta)) f

The Hölder order step on a bounded set. Lowering the exponent from α to β ≤ α costs exactly the (α-β)-th power of the diameter.

2. The s-uniform package

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_comparator_schauder_package_uniform {d : ℕ} (dimension : 2 ≤ d) : ∃ (Csch : ℝ), 0 < Csch ∧ ∀ (s : ℝ), 0 < s → s ≤ 1 / 2 → ∀ (m : ℤ) (sigma : ℝ), 0 < sigma → ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (Kg KhInf Kh : ℝ), Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → ∃ (v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) (HCPolySupport.originCube d m) v h g ∧ ∃ (Ksup : ℝ) (KHol : ℝ), 0 ≤ Ksup ∧ 0 ≤ KHol ∧ (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖v.grad x‖ ≤ Ksup) ∧ Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s KHol v.grad ∧ wsInftyGauge (HCPolySupport.originCube d m) s Ksup KHol ≤ Csch * (Real.rpow 3 (s * ↑m))⁻¹ * dataBracket sigma (Real.rpow 3 (↑m / 2)) Kg KhInf Kh

THE s-UNIFORM SCHAUDER PACKAGE.

One constant, produced before the exponent s, the scale m, the diffusivity and the data, serving the whole admissible range 0 < s ≤ 1/2: the comparator of HomStepFourSchauder.exists_comparator_schauder_package at the SAME constant for every s.

The proof runs the s = 1/2 package once and lowers the Hölder exponent on □_m; the loss 3^{m(1/2-s)} is exactly cancelled by the gauge's own 3^{-sm}, so no constant is spent.

3. The s-free constant and the K_abs closure

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.stepFourSchauderConstU (d : ℕ) : ℝ

THE s-UNIFORM SCHAUDER CONSTANT. Unlike the s-indexed Step-4 Schauder constant, this is a Classical.choose of an s-FREE existential, so it is a function of d alone.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.stepFourSchauderConstU d = if h : 2 ≤ d then Classical.choose ⋯ else 0

theorem Algsuperdiff.Section4.Provider.Homogenization.stepFourSchauderConstU_pos {d : ℕ} (hd : 2 ≤ d) : 0 < stepFourSchauderConstU d

theorem Algsuperdiff.Section4.Provider.Homogenization.stepFourSchauderConstU_nonneg (d : ℕ) : 0 ≤ stepFourSchauderConstU d

theorem Algsuperdiff.Section4.Provider.Homogenization.spineClauseConst_le_abs (d : ℕ) {s p Cw Cw0 : ℝ} (hCw : 0 ≤ Cw) (hCwle : Cw ≤ Cw0) (hguard : s + ↑d / p ≤ 1 / 2) : spineClauseConst d s p Cw (stepFourSchauderConstU d) ≤ (2 * stepFourSchauderConstU d + 288 * ↑d ^ 2) * Cw0

THE K_abs FRAME CONDITION, CLOSED BEFORE THE MODEL.

At the uniform Schauder constant, the absorbed-constant condition of the re-cut bundle holds at

  K_abs:= (2 · stepFourSchauderConstU d + 288 d²) · C_w⁰,

which names only the dimension and an envelope C_w⁰ for the pairing constant — no s, hence no model. The only s-dependence of spineClauseConst is the lifting factor liftGeomFactor (s + d/p), and the bundle's OWN guard s + d/p ≤ 1/2 bounds it by 3.