Central Cycle Realizations

Abstract

The normalized product around the cycle is a central Hermitian involution K.

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 (pathWord).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ \forall (A:\mathbb{N}\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{pathWord}(R:=R)(A:=A)(k:=k):R)=(((\mathrm{List}.\mathrm{range}k).\mathrm{map}A).\mathrm{prod})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.pathWord (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pathWord.

Definition 1.2 (loopSign).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ (\mathrm{loopSign}(n:=n):\mathbb{C})=(((-1){)}^n)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.loopSign (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines loopSign.

Definition 1.3 (normalizedLoop).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (n:\mathbb{N}),\\ \forall (A:\mathbb{N}\to R),\\ \forall (B:R),\\ (\mathrm{normalizedLoop}(R:=R)(n:=n)(A:=A)(B:=B):R)=(\mathrm{loopSign}n\cdot (\mathrm{pathWord}A(2\cdot n+1)\cdot B))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.normalizedLoop (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines normalizedLoop.

Lemma 1.4 (central relabel parent).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (B:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (t:\mathbb{R}),\\ \forall (v_0:\mathrm{Fin}m),\\ \forall (K:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (K.\mathrm{IsHermitian})\to \\ (K\cdot K=1)\to \\ (\forall v,K\cdot Av=Av\cdot K)\to \\ (\forall v,Bv=\mathrm{if}v=v_0\mathrm{then}K\cdot Av\mathrm{else}Av)\to \\ (\forall v,(Av).\mathrm{trace}=0)\to \\ (\forall v,(Bv).\mathrm{trace}=0)\to \\ (\mathrm{JM}Bt)\to \\ \mathrm{JM}At\end{array}$$

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

Source. Repository-derived.

Commentary.

This central relabel parent identity is used in the CentralCycleRealizations construction.

Lemma 1.5 (natural cycle adj).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ (2\le M)\to \\ \forall (u:\mathrm{Fin}M),\\ \forall (v:\mathrm{Fin}M),\\ (\mathrm{SimpleGraph}.\mathrm{cycleGraph}M).\mathrm{Adj}uv⟺u.\mathrm{val}+1=v.\mathrm{val}\vee v.\mathrm{val}+1=u.\mathrm{val}\vee (u.\mathrm{val}=0\wedge v.\mathrm{val}+1=M)\vee (v.\mathrm{val}=0\wedge u.\mathrm{val}+1=M)\end{array}$$

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

Source. Repository-derived.

Commentary.

This natural cycle adj identity is used in the CentralCycleRealizations construction.

Definition 1.6 (cyclePrefix).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (M:\mathbb{N}),\\ \forall (A:\mathrm{Fin}M\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (k:\mathbb{N}),\\ (\mathrm{cyclePrefix}(d:=d)(M:=M)(A:=A)(k:=k):\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})=(\mathrm{if}k+1<M\mathrm{then}A⟨k,\cdot ⟩\mathrm{else}1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.cyclePrefix (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines cyclePrefix.

Lemma 1.7 (realization cycle loop).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (1\le n)\to \\ \forall (A:\mathrm{Fin}(2\cdot n+2)\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{cycleGraph}(2\cdot n+2))A)\to \\ \mathrm{let}K:=\mathrm{normalizedLoop}n(\mathrm{cyclePrefix}A)(A⟨2\cdot n+1,\cdot ⟩);K.\mathrm{IsHermitian}\wedge K\cdot K=1\wedge (\forall j,K\cdot Aj=Aj\cdot K)\wedge K\cdot A⟨2\cdot n+1,\cdot ⟩=\mathrm{loopSign}n\cdot \mathrm{pathWord}(\mathrm{cyclePrefix}A)(2\cdot n+1)\end{array}$$

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

Source. Repository-derived.

Commentary.

This realization cycle loop identity is used in the CentralCycleRealizations construction.

Lemma 1.8 (cycle majorana extension).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (1\le n)\to \\ \forall (A:\mathrm{Fin}(2\cdot n+2)\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{cycleGraph}(2\cdot n+2))A)\to \\ \mathrm{let}P:=\mathrm{cyclePrefix}A;\mathrm{let}K:=\mathrm{normalizedLoop}nP(A⟨2\cdot n+1,\cdot ⟩);\mathrm{let}g:=\mathrm{pathMajorana}(\mathrm{liftPath}P)(\mathrm{liftSeed}d);(\forall k,k\le 2\cdot n+1\to gk\cdot gk=1)\wedge (\forall k,k\le 2\cdot n+1\to \mathrm{star}(gk)=gk)\wedge (\forall j,j\le 2\cdot n+1\to \forall i,i<j\to gi\cdot gj=-(gj\cdot gi))\wedge (\forall k,k<2\cdot n+1\to \mathrm{Complex}.I\cdot (gk\cdot g(k+1))=\mathrm{liftPath}Pk)\wedge (-\mathrm{Complex}.I)\cdot (g(2\cdot n+1)\cdot g0)=(K\cdot A⟨2\cdot n+1,\cdot ⟩)(\mathrm{Matrix}.\mathrm{kronecker})\mathrm{qubitZ}\end{array}$$

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

Source. Repository-derived.

Commentary.

The normalized product around the cycle is a central Hermitian involution K. It corrects the closing observable before the path extension. The last equation retains K explicitly and verifies the antiperiodic closing bond; no irreducibility or fixed central-sector assumption is imposed.

References

• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.central_relabel_parent
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.cyclePrefix
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.cycle_majorana_extension
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.loopSign
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.natural_cycle_adj
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.normalizedLoop
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.pathWord
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CentralCycleRealizations.realization_cycle_loop
• Dependency: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations