CoarseIndexBridges

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

G-small-1, G-small-2, G-M2: the r = s/2 pin's small bridges

Nothing here imports that file, and nothing here claims the anchor or any source node.

The three gaps this module closes

Three small bridges are then needed.

• G-small-1 (§1): the two coarse caps the Dirichlet energy estimate reads at that pin — Λ_{s/2,2} and λ_{s/4,2}^{-1} at the (n+3) re-based family on the covering cube — capped against σ_{n+3} on the frozen good event 𝒢(n+3, z; s/8, 1/2). Both indices lie in (s/8, 1/2] for every s ∈ (0,1], which is exactly why s/2 is the pin: at the earlier r = s the index Λ_{s,2} leaves the good-event window for s ∈ (1/2, 1]. The proof is one parametric instance of BoundaryCoveringSlot's own two-lemma pattern (off-grid error transport + ratio cap).
• G-small-2 (§2): the index conversion [·]_{s/2} → [·]_s on the scale-normalized positive Besov carrier. Finding: this costs nothing. CoarseGraining already proves the exact monotonicity (cubeBesovPositiveVectorSeminormTwo_le_of_exponent_le_of_bddAbove): the depth weights are 3^{u j} with j ≥ 0, increasing in u. No 3-power and no constant appear — strictly better than the plan's budgeted 3^{(s/2)(n+3)}-type factor. Recorded as an improvement.
• G-M2 (§3): the ForceBesovRegularity binders that BoundaryEnergyRebase.exists_boundaryWindowEnergy_rebased_le_dirichletDatumRHS asks of its caller, at the pin r = s/2, for the transported force `y ↦ −g(y
  • c)and the transported boundary gradienty ↦ ∇h(y + c), from the anchor's clause-(iv) MemLpdata on□_m`.

References

• CoarseGraining: Deterministic/WeakNormInterfacesPositiveQTwo.lean, Deterministic/CoarsePoincare/Regularity.lean.

1. G-small-1: the q = 2 ratio caps at the pin's two indices

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst_pinHalf_le {d : ℕ} {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : offGridStabilityConst d (s / 2) (s / 8) ≤ 192 * ↑d

The off-grid stability constant at the pin's two indices is below the same 192 d the proved s/6 slot uses.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridStabilityConst_pinQuarter_le {d : ℕ} {s : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) : offGridStabilityConst d (s / 4) (s / 8) ≤ 192 * ↑d

The off-grid stability constant at the pin's lower index.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_coveringCubeRatioCap_le_gapThree (d : ℕ) [NeZero d] : ∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (z : HCPolySupport.Vec d) (t : ℝ), s / 8 < t → t ≤ 1 / 2 → offGridStabilityConst d t (s / 8) ≤ 192 * ↑d → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (x : HCPolySupport.Vec d), HCPolySupport.translateSet (wellPlacedCentre x m (n + 2) - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2))) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d (n + 2)) t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) ≤ K ∧ ↑(Section3.Annealed.sigmaBar M (n + 3)) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d (n + 2)) t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega))⁻¹ ≤ K

G-small-1, parametric form. On the frozen good event, at any index t ∈ (s/8, 1/2] whose off-grid stability constant is below 192 d, the covering cube's q = 2 ellipticity ratios at the (n+3) re-based family are bounded by an absolute K(d) against σ_{n+3}.

The s/6 instance is BoundaryCoveringSlot.ae_coveringCubeCaps_le; this is the same two-step pattern with the index left free, so the Dirichlet-energy indices s/2 and s/4 of the r = s/2 pin are covered.

6. The recovery record: the proved binder implies the hinge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_coveringCubeRatioCap_le (d : ℕ) [NeZero d] : ∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (z : HCPolySupport.Vec d) (t : ℝ), s / 8 < t → t ≤ 1 / 2 → offGridStabilityConst d t (s / 8) ≤ 192 * ↑d → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d (n + 2)) t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega) ≤ K ∧ ↑(Section3.Annealed.sigmaBar M (n + 3)) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d (n + 2)) t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) (wellPlacedCentre x m (n + 2)) z omega))⁻¹ ≤ K

2. G-small-2: the positive-Besov index conversion, at no cost

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scaleNormalizedPositiveBesovVectorSeminormTwo_le_of_exponent_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) {u t : ℝ} (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (hut : u ≤ t) (hF : HCPolySupport.Book.Ch03.ForceBesovRegularity Q t F) : HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q u F ≤ HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q t F

G-small-2. The scale-normalized positive Besov seminorm is monotone in the index: the pin's [·]_{s/2} is bounded by the frozen clause's [·]_s with no constant and no scale factor.

This is CoarseGraining's own cubeBesovPositiveVectorSeminormTwo_le_of_exponent_le_of_bddAbove read on the public alias; the plan budgeted a 3^{(s/2)(n+3)}-type factor for this step, which turns out to be unnecessary.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceBesovRegularity_of_exponent_le {d : ℕ} {Q : HCPolySupport.TriadicCube d} {u t : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.Book.Ch03.ForceBesovRegularity Q t F) (hut : u ≤ t) : HCPolySupport.Book.Ch03.ForceBesovRegularity Q u F

The clause-(iv) regularity descends to any lower index — CoarseGraining's CubeVectorBesovHRegularity.of_exponent_le, named for the pin.

3. G-M2: the covering cube's ForceBesovRegularity binders

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceBesovRegularity_coveringCube_neg_of_clause_iv {d : ℕ} [NeZero d] {n m : ℤ} {x : HCPolySupport.Vec d} {s u : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hs : 0 < s) (hs1 : s ≤ 1) (hu : u ≤ s) (hL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) u fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))

G-M2, the force half. The transported, negated force y ↦ −g(y + c) is ForceBesovRegularity on the covering cube at every index u ≤ s, from the anchor's clause-(iv) data on □_m.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceBesovRegularity_coveringCube_datumGrad_of_clause_iv {d : ℕ} [NeZero d] {n m : ℤ} {x : HCPolySupport.Vec d} {s u : ℝ} {H : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hs : 0 < s) (hs1 : s ≤ 1) (hu : u ≤ s) (hL2 : MeasureTheory.MemLp H 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 H) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d (n + 2)) u fun (y : HCPolySupport.Vec d) => H (y + wellPlacedCentre x m (n + 2))

G-M2, the datum half. The transported boundary gradient y ↦ ∇h(y + c) is ForceBesovRegularity on the covering cube at every index u ≤ s, from the anchor's clause-(iv) data on □_m.