StitchDisplayLegs

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

The scalar leg, priced on the display

Why the pin is consumed twice

The contract asked the residue at the four s-powers (0, 0, −2, −3 σ⁻¹); the composition delivers it at (0, −6, −6, −7 σ⁻¹), the display's own powers. That is enough exactly because the pin appears on both sides of the S-loop:

• once inside ResiduePlugin.exists_flushResidue_le_displayLegs_of_epsPin, where loop_resolution closes the S ↦ R ↦ S cycle;
• once here, as p := s^{-4}·𝓔 ≤ 1, which is what lets the widened residue's three tail legs be absorbed back into the display's tail legs (sLeg_of_displayResidue).

Only the first leg keeps the factor p, and that is the display's own first leg.

References

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sLeg_of_displayResidue_errorWeighted {p CB K X Ln Lh Lg Sm Hn R3n S dR : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hCB0 : 0 ≤ CB) (hK0 : 0 ≤ K) (hX0 : 0 ≤ X) (hLn0 : 0 ≤ Ln) (hLh0 : 0 ≤ Lh) (hLg0 : 0 ≤ Lg) (hR3n0 : 0 ≤ R3n) (hdR0 : 0 ≤ dR) (hSm : Sm ≤ dR * Hn) (hRHn : dR * (p * (R3n * Hn)) ≤ dR * Ln) (hS : S ≤ CB * (X + R3n * Sm + K * (X + Ln + Lh + Lg))) : p * S ≤ CB * (1 + 2 * K + dR) * (p * X + Ln + Lh + Lg)

Scalar absorption retaining the error prefactor in the flat leg.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sLeg_of_displayResidue {p CB K X Ln Lh Lg Sm Hn R3n S dR : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hCB0 : 0 ≤ CB) (hK0 : 0 ≤ K) (hX0 : 0 ≤ X) (hLn0 : 0 ≤ Ln) (hLh0 : 0 ≤ Lh) (hLg0 : 0 ≤ Lg) (hR3n0 : 0 ≤ R3n) (hdR0 : 0 ≤ dR) (hSm : Sm ≤ dR * Hn) (hRHn : dR * (R3n * Hn) ≤ dR * Ln) (hS : S ≤ CB * (X + R3n * Sm + K * (X + Ln + Lh + Lg))) : p * S ≤ CB * (1 + 2 * K + dR) * (p * X + Ln + Lh + Lg)

The contested arithmetic, in the abstract.

If the pin gives A p <= 1 with A >= 1, then the widened residue `K (X + Ln

• Lh + Lg)-- whose legs already sit at the display's owns-powers -- multiplied by pand by the scalar control's constant, is dominated by the display's four legsp X, Ln, Lh, Lg. Nothing here is a norm: X, Ln, Lh, Lg, Sm, Hn` are free nonnegative reals.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_scalarLeg_le_displayLegs_of_epsPin_errorWeighted (d : ℕ) [NeZero d] : ∃ (C : ℝ) (A : ℝ) (Cout : ℝ), 0 < C ∧ 0 < A ∧ 0 ≤ Cout ∧ ∀ (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 → ∀ (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) → ∀ (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))) → s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ Cout * (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 (-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)

Error-weighted scalar assembly, including the shared window and norm preparation.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_scalarLeg_le_displayLegs_of_epsPin (d : ℕ) [NeZero d] : ∃ (C : ℝ) (A : ℝ) (Cout : ℝ), 0 < C ∧ 0 < A ∧ 0 ≤ Cout ∧ ∀ (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 → ∀ (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) → ∀ (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))) → s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) * |HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => u.toFun y - hdat.toFun y| ≤ Cout * (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 (-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)

The display's boundary leg, produced.

At the anchor's own binders and under the disclosed pin, the frozen display's S-leg s^{-4} * E * |avg_{V1}(u - h)| is dominated by the display's own four legs at sigmabar_{n+3}. This is the end-to-end statement: the producer exists once the pin is granted.