Intrinsic radical squares at interior interval targets

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_radicalSquare_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (a b : S.standardFormSupportedLabel m) (ht0 : 0 ≤ ↑b.snd) (htm : ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) (f : S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) : f.hom ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom (S.standardFormSupportedFamily m a).obj (S.standardFormSupportedFamily m b).obj ↔ f ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)

At an interior target, restriction preserves and reflects membership in the square of the intrinsic categorical radical.