EdBridgeStepFourDatumSplitErrorWeighted

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

The Step-4 bridge's δ slot at the error-weighted five-leg expansion

EdBridgeStepFourDatumSplit.excessDecay_stepFour_slot_general_datumSplit runs the residue chain against the datum-split join and packages the remainder into EdBridgeStepFour.edBridgeDelta. The error-weighted sibling of that join, EdAssemblyJoinDatumSplitErrorWeighted.excessDecay_oneStep_anchored_datumSplit_errorWeighted, carries as its fifth leg the 𝓔-multiplied flat ∇h average in place of the normalized L² datum. This module is the matching δ packaging and slot:

• edBridgeDeltaBracketErrorWeighted — edBridgeDeltaBracket with its fourth summand replaced by the error-weighted leg

     C s^{-6} · 𝓔_{n+1}(τ_z ω) · 3^{n-2} · ‖(∇h)_{U_n}‖ ,
  

  every other byte unchanged;
• edBridgeDeltaErrorWeighted — the same weight-and-normalizer wrapper W · (3^{-n} · bracket);
• excessDecay_stepFour_slot_general_datumSplit_errorWeighted — the Step-4 decay slot at every centre, off the error-weighted join, in the shape the error-weighted Step-4 collapse and the proved budget composition stepFourDeltaOutErrorWeighted_add_datumLeg_le_boundaryThreeLegs consume: contraction, ε·|∇ℓ|, and δ + datum leg.

Why the swap is free

edBridge_recombine_datum is generic in the remainder Rhat: the datum leg Leg and the four-leg bracket enter only additively, and the k₀ selection of exists_edBridgeStepGen touches neither. The error-weighted leg sits in the bracket's fourth slot on BOTH sides of the recombination's hBig, so it cancels there; the δ-gate hgate, the ε identity and the contraction absorption are unchanged character for character.

References

• ABK26, l.excess.decay.good.scales; t.regularity Step 4.

1. The error-weighted four-leg bracket and its δ

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeDeltaBracketErrorWeighted {d : ℕ} (M : Section3.ABKModel d) (C : ℝ) (L m : ℤ) (s : ℝ) (t : { t : ℝ // 0 < t }) (z : HCPolySupport.Vec d) (gflux gradh : HCPolySupport.Vec d → HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) : ℝ

The four-leg bracket of the bridge's δ_j at the error-weighted clause.

EdBridgeStepFour.edBridgeDeltaBracket with the fourth summand — the flat ∇h datum leg — carrying the clause's own 𝓔 factor and reading the AV ‖(∇h)_{U_n}‖ in place of the normalized L² norm on U_{n+1}. The first three summands are unchanged.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.edBridgeDeltaErrorWeighted {d : ℕ} (M : Section3.ABKModel d) (C W : ℝ) (L m : ℤ) (s : ℝ) (t : { t : ℝ // 0 < t }) (z : HCPolySupport.Vec d) (gflux gradh : HCPolySupport.Vec d → HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (n : ℤ) : ℝ

The bridge's δ_j at j = n+1, at the error-weighted clause: the error-weighted four-leg bracket at the one-step's own remainder weight and scale normalizer 3^{-n}.

Equations

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

2. The Step-4 slot at the error-weighted join

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_stepFour_slot_general_datumSplit_errorWeighted (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ) (Ccap : ℝ) (Cb : ℝ), 0 < C ∧ 0 < Ccap ∧ 0 ≤ Cb ∧ ∃ (k₀ : ℕ), 3 ≤ k₀ ∧ ∀ (k : ℕ), k₀ ≤ k → ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ Ccap⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ (hs : 0 < s), ∀ delta ∈ Set.Ioc 0 1, delta ≤ 64 * (C ^ 2)⁻¹ * s ^ 6 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (s / 8 * √delta) → edBridgeEpsConstGen d (max (Schauder.schauderWindowConst d) Cb) C k * Ccap * s.rpow (-3) * √delta ≤ 1 / 2 * 3 ^ (-(1 / 4) * (↑k + 1)) → ∀ (L m : ℤ), m ≤ L → ∀ z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (n : ℤ), n + 1 ≤ m → omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 1) z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ (u hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (gflux : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u hdat gflux → MeasureTheory.MemLp gflux 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 gflux) 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))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre z m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))) 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) → ∀ (Kh : ℝ), 0 ≤ Kh → ((fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ∨ ∃ (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (v₁ : HCPolySupport.Vec d → ℝ) (cl : ℝ) (Al : HCPolySupport.Vec d), (MeetsUpperFace z m (n - 2) i ∨ MeetsLowerFace z m (n - 2) i) ∧ ⋯ ∧ ⋯) → ∀ (c : ℝ) (gmin : HCPolySupport.Vec d), Support.IsAffineMinimizer (truncatedWindow z m (n + 1)) u.toFun c gmin → Support.affineExcess (truncatedWindow z m (n + 1 - ↑(k + 1))) u.toFun ≤ 3 ^ (-(1 / 4) * (↑k + 1)) * Support.affineExcess (truncatedWindow z m (n + 1)) u.toFun + edBridgeEps M (edBridgeEpsConstGen d (max (Schauder.schauderWindowConst d) Cb) C k) L s ⟨s / 8, ⋯⟩ z omega n * Support.slopeMagnitude gmin + (edBridgeDeltaErrorWeighted M C (edBridgeRemWeightGen d (max (Schauder.schauderWindowConst d) Cb) k) L m s ⟨s / 8, ⋯⟩ z gflux hdat.grad omega n + edBridgeDatumLeg d (max (Schauder.schauderWindowConst d) Cb) k n Kh)

The Step-4 decay slot at every centre, with the printed datum leg, off the error-weighted anchor.

EdBridgeStepFourDatumSplit.excessDecay_stepFour_slot_general_datumSplit run against the error-weighted join. The window hypothesis is the join's own disjunction's honest binders; the conclusion is the interior slot's, with the δ leg now edBridgeDeltaErrorWeighted — the 𝓔-multiplied flat ∇h average in the fourth slot — plus the additive datum summand edBridgeDatumLeg d (max (schauderWindowConst d) C_b) k n K_h.