The flat Clifford spectral bound

Abstract

A flat real skew coupling has an exact physical Clifford ground density.

Natural subtraction is truncated at zero. All other divisions are in Real or Complex. Scalar casts retain their target type. Matrix products are operator products, and Matrix.conjTranspose is conjugate transpose. Subtype.val is the value of a density; Equiv.symm applied to CStarMatrix.ofMatrix recovers its ordinary matrix. Assignment N is the occupation basis Fin N → Bool. Implicit Lean mode and dimension arguments may be displayed explicitly. Bracketed Fintype, DecidableEq and Nonempty assumptions are anonymous instance arguments.

Theorem 1.1 (Exact ground density for a flat skew coupling).

$$\forall alpha\in Type,\forall Omega\in Type,[\mathrm{Fintype}\left(alpha\right)][\mathrm{DecidableEq}\left(alpha\right)][\mathrm{Fintype}\left(Omega\right)][\mathrm{DecidableEq}\left(Omega\right)][\mathrm{Nonempty}\left(Omega\right)]\forall L\in Nat,\forall A\in \mathrm{Matrix}\left(alpha,alpha,Real\right),\forall d\in Real,\forall gamma\in alpha\to \mathrm{Matrix}\left(Omega,Omega,Complex\right),\forall T\in \mathrm{Matrix}\left(Omega,Omega,Complex\right),((((((((\mathrm{Fintype}.\mathrm{card}\left(alpha\right)=2\cdot L)\wedge (\mathrm{Fintype}.\mathrm{card}\left(Omega\right)=2^L))\wedge (\mathrm{Matrix}.\mathrm{transpose}\left(A\right)=-A))\wedge (0\le d))\wedge (A\cdot A=\mathrm{SMul}.\mathrm{smul}\left(-d,(1:\mathrm{Matrix}\left(alpha,alpha,Real\right))\right)))\wedge (\forall p\in alpha,\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{val}\left(gamma,p\right)\right)))\wedge (\forall p\in alpha,\forall u\in alpha,\mathrm{val}\left(gamma,p\right)\cdot \mathrm{val}\left(gamma,u\right)+\mathrm{val}\left(gamma,u\right)\cdot \mathrm{val}\left(gamma,p\right)=\mathrm{ite}\left(p=u,\mathrm{SMul}.\mathrm{smul}\left((2:Complex),(1:\mathrm{Matrix}\left(Omega,Omega,Complex\right))\right),0\right)))\wedge (\forall p\in alpha,T\cdot \mathrm{val}\left(gamma,p\right)=-\left(\mathrm{val}\left(gamma,p\right)\cdot T\right)))\Rightarrow ((\mathrm{IsSelfAdjoint}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(\mathrm{SMul}.\mathrm{smul}\left(\frac{\mathrm{Complex}.I}{2},\sum _{p:alpha}(\sum _{t:alpha}(\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(A,p,t\right):Complex),\mathrm{val}\left(gamma,p\right)\cdot \mathrm{val}\left(gamma,t\right)\right)))\right)\right)\right))\wedge (\exists rho\in \mathrm{DensityState}\left(Omega\right),(((\mathrm{IsStarProjection}\left(\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right)\right)\right))\wedge (\mathrm{Commute}\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right),\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(T\right)\right)))\wedge (\mathrm{SMul}.\mathrm{smul}\left(\frac{\mathrm{Complex}.I}{2},\sum _{p:alpha}(\sum _{t:alpha}(\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(A,p,t\right):Complex),\mathrm{val}\left(gamma,p\right)\cdot \mathrm{val}\left(gamma,t\right)\right)))\right)\cdot \mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right)\right)=\mathrm{SMul}.\mathrm{smul}\left(-(L:Complex)\cdot (\mathrm{Real}.\mathrm{sqrt}\left(d\right):Complex),\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right)\right)\right)))\wedge (\forall omega\in \mathrm{DensityState}\left(Omega\right),-(L:Real)\cdot \mathrm{Real}.\mathrm{sqrt}\left(d\right)\le \mathrm{meanEnergy}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(\mathrm{SMul}.\mathrm{smul}\left(\frac{\mathrm{Complex}.I}{2},\sum _{p:alpha}(\sum _{t:alpha}(\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(A,p,t\right):Complex),\mathrm{val}\left(gamma,p\right)\cdot \mathrm{val}\left(gamma,t\right)\right)))\right)\right),omega\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/FlatCliffordGround.flat_clifford_ground (✓ std3). ∎

Source. Repository-derived.

Commentary.

A real orthogonal paired basis has frequency squareRoot(d) in every plane. Orthogonal combinations preserve the Clifford relations and the parity anticommutation. Their joint minus density attains the lower bound for the original double-sum operator.

References

• Truth anchor: D5/S3/Quantum/Fermionic/FlatCliffordGround.flat_clifford_ground
• Dependency: D5/S3/QuadraticForms/PositiveDefiniteWilliamson
• Dependency: D5/S3/Quantum/Fermionic/CliffordGroundDensity