Clifford Bond Parents

Abstract

Average the positive Fourier vacuum over Clifford monomials, label each outcome by its bond conjugation signs, and push it to Boolean assignments.

Formulas retain Lean application and binder notation. Omega denotes the outcome-index type Ω, whereas ω denotes an outcome. Square brackets denote anonymous typeclass assumptions. Scalar coercions display their target types; angle brackets suppress the proof field of a Fin value. The identity is written as 1. Products of matrices and scalar actions use a centered dot; the operand types distinguish them. Infix Matrix.kronecker denotes the Lean kronecker notation.

Definition 1.1 (cycleCoeff).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \forall (v:\mathrm{Fin}(2\cdot L)),\\ (\mathrm{cycleCoeff}(L:=L)(v:=v):\mathbb{C})=(\mathrm{if}v.\mathrm{val}+1<2\cdot L\mathrm{then}\mathrm{Complex}.I\mathrm{else}-\mathrm{Complex}.I)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycleCoeff (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines cycleCoeff.

Definition 1.2 (cycleMajoranaBond).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (v:\mathrm{Fin}(2\cdot L)),\\ (\mathrm{cycleMajoranaBond}(\iota :=\iota )(L:=L)(g:=g)(v:=v):\mathrm{Matrix}\iota \iota \mathbb{C})=(\mathrm{cycleCoeff}Lv\cdot (gv\cdot g(\mathrm{finRotate}(2\cdot L)v)))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycleMajoranaBond (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines cycleMajoranaBond.

Lemma 1.3 (cycle majorana parent).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (n:\mathbb{N}),\\ (1\le n)\to \\ \forall (g:\mathrm{Fin}(2\cdot (n+1))\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ (\forall j,gj\cdot gj=1)\to \\ (\forall j,\mathrm{star}(gj)=gj)\to \\ (\forall jk,j\ne k\to gj\cdot gk=-(gk\cdot gj))\to \\ \exists E:(\mathrm{Fin}(2\cdot (n+1))\to \mathrm{Bool})\to \mathrm{Matrix}\iota \iota \mathbb{C},(\forall a,(Ea).\mathrm{PosSemidef})\wedge (\sum a,Ea=1)\wedge (\forall v,\sum a,\mathrm{outcomeSign}(av)\cdot Ea=(\mathrm{visibility}n:\mathbb{C})\cdot \mathrm{cycleMajoranaBond}gv)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycle_majorana_parent (✓ std3). ∎

Source. Repository-derived.

Commentary.

Average the positive Fourier vacuum over Clifford monomials, label each outcome by its bond conjugation signs, and push it to Boolean assignments. The average normalizes the parent and the Fourier covariance fixes every antiperiodic bond marginal at the threshold.

Lemma 1.4 (consecutive majorana parent).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (n:\mathbb{N}),\\ \forall (q:\mathbb{N}),\\ (1\le n)\to \\ \forall (g:\mathrm{Fin}(2\cdot (n+1))\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ (\forall j,gj\cdot gj=1)\to \\ (\forall j,\mathrm{star}(gj)=gj)\to \\ (\forall jk,j\ne k\to gj\cdot gk=-(gk\cdot gj))\to \\ \forall (j:\mathrm{Fin}q\to \mathrm{Fin}(2\cdot (n+1))),\\ \forall (k:\mathrm{Fin}q\to \mathrm{Fin}(2\cdot (n+1))),\\ (\forall v,(kv).\mathrm{val}=(jv).\mathrm{val}+1)\to \\ \exists E:(\mathrm{Fin}q\to \mathrm{Bool})\to \mathrm{Matrix}\iota \iota \mathbb{C},(\forall a,(Ea).\mathrm{PosSemidef})\wedge (\sum a,Ea=1)\wedge (\forall v,\sum a,\mathrm{outcomeSign}(av)\cdot Ea=(\mathrm{visibility}n:\mathbb{C})\cdot (\mathrm{Complex}.I\cdot (g(jv)\cdot g(kv))))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.consecutive_majorana_parent (✓ std3). ∎

Source. Repository-derived.

Commentary.

This consecutive majorana parent identity is used in the CliffordBondParents construction.

References

• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.consecutive_majorana_parent
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycleCoeff
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycleMajoranaBond
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordBondParents.cycle_majorana_parent
• Dependency: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum