InteriorGlueCap

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

The cap at the root: the off-grid child error against the anchor's own

fluxCorrectedErrorRepresentative

This module closes the two remaining steps:

• the sample translation, which is legitimate because every real translation preserves the cutoff-sample law (GoodEvents.measurePreserving_translateCutoffSample).

The result is stated on one probability-one event, for every real translate w at once, exactly as the assembly consumes it; the anchor's own geometry binder supplies w := x − z through InteriorGlue.translateSet_cubeSet_subset_of_anchorGeometry.

What this does not do

The left-hand side is the off-grid error of the child cube, in the parent's z-frame. Nothing here assumes it.

References

• ABK26, e.mathcalE.stability.applied; l.harmonic.approximation.good.scales.

1. The root specialization

theorem Algsuperdiff.Section4.Provider.ExcessDecay.fluxCorrectedErrorFunctionalAtRoot_eq_representative {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (u : { u : ℝ // 0 < u }) : fluxCorrectedErrorFunctionalAtRoot M L k (HCPolySupport.originCube d k) (HCPolySupport.originCube d k) (↑u) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M k)) = Support.fluxCorrectedErrorRepresentative M L k u

At the anchor's own root the F1' functional is the proved representative: fluxCorrectedErrorFunctionalAtRoot at root = Q = □_{n+2} with the comparator σ_{n+2} Id reduces to Support.fluxCorrectedErrorRepresentative, definitionally.

2. The cap at the root, at the untranslated sample

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_offGridChildError_le_fluxCorrectedErrorRepresentative {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) {t u : ℝ} (hu0 : 0 < u) (hut : u < t) (ht : t ≤ 1 / 2) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (w : HCPolySupport.Vec d), HCPolySupport.translateSet w (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2)) → offGridErrorFunctional w (HCPolySupport.originCube d n) t (Support.fluxCorrectedRegField M L (n + 2) (HCPolySupport.originCube d (n + 2)) omega).toFun (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 2))) ≤ √(offGridStabilityConst d t u) * (3 ^ (2 * u) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨u, hu0⟩ omega)

The off-grid child error against the anchor's representative.

On one probability-one event, for every real translate w with w + □_n ⊆ □_{n+2} (half-open),

  𝓔_{t,∞,2}(w + □_n; ã_{L,n+2}, σ_{n+2}) ≤ C(d,t,u)^{1/2} · 3^{2u} ·
      𝓔_{u,∞,2}(□_{n+2}; ã_{L,n+2}, σ_{n+2}) ,

the right-hand factor being the frozen theorem's own fluxCorrectedErrorRepresentative M L (n+2) ⟨u⟩.

3. The cap at the translated sample

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_offGridChildError_le_representative_translate {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {t u : ℝ} (hu0 : 0 < u) (hut : u < t) (ht : t ≤ 1 / 2) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (w : HCPolySupport.Vec d), HCPolySupport.translateSet w (HCPolySupport.cubeSet (HCPolySupport.originCube d n)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2)) → offGridErrorFunctional w (HCPolySupport.originCube d n) t (Support.fluxCorrectedRegField M L (n + 2) (HCPolySupport.originCube d (n + 2)) (Section3.Cutoff.translateCutoffSample z omega)).toFun (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 2))) ≤ √(offGridStabilityConst d t u) * (3 ^ (2 * u) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨u, hu0⟩ (Section3.Cutoff.translateCutoffSample z omega))

The same estimate at the anchor's translated sample.

The anchor reads its error at translateCutoffSample z ω; every real translation preserves the cutoff-sample law, so the probability-one event transports.

4. The anchor's own slot, entered at the geometry binder

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_offGridChildError_le_representative_harmonicSlot {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) → offGridErrorFunctional (x - z) (HCPolySupport.originCube d n) (s / 6) (Support.fluxCorrectedRegField M L (n + 2) (HCPolySupport.originCube d (n + 2)) (Section3.Cutoff.translateCutoffSample z omega)).toFun (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 glue item, at the anchor's binders.

At the printed slot (t, u) = (s/6, s/8) and the anchor's geometry binder, the off-grid error of the anchor's own child window x + □_n, read in the parent's z-frame at the translate w = x − z, is bounded by the anchor's own fluxCorrectedErrorRepresentative M L (n+2) ⟨s/8⟩ at the translated sample, with the absolute depth factor 3^{s/4} (at most 3^{1/4} < 1.32).