HermitianHypersurfaceCalculus

Abstract

Hermitian density coordinates and hypersurface calculus with the positive cubic derivative.

Definition 1.1 (G).

$$\forall (n:\mathbb{N}),\forall (k:\mathrm{Fin}\left((n^2)-(1)\right)),G\left(n,k\right)=\mathrm{fun}(r:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(s:\mathrm{Fin}\left(n\right))\mapsto \mathrm{let}row:=\mathrm{Nat}.\mathrm{div}\left(\mathrm{val}\left(k\right),n\right);\mathrm{let}col:=\mathrm{Nat}.\mathrm{mod}\left(\mathrm{val}\left(k\right),n\right);\mathrm{if}(row=col)\mathrm{then}((\mathrm{if}((\mathrm{val}\left(r\right)=row)\wedge (\mathrm{val}\left(s\right)=row))\mathrm{then}(1)\mathrm{else}(0))-(\mathrm{if}((\mathrm{val}\left(r\right)=(n)-(1))\wedge (\mathrm{val}\left(s\right)=(n)-(1)))\mathrm{then}(1)\mathrm{else}(0)))\mathrm{else}(\mathrm{if}(row<col)\mathrm{then}(\mathrm{if}(((\mathrm{val}\left(r\right)=row)\wedge (\mathrm{val}\left(s\right)=col))\vee ((\mathrm{val}\left(r\right)=col)\wedge (\mathrm{val}\left(s\right)=row)))\mathrm{then}(1)\mathrm{else}(0))\mathrm{else}((\mathrm{if}((\mathrm{val}\left(r\right)=row)\wedge (\mathrm{val}\left(s\right)=col))\mathrm{then}(\mathrm{Complex}.I)\mathrm{else}(0))-(\mathrm{if}((\mathrm{val}\left(r\right)=col)\wedge (\mathrm{val}\left(s\right)=row))\mathrm{then}(\mathrm{Complex}.I)\mathrm{else}(0))))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.G (✓ std3).

Source. Repository-derived.

Commentary.

The natural matrix-grid index omits the last diagonal position. Nat.div and Nat.mod are natural-number division and remainder. Diagonal directions subtract the final diagonal entry; the two ordered off-diagonal positions give the real and imaginary Hermitian directions.

Definition 1.2 (rho).

$$\forall (n:\mathbb{N}),\forall (x:(\mathrm{Fin}\left((n^2)-(1)\right))\to (\mathbb{R})),\mathrm{rho}\left(x\right)=(\frac{1}{n:\mathbb{R}})\cdot (1:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right))+\sum _{k:\mathrm{Fin}\left((n^2)-(1)\right)}((x\left(k\right))\cdot (G\left(n,k\right)))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.rho (✓ std3).

Source. Repository-derived.

Commentary.

The affine chart has trace-one center and traceless Hermitian coordinate directions. Scalar multiplication is over the real numbers.

Definition 1.3 (chartPoint).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),\mathrm{chartPoint}\left(A\right)=\mathrm{fun}(k:\mathrm{Fin}\left((n^2)-(1)\right))\mapsto \mathrm{let}row:=\mathrm{Nat}.\mathrm{div}\left(\mathrm{val}\left(k\right),n\right);\mathrm{let}col:=\mathrm{Nat}.\mathrm{mod}\left(\mathrm{val}\left(k\right),n\right);\mathrm{if}h:(row<n)\wedge (col<n)\mathrm{then}(\mathrm{let}entry:=A\left(⟨row,h.1⟩,⟨col,h.2⟩\right);\mathrm{if}(row=col)\mathrm{then}((entry.\mathrm{re})-(\frac{1}{n:\mathbb{R}}))\mathrm{else}(\mathrm{if}(row<col)\mathrm{then}(entry.\mathrm{re})\mathrm{else}(entry.\mathrm{im})))\mathrm{else}0$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.chartPoint (✓ std3).

Source. Repository-derived.

Commentary.

The inverse chart reads the real upper entries, the imaginary lower entries, and the centered diagonal entries. The bound proof h supplies the two Fin indices. Nat.div and Nat.mod use natural-number division and remainder.

Theorem 1.4 (rho_isHermitian).

$$\forall (n:\mathbb{N}),\forall (x:(\mathrm{Fin}\left((n^2)-(1)\right))\to (\mathbb{R})),\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{rho}\left(x\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every chart value is Hermitian.

Theorem 1.5 (rho_trace).

$$\forall (n:\mathbb{N}),(0<n)\Rightarrow (\forall (x:(\mathrm{Fin}\left((n^2)-(1)\right))\to (\mathbb{R})),\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{rho}\left(x\right)\right)=1)$$

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

Source. Repository-derived.

Commentary.

For positive matrix dimension the chart value has trace one.

Theorem 1.6 (chart_left_inverse).

$$\forall (n:\mathbb{N}),(0<n)\Rightarrow (\forall (x:(\mathrm{Fin}\left((n^2)-(1)\right))\to (\mathbb{R})),\mathrm{chartPoint}\left(\mathrm{rho}\left(x\right)\right)=x)$$

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

Source. Repository-derived.

Commentary.

Reading the coordinates of a chart value recovers every original coordinate.

Theorem 1.7 (hermitian_trace_one_chart_equiv).

$$\forall (n:\mathbb{N}),(0<n)\Rightarrow (\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(A\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(A\right)=1)\Rightarrow (\mathrm{rho}\left(\mathrm{chartPoint}\left(A\right)\right)=A)))$$

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

Source. Repository-derived.

Commentary.

Reconstructing a Hermitian trace-one matrix from its chart coordinates recovers the matrix. The final diagonal coordinate follows from the trace equation.

Theorem 1.8 (hermitian_posdef_open).

$$\forall (n:\mathbb{N}),\mathrm{IsOpen}\left(\{A:\{A:\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right)//\mathrm{Matrix}.\mathrm{IsHermitian}\left(A\right)\}\mid \mathrm{Matrix}.\mathrm{PosDef}\left(\mathrm{val}\left(A\right)\right)\}\right)$$

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

Source. Repository-derived.

Commentary.

Positive definite matrices form an open set in the Hermitian subspace.

Theorem 1.9 (positive_chart_open).

$$\forall (n:\mathbb{N}),\mathrm{IsOpen}\left(\{x:(\mathrm{Fin}\left((n^2)-(1)\right))\to (\mathbb{R})\mid \mathrm{Matrix}.\mathrm{PosDef}\left(\mathrm{rho}\left(x\right)\right)\}\right)$$

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

Source. Repository-derived.

Commentary.

Positive definiteness is an open condition in the density coordinates.

Definition 1.10 (christoffel).

$$\forall \{m:\mathbb{N}\}(g:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(x:\mathrm{Fin}m\to \mathbb{R})(kij:\mathrm{Fin}m),\mathrm{christoffel}gxkij=(1/2:\mathbb{R})\ast \sum l,(gx{)}^{-1}kl\ast (\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto gtlj)x(\mathrm{Pi}.\mathrm{single}i1)+\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto gtli)x(\mathrm{Pi}.\mathrm{single}j1)-\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto gtij)x(\mathrm{Pi}.\mathrm{single}l1))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.christoffel (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of christoffel.

Definition 1.11 (ricci).

$$\forall \{m:\mathbb{N}\}(g:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(x:\mathrm{Fin}m\to \mathbb{R})(ij:\mathrm{Fin}m),\mathrm{ricci}gxij=\sum k,(\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto \mathrm{christoffel}gtkij)x(\mathrm{Pi}.\mathrm{single}k1)-\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto \mathrm{christoffel}gtkik)x(\mathrm{Pi}.\mathrm{single}j1)+\sum l,(\mathrm{christoffel}gxkkl\ast \mathrm{christoffel}gxlij-\mathrm{christoffel}gxkjl\ast \mathrm{christoffel}gxlik))$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.ricci (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of ricci.

Definition 1.12 (scalarCurvature).

$$\forall \{m:\mathbb{N}\}(g:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(x:\mathrm{Fin}m\to \mathbb{R}),\mathrm{scalarCurvature}gx=\sum i,\sum j,(gx{)}^{-1}ij\ast \mathrm{ricci}gxij$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.scalarCurvature (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of scalarCurvature.

Theorem 1.13 (coordinate_gauss_scalar_of_ricci).

$$\forall \{m:\mathbb{N}\}(g:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(x:\mathrm{Fin}m\to \mathbb{R})(b:\mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R}),((gx).\mathrm{IsSymm})\to ((\mathrm{Matrix}.\mathrm{of}(\mathrm{fun}ij\mapsto \mathrm{ricci}gxij))=((gx{)}^{-1}\ast b).\mathrm{trace}\cdot b-b\ast (gx{)}^{-1}\ast b)\to \mathrm{scalarCurvature}gx=((gx{)}^{-1}\ast b).{\mathrm{trace}}^2-(((gx{)}^{-1}\ast b{)}^2).\mathrm{trace}$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.14 (structureRHS).

$$\forall \{m:\mathbb{N}\}\{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{NormedSpace}\mathbb{R}E](e:\mathrm{Fin}m\to (\mathrm{Fin}m\to \mathbb{R})\to E)(N:(\mathrm{Fin}m\to \mathbb{R})\to E)(\Gamma :(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Fin}m\to \mathrm{Fin}m\to \mathrm{Fin}m\to \mathbb{R})(b:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Fin}m\to \mathrm{Fin}m\to \mathbb{R})(ij:\mathrm{Fin}m)(t:(\mathrm{Fin}m\to \mathbb{R})),\mathrm{structureRHS}eN\Gamma bijt=(\sum l,\Gamma tlij\cdot elt)+btij\cdot Nt$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.structureRHS (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of structureRHS.

Theorem 1.15 (ricci_of_structure).

$$\forall \{m:\mathbb{N}\}\{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{NormedSpace}\mathbb{R}E](g:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(e:\mathrm{Fin}m\to (\mathrm{Fin}m\to \mathbb{R})\to E)(N:(\mathrm{Fin}m\to \mathbb{R})\to E)(b:(\mathrm{Fin}m\to \mathbb{R})\to \mathrm{Fin}m\to \mathrm{Fin}m\to \mathbb{R})(x:(\mathrm{Fin}m\to \mathbb{R}))(a:\mathrm{Fin}m\to E{\to }_L[\mathbb{R}]\mathbb{R})(ij:\mathrm{Fin}m),(\forall l,\mathrm{DifferentiableAt}\mathbb{R}(el)x)\to (\mathrm{DifferentiableAt}\mathbb{R}Nx)\to (\forall lij,\mathrm{DifferentiableAt}\mathbb{R}(\mathrm{fun}t\mapsto \mathrm{christoffel}gtlij)x)\to (\forall ij,\mathrm{DifferentiableAt}\mathbb{R}(\mathrm{fun}t\mapsto btij)x)\to (\forall kl,ak(elx)=\mathrm{if}k=l\mathrm{then}1\mathrm{else}0)\to (\forall k,ak(Nx)=0)\to (\forall ij,(\mathrm{fun}t\mapsto \mathrm{fderiv}\mathbb{R}(ei)t(\mathrm{Pi}.\mathrm{single}j1)){=}^f[\mathrm{nhds}x]\mathrm{structureRHS}eN(\mathrm{christoffel}g)bij)\to (\forall ijk,\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto \mathrm{fderiv}\mathbb{R}(ei)t(\mathrm{Pi}.\mathrm{single}j1))x(\mathrm{Pi}.\mathrm{single}k1)=\mathrm{fderiv}\mathbb{R}(\mathrm{fun}t\mapsto \mathrm{fderiv}\mathbb{R}(ei)t(\mathrm{Pi}.\mathrm{single}k1))x(\mathrm{Pi}.\mathrm{single}j1))\to (\forall kij,\mathrm{christoffel}gxkij=\mathrm{christoffel}gxkji)\to (\forall kj,ak(\mathrm{fderiv}\mathbb{R}Nx(\mathrm{Pi}.\mathrm{single}j1))=-\sum l,(gx{)}^{-1}kl\ast bxjl)\to \mathrm{ricci}gxij=bxij\ast (\sum k,\sum l,(gx{)}^{-1}kl\ast bxkl)-\sum k,\sum l,bxik\ast (gx{)}^{-1}kl\ast bxjl$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.16 (inverse_entry_contDiffAt).

$$\forall \{m:\mathbb{N}\}\{E:\mathrm{Type}\}[\mathrm{NormedAddCommGroup}E][\mathrm{NormedSpace}\mathbb{R}E](g:E\to \mathrm{Matrix}(\mathrm{Fin}m)(\mathrm{Fin}m)\mathbb{R})(x:E)(ij:\mathrm{Fin}m),(\forall ij,\mathrm{ContDiffAt}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })(\mathrm{fun}t\mapsto gtij)x)\to ((gx).\det \ne 0)\to \mathrm{ContDiffAt}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })(\mathrm{fun}t\mapsto (gt{)}^{-1}ij)x$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.17 (herm_inner).

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

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.herm_inner (✓ 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 closed defining function of the real trace pairing on Hermitian matrices. The declaration name is herm_inner; the formula displays its defining expression.

Definition 1.18 (cubeDerivative).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{cubeDerivative}Y=((\mathrm{selfAdjointPartL}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{toLinearMap}.\mathrm{comp}((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))(Y.{\mathrm{val}}^2)+((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))Y.\mathrm{val}).\mathrm{comp}((\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{flip}Y.\mathrm{val})+(\mathrm{LinearMap}.\mathrm{mul}\mathbb{R}(A:=\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{flip}(Y.{\mathrm{val}}^2))).\mathrm{comp}(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})).\mathrm{subtype}$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cubeDerivative (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of cubeDerivative.

Theorem 1.19 (positive_hermitian_cube_derivative_equiv).

$$\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{Function}.\mathrm{Bijective}(\mathrm{cubeDerivative}Y)$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.20 (cubeDerivativeEquiv).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))(\mathrm{hY}:Y.\mathrm{val}.\mathrm{PosDef})(\mathrm{hB}:\mathrm{Function}.\mathrm{Bijective}(\mathrm{cubeDerivative}Y)),\mathrm{cubeDerivativeEquiv}Y\mathrm{hY}=(\mathrm{LinearEquiv}.\mathrm{ofInjectiveEndo}(\mathrm{cubeDerivative}Y)\mathrm{hB}.1).\mathrm{toContinuousLinearEquiv}$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cubeDerivativeEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The full equivalence construction from the cubic derivative. The injectivity proof is displayed as a bound proof argument; proof irrelevance identifies it with the established positive-derivative proof.

Definition 1.21 (cube).

$$\forall \{n:\mathbb{N}\}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})),\mathrm{cube}Y=\mathrm{selfAdjointPartL}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C})(Y.{\mathrm{val}}^3)$$

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cube (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of cube.

Theorem 1.22 (cube_val).

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

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.23 (cube_contDiff).

$$\forall (n:\mathbb{N}),\mathrm{ContDiff}\mathbb{R}(\mathrm{top}:{\mathbb{N}}_{\infty })((\mathrm{fun}(Y:\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))\mapsto \mathrm{cube}Y))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.24 (cube_hasFDerivAt).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),\mathrm{HasFDerivAt}\mathrm{cube}(\mathrm{cubeDerivative}Y).\mathrm{toContinuousLinearMap}Y$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Definition 1.25 (F).

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

Formalization. D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.F (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of F.

Definition 1.26 (DF).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),\mathrm{DF}Y=(3:\mathbb{R})\cdot (((\mathrm{Complex}.\mathrm{reCLM}.\mathrm{comp}(\mathrm{Matrix}.\mathrm{traceLinearMap}(\mathrm{Fin}n)\mathbb{RC}:(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}){\to }_l[\mathbb{R}]\mathbb{C}).\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}}^2)).\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/HermitianHypersurfaceCalculus.DF (✓ std3).

Source. Repository-derived.

Commentary.

The defining expression of DF.

Theorem 1.27 (F_hasFDerivAt).

$$\forall \{n:\mathbb{N}\}(Y:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),\mathrm{HasFDerivAt}F(\mathrm{DF}Y)Y$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

Theorem 1.28 (F_fderiv).

$$\forall \{n:\mathbb{N}\}(YV:(\mathrm{selfAdjoint}.\mathrm{submodule}\mathbb{R}(\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))),\mathrm{fderiv}\mathbb{R}FYV=3\ast \mathrm{RCLike}.\mathrm{re}(\mathrm{Matrix}.\mathrm{trace}(((Y.{\mathrm{val}}^2))\ast (V.\mathrm{val})))$$

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

Source. Repository-derived.

Commentary.

The stated identity or implication holds for every displayed parameter.

References

• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.DF
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.F
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.F_fderiv
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.F_hasFDerivAt
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.G
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.chartPoint
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.chart_left_inverse
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.christoffel
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.coordinate_gauss_scalar_of_ricci
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cube
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cubeDerivative
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cubeDerivativeEquiv
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cube_contDiff
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cube_hasFDerivAt
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.cube_val
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.herm_inner
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.hermitian_posdef_open
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.hermitian_trace_one_chart_equiv
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.inverse_entry_contDiffAt
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.positive_chart_open
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.positive_hermitian_cube_derivative_equiv
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.rho
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.rho_isHermitian
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.rho_trace
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.ricci
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.ricci_of_structure
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.scalarCurvature
• Truth anchor: D5/S3/Geometry/AlphaGeometry/HermitianHypersurfaceCalculus.structureRHS