HermitianCubeDerivative

Abstract

The smooth cube-root immersion and its Hermitian normal and operator traces.

For any finite index type, let H be the real vector space of complex Hermitian matrices and let Omega consist of its positive definite matrices. The actual functional-calculus map R(A) = CFC.sqrt(A), lifted to H using its nonnegativity, is infinitely differentiable at every point of Omega. The matrix-valued map has the same regularity by the continuous linear inclusion of H. The differentiability order is the smooth order, not the analytic order.

The square map has derivative jordan(Y), the operator V mapped to YV + VY, by square_hasFDerivAt, and is smooth by square_contDiff. The original diagonalH, hermitianConj, diagonal_conjugated_jordan and jordan_conjugation identify this operator in real coordinates with multiplication by the coefficients lambda(i) + lambda(j). Positive definiteness makes every coefficient positive, so the operator is injective and hence a continuous linear equivalence in finite dimension. At Y = R(A), CFC.sq_sqrt gives square(Y) = A. On the positive definite neighborhood of Y, CFC.sqrt_sq gives R(square(X)) = X. HasStrictFDerivAt.localInverse_unique identifies R with the same local inverse furnished by the inverse function theorem, whose smoothness follows from ContDiffAt.to_localInverse. This argument does not assume continuity of R.

A fixed equivalence from the index type to Fin(cardinality) transports the self-adjoint subspaces by a real continuous linear equivalence. Reindexing preserves positive definiteness; CFC.sqrt_unique identifies the transported nonnegative square root with the actual root. The zero-dimensional space is included. Repeated positive eigenvalues cause no exception because the coefficients are sums, rather than differences, and the eigenbasis is chosen only at the fixed base point.

Definition 1.1 (alphaEmbed3).

$$\forall \{n:\mathbb{N}\}(A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),alphaEmbed3A=(3:\mathbb{C})\cdot \mathrm{CFC}.\mathrm{rpow}A(1/3:\mathbb{R})$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.alphaEmbed3 (✓ 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.5 (printed p. 11): “The α-geometry on D¹ₙ is the geometry induced by the pull-back of the map Aₚ(ρ): D¹ₙ → Mₙ defined by” Aₚ(ρ) := pρ^(1/p) for p ∈ R \ {0}, and log(ρ) for p = ∞, where p = 2/(1−α). Here p = 3 and CFC.rpow is the operator functional calculus.

Definition 1.2 (root).

$$\forall \{n:\mathbb{N}\}(A:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))(h:\mathrm{IsSelfAdjoint}(\mathrm{CFC}.\mathrm{rpow}A.\mathrm{val}(1/3:\mathbb{R}))),\mathrm{root}A=(⟨\mathrm{CFC}.\mathrm{rpow}A.\mathrm{val}(1/3:\mathbb{R}),h⟩:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.root (✓ std3).

Source. Repository-derived.

Commentary.

The operator cube root in the real Hermitian subspace. The self-adjointness proof field is explicitly bound; proof irrelevance fixes the subtype value.

Theorem 1.3 (root_posdef).

$$\forall \{n:\mathbb{N}\}(A:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(A.\mathrm{val}.\mathrm{PosDef})\to (\mathrm{root}A).\mathrm{val}.\mathrm{PosDef}$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.4 (root_contDiffAt_cube).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(Y.\mathrm{val}.\mathrm{PosDef})\to \mathrm{ContDiffAt}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })\mathrm{root}(\mathrm{cube}Y)$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.5 (rhoH).

$$\forall \{n:\mathbb{N}\}(x:\mathrm{Fin}(n^2-1)\to \mathbb{R}),\mathrm{rhoH}x=\mathrm{selfAdjointPartL}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})(\mathrm{rho}x)$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.rhoH (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of rhoH.

Theorem 1.6 (rhoH_val).

$$\forall \{n:\mathbb{N}\}(x:(\mathrm{Fin}(n^2-1)\to \mathbb{R})),(\mathrm{rhoH}x).\mathrm{val}=\mathrm{rho}x$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.7 (immersion).

$$\forall \{n:\mathbb{N}\}(x:(\mathrm{Fin}(n^2-1)\to \mathbb{R})),\mathrm{immersion}x=\mathrm{root}(\mathrm{rhoH}x)$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.immersion (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of immersion.

Theorem 1.8 (immersion_contDiffAt).

$$\forall \{n:\mathbb{N}\}(x:(\mathrm{Fin}(n^2-1)\to \mathbb{R})),((\mathrm{rho}x).\mathrm{PosDef})\to \mathrm{ContDiffAt}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })\mathrm{immersion}x$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.9 (immersion_derivative_injective).

$$\forall \{n:\mathbb{N}\}(x:(\mathrm{Fin}(n^2-1)\to \mathbb{R})),(0<n)\to ((\mathrm{rho}x).\mathrm{PosDef})\to \mathrm{Function}.\mathrm{Injective}(\mathrm{fderiv}\mathbb{R}\mathrm{immersion}x)$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.10 (immersion_level_one).

$$\forall \{n:\mathbb{N}\}(x:(\mathrm{Fin}(n^2-1)\to \mathbb{R})),(0<n)\to ((\mathrm{rho}x).\mathrm{PosDef})\to F(\mathrm{immersion}x)=1$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.11 (herm_inner_smul_left).

$$\forall \{n:\mathbb{N}\}(c:\mathbb{R})(AB:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((c\cdot A))\ast (B)))=c\ast \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast (B)))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.12 (herm_inner_smul_right).

$$\forall \{n:\mathbb{N}\}(c:\mathbb{R})(AB:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast ((c\cdot B))))=c\ast \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast (B)))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.13 (herm_inner_add_right).

$$\forall \{n:\mathbb{N}\}(ABC:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast ((B+C))))=\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast (B)))+\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast (C)))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.14 (herm_inner_symm).

$$\forall \{n:\mathbb{N}\}(AB:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((A)\ast (B)))=\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}((B)\ast (A)))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.15 (trace_pow_eq_eigenvalues).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))(k:\mathbb{N}),(Y.{\mathrm{val}}^k).\mathrm{trace}.\mathrm{re}=\sum i,(Y.\mathrm{property}.\mathrm{isHermitian}.\mathrm{eigenvalues}i{)}^k$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.16 (S4).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),S4Y=(Y.{\mathrm{val}}^4).\mathrm{trace}.\mathrm{re}$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.S4 (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of S4.

Theorem 1.17 (S4_eq_sum).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),S4Y=\sum i,Y.\mathrm{property}.\mathrm{isHermitian}.\mathrm{eigenvalues}{i}^4$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.18 (S4_pos).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(0<n)\to (Y.\mathrm{val}.\mathrm{PosDef})\to 0<S4Y$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.19 (normal).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),\mathrm{normal}Y=(\mathrm{Real}.\mathrm{sqrt}(S4Y){)}^{-1}\cdot (⟨Y.{\mathrm{val}}^2,Y.\mathrm{property}.\mathrm{pow}2⟩:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.normal (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of normal.

Theorem 1.20 (normal_val).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(\mathrm{normal}Y).\mathrm{val}=(\mathrm{Real}.\mathrm{sqrt}(S4Y){)}^{-1}\cdot Y.{\mathrm{val}}^2$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.21 (normal_unit).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(0<S4Y)\to \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((\mathrm{normal}Y).\mathrm{val})\ast ((\mathrm{normal}Y).\mathrm{val})))=1$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.22 (DF_normal).

$$\forall \{n:\mathbb{N}\}(YV:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(0<S4Y)\to \mathrm{fderiv}\mathbb{R}FYV=3\ast \mathrm{Real}.\mathrm{sqrt}(S4Y)\ast \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((\mathrm{normal}Y).\mathrm{val})\ast (V.\mathrm{val})))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.23 (jordan).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{jordan}Y=(\mathrm{selfAdjointPartL}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{comp}((((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{toContinuousBilinearMap}Y.\mathrm{val}).\mathrm{comp}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{subtypeL})+(((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{toContinuousBilinearMap}).\mathrm{flip}Y.\mathrm{val}).\mathrm{comp}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{subtypeL})$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.jordan (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of jordan.

Theorem 1.24 (jordan_val).

$$\forall \{n:\mathbb{N}\}(YV:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(\mathrm{jordan}YV).\mathrm{val}=Y.\mathrm{val}\ast V.\mathrm{val}+V.\mathrm{val}\ast Y.\mathrm{val}$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.25 (square).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{square}Y=(⟨Y.{\mathrm{val}}^2,Y.\mathrm{property}.\mathrm{pow}2⟩:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.square (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of square.

Definition 1.26 (DS4).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),DS4Y=(4:\mathbb{R})\cdot (((\mathrm{Complex}.\mathrm{reCLM}.\mathrm{comp}(\mathrm{Matrix}.\mathrm{traceLinearMap}(\mathrm{Fin}n)\mathbb{RC}).\mathrm{toContinuousLinearMap})).\mathrm{comp}(((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{toContinuousBilinearMap}(Y.{\mathrm{val}}^3)).\mathrm{comp}((\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))).\mathrm{subtypeL}))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.DS4 (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of DS4.

Definition 1.27 (projection).

$$\forall \{n:\mathbb{N}\}(YV:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{projection}YV=V-\mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((\mathrm{normal}Y).\mathrm{val})\ast (V.\mathrm{val})))\cdot \mathrm{normal}Y$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.projection (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of projection.

Theorem 1.28 (regular_level_set_shape_operator).

$$\forall \{n:\mathbb{N}\}(YV:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(0<S4Y)\to \mathrm{fderiv}\mathbb{R}\mathrm{normal}YV=(\mathrm{Real}.\mathrm{sqrt}(S4Y){)}^{-1}\cdot \mathrm{projection}Y(\mathrm{jordan}YV)$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.29 (normal_contDiffAt).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),(0<S4Y)\to \mathrm{ContDiffAt}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })\mathrm{normal}Y$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.30 (readoutEquiv).

$$\forall (n:\mathbb{N}),\mathrm{let}f:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})){\to }_l[\mathbb{R}](\mathrm{Fin}n\times \mathrm{Fin}n\to \mathbb{R}):=\mathrm{LinearMap}.\mathrm{pi}(\mathrm{fun}(p:\mathrm{Fin}n\times \mathrm{Fin}n)\mapsto (\mathrm{if}p.1\le p.2\mathrm{then}\mathrm{Complex}.\mathrm{reCLM}.\mathrm{toLinearMap}\mathrm{else}\mathrm{Complex}.\mathrm{imCLM}.\mathrm{toLinearMap}).\mathrm{comp}(((\mathrm{LinearMap}.\mathrm{proj}p.2).\mathrm{comp}(\mathrm{LinearMap}.\mathrm{proj}p.1)).\mathrm{comp}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{subtype}));\forall (\mathrm{hB}:\mathrm{Function}.\mathrm{Bijective}f),\mathrm{readoutEquiv}n=\mathrm{LinearEquiv}.\mathrm{ofBijective}f\mathrm{hB}$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.readoutEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The full real-coordinate equivalence construction. Its coordinate map is displayed as the local f, and its bijectivity proof is bound explicitly; proof irrelevance fixes the inverse equivalence.

Theorem 1.31 (hermitian_jordan_operator_trace_formulas).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{LinearMap}.\mathrm{trace}\mathbb{R}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))(\mathrm{jordan}Y).\mathrm{toLinearMap}=2\ast (n:\mathbb{R})\ast (\sum i,Y.\mathrm{property}.\mathrm{isHermitian}.\mathrm{eigenvalues}i)\wedge \mathrm{LinearMap}.\mathrm{trace}\mathbb{R}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))((\mathrm{jordan}Y).{\mathrm{toLinearMap}}^2)=2\ast (n:\mathbb{R})\ast (\sum i,Y.\mathrm{property}.\mathrm{isHermitian}.\mathrm{eigenvalues}{i}^2)+2\ast (\sum i,Y.\mathrm{property}.\mathrm{isHermitian}.\mathrm{eigenvalues}i{)}^2$$

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

Source. Repository-derived.

Commentary.

The real Hermitian Jordan operator has diagonal eigenvalues 2λᵢ and off-diagonal eigenvalues λᵢ + λⱼ. Their real multiplicities determine the first two operator traces.

Definition 1.32 (rankOneProjection).

$$\forall (V:\mathrm{Type})[\mathrm{AddCommGroup}V][\mathrm{Module}\mathbb{R}V](f:V{\to }_l[\mathbb{R}]\mathbb{R})(u:V),\mathrm{rankOneProjection}fu=1-\mathrm{LinearMap}.\mathrm{smulRight}fu$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.rankOneProjection (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of projection.

Theorem 1.33 (gauss_trace_rank_one_contraction).

$$\forall \{V:\mathrm{Type}\}[\mathrm{AddCommGroup}V][\mathrm{Module}\mathbb{R}V][\mathrm{Module}.\mathrm{Free}\mathbb{R}V][\mathrm{Module}.\mathrm{Finite}\mathbb{R}V](f:V{\to }_l[\mathbb{R}]\mathbb{R})(u:V)(K:\mathrm{Module}.\mathrm{End}\mathbb{R}V)(s:\mathbb{R}),(fu=1)\to (s\ne 0)\to (\mathrm{LinearMap}.\mathrm{trace}\mathbb{R}V(s^{-1}\cdot (\mathrm{rankOneProjection}fu\ast K\ast \mathrm{rankOneProjection}fu)){)}^2-\mathrm{LinearMap}.\mathrm{trace}\mathbb{R}V((s^{-1}\cdot (\mathrm{rankOneProjection}fu\ast K\ast \mathrm{rankOneProjection}fu){)}^2)=((\mathrm{LinearMap}.\mathrm{trace}\mathbb{R}VK{)}^2-\mathrm{LinearMap}.\mathrm{trace}\mathbb{R}V(K^2)-2\ast \mathrm{LinearMap}.\mathrm{trace}\mathbb{R}VK\ast f(Ku)+2\ast f((K^2)u))/s^2$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

References

• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.DF_normal
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.DS4
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.S4
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.S4_eq_sum
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.S4_pos
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.alphaEmbed3
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.gauss_trace_rank_one_contraction
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.herm_inner_add_right
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.herm_inner_smul_left
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.herm_inner_smul_right
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.herm_inner_symm
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.hermitian_jordan_operator_trace_formulas
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.immersion
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.immersion_contDiffAt
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.immersion_derivative_injective
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.immersion_level_one
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.jordan
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.jordan_val
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.normal
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.normal_contDiffAt
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.normal_unit
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.normal_val
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.projection
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.rankOneProjection
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.readoutEquiv
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.regular_level_set_shape_operator
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.rhoH
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.rhoH_val
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.root
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.root_contDiffAt_cube
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.root_posdef
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.square
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianCubeDerivative.trace_pow_eq_eigenvalues
• Dependency: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus