The physical Clifford ground sector

Abstract

Paired Clifford bilinears have a physical trace-one ground projector.

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 (Trace-one ground projector and universal lower bound).

$$\forall kappa\in Type,\forall Omega\in Type,[\mathrm{Fintype}\left(kappa\right)][\mathrm{DecidableEq}\left(kappa\right)][\mathrm{Fintype}\left(Omega\right)][\mathrm{DecidableEq}\left(Omega\right)][\mathrm{Nonempty}\left(Omega\right)]\forall eta\in \mathrm{Sum}\left(kappa,kappa\right)\to \mathrm{Matrix}\left(Omega,Omega,Complex\right),\forall T\in \mathrm{Matrix}\left(Omega,Omega,Complex\right),((((\mathrm{Fintype}.\mathrm{card}\left(Omega\right)=2^{\mathrm{Fintype}.\mathrm{card}\left(kappa\right)})\wedge (\forall p\in \mathrm{Sum}\left(kappa,kappa\right),\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{val}\left(eta,p\right)\right)))\wedge (\forall p\in \mathrm{Sum}\left(kappa,kappa\right),\forall t\in \mathrm{Sum}\left(kappa,kappa\right),\mathrm{val}\left(eta,p\right)\cdot \mathrm{val}\left(eta,t\right)+\mathrm{val}\left(eta,t\right)\cdot \mathrm{val}\left(eta,p\right)=\mathrm{ite}\left(p=t,\mathrm{SMul}.\mathrm{smul}\left((2:Complex),(1:\mathrm{Matrix}\left(Omega,Omega,Complex\right))\right),0\right)))\wedge (\forall p\in \mathrm{Sum}\left(kappa,kappa\right),T\cdot \mathrm{val}\left(eta,p\right)=-\left(\mathrm{val}\left(eta,p\right)\cdot T\right)))\Rightarrow (\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 (\sum _{k:kappa}(\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Complex}.I,\mathrm{val}\left(eta,\mathrm{Sum}.\mathrm{inl}\left(k\right)\right)\cdot \mathrm{val}\left(eta,\mathrm{Sum}.\mathrm{inr}\left(k\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(-(\mathrm{Fintype}.\mathrm{card}\left(kappa\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),-(\mathrm{Fintype}.\mathrm{card}\left(kappa\right):Real)\le \mathrm{meanEnergy}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(\sum _{k:kappa}(\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Complex}.I,\mathrm{val}\left(eta,\mathrm{Sum}.\mathrm{inl}\left(k\right)\right)\cdot \mathrm{val}\left(eta,\mathrm{Sum}.\mathrm{inr}\left(k\right)\right)\right))\right),omega\right)))$$

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

Source. Repository-derived.

Commentary.

Each bilinear is a Hermitian involution. A single Majorana reverses its own bilinear and preserves the others, giving a joint minus projection of trace one. Complementary plus projections bound the energy of every density.

References

• Truth anchor: D5/S3/Quantum/Fermionic/CliffordGroundDensity.paired_clifford_ground
• Dependency: D5/S3/Quantum/Fermionic/JointSignProjectors
• Dependency: D5/S3/Quantum/Information/CorrelatedGibbsEnergyIdentity