ResidueCapChild

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

The child cube's cap family, re-cut at hinge (C)

Nothing here imports that file, and nothing here claims the anchor or any source node.

What is proved

ReindexSlot.ae_offGridChildError_le_representative_harmonicSlot_addThree and the four caps built on it in ReindexEllipticity (§1--§4) are stated at the anchor's geometry binder x + □_n ⊆ (z+□_{n+1}) ∩ □_m. Their proofs use that binder for exactly one thing: the half-open containment

  (C)   translateSet (x − z) (cubeSet □_n) ⊆ cubeSet □_{n+3} .

This module restates the five caps with (C) itself as the binder. Each is a strict generalization of the proved statement — the proved one is recovered by translateSet_cubeSet_subset_of_anchorGeometry composed with the half-open nesting cubeSet_originCube_add_two_subset — and each proof is the proved proof with the hinge supplied rather than derived. The point is ResidueCapGeometry.translateSet_cubeSet_flushSubCube_subset_anchorParent: the flush sub-cube K', which provably fails the anchor's binder (ResidueAbsorption), satisfies (C).

References

• ABK26, e.mathcalE.stability.applied; e.bound.Lambdas.by.Es.v2; p.general.coarse.graining.

1. The off-grid child error, at hinge (C)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_offGridChildError_le_representative_gapThree {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), HCPolySupport.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → offGridErrorFunctional (x - z) (HCPolySupport.originCube d n) (s / 6) (Support.fluxCorrectedRegField M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)).toFun (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 3))) ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The off-grid child error against the (n+3) representative, at hinge (C).

ReindexSlot.ae_offGridChildError_le_representative_harmonicSlot_addThree, with the anchor's geometry binder replaced by the half-open containment it is used to prove. Nothing else changes; the depth factor is still 3^{3s/8}.

2. The frame bridge at hinge (C)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_homogenizationErrorOnCube_rebased_le_representative_gapThree {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), HCPolySupport.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → 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 + 3) x z omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 3))) ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The child-frame 𝓔_{s/6,∞,2} at the n+3 family, at hinge (C).

3. The energy leg's 𝓔 factor at hinge (C)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_coarseGrainingErrorAtDepth_rebased_le_representative_gapThree {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), HCPolySupport.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (scalarComparator ⋯) (s / 3) 0 ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The q = 1 error at depth 0 of the re-cut slot, at hinge (C).

4. The ellipticity ratio at hinge (C)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_ellipticityRatio_rebased_le_representative_gapThree {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), HCPolySupport.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → max ((↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ * HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) x z omega)) (↑(Section3.Annealed.sigmaBar M (n + 3)) * (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) (s / 6) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (parentRebasedFamily M L (n + 3) x z omega))⁻¹) ≤ 2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨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, at hinge (C).

5. CoarseGraining's forcing bracket at hinge (C)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_forceBracket_rebased_le_gapThree {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), HCPolySupport.translateSet (x - z) (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3)) → coarseGrainingForceBracket (HCPolySupport.originCube d n) (parentRebasedFamily M L (n + 3) x z omega) (scalarComparator ⋯) (s / 3) ≤ √(2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1)) * (√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) + 2 * (2 * ↑d * ((√(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))) ^ 2 + 1))

The forcing bracket at the child frame, at hinge (C). The comparator's scale σ_{n+3} cancels between the ellipticity factors and the matrix norm, exactly as at the proved slot.