FaithfulPerronRegularization

Abstract

FaithfulPerronRegularization for the spectral bound of conditionally two-positive maps.

Definition 1.1 (Regularized).

$$\forall (d:\mathbb{N})(T:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(\mathrm{epsilon}:\mathbb{R})(X:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),\mathrm{Regularized}T\mathrm{epsilon}X=TX+(\mathrm{epsilon}:\mathbb{C})\cdot (\mathrm{Matrix}.\mathrm{trace}X\cdot (1:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))$$

Formalization. D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.Regularized (✓ std3).

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for Regularized. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Definition 1.2 (PerronCertificate).

$$\forall (d:\mathbb{N})(T:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(p:\mathrm{PerronCertificate}T),p.\mathrm{rho}.\mathrm{PosDef}\wedge \mathrm{Matrix}.\mathrm{trace}p.\mathrm{rho}=1\wedge Tp.\mathrm{rho}=(p.c:\mathbb{C})\cdot p.\mathrm{rho}\wedge 0<p.c\wedge p.c=\mathrm{maxReSpectrum}T\wedge \mathrm{spectralRadius}\mathbb{C}T.\mathrm{toContinuousLinearMap}=\mathrm{ENNReal}.\mathrm{ofReal}p.c$$

Formalization. D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.PerronCertificate (✓ std3).

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The carrier contains rho and c with all six displayed constraints: positive definiteness, normalized matrix trace, the eigenmatrix equation, positivity of c, maximal real part, and the spectral radius. The displayed fields rho : Matrix (Fin d) (Fin d) ℂ and c : ℝ have these types.

Definition 1.3 (RegularizedPerronGoal).

$$\mathrm{RegularizedPerronGoal}\iff \forall (d:\mathbb{N}),0<d\to \forall (T:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(\epsilon :\mathbb{R}),0<\epsilon \to (\mathrm{KPositive}2dT)\to \mathrm{Nonempty}(\mathrm{PerronCertificate}(\mathrm{Regularized}T\epsilon ))$$

Formalization. D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.RegularizedPerronGoal (✓ std3).

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for RegularizedPerronGoal. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.4 (strict positive perron eigenmatrix).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}d],\forall (T:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),(\forall X:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),X.\mathrm{PosSemidef}\to (TX).\mathrm{PosSemidef})\to (\forall X:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),X.\mathrm{PosSemidef}\to X\ne 0\to (TX).\mathrm{PosDef})\to \exists (\rho :(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(c:\mathbb{R}),\rho .\mathrm{PosDef}\wedge \mathrm{Matrix}.\mathrm{trace}\rho =1\wedge 0<c\wedge T\rho =(c:\mathbb{C})\cdot \rho$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.strict_positive_perron_eigenmatrix (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

Compactness of the normalized positive cone gives a minimum Collatz parameter. Strict positivity makes its minimizing matrix faithful. A nonzero residual can be lowered, contradicting minimality, so the minimizer is an eigenmatrix with a positive eigenvalue.

Theorem 1.5 (regularized perron certificate).

$$\mathrm{RegularizedPerronGoal}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.regularized_perron_certificate (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The trace-to-identity perturbation is strictly positivity improving. Its faithful Perron eigenmatrix controls every eigenvalue modulus; the Perron eigenvalue is both the maximal real part and the spectral radius.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.PerronCertificate
• Truth anchor: D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.Regularized
• Truth anchor: D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.RegularizedPerronGoal
• Truth anchor: D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.regularized_perron_certificate
• Truth anchor: D5/S3/Quantum/QuantumChannels/FaithfulPerronRegularization.strict_positive_perron_eigenmatrix
• Dependency: D5/S3/Quantum/Fibers/PhysicalFiber
• Dependency: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace
• Dependency: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation