Feasible spectral perturbation

Abstract

Seven spectral levels admit a nonzero trace-zero perturbation preserving both positive pencils for a positive radius.

Theorem 1.1 (A positive feasible radius).

$$\forall (l:Fin\left(9\right)\to \mathbb{R}),((Antitone\left(l\right))\wedge (\forall (i:Fin\left(9\right)),0\le l\left(i\right))\wedge (\sum _{i:Fin\left(9\right)}l\left(i\right)=1)\wedge ((K1\left(l\right)).PosSemidef)\wedge ((K2\left(l\right)).PosSemidef)\wedge (7\le (Set.range\left(l\right)).ncard))\Rightarrow (\exists (v:Fin\left(9\right)\to \mathbb{R}),(v\ne 0)\wedge (\exists (r:\mathbb{R}),(0<r)\wedge (\forall (t:\mathbb{R}),(abs\left(t\right)<r)\Rightarrow ((Antitone\left(l+HSMul.hSMul\left(t,v\right)\right))\wedge (\forall (i:Fin\left(9\right)),0\le (l+HSMul.hSMul\left(t,v\right))\left(i\right))\wedge (\sum _{i:Fin\left(9\right)}(l+HSMul.hSMul\left(t,v\right))\left(i\right)=1)\wedge ((K1\left(l+HSMul.hSMul\left(t,v\right)\right)).PosSemidef)\wedge ((K2\left(l+HSMul.hSMul\left(t,v\right)\right)).PosSemidef)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritSpectralFeasiblePerturbation.spectral_radius (✓ std3). ∎

Source. Repository-derived.

Commentary.

Seven distinct levels give a nonzero block-preserving trace-zero direction. The dependency between the two pencil kernel equations leaves at most six independent constraints. Positive leading minors and continuity give a radius preserving positive semidefiniteness, order, nonnegativity, and mass.

References

• Truth anchor: D5/S3/Quantum/Entanglement/AbsolutePPT/QutritSpectralFeasiblePerturbation.spectral_radius
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/QutritSixLevelExtremality