CubeRootSpectralMonotonicity

Abstract

Moment-deficit positivity and strict spectral cube-root T-transform growth.

Definition 1.1 (spectralN).

$$\forall \{n:\mathbb{N}\}(r:\mathrm{Fin}n\to \mathbb{R}),\mathrm{spectralN}r=((4\ast (n:\mathbb{R}{)}^2-2)\ast (Pnr1{)}^2-2\ast (n:\mathbb{R})\ast Pnr2)\ast Pnr4-8\ast (n:\mathbb{R})\ast Pnr1\ast Pnr5+8\ast Pnr6$$

Formalization. D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.spectralN (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of spectralN.

Definition 1.2 (spectralRatio).

$$\forall \{n:\mathbb{N}\}(r:\mathrm{Fin}n\to \mathbb{R}),\mathrm{spectralRatio}r=\mathrm{spectralN}r/(9\ast (Pnr4{)}^2)$$

Formalization. D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.spectralRatio (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of spectralRatio.

Definition 1.3 (lambdaRatio).

$$\forall \{n:\mathbb{N}\}(l:\mathrm{Fin}n\to \mathbb{R}),\mathrm{lambdaRatio}l=\mathrm{spectralRatio}(\mathrm{fun}i\mapsto l{i}^{(1/3:\mathbb{R})})$$

Formalization. D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.lambdaRatio (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of lambdaRatio.

Theorem 1.4 (lambdaRatio_perm).

$$\forall \{n:\mathbb{N}\}(l:\mathrm{Fin}n\to \mathbb{R})(p:\mathrm{Equiv}.\mathrm{Perm}(\mathrm{Fin}n)),\mathrm{lambdaRatio}(l\circ p)=\mathrm{lambdaRatio}l$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.5 (strict_t_transform_any_pair).

$$\forall (n:\mathbb{N})(l:\mathrm{Fin}n\to \mathbb{R})(ij:\mathrm{Fin}n)(t:\mathbb{R}),(2\le n)\to (\forall k,0<lk)\to (lj<li)\to (0<t)\to (t<1)\to \mathrm{lambdaRatio}l<\mathrm{lambdaRatio}(((1-t)\cdot l+t\cdot (l\circ \mathrm{Equiv}.\mathrm{swap}ij)))$$

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

Source. Repository-derived.

Commentary.

A strict equalizing T-transform increases the spectral curvature ratio. The derivative is positive before the midpoint; permutation symmetry handles the other half.

References

• Truth anchor: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.lambdaRatio
• Truth anchor: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.lambdaRatio_perm
• Truth anchor: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.spectralN
• Truth anchor: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.spectralRatio
• Truth anchor: D5/S3/Geometry/AlphaGeometry/CubeRootSpectralMonotonicity.strict_t_transform_any_pair
• Dependency: D5/S3/Geometry/AlphaGeometry/PairCurvatureInequality