Identifying the edge average

Abstract

The literal unordered edge average equals the flat coordinate Clifford operator.

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 (The factor of two in the dense Clifford sum).

$$\forall n\in Nat,\forall m\in Nat,\forall q\in Nat,\forall r\in Nat,\forall e\in \mathrm{Equiv}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(q\right)\to \mathrm{Index}\left(r\right)\right),\forall a\in \mathrm{Equiv}\left(\mathrm{Fin}\left(q\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right)\right),\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{averagedHamiltonian}\left(\mathrm{SimpleGraph}.\mathrm{comap}\left(\mathrm{coordinateGraph}\left(q,\mathrm{Index}\left(r\right)\right),e\right),\mathrm{coordinateCoupling}\left(r,e,a\right)\right)\right)=\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Finset}.\mathrm{card}\left(\mathrm{SimpleGraph}.\mathrm{edgeFinset}\left(\mathrm{SimpleGraph}.\mathrm{comap}\left(\mathrm{coordinateGraph}\left(q,\mathrm{Index}\left(r\right)\right),e\right)\right)\right):Real)\right),\mathrm{SMul}.\mathrm{smul}\left(\frac{\mathrm{Complex}.I}{2},\sum _{p:\mathrm{Prod}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(q\right)\right)}(\sum _{t:\mathrm{Prod}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(q\right)\right)}(\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(\mathrm{coordinateSkew}\left(q,r\right),\mathrm{Prod}.\mathrm{mk}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(p\right)\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right),\mathrm{Prod}.\mathrm{mk}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(t\right)\right),\mathrm{Prod}.\mathrm{snd}\left(t\right)\right)\right):Complex),\mathrm{majorana}\left(n\cdot m,\mathrm{finProdFinEquiv}\left(\mathrm{Prod}.\mathrm{mk}\left(\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{fst}\left(\mathrm{val}\left(a,\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(\mathrm{val}\left(a,\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\right)\right)\cdot \mathrm{majorana}\left(n\cdot m,\mathrm{finProdFinEquiv}\left(\mathrm{Prod}.\mathrm{mk}\left(\mathrm{Prod}.\mathrm{fst}\left(t\right),\mathrm{Prod}.\mathrm{fst}\left(\mathrm{val}\left(a,\mathrm{Prod}.\mathrm{snd}\left(t\right)\right)\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(\mathrm{val}\left(a,\mathrm{Prod}.\mathrm{snd}\left(t\right)\right)\right)\right)\right)))\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every unordered coordinate edge has two orientations. Skewness of its real coefficient cancels the sign from reversing its two Majoranas, so the dense double sum counts its interaction twice. The identity keeps the literal reciprocal edge count.

References

• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateAverage.coordinate_average
• Dependency: D5/S3/Quantum/Fermionic/CoordinateCliffordSpectrum
• Dependency: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian