QuantumCubeRootScalarCurvatureMonotone

Abstract

Quantum cube-root scalar curvature is strictly Schur-increasing.

Definition 1.1 (densityStates).

$$\forall (n:\mathbb{N}),\mathrm{densityStates}n=\{A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}\mid A.\mathrm{PosDef}\wedge A.\mathrm{trace}=1\}$$

Formalization. D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.densityStates (✓ std3).

Citation. Paolo Gibilisco; Tommaso Isola (2005). On the monotonicity of scalar curvature in classical and quantum information geometry. DOI: 10.1063/1.1834693. URL: https://arxiv.org/abs/math-ph/0407007v2.

Commentary.

Definition 2.5 (printed p. 4) defines “D¹ₙ := {ρ ∈ Mⁿ | Trρ = 1, ρ > 0}”. The carrier is the space of complex n by n matrices; Matrix.PosDef supplies Hermitian symmetry and strict positivity.

Definition 1.2 (metric).

$$\forall \{n:\mathbb{N}\}(x:\mathrm{Fin}(n^2-1)\to \mathbb{R}),\mathrm{metric}x=\mathrm{fun}(ij:\mathrm{Fin}(n^2-1))\mapsto \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((\mathrm{fderiv}\mathbb{R}(alphaEmbed3\circ \mathrm{rho})x(\mathrm{Pi}.\mathrm{single}i1)))\ast ((\mathrm{fderiv}\mathbb{R}(alphaEmbed3\circ \mathrm{rho})x(\mathrm{Pi}.\mathrm{single}j1)))))$$

Formalization. D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.metric (✓ std3).

Citation. Paolo Gibilisco; Tommaso Isola (2005). On the monotonicity of scalar curvature in classical and quantum information geometry. DOI: 10.1063/1.1834693. URL: https://arxiv.org/abs/math-ph/0407007v2.

Commentary.

The defining expression of metric.

Definition 1.3 (scal3).

$$\forall \{n:\mathbb{N}\}(A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),scal3A=\mathrm{scalarCurvature}\mathrm{metric}(\mathrm{chartPoint}A)$$

Formalization. D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.scal3 (✓ std3).

Citation. Paolo Gibilisco; Tommaso Isola (2005). On the monotonicity of scalar curvature in classical and quantum information geometry. DOI: 10.1063/1.1834693. URL: https://arxiv.org/abs/math-ph/0407007v2.

Commentary.

Definition 4.6 (printed p. 11): “We denote by Scalₚ(ρ) the scalar curvature of the α-geometry (with p = 2/(1−α)) at the point ρ ∈ D¹ₙ.” The p = 3 curvature is the coordinate Christoffel–Ricci contraction of the pull-back metric.

Definition 1.4 (eig).

$$\forall \{n:\mathbb{N}\}(A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\mathrm{eig}A=\mathrm{if}h:A.\mathrm{IsHermitian}\mathrm{then}h.\mathrm{eigenvalues}\mathrm{else}0$$

Formalization. D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.eig (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of eig.

Definition 1.5 (claim).

$$\mathrm{claim}=\forall n:\mathbb{N},2\le n\to \forall AB:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C},A\in \mathrm{densityStates}n\to B\in \mathrm{densityStates}n\to \mathrm{PositiveSimplexGeometryAndMixing}.\mathrm{moreMixed}(\mathrm{eig}A)(\mathrm{eig}B)\to scal3B\le scal3A\wedge ((\neg \exists \mathrm{pi}:\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}n),\mathrm{eig}A=\mathrm{eig}B\circ \mathrm{pi})\to scal3B<scal3A)$$

Formalization. D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.claim (✓ std3).

Citation. Paolo Gibilisco; Tommaso Isola (2005). On the monotonicity of scalar curvature in classical and quantum information geometry. DOI: 10.1063/1.1834693. URL: https://arxiv.org/abs/math-ph/0407007v2.

Commentary.

Conjecture 4.2 (printed p. 11): “Suppose n ≥ 2. For the function Scalₚ(·): D¹ₙ → R one has the following properties: - if p ∈ (1, 2) then Scalₚ(·) is a strictly Schur-decreasing function; - if p ∈ (2, +∞] then Scalₚ(·) is a strictly Schur-increasing function.” This statement encodes the p = 3 clause, with faithful complex density matrices, the fixed eigenvalue vector, and strictness away from permutations.

Theorem 1.6 (scal3_eq_spectral_ratio).

$$\forall (n:\mathbb{N})(A:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),(2\le n)\to (A\in \mathrm{densityStates}n)\to scal3A=\mathrm{CubeRootSpectralMonotonicity}.\mathrm{Vector}.\mathrm{lambdaRatio}(\mathrm{eig}A)$$

Proof. Machine-checked in Lean as D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.scal3_eq_spectral_ratio (✓ std3). ∎

Source. Repository-derived.

Commentary.

The intrinsic coordinate curvature equals the ratio of cube-root eigenvalue power sums. The normal derivative, Gauss contraction, and real Hermitian Jordan traces give this identity.

Theorem 1.7 (result).

$$\forall n:\mathbb{N},2\le n\to \forall AB:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C},A\in \mathrm{densityStates}n\to B\in \mathrm{densityStates}n\to \mathrm{PositiveSimplexGeometryAndMixing}.\mathrm{moreMixed}(\mathrm{eig}A)(\mathrm{eig}B)\to scal3B\le scal3A\wedge ((\neg \exists \mathrm{pi}:\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}n),\mathrm{eig}A=\mathrm{eig}B\circ \mathrm{pi})\to scal3B<scal3A)$$

Proof. Machine-checked in Lean as D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.result (✓ std3). ∎

Resolves. Problems/gibilisco-isola-2004-quantum-cube-root-scalar-curvature (proved) by D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.result.

Source. Repository-derived.

Acknowledgement. Paolo Gibilisco; Tommaso Isola (2005). On the monotonicity of scalar curvature in classical and quantum information geometry. DOI: 10.1063/1.1834693. URL: https://arxiv.org/abs/math-ph/0407007v2.

Commentary.

The quantum cube-root pull-back curvature increases under the source majorization order, strictly unless the eigenvalue vectors differ by a permutation.

References

• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.claim
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.densityStates
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.eig
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.metric
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.result
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.scal3
• Truth anchor: D5/S3/Geometry/AlphaGeometry/QuantumCubeRootScalarCurvatureMonotone.scal3_eq_spectral_ratio
• Dependency: D5/S3/Geometry/AlphaGeometry/CoordinateCurvatureMajorization
• Dependency: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative
• Dependency: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus