HomSpineSupFormClause

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

The D1 re-cut, fork (iii): the SUP-over-depths clause carrier

Why a sup-over-depths carrier

The manuscript aggregates depths by SUP, not by ℓ^p. Its Step-3 display reads

  3^{-ms} σ_m ‖∇u - ∇v‖_{W_hat^{-s,∞}(□_m)}
    ≤ C s^{-1} σ_m^{1/2} 𝓔_{s₁,∞,1} ·
        sup_{k ≤ n} 3^{-(s-s₁)(n-k)} max_{z ∈ 3^k ℤ^d ∩ □_m}
          ν^{1/2} ‖∇u‖_{L²(z+□_k)}  +  (forcing term),

i.e. p = ∞ on BOTH sides. This repository's earlier clause carrier put the ℓ^p-over-depths aggregate on the left. That was a transcription choice, not the print's shape, and the refutation record (HomSpineCzGridGaugeRefuted) together with its |log γ|^{1/p} necessity are properties OF THAT CHOICE: the flat field's sup is O(1) while its ℓ^p aggregate is not.

This file gives the sup-over-depths sibling and the one fact that makes the re-cut worth doing:

• negBesovSupPartialNorm — sup_{j ≤ N} of the SAME per-depth gauge terms (negBesovLpDepthSeminorm) the ℓ^p carrier sums. No new geometry: the depth weight is the print's own 3^{-s j}.

• NegBesovSupGaugeBound — the unbounded-N form, ∀ j, which is exactly what every downstream consumer of the ℓ^p gauge actually uses (see HomSpineSupFormRethread).

• CoarseGrainingSupMultiscale — the clause sibling at the sup left-hand side, with the energy slot LEFT AT ITS ℓ^p SPELLING (that slot is where the finite-p CoarseGraining theorem enters; see the D3 section below). One caveat. The depth-j GLOBAL comparison named below is not realizable at a γ-uniform constant: there is a far-band Gagliardo cost Σ_{i<j} 3^{-i s p'} ≍ min(j, (s p')⁻¹) for the depth-j checkerboard test, saturating at ≈|log γ|^{1/p'} over the Step-3 depth range ⌈10|log γ|⌉. The print's carrier is per CELL, not per depth: the per-cell re-cut of §§1--4 reads the gauge at sup_j max_{R ∈ D_j} and needs only a single-CELL test. Everything here remains correct and is the intermediate reading (sup over depths of the ℓ^p cell mean); §5 (D3) is independent of the cut.

• NegativeBesovGridSmoothDualConverseAtDepth + ofReal_negBesovSupPartialNorm_le_of_depthConverse — THE CONSUMPTION INTERFACE. The sup-form clause needs the grid/smooth-dual comparison only ONE DEPTH AT A TIME; the depth-uniform constant CA is the only input, and no sum over depths is ever formed. This is the slot the single-depth single-depth dual test family fills; it is a NAMED INPUT here, never proved. So the supply's clause conjunct is producible at a γ-uniform constant exactly when CA is γ-uniform; the refuted depth-summed (★) is never used.

The D3 factor

coarseGrainingGeomFactor p w = (1 - 3^{-wp})^{-1/p} is the price the finite-p energy slot pays over the print's sup-form energy datum (the mesoscale energy bound). It is ≤ 3/2 with NO γ-dependence as soon as 1 ≤ w·p, and it is at least (w·p·log 3)^{-1/p} always, so on the complementary range w·p ≤ 1 it is genuinely of size (w p)^{-1/p}.

At the §4.5 pin w = s/4 this says: the factor is O(1) iff s·p ≳ 4, i.e. iff p is allowed to grow like |log γ|. So D3 is not a second, independent obstruction — it is the SAME question as item (a) (a p-uniform Calderón--Zygmund constant on a range reaching p ≈ 4/s), quantified.

1. The sup-over-depths gauge carrier

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.negBesovSupPartialNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (N : ℕ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : ℝ

The sup-over-depths partial gauge, sup_{j ≤ N} 3^{-sj} [·]_{depth j}.

The p = ∞ sibling of the ℓ^p-over-depths gauge: the SAME per-depth terms, with the outer ℓ^p sum replaced by the maximum. This is the aggregation shape the manuscript's W_hat^{-s,∞} display uses.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovSupPartialNorm_def {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (N : ℕ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : negBesovSupPartialNorm Q s p N F = (Finset.range (N + 1)).sup' ⋯ fun (j : ℕ) => negBesovLpDepthSeminorm Q s p F j

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm_le_negBesovSupPartialNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) {j N : ℕ} (hjN : j ≤ N) : negBesovLpDepthSeminorm Q s p F j ≤ negBesovSupPartialNorm Q s p N F

Every depth term the sup reaches is below it.

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovSupPartialNorm_le {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s p B : ℝ} {N : ℕ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : ∀ j ≤ N, negBesovLpDepthSeminorm Q s p F j ≤ B) : negBesovSupPartialNorm Q s p N F ≤ B

The sup is below any bound on the depth terms it reaches.

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovSupPartialNorm_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (N : ℕ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ negBesovSupPartialNorm Q s p N F

2. The unbounded-depth form, and its two equivalent readings

def Algsuperdiff.Section4.Provider.Homogenization.NegBesovSupGaugeBound {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p A : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

The sup-form gauge bound at level A: every depth term of the printed grid gauge is below A. This is 3^{-ms}[F]_{B^{-s}_{p,∞}(□_m)} ≤ A, the p = ∞ depth aggregation the manuscript's display carries.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.NegBesovSupGaugeBound Q s p A F = ∀ (j : ℕ), Algsuperdiff.Section4.Provider.Homogenization.negBesovLpDepthSeminorm Q s p F j ≤ A

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovSupGaugeBound_iff_forall_partial {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s p A : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} : NegBesovSupGaugeBound Q s p A F ↔ ∀ (N : ℕ), negBesovSupPartialNorm Q s p N F ≤ A

The two readings agree: a level for every truncation is a level for every depth.

theorem Algsuperdiff.Section4.Provider.Homogenization.NegBesovSupGaugeBound.nonneg {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s p A : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : NegBesovSupGaugeBound Q s p A F) : 0 ≤ A

3. The clause sibling at the sup left-hand side

def Algsuperdiff.Section4.Provider.Homogenization.CoarseGrainingSupMultiscale {d : ℕ} (Q : HCPolySupport.TriadicCube d) (jn : ℕ) (Ccg s s1 s2 p sigma E1 E2 Dg : ℝ) (Gen : HCPolySupport.TriadicCube d → ℝ) (Fgrad Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

THE SUP-FORM MULTISCALE CLAUSE — the print's own aggregation.

The transcribed multiscale clause with the left-hand ℓ^p-over-depths aggregate replaced by the sup, i.e. the manuscript's Step-3 display shape. The energy slot is deliberately LEFT at its ℓ^p spelling: that slot is the one the finite-p CoarseGraining theorem (exists_localCoarseGrainingLp) supplies, and moving it to the sup is the D3 question, not a transcription choice (section 5).

THIS IS A HYPOTHESIS. It is never proved in this repository.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.CoarseGrainingSupMultiscale.gradGauge {d : ℕ} {Q : HCPolySupport.TriadicCube d} {jn : ℕ} {Ccg s s1 s2 p sigma E1 E2 Dg : ℝ} {Gen : HCPolySupport.TriadicCube d → ℝ} {Fgrad Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : CoarseGrainingSupMultiscale Q jn Ccg s s1 s2 p sigma E1 E2 Dg Gen Fgrad Fflux) {S : ℝ} (hS : ∀ (N : ℕ), coarseGrainingEnergyPartial Q p (s - s1) jn N Gen ≤ S) (hsigma : 0 < sigma) : NegBesovSupGaugeBound Q s p (sigma⁻¹ * coarseGrainingFinitePRHS Ccg s s2 sigma E1 E2 Dg S (Q.scale - ↑jn)) Fgrad

The Step-3c leg of the sup-form clause.

The flux leg is discarded (the source's own route (ii) in the paper) and the printed σ_m weight stripped; the output is the sup-form gauge bound at the level the Step-3c consumers take.

4. THE CONSUMPTION INTERFACE: one depth at a time

def Algsuperdiff.Section4.Provider.Homogenization.NegativeBesovGridSmoothDualConverseAtDepth {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (j : ℕ) (CA : ENNReal) : Prop

The single-depth grid/smooth-dual comparison.

The depth-summed grid/smooth-dual converse asks for the FULL ℓ^p-over-depths Besov seminorm against the smooth dual — that is the shape refuted above, because the depth sum contributes (1-3^{-sp})^{-1/p}. The sup-form clause never forms that sum: it needs the comparison at ONE depth j at a time, with the constant CA uniform in j,

  ( 3^{sp(m-j)} avsum_{R ∈ D_j} ‖(F)_R‖^p )^{1/p}
      ≤ CA · ‖F‖_{W_hat^{-s,p}(□_m), smooth dual}.

THIS IS A HYPOTHESIS, and it is the ONLY external input of supGauge_of_depthConverse. It is the slot the single-depth dual-test family (a dual test family at one depth) fills: one test function per depth, not one test function per depth-tower.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_negBesovLpDepthSeminorm_le_of_depthConverse {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {CA : ENNReal} {j : ℕ} (hconv : NegativeBesovGridSmoothDualConverseAtDepth Q s p j CA) (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) : ENNReal.ofReal (negBesovLpDepthSeminorm Q (↑s) p.exponent.toReal F.toField j) ≤ ENNReal.ofReal (gridScaleGauge d (↑s) Q.scale) * (CA * HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s p F)

One depth term of this development gauge against the smooth dual.

The depth-j bridge ofReal_negBesovLpDepthSeminorm_rpow_le, rooted, composed with the single-depth comparison. No sum over depths occurs.

theorem Algsuperdiff.Section4.Provider.Homogenization.ofReal_negBesovSupPartialNorm_le_of_depthConverse {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) {CA : ENNReal} (N : ℕ) (hconv : ∀ (j : ℕ), NegativeBesovGridSmoothDualConverseAtDepth Q s p j CA) (F : HCPolySupport.CubeEuclideanLpField Q HCPolySupport.FiniteLpExponent.two) : ENNReal.ofReal (negBesovSupPartialNorm Q (↑s) p.exponent.toReal N F.toField) ≤ ENNReal.ofReal (gridScaleGauge d (↑s) Q.scale) * (CA * HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm Q s p F)

THE SUP-FORM GAUGE, FROM THE SINGLE-DEPTH COMPARISON ALONE.

Given the single-depth comparison at every depth with one constant CA, the whole sup-over-depths partial gauge is below √d · 3^{-sm} · CA times the smooth dual norm — with NO geometric factor and NO depth sum, because the sup is realized depth-wise.

This is the exact shape in which the sup-form clause consumes the family.