Finite interaction neighborhoods

The covering argument enlarges a finite seed window three times by adjoining all objects having a nonzero Hom in either direction with an object already present. This file isolates the relation-theoretic content of that construction. Locally finite interaction neighborhoods remain finite under iteration, and an invariant interaction relation makes every iterated window equivariant under the deck-group action. The resulting three-step window can therefore be passed directly to finite residual quotient separation.

def MagnitudeConjecture.CoveringSeparation.interactionNeighborhood {X : Type v} (R : X → X → Prop) (W : Set X) : Set X

Enlarge a set by taking every point interacting with one of its points.

@[simp]

theorem MagnitudeConjecture.CoveringSeparation.mem_interactionNeighborhood_iff {X : Type v} (R : X → X → Prop) (W : Set X) (y : X) : y ∈ interactionNeighborhood R W ↔ ∃ x ∈ W, R x y

theorem MagnitudeConjecture.CoveringSeparation.subset_interactionNeighborhood {X : Type v} (R : X → X → Prop) (reflexive : ∀ (x : X), R x x) (W : Set X) : W ⊆ interactionNeighborhood R W

A reflexive interaction relation makes each window lie in its first enlargement.

theorem MagnitudeConjecture.CoveringSeparation.interactionNeighborhood_mono {X : Type v} (R : X → X → Prop) : Monotone (interactionNeighborhood R)

Interaction-neighborhood enlargement is monotone in the seed set.

theorem MagnitudeConjecture.CoveringSeparation.interactionNeighborhood_finite {X : Type v} (R : X → X → Prop) (locallyFinite : ∀ (x : X), {y : X | R x y}.Finite) (W : Set X) (hW : W.Finite) : (interactionNeighborhood R W).Finite

A finite set has finite interaction neighborhood when every point has only finitely many interaction neighbors.

def MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood {X : Type v} (R : X → X → Prop) : ℕ → Set X → Set X

Iteration of interaction-neighborhood enlargement. In the manuscript, iterateInteractionNeighborhood R i U₀ is the control window Uᵢ.

@[simp]

theorem MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood_zero {X : Type v} (R : X → X → Prop) (W : Set X) : iterateInteractionNeighborhood R 0 W = W

@[simp]

theorem MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood_succ {X : Type v} (R : X → X → Prop) (n : ℕ) (W : Set X) : iterateInteractionNeighborhood R (n + 1) W = interactionNeighborhood R (iterateInteractionNeighborhood R n W)

theorem MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood_finite {X : Type v} (R : X → X → Prop) (locallyFinite : ∀ (x : X), {y : X | R x y}.Finite) (W : Set X) (hW : W.Finite) (n : ℕ) : (iterateInteractionNeighborhood R n W).Finite

Every finite seed has finite iterated neighborhoods.

theorem MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood_subset_succ {X : Type v} (R : X → X → Prop) (reflexive : ∀ (x : X), R x x) (W : Set X) (n : ℕ) : iterateInteractionNeighborhood R n W ⊆ iterateInteractionNeighborhood R (n + 1) W

For a reflexive relation the control windows form an increasing sequence.

theorem MagnitudeConjecture.CoveringSeparation.interactionNeighborhood_smul {X : Type v} {G : Type u} [Group G] [MulAction G X] (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (g : G) (W : Set X) : interactionNeighborhood R (g • W) = g • interactionNeighborhood R W

Invariance of the interaction relation makes one neighborhood enlargement commute with the group action.

theorem MagnitudeConjecture.CoveringSeparation.iterateInteractionNeighborhood_smul {X : Type v} {G : Type u} [Group G] [MulAction G X] (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (g : G) (W : Set X) (n : ℕ) : iterateInteractionNeighborhood R n (g • W) = g • iterateInteractionNeighborhood R n W

Every iterated control window commutes with the group action.

def MagnitudeConjecture.CoveringSeparation.threeStepControlWindow {X : Type v} (R : X → X → Prop) (W : Set X) : Set X

The manuscript's control window after three successive Hom-neighborhood enlargements.

theorem MagnitudeConjecture.CoveringSeparation.threeStepControlWindow_finite {X : Type v} (R : X → X → Prop) (locallyFinite : ∀ (x : X), {y : X | R x y}.Finite) (W : Set X) (hW : W.Finite) : (threeStepControlWindow R W).Finite

The three-step control window of a finite seed is finite.

theorem MagnitudeConjecture.CoveringSeparation.threeStepControlWindow_smul {X : Type v} {G : Type u} [Group G] [MulAction G X] (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (g : G) (W : Set X) : threeStepControlWindow R (g • W) = g • threeStepControlWindow R W

The three-step control-window construction is equivariant.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_preserving_threeStepControlWindow {X : Type v} {G : Type u} [Group G] [MulAction G X] [Group.ResiduallyFinite G] (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (reflexive : ∀ (x : X), R x x) (neighborsFinite : ∀ (x : X), {y : X | R x y}.Finite) (translationsFinite : ∀ (x y : X), {g : G | R x (g • y)}.Finite) (W : Set X) (hW : W.Finite) : ∃ (N : FiniteIndexNormalSubgroup G), Set.InjOn (fun (x : X) => Quotient.mk'' x) (threeStepControlWindow R W) ∧ ∀ ⦃x y : X⦄, x ∈ threeStepControlWindow R W → y ∈ threeStepControlWindow R W → (OrbitQuotientInteracts N.toSubgroup R (Quotient.mk'' x) (Quotient.mk'' y) ↔ R x y)

Residual finiteness produces a finite quotient that embeds and preserves all interactions in the manuscript's finite three-step control window.

theorem MagnitudeConjecture.CoveringSeparation.exists_finiteIndexNormalSubgroup_preserving_threeStepControlWindow_of_finite_support {X : Type v} {G : Type u} [Group G] [MulAction G X] {O : Type w} [MulAction G O] [IsCancelSMul G O] [Group.ResiduallyFinite G] (support : X → Set O) (support_finite : ∀ (x : X), (support x).Finite) (support_smul : ∀ (g : G) (x : X) (o : O), o ∈ support (g • x) ↔ g⁻¹ • o ∈ support x) (R : X → X → Prop) (invariant : ∀ (g : G) (x y : X), R (g • x) (g • y) ↔ R x y) (reflexive : ∀ (x : X), R x x) (neighborsFinite : ∀ (x : X), {y : X | R x y}.Finite) (interaction_meets_support : ∀ {x y : X}, R x y → ∃ o ∈ support x, o ∈ support y) (W : Set X) (hW : W.Finite) : ∃ (N : FiniteIndexNormalSubgroup G), Set.InjOn (fun (x : X) => Quotient.mk'' x) (threeStepControlWindow R W) ∧ ∀ ⦃x y : X⦄, x ∈ threeStepControlWindow R W → y ∈ threeStepControlWindow R W → (OrbitQuotientInteracts N.toSubgroup R (Quotient.mk'' x) (Quotient.mk'' y) ↔ R x y)

Finite equivariant supports discharge the translate-finiteness hypothesis for separation of the three-step window.