CoveringSlotObstruction

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

Where the boundary covering cube sits relative to the good-event slot

  max { σ_{n+2}⁻¹ Λ_{s/8,2}(□_{n+2}; ã) , σ_{n+2} λ_{s/8,2}(□_{n+2}; ã)⁻¹ }

at the sample τ_z ω — physically the cube z + □_{n+2}. So the question is one about two cubes of the same scale: c + □_{n+2} versus z + □_{n+2}.

This module answers it geometrically, in both directions.

• eq_of_image_add_openCubeSet_subset — two open triadic cubes of the same scale are nested only when their centres coincide.
• inter_frontier_eq_empty_of_subset_openCubeSet — a set inside the open cube □_m misses ∂□_m.
• gate_of_coveringCube_subset_slot — the obstruction. Any centre c whose cube c + □_{n+2} both (i) stays inside □_m (which the boundary lane requires: the anchor's solution u lives on □_m only) and (ii) stays inside the good-event slot's cube z + □_{n+2}, forces the anchor's own interior gate (z + □_{n+2}) ∩ ∂□_m = ∅. Contrapositive: on the branch the interior chain leaves open — the boundary regime — no admissible covering cube of the covering scale fits inside the slot cube, so no covering, subadditivity or descendant argument indexed by 𝒢(n+2, z) can reach the covering cube's ellipticity data.
• image_add_wellPlacedCentre_subset_image_add_openCubeSet_succ — the positive half. The covering cube always fits inside z + □_{k+1}; at k = n+2 that is z + □_{n+3}, the anchor's own window cube. So a slot at index n+3 does reach it, and the proved off-grid transport (OffGridComposeAssembly/OffGridErrorFluxCorrected, which require exactly a containment w + □_k ⊆ □_K of the off-grid cube in a grid cube) applies with K = n+3 at depth one.

Nothing here transports any coefficient, error or ellipticity quantity: this module is pure cube geometry, exactly like BoundaryCoveringGeometry. In particular nothing below is an instance, or a fraction, of any source node.

References

• ABK26, l.harmonic.approximation.good.scales; the boundary application of l.coarse.grained.Caccioppoli.RHS.

1. Two open cubes of the same scale

2. The frontier gate from a containment in □_m

3. The obstruction

4. The positive half: the covering cube fits one scale up

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_wellPlacedCentre_coord_bound {d : ℕ} {m k : ℤ} (hkm : k ≤ m) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (i : Fin d) : -(1 / 2 * 3 ^ k) < x i - wellPlacedCentre x m k i ∧ x i - wellPlacedCentre x m k i < 1 / 2 * 3 ^ k

The clamp moves each coordinate by less than half a side of □_k.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_subset_image_add_openCubeSet_succ {d : ℕ} {m k : ℤ} {x z : HCPolySupport.Vec d} (hkm : k ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hxz : x - z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (k - 1))) : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m k + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (k + 1))

The positive half.

The boundary covering cube always sits inside z + □_{k+1}, provided the window centre x is within half a side of □_{k-1} of z — which is exactly what the anchor's geometry binder gives at k = n+2.

Consequently a good-event slot at index n+3 does reach the covering cube: the proved off-grid transports require precisely a containment of the off-grid cube in a grid cube, and this is that containment at depth one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_mem_openCubeSet_of_anchorGeometry {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hgeom : (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)) : x - z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1))

The anchor's geometry binder, read as a bound on x - z.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_add_wellPlacedCentre_subset_anchorParent {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hgeom : (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) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3))

The covering cube inside the anchor's own window cube.

At the boundary lane's covering scale k = n+2, under the frozen theorem's own binders, c + □_{n+2} ⊆ z + □_{n+3}. Together with gate_of_wellPlacedCentre_subset_slot this is the exact measurement: the covering cube is outside the n+2 slot on the boundary branch, and inside the n+3 one always.