ResiduePlugin

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

The plug-in: route 1 closed at an explicit ε-smallness

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

What is proved

ResidueRouteOne.exists_flushResidue_route1_composed prices the harmonic approximation residue at the flush sub-cube on five legs, the first and the last carrying s^{-4}·𝓔 and the last being the boundary scalar S at the flush cube K — a self-consistency loop. ResidueScalarFlush closes that loop: it bounds S by the same window legs plus the residue itself.

exists_flushResidue_le_displayLegs_of_epsPin runs the loop under one explicit, disclosed hypothesis

  hepsPin :  A · 𝓔  ≤  s⁴ ,        𝓔 = fluxCorrectedErrorRepresentative M L (n+3)
                                        ⟨s/8⟩ (translate z ω) ,

with A > 0 produced by the theorem, and delivers, for every Δ-harmonic comparator w = u + ρ, ρ ∈ H¹₀(K'),

  ‖u − w‖_{L²(K')} ≤ K · ( ‖u − (u)_{W'}‖_{L²(W')}
                          + s^{-6}·3^{n}·‖∇h‖_{L²(W')}
                          + s^{-6}·3^{(1+s)n}·[∇h]_{H^s(W')}
                          + s^{-7}·σ_{n+3}^{-1}·3^{(1+s)n}·[g]_{H^s(W')} ) .

Nothing in this module asserts it.

The room, honestly stated (a correction to's table)

's legal-producer contract asks for the residue at the four s-powers (0, 0, −2, −3σ^{-1}). Route 1 does not meet that contract, and cannot:

• the 3^n‖∇h‖ and 3^{(1+s)n}[∇h] legs arrive at s^{-6}, and the 3^{(1+s)n}[g] leg at s^{-7}σ^{-1} — the frozen display's own powers;
• the [g] leg's dominant part comes from the coarse-graining force term and the interior correction leg, neither of which carries 𝓔, so no ε-smallness improves it.

The contract is nevertheless sufficient, not necessary. The pin is therefore consumed twice — once to resolve the S-loop here, once downstream to absorb the residue's own s-powers.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2.

1. The loop-resolution arithmetic

2. The plug-in corollary

theorem Algsuperdiff.Section4.Provider.ExcessDecay.residuePlugin_comparisonBounds1 (d : ℕ) (CS : ℝ) : (∀ {n m : ℤ} {z : HCPolySupport.Vec d} {i : Fin d} {σ : ℝ}, n + 2 ≤ m → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → σ = 1 ∨ σ = -1 → wellPlacedHalfGap m (n + 2) < σ * z i → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.HasZeroTraceDifferenceOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u h → ∀ (R : ℝ), (∀ (w : HCPolySupport.H1Function (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (rho : HCPolySupport.H10Function (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet (flushSubCentre z m n i σ) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) w → (∀ (y : HCPolySupport.Vec d), w.toFun y = u.toFun y + rho.toFun y) → (∀ (y : HCPolySupport.Vec d), w.grad y = u.grad y + rho.grad y) → (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i σ + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w.toFun y) ≤ R) → |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - h.toFun y| ≤ CS * ((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 + 3 ^ n * ∑ i' : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => h.grad y i') 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + R)) → ∀ (M : Section3.ABKModel d) (L m n : ℤ), ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ (i : Fin d) (sigma : ℝ), sigma = 1 ∨ sigma = -1 → wellPlacedHalfGap m (n + 2) < sigma * z i → n + 2 ≤ m → ∀ (omega : Section3.Cutoff.CutoffSample d) (u hdat : 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 hdat g → (∀ (Rarg : ℝ), (∀ (w' : HCPolySupport.H1Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (rho' : HCPolySupport.H10Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) w' → (∀ (y : HCPolySupport.Vec d), w'.toFun y = u.toFun y + rho'.toFun y) → (∀ (y : HCPolySupport.Vec d), w'.grad y = u.grad y + rho'.grad y) → (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w'.toFun y) ≤ Rarg) → |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ CS * ((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 + 3 ^ n * ∑ i' : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => hdat.grad y i') 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal + Rarg)) ∧ ∑ i' : Fin d, (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => hdat.grad y i') 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal ≤ ↑d * (MeasureTheory.eLpNorm hdat.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 ∧ 3 ^ n = Real.rpow 3 ↑n

theorem Algsuperdiff.Section4.Provider.ExcessDecay.harmonic_budget_of_setEq {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hUV : U = V) (f : HCPolySupport.Vec d → ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) {B : ℝ} (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict U)) (hcomp : ∀ (v : HCPolySupport.H1Function U) (w : HCPolySupport.H10Function U), Support.IsWeaklyHarmonicOn U v → (∀ (y : HCPolySupport.Vec d), v.toFun y = f y - w.toFun y) → (∀ (y : HCPolySupport.Vec d), v.grad y = F y - w.grad y) → (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn U)).toReal ≤ B) (w' : HCPolySupport.H1Function V) (rho' : HCPolySupport.H10Function V) (hharm' : Support.IsWeaklyHarmonicOn V w') (hval' : ∀ (y : HCPolySupport.Vec d), w'.toFun y = f y + rho'.toFun y) (hgrad' : ∀ (y : HCPolySupport.Vec d), w'.grad y = F y + rho'.grad y) : (Support.normalizedL2On U fun (y : HCPolySupport.Vec d) => f y - w'.toFun y) ≤ B

A subtraction-form harmonic budget also controls the additive zero-trace split.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_flushResidue_le_displayLegs_of_epsPin_errorWeighted (d : ℕ) [NeZero d] : ∃ (C : ℝ) (A : ℝ) (K : ℝ), 0 < C ∧ 0 < A ∧ 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.openCubeSet (HCPolySupport.originCube d m), ∀ (i : Fin d) (sigma : ℝ), sigma = 1 ∨ sigma = -1 → wellPlacedHalfGap m (n + 2) < sigma * z i → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → A * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ s ^ 4 → ∀ (u hdat : 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 hdat 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 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (w : HCPolySupport.H1Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (rho : HCPolySupport.H10Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) w → (∀ (y : HCPolySupport.Vec d), w.toFun y = u.toFun y + rho.toFun y) → (∀ (y : HCPolySupport.Vec d), w.grad y = u.grad y + rho.grad y) → (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w.toFun y) ≤ K * ((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 (-6) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm hdat.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 + 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 hdat.grad).toReal + s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * 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)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_flushResidue_le_displayLegs_of_epsPin (d : ℕ) [NeZero d] : ∃ (C : ℝ) (A : ℝ) (K : ℝ), 0 < C ∧ 0 < A ∧ 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.openCubeSet (HCPolySupport.originCube d m), ∀ (i : Fin d) (sigma : ℝ), sigma = 1 ∨ sigma = -1 → wellPlacedHalfGap m (n + 2) < sigma * z i → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → A * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ s ^ 4 → ∀ (u hdat : 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 hdat 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 hdat.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (w : HCPolySupport.H1Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) (rho : HCPolySupport.H10Function (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))), Support.IsWeaklyHarmonicOn (HCPolySupport.translateSet (flushSubCentre z m n i sigma) (HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) w → (∀ (y : HCPolySupport.Vec d), w.toFun y = u.toFun y + rho.toFun y) → (∀ (y : HCPolySupport.Vec d), w.grad y = u.grad y + rho.grad y) → (Support.normalizedL2On ((fun (y : HCPolySupport.Vec d) => flushSubCentre z m n i sigma + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) fun (y : HCPolySupport.Vec d) => u.toFun y - w.toFun y) ≤ K * ((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 (-6) * Real.rpow 3 ↑n * (MeasureTheory.eLpNorm hdat.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 + 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 hdat.grad).toReal + s.rpow (-7) * (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * 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)