Real quadratic edge interactions

Abstract

Real conference coefficients realize normalized quadratic coordinate interactions.

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.

Definition 1.1 (Real quadratic inter-site term).

$$\forall n\in Nat,\forall m\in Nat,\forall v\in \mathrm{Fin}\left(n\right),\forall w\in \mathrm{Fin}\left(n\right),\forall K\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),Real\right),\mathrm{quadraticEdge}\left(v,w,K\right)=\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Complex}.I,\sum _{p:\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right)}(\sum _{t:\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right)}(\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(K,p,t\right):Complex),\mathrm{majorana}\left(n\cdot m,\mathrm{finProdFinEquiv}\left(\mathrm{Prod}.\mathrm{mk}\left(v,\mathrm{Prod}.\mathrm{fst}\left(p\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\cdot \mathrm{majorana}\left(n\cdot m,\mathrm{finProdFinEquiv}\left(\mathrm{Prod}.\mathrm{mk}\left(w,\mathrm{Prod}.\mathrm{fst}\left(t\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(t\right)\right)\right)))\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.quadraticEdge (✓ std3).

Source. Repository-derived.

Commentary.

The real coefficient matrix multiplies the actual Jordan-Wigner Majorana matrices, with the factor i exactly as displayed.

Definition 1.2 (Literal edge average).

$$\forall n\in Nat,\forall m\in Nat,\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),\forall K\in \mathrm{SimpleGraph}.\mathrm{edgeSet}\left(G\right)\to \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),Real\right),\mathrm{averagedHamiltonian}\left(G,K\right)=\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Finset}.\mathrm{card}\left(\mathrm{SimpleGraph}.\mathrm{edgeFinset}\left(G\right)\right):Real)\right),\sum _{z:\mathrm{SimpleGraph}.\mathrm{edgeSet}\left(G\right)}(\mathrm{quadraticEdge}\left(\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{val}\left(K,z\right)\right))\right)$$

Formalization. D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.averagedHamiltonian (✓ std3).

Source. Repository-derived.

Commentary.

The sum runs over all actual unordered edges and is multiplied by the reciprocal of their cardinality.

Definition 1.3 (Interaction admissibility).

$$\forall n\in Nat,\forall m\in Nat,\forall G\in \mathrm{SimpleGraph}\left(\mathrm{Fin}\left(n\right)\right),\forall K\in \mathrm{SimpleGraph}.\mathrm{edgeSet}\left(G\right)\to \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),Real\right),(\mathrm{admissibleEdges}\left(G,K\right))\iff (\forall z\in \mathrm{SimpleGraph}.\mathrm{edgeSet}\left(G\right),((\mathrm{IsSelfAdjoint}\left(\mathrm{quadraticEdge}\left(\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{val}\left(K,z\right)\right)\right))\wedge (\Vert \mathrm{quadraticEdge}\left(\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{val}\left(K,z\right)\right)\Vert \le 1))\wedge (\mathrm{Commute}\left(\mathrm{quadraticEdge}\left(\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right),\mathrm{val}\left(K,z\right)\right),\mathrm{CStarMatrix}.\mathrm{ofMatrix}\left(\mathrm{numberParity}\left(n\cdot m\right)\right)\right)))$$

Formalization. D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.admissibleEdges (✓ std3).

Source. Repository-derived.

Commentary.

Admissibility means Hermitian, operator norm at most one, and commutation with total occupation parity on each edge.

Definition 1.4 (Conference edge coefficients).

$$\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),\forall z\in \mathrm{SimpleGraph}.\mathrm{edgeSet}\left(\mathrm{SimpleGraph}.\mathrm{comap}\left(\mathrm{coordinateGraph}\left(q,\mathrm{Index}\left(r\right)\right),e\right)\right),\forall p\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),\forall u\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),Bool\right),\mathrm{val}\left(\mathrm{coordinateCoupling}\left(r,e,a,z\right),p,u\right)=\mathrm{ite}\left((p=u)\wedge (\forall b\in \mathrm{Fin}\left(q\right),(b\ne \mathrm{Equiv}.\mathrm{symm}\left(a\right)\left(p\right))\Rightarrow (\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),b\right)=\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),b\right))),(\mathrm{val}\left(\mathrm{conference}\left(r\right),\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),\mathrm{Equiv}.\mathrm{symm}\left(a\right)\left(p\right)\right),\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),\mathrm{Equiv}.\mathrm{symm}\left(a\right)\left(p\right)\right)\right):Real),0\right)$$

Formalization. D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.coordinateCoupling (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient is diagonal in the local Majorana index and uses the single coordinate in which the edge endpoints differ.

Theorem 1.5 (Admissible interactions on the coordinate graph).

$$\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{admissibleEdges}\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))\wedge (\forall z\in \mathrm{SimpleGraph}.\mathrm{edgeSet}\left(\mathrm{SimpleGraph}.\mathrm{comap}\left(\mathrm{coordinateGraph}\left(q,\mathrm{Index}\left(r\right)\right),e\right)\right),\exists t\in \mathrm{Fin}\left(q\right),(\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),t\right)\ne \mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),t\right))\wedge (\mathrm{coordinateCoupling}\left(r,e,a,z\right)=\mathrm{Matrix}.\mathrm{single}\left(\mathrm{val}\left(a,t\right),\mathrm{val}\left(a,t\right),(\mathrm{val}\left(\mathrm{conference}\left(r\right),\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{fst}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),t\right),\mathrm{val}\left(\mathrm{val}\left(e,\mathrm{Prod}.\mathrm{snd}\left(Sym2.\mathrm{out}\left(\mathrm{Subtype}.\mathrm{val}\left(z\right)\right)\right)\right),t\right)\right):Real)\right)))$$

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

Source. Repository-derived.

Commentary.

Every actual coordinate edge has one signed coefficient, giving a Hermitian involution with operator norm one and even total parity.

References

• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.admissibleEdges
• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.averagedHamiltonian
• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.coordinateCoupling
• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.coordinate_edges_admissible
• Truth anchor: D5/S3/Quantum/Fermionic/CoordinateEdgeHamiltonian.quadraticEdge
• Dependency: D5/S3/Quantum/Fermionic/CompleteCartesianGraph
• Dependency: D5/S3/Quantum/Fermionic/ConferenceMatrices
• Dependency: D5/S3/Quantum/Fermionic/FockMajoranaCarrier