Shift orthogonality on additive control windows

Pairwise nonidentity shift-Hom vanishing for a finite family of indecomposable modules extends to every finite biproduct in its additive hull. This is the bridge from residual separation of the manuscript's finite vertex set to fullness of push-down on the categorical window that contains relevant factorization cores.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteModuleWindowShiftHomOrthogonal_isoClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : FiniteIndecomposableModuleFamily) : D.FiniteModuleWindowShiftHomOrthogonal (Set.range S.obj) → D.FiniteModuleWindowShiftHomOrthogonal S.isoClosure

Nonidentity shift-Hom vanishing on the literal finite range of chosen representatives extends across isomorphisms.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteModuleWindowShiftHomOrthogonal_additiveClosure {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : FiniteIndecomposableModuleFamily) : D.FiniteModuleWindowShiftHomOrthogonal S.isoClosure → D.FiniteModuleWindowShiftHomOrthogonal S.additiveClosure

Nonidentity shift-Hom vanishing on the finite indecomposable generators extends to their full additive hull.