Strict positivity of the localized principal Koszul Euler characteristic over the base ring.

theorem AlgebraicAnalysis.BaseLocalizedKoszulPositivity.localized_length_cokernel_gt_kernel {R : Type u_1} {C : Type u_2} {E : Type u_3} [CommRing R] [CommRing C] [Algebra R C] [AddCommGroup E] [Module R E] [Module C E] [IsScalarTower R C E] [IsNoetherianRing R] [IsNoetherianRing C] [Module.Finite C E] (x : C) [Module.Finite R ↥(↑R ((LinearMap.lsmul C E) x)).ker] [Module.Finite R (E ⧸ (↑R ((LinearMap.lsmul C E) x)).range)] (q : PrimeSpectrum R) (hqmem : q ∈ Module.support R (E ⧸ (↑R ((LinearMap.lsmul C E) x)).range)) (hqmin : ∀ p ∈ Module.support R (E ⧸ (↑R ((LinearMap.lsmul C E) x)).range), p.asIdeal ≤ q.asIdeal → q.asIdeal ≤ p.asIdeal) (havoid : ∀ p ∈ (Module.annihilator C E).minimalPrimes, x ∉ p) : Module.length (Localization q.asIdeal.primeCompl) (LocalizedModule q.asIdeal.primeCompl (E ⧸ (↑R ((LinearMap.lsmul C E) x)).range)) > Module.length (Localization q.asIdeal.primeCompl) (LocalizedModule q.asIdeal.primeCompl ↥(↑R ((LinearMap.lsmul C E) x)).ker)