Uniform residual separation for object-deletion stages

The manuscript first chooses one finite module family controlling every intermediate object-deletion stage and then uses residual finiteness once on that family. This file joins those two already formalized steps: the subgroup is independent of the deletion stage, and its nonidentity shifted Homs vanish on the entire additive closure of the common control family.

theorem MagnitudeConjecture.ObjectDeletion.exists_uniformControlFamily_and_residuallySeparatedWindow_for_threeStepDeletionStages {k : Type v} [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type v} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoveringHom.CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [Group.ResiduallyFinite G] (hlocal : CoveringHom.IsLocallyRepresentationFinite) (y : C) (Allowed : Set C → Prop) (Control : Set C → CoveringHom.FiniteIndecomposableModuleFamily → Prop) (exists_control : ∀ (E : Set C), Allowed E → ∃ (V : CoveringHom.FiniteIndecomposableModuleFamily), Control E V) (control_invariant : ∀ {E F : Set C}, Allowed E → Allowed F → deletionSurvivingIndices C (CoveringHom.finiteThreeStepControlFamily hlocal y) E = deletionSurvivingIndices C (CoveringHom.finiteThreeStepControlFamily hlocal y) F → ∀ {V : CoveringHom.FiniteIndecomposableModuleFamily}, Control E V ↔ Control F V) (control_upward : ∀ (E : Set C), Allowed E → ∀ {V U : CoveringHom.FiniteIndecomposableModuleFamily}, Control E V → V.isoClosure ⊆ U.isoClosure → Control E U) : ∃ (U : CoveringHom.FiniteIndecomposableModuleFamily), (∀ (E : Set C), Allowed E → Control E U) ∧ ∃ (N : FiniteIndexNormalSubgroup G), (∀ g ∈ CoveringHom.finiteModuleFamilySupportBadDegrees U, g ∉ N) ∧ (D.restrict N.toSubgroup).FiniteModuleWindowShiftHomOrthogonal U.additiveClosure

One application of residual finiteness separates the common finite control family selected from all realized survivor signatures. This is the formal conjunction of the manuscript's finite-union step and its choice of the normal finite-index subgroup Γ.