StepSevenCaccFinalChain

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

1. The Step-7 end chain with hgrad discharged

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenEnd_chain_interior (d : ℕ) [NeZero d] : ∃ (Cch : ℝ) (Cc : ℝ), 0 < Cch ∧ 0 < Cc ∧ ∀ (M : Section3.ABKModel d) (L : ℤ) {alpha : ℝ} {n m k n' mf : ℤ} (Qf : HCPolySupport.TriadicCube d) {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g gcacc : HCPolySupport.Vec d → HCPolySupport.Vec d} {z c : HCPolySupport.Vec d} (uglob : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n')).carrier) (omega : Section3.Cutoff.CutoffSample d) (u : HCPolySupport.Book.Ch03.ForcedCubeSolution (HCPolySupport.originCube d k) a g) {Ccmp Kg Kd Ks Ctr CB CBc sigma sigmac shomM gradM dataG W G H C1 delta Cosc : ℝ} {B : ℕ}, (∀ (y : HCPolySupport.Vec d), u.toH1.toFun y = uglob.toFun (y + c)) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → k ≤ m → ExcessDecay.truncatedWindow z m k ⊆ (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) → MeasureTheory.IntegrableOn uglob.toFun (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => uglob.toFun x ^ 2) (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn uglob.toFun ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => uglob.toFun x ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (uglob.toFun x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) uglob.toFun) ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → 0 ≤ CB → 0 ≤ Ks → 0 ≤ Ccmp → 0 < sigma → 0 < shomM → 0 ≤ gradM → 0 ≤ dataG → 0 ≤ W → 0 ≤ G → 0 ≤ H → HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d k) stepSevenCgS g → StepSevenLambdaCaps (HCPolySupport.originCube d (k + 1)) a sigma CB → HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm (HCPolySupport.originCube d k) a u ≤ Kg * gradM → HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d k) stepSevenCgS g ≤ Kd * dataG → sigma⁻¹ ≤ Ks * shomM⁻¹ → √Ks * Kg ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → Ks * Kd ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → sigmac ≤ Ccmp * shomM → (∀ (y : HCPolySupport.Vec d), v.toFun y = uglob.toFun (y + z)) → (∀ (y : HCPolySupport.Vec d), v.grad y = uglob.grad (y + z)) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → n' ≤ m - 1 → n + 1 ≤ n' - 2 → HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d n') (Support.fluxCorrectedCoeffFamily M L mf Qf (Section3.Cutoff.translateCutoffSample z omega)) v gcacc → ⋯

** gap 2, closed on the interior branch: the Step-7 end chain with hgrad GONE.**

StepSevenLambdaChain.exists_stepSevenEnd_chain_of_caps with its one surviving conditional input replaced by the produced display StepSevenCaccFinalDisplay.exists_stepSevenGradientWithShom_interior_of_caps. Every other binder of the parent chain is carried verbatim; the new binders are the pinned Caccioppoli's own (equation, forcing regularity, the clause-(B) record at the good scale), the printed interior gate, the Step-7c scalar budget, and hosc.

2. The same, entered at t.regularity's own Dirichlet datum

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenEnd_chain_interior_of_dirichlet (d : ℕ) [NeZero d] : ∃ (Cch : ℝ) (Cc : ℝ), 0 < Cch ∧ 0 < Cc ∧ ∀ (M : Section3.ABKModel d) (L : ℤ) {alpha : ℝ} {n m k n' mf : ℤ} (Qf : HCPolySupport.TriadicCube d) {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {z c : HCPolySupport.Vec d} (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (omega : Section3.Cutoff.CutoffSample d) (u : HCPolySupport.Book.Ch03.ForcedCubeSolution (HCPolySupport.originCube d k) a g) {Ccmp Kg Kd Ks Ctr CB CBc sigma sigmac shomM gradM dataG W G H C1 delta Cosc : ℝ} {B : ℕ}, (∀ (y : HCPolySupport.Vec d), u.toH1.toFun y = uglob.toFun (y + c)) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → k ≤ m → ExcessDecay.truncatedWindow z m k ⊆ (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) → MeasureTheory.IntegrableOn uglob.toFun (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => uglob.toFun x ^ 2) (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn uglob.toFun ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => uglob.toFun x ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (uglob.toFun x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) uglob.toFun) ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → 0 ≤ CB → 0 ≤ Ks → 0 ≤ Ccmp → 0 < sigma → 0 < shomM → 0 ≤ gradM → 0 ≤ dataG → 0 ≤ W → 0 ≤ G → 0 ≤ H → HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d k) stepSevenCgS g → StepSevenLambdaCaps (HCPolySupport.originCube d (k + 1)) a sigma CB → HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm (HCPolySupport.originCube d k) a u ≤ Kg * gradM → HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d k) stepSevenCgS g ≤ Kd * dataG → sigma⁻¹ ≤ Ks * shomM⁻¹ → √Ks * Kg ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → Ks * Kd ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → sigmac ≤ Ccmp * shomM → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → n' ≤ m - 1 → n + 1 ≤ n' - 2 → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) uglob hdat gsrc → MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp ⋯ 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ⋯ → ⋯

The interior Step-7 end chain from the Dirichlet datum alone.

exists_stepSevenEnd_chain_interior with the Caccioppoli side entered at t.regularity Step 3's own datum: the transported solution v, its two frame identities and its forced equation are BUILT (StepSevenCaccFinalInterior.exists_stepSevenCaccInteriorSolution), and the forcing binder at the good-scale cube is produced from the §4.4 H^{1/4} datum on □_m through the Gagliardo ↔ Besov bridge (residue, StepSevenCaccFinalInterior.forceBesovRegularity_stepSevenCacc_interior) — the two MemLp hypotheses below are literally the two forcing binders's Step-6 interior endpoint.