InteriorEllipticity

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

The child-frame coarse-graining objects, capped at the anchor's own slot

With the re-based family and the re-cut slot of InteriorEllipticitySlot, both coarse-graining objects the interior clause's right-hand side carries at the child cube □_n — the q = 1 error at depth 0 and the ellipticity factors λ_{s/6,2}, Λ_{s/6,2} inside CoarseGraining's forcing bracket — are read at the index s/6.

Two steps, both proved elsewhere and composed here:

• the off-grid cap (InteriorGlueCap, printed slot (s/6, s/8)): that functional is bounded by the anchor's own fluxCorrectedErrorRepresentative M L (n+2) ⟨s/8⟩ at the translated sample;
• the good event (GoodEventCaps): the representative is bounded by C/2.

The result is the pair of caps the interior assembly consumes: the energy leg's 𝓔 factor retained at the anchor's printed index (it is a factor of the anchor's own first summand), and the forcing bracket collapsed to a constant.

Why the slot sits at s/6

At r = s/3 the child's index is s/6 > s/8 and the proved cap applies verbatim. See InteriorEllipticitySlot.

References

• ABK26, e.mathcalE.stability.applied; e.bound.Lambdas.by.Es.v2; e.homogenization.L2.interior.

0. The comparator, in the two spellings

1. The frame bridge at the re-based family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.homogenizationErrorOnCube_parentRebasedFamily_eq_offGrid {d : ℕ} (M : Section3.ABKModel d) (L k n : ℤ) (x z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {t : ℝ} (ht : 0 < t) (a0 : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d n) t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L k x z omega) a0 = offGridErrorFunctional (x - z) (HCPolySupport.originCube d n) t (Support.fluxCorrectedRegField M L k (HCPolySupport.originCube d k) (Section3.Cutoff.translateCutoffSample z omega)).toFun a0

The child-frame error object is the off-grid error at w = x − z.

Exact; no constant. The family hypothesis of InteriorGlueFrame is the frame identity.

2. The q = 2 error at the child cube, capped at the anchor's index

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_homogenizationErrorOnCube_rebased_le_representative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d n) (s / 6) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 2) x z omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 2))) ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The child-frame 𝓔_{s/6,∞,2}, against the anchor's own representative.

On one probability-one event, for every off-lattice centre x and every ambient scale m the anchor's geometry binder relates.

3. The energy leg's 𝓔 factor, at the printed index

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_coarseGrainingErrorAtDepth_rebased_le_representative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 2) x z omega) (scalarComparator ⋯) (s / 3) 0 ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The q = 1 error at depth 0 of the re-cut slot, at the anchor's own representative.

𝓔_{s/3,∞,1}(□_n; ã_x, σ) ≤ √C(d) · 3^{s/4} · 𝓔_{s/8,∞,2}(□_{n+2}; ã_z, σ), the right-hand factor being the anchor's printed fluxCorrectedErrorRepresentative M L (n+2) ⟨s/8⟩. This is the factor the frozen statement's first interior summand carries; it is not capped here.

4. The ellipticity ratio at the child frame

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_ellipticityRatio_rebased_le_representative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → max ((↑(Section3.Annealed.sigmaBar M (n + 2)))⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 2) x z omega)) (↑(Section3.Annealed.sigmaBar M (n + 2)) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 2) x z omega))⁻¹) ≤ 2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1)

e.bound.Lambdas.by.Es.v2 at the child cube, in the child's own frame.

The coarse-grained ellipticity factors of the re-based family at the slot index s/6, against the anchor's own representative.

5. CoarseGraining's forcing bracket at the child frame

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_half_eq_sqrt (x : ℝ) : x.rpow (1 / 2) = √x

Three Real.rpow normalizations, in the Real.sqrt spelling the bracket arithmetic uses.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_half_eq_sqrt_inv {x : ℝ} (hx : 0 < x) : x.rpow (-(1 / 2)) = √x⁻¹

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_neg_one_eq_inv {x : ℝ} (hx : 0 < x) : x.rpow (-1) = x⁻¹

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingForceBracket_le_of_ratio_and_error {d : ℕ} [NeZero d] (n : ℤ) (A : HCPolySupport.Book.Ch03.CoeffFamily d) {s sig Eb Kb : ℝ} (hs : 0 < s) (hsig : 0 < sig) (hKb : 0 ≤ Kb) (hrat : max (sig⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A) (sig * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A)⁻¹) ≤ Kb) (hErrDepth : HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth (HCPolySupport.originCube d n) A (scalarComparator hsig) (s / 3) 0 ≤ Eb) : coarseGrainingForceBracket (HCPolySupport.originCube d n) A (scalarComparator hsig) (s / 3) ≤ √Kb * Eb + 2 * Kb

A scalar comparator and ellipticity-ratio bound control the force bracket. This estimate is independent of how the coefficient family was rebased.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_forceBracket_rebased_le {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → coarseGrainingForceBracket (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 2) x z omega) (scalarComparator ⋯) (s / 3) ≤ √(2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1)) * (√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) + 2 * (2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (2 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1))

The forcing bracket at the child frame, in terms of the anchor's own representative.

The comparator's scale σ_{n+2} cancels between the ellipticity factors and the matrix norm, so the bound is σ-free: it depends only on d, on the proved off-grid constant and on the anchor's 𝓔_{s/8} representative. On the good event the representative is a constant, so the whole bracket is.