ProviderBoundary

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

The boundary obligation, discharged

The stitch, in one paragraph

Feeding S := |(u − h)_{V₁}| itself, StitchDisplayLegs.exists_scalarLeg_le_displayLegs_of_epsPin prices that summand on the display's own four legs — provided the pin A·𝓔 ≤ s⁴ holds. And the pin is exactly what the re-gating bought: on the clause event 𝒢(n+3, z; s/8, C⁻¹s⁴) the proved caps step GoodEventCaps.ae_errorRepresentative_le_of_mem_goodEventAt — whose ε-slot is universally quantified — gives 𝓔 ≤ C₀·C⁻¹·s⁴, so A·𝓔 ≤ s⁴ as soon as the statement's own existential constant satisfies C ≥ A·C₀. That is legitimate because C is chosen last, after the d-only constants C₀ and A.

The final constant

C:= max (max (max C_asm C_disp) (max C₀ C_σ)) (max (max 2 (A·C₀)) (C_asm·(1 + 4·C_out))), where every entry is a d-only constant produced before C:

• C_disp — the display-legs pricing;
• C₀ — the caps step;
• C_σ — the σ gap-3 conversion;
• 2 — makes C⁻¹s⁴ ≤ 1/2, keeping the clause event inside the annular anchor's admissible ε-window and funding the (1/2)-form hypotheses of the two proved inputs a fortiori;
• A·C₀ — the pin;
• C_asm·(1 + 4·C_out) — the conclusion's absorption.

References

• ABK26, l.harmonic.approximation.good.scales; the frozen block of Algsuperdiff/Section4/Provider/ExcessDecay/ProviderEpsFree.lean (read for the byte-verification, never imported).

1. The absorption arithmetic

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundaryScalarLeg_absorb {LHS CA Cout Ctot L1 L1' L2 L2' L3 L4 P : ℝ} (hmain : LHS ≤ CA * (L1 + L2 + L3 + L4) + CA * P) (hP : P ≤ Cout * (L1' + L4 + L3 + L2')) (hL1' : L1' ≤ L1) (hL2' : L2' ≤ 4 * L2) (hCA : 0 ≤ CA) (hCout : 0 ≤ Cout) (hL1 : 0 ≤ L1) (hL2 : 0 ≤ L2) (hL3 : 0 ≤ L3) (hL4 : 0 ≤ L4) (hC : CA * (1 + 4 * Cout) ≤ Ctot) : LHS ≤ Ctot * (L1 + L2 + L3 + L4)

The scalar leg, absorbed into the display.

Everything below is free-real arithmetic on nonnegative data.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.epsPin_of_caps {A C0 Ct E s : ℝ} (hA : 0 ≤ A) (hCt : 0 < Ct) (hpin : A * C0 ≤ Ct) (hs : 0 ≤ s) (hcap : E ≤ C0 * (Ct⁻¹ * s ^ 4)) : A * E ≤ s ^ 4

The pin, from the clause threshold.

A·𝓔 ≤ s⁴ whenever the caps step gives 𝓔 ≤ C₀·(C⁻¹·s⁴) and the statement's own constant was chosen with A·C₀ ≤ C.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundary_provider_constant (CA CD C0 CS A Cout : ℝ) : ∃ (Ct : ℝ), CA ≤ Ct ∧ CD ≤ Ct ∧ C0 ≤ Ct ∧ CS ≤ Ct ∧ 2 ≤ Ct ∧ A * C0 ≤ Ct ∧ CA * (1 + 4 * Cout) ≤ Ct

A single boundary-provider constant controls all source thresholds and absorptions.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boundary_clause_epsilon_data {d : ℕ} {M : Section3.ABKModel d} {s Ct : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (hCt2 : 2 ≤ Ct) (hfund : M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (Ct⁻¹ * s ^ 4)) : 0 < Ct⁻¹ * s ^ 4 ∧ Ct⁻¹ * s ^ 4 ≤ 1 / 2 ∧ M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2)

The boundary clause epsilon lies in the half-event range and inherits funding.

2. The boundary obligation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryClauseReal_errorWeighted (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (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 * (C⁻¹ * s ^ 4) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (x z : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → z ∈ 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) → (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≠ ∅ → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (C⁻¹ * s ^ 4) → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 h.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) v → (∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) → (∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) → (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))).toReal ≤ C * (s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * ((MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + s.rpow (-(3 / 2)) * Real.rpow 3 ↑n * ‖HCPolySupport.volumeAverageVec ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.grad‖) + s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 ((1 + s) * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal + s.rpow (-6) * Real.rpow 3 ((1 + s) * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s h.grad).toReal + s.rpow (-6) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm h.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal)

The boundary-provider estimate retaining its final gradient error weight.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_boundaryClauseReal (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (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 * (C⁻¹ * s ^ 4) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 3 ≤ m → ∀ (x z : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → z ∈ 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) → (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ≠ ∅ → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (C⁻¹ * s ^ 4) → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 h.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) v → (∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) → (∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) → (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))).toReal ≤ C * (s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * ((MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + s.rpow (-(3 / 2)) * Real.rpow 3 ↑n * ‖HCPolySupport.volumeAverageVec ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.grad‖) + s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 ((1 + s) * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal + s.rpow (-6) * Real.rpow 3 ((1 + s) * ↑n) * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s h.grad).toReal + s.rpow (-6) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm h.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal)

The frozen general clause in real form, restricted to the boundary regime (z+□_{n+2}) ∩ ∂□_m ≠ ∅ — RebaseSealDistance's hbdry — with no hypothesis beyond the frozen statement's own binders.