RootInterfaceGate

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

1. The sharp criterion for the cube gate

theorem Algsuperdiff.Section4.Provider.Regularity.image_add_subset_openCubeSet_of_forall_abs_le {d : ℕ} {m q : ℤ} {z : HCPolySupport.Vec d} (h : ∀ (i : Fin d), |z i| + 1 / 2 * 3 ^ q ≤ 1 / 2 * 3 ^ m) : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The cube gate from the coordinate gaps. If every coordinate of z clears ½·3^m − ½·3^q, the translated cube z + □_q sits inside □_m.

theorem Algsuperdiff.Section4.Provider.Regularity.image_add_subset_openCubeSet_iff {d : ℕ} {m q : ℤ} {z : HCPolySupport.Vec d} : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ↔ ∀ (i : Fin d), |z i| + 1 / 2 * 3 ^ q ≤ 1 / 2 * 3 ^ m

The gate criterion, both directions. z + □_q ⊆ □_m holds exactly when every coordinate of z clears the gap ½·3^m − ½·3^q.

3. The truncated form, and the join's geometric half

theorem Algsuperdiff.Section4.Provider.Regularity.truncatedWindow_eq_image_add_iff {d : ℕ} {m q : ℤ} {z : HCPolySupport.Vec d} : ExcessDecay.truncatedWindow z m q = (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d q) ↔ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The truncated window is untruncated exactly on the gated scales. This is the dichotomy in the carrier the chain uses: (z + □_q) ∩ □_m = z + □_q iff the gate holds, and otherwise the intersection is a subset.

theorem Algsuperdiff.Section4.Provider.Regularity.gate_or_exists_meetsFace {d : ℕ} (z : HCPolySupport.Vec d) (m q : ℤ) : (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d q) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ∨ ∃ (i : Fin d), ExcessDecay.MeetsUpperFace z m q i ∨ ExcessDecay.MeetsLowerFace z m q i

The join's window hypothesis holds centre scale.

ExcessDecay.excessDecay_oneStep_anchored replaces the interior gate by the disjunction "gate OR a met face of ∂□_m"; its geometric half is a tautology, because a window that meets no face of ∂□_m in any coordinate clears the gap in every coordinate. So the boundary hstep4 run owes the geometry nothing: what it still needs from the join's second disjunct is the competitor data (the MemLp clauses, met-face oddness and classical harmonicity on the doubled window), which is analytic.