ReindexComposed

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

The general clause at frontier-empty windows, composed at the slot n+3

GeneralClauseInteriorComposed composes the proved chain at the slot n+2; this module re-runs the same composition at the frozen slot n+3:

  1_𝒢 ‖u − v‖_{L²(x+□_n)}
      ≤ C ( s^{-4} 𝓔_{s/8}(z+□_{n+3}; ã_{L,n+3}, σ_{n+3}) ‖u − (u)_W‖_{L²(W)}
          + s^{-7} σ_{n+3}^{-1} 3^{(1+s)n} [g]_{H^s(W)} ) ,
      W = (z + □_{n+2}) ∩ □_m ,

on the good event 𝒢(n+3, z; s/8, 1/2) and under the frozen binder n + 3 ≤ m. Three inputs move, nothing else:

• the energy leg — ReindexEnergy.ae_constantDatumEnergy_anchorWindow_addThree;
• the child-frame objects — ReindexEllipticity's two caps, at the depth-3 off-grid factor 3^{3s/8} in place of 3^{s/4};
• the caps — ReindexSlot.ae_errorRepresentative_le_harmonicSlot_addThree, read at L ≥ n+3, which is exactly what the frozen binder n + 3 ≤ m ≤ L supplies.

The energy leg's identity is slot-free. The bridge InteriorEnergyBridge.h1EnergyNormOnCube_parentRebasedFamily_eq and the ν-identification NuIdentification.localizedCoeffEnergyValue_fluxCorrectedCoeffFamily_eq both evaluate to ν ⨍|∇u|², with no dependence on the flux slot or on the cube carrying the correction; so the bridge below is proved on the anchor's own (n+2)-containment z + □_{n+2} ⊆ □_m — the frozen gate's own consequence — and never needs z + □_{n+3} ⊆ □_m, which the anchor does not supply.

The constant kappa = √(192 d)·3 is unchanged: the depth factor 3^{3(s/8)} still satisfies 3^{3(s/8)} ≤ 3 on s ≤ 1 (indeed 3s/8 ≤ 3/8), so the one extra depth is absorbed with no constant move at all.

Deviations from the printed statement

• the off-grid depth factor is 3^{3s/8} (proved: 3^{s/4}) — one extra 3^{s/8} ≤ 3^{1/8}, absorbed inside the unchanged kappa;
• the centre-child cap costs 3^{s/8} ≤ 3^{1/8}, absorbed in ReindexSlot's own constant;
• the σ index: the force leg carries σ_{n+3}^{-1}; the frozen statement carries σ_n^{-1}, and ReindexSlot.exists_inv_sigmaBar_add_three_le converts at the factor 4 — the same constant as the proved two-scale conversion, the gap being free;
• no γ-move and no s-exponent move is made anywhere.

References

• ABK26, l.harmonic.approximation.good.scales; e.homogenization.L2.interior.

1. The sharpened arithmetic, at the n+3 comparator

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_constantDatumAnchorEnergyRHSOn_addThree_le {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {s : ℝ} (hs : 0 < s) (W : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) : √(constantDatumAnchorEnergyRHSOnAddThree M n s W f g) ≤ √↑(Section3.Annealed.sigmaBar M (n + 3)) * Real.rpow 3 (-↑(n + 2)) * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverage W f) 2 (Support.normalizedVolumeMeasureOn W)).toReal + s.rpow (-3) * √(↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * Real.rpow 3 (s * ↑(n + 2)) * (Support.normalizedGagliardoESeminormOn W s g).toReal

The two legs of the n+3 Caccioppoli right-hand side.

  ( σ_{n+3} 3^{-2(n+2)} X² + s^{-6} σ_{n+3}^{-1} 3^{2s(n+2)} Y² )^{1/2}
      ≤ σ_{n+3}^{1/2} 3^{-(n+2)} X  +  s^{-3} σ_{n+3}^{-1/2} 3^{s(n+2)} Y .

2. The slot-free energy bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.h1EnergyNormOnCube_parentRebasedFamily_addThree_eq_sqrt_localizedCoeffEnergyValue {d : ℕ} {n m : ℤ} (M : Section3.ABKModel d) (L : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (hx : HCPolySupport.translateSet x (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hz : HCPolySupport.translateSet z (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : HCPolySupport.Book.Ch03.h1EnergyNormOnCube (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (HCPolySupport.H1Function.untranslate x (u.restrict ⋯ hx)) = √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue ((fun (y : HCPolySupport.Vec d) => x - z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) ((Support.fluxCorrectedCoeffFamily M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)).coeffOn (HCPolySupport.originCube d (n + 2))) (HCPolySupport.H1Function.untranslate z (u.restrict ⋯ hz)))

The energy leg at the (n+3) re-based family.

The coefficient-energy norm carried by the child-frame coarse-graining energy term at the (n+3) re-based family is exactly the square root of the localized coefficient energy that ReindexEnergy bounds — same solution, same window, two frames. Both sides are ν ⨍|∇u|², so the flux slot never enters and the containment needed is the anchor's own z + □_{n+2} ⊆ □_m.

3. The composed general clause at the slot n+3

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_generalClauseInterior_honest_addThree (d : ℕ) [NeZero d] : ∃ (C : ℝ) (Cfin : ℝ), 0 < C ∧ 0 < Cfin ∧ ∀ (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), 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, ⋯⟩ (1 / 2) → ∀ (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))) → ∀ (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 ≤ Cfin * (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 + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).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 + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal)

The general clause at frontier-empty windows, in real form.

GeneralClauseInteriorComposed.exists_generalClauseInterior_honest at the frozen slot: the good event, the flux-corrected error index and the σ index all read n+3, and the binder is the frozen binder n + 3 ≤ m. Every s-power, every 3-power and every window is the proved one.