CoordinateCurvatureMajorization

Abstract

Strict positive T-transform chains for spectral cube-root curvature.

Theorem 1.1 (spectral_moreMixed_monotone).

$$\forall \{n:\mathbb{N}\}(pq:\mathrm{Fin}n\to \mathbb{R}),(2\le n)\to (p\in \mathrm{simplex}n)\to (q\in \mathrm{simplex}n)\to (\mathrm{moreMixed}qp)\to \mathrm{lambdaRatio}p\le \mathrm{lambdaRatio}q$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.2 (spectral_moreMixed_strict).

$$\forall \{n:\mathbb{N}\}(pq:\mathrm{Fin}n\to \mathbb{R}),(2\le n)\to (p\in \mathrm{simplex}n)\to (q\in \mathrm{simplex}n)\to (\mathrm{moreMixed}qp)\to (\neg \exists \pi :\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}n),q=p\circ \pi )\to \mathrm{lambdaRatio}p<\mathrm{lambdaRatio}q$$

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

Source. Repository-derived.

Commentary.

The positive T-transform chain contains a strict step unless its endpoints differ by a permutation. Monotonicity before and after that step gives strict spectral curvature comparison.

References

• Truth anchor: D5/S3/Geometry/AlphaGeometry/CoordinateCurvatureMajorization.spectral_moreMixed_monotone
• Truth anchor: D5/S3/Geometry/AlphaGeometry/CoordinateCurvatureMajorization.spectral_moreMixed_strict
• Dependency: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity
• Dependency: D5/S3/Geometry/AlphaGeometry/LogScalarCurvatureMonotone