Clifford Path Realizations

Abstract

One qubit ancilla gives a seed that anticommutes with the first path generator and commutes with all subsequent generators.

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

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ \forall (G:\mathrm{SimpleGraph}(\mathrm{Fin}m)),\\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \mathrm{Realization}(m:=m)(d:=d)(G:=G)(A:=A)⟺(1\le d\wedge (\forall (v:\mathrm{Fin}m),(Av).\mathrm{IsHermitian})\wedge (\forall (v:\mathrm{Fin}m),Av\cdot Av=1)\wedge (\forall (uv:\mathrm{Fin}m),u\ne v\to G.\mathrm{Adj}uv\to Au\cdot Av=-(Av\cdot Au))\wedge (\forall (uv:\mathrm{Fin}m),u\ne v\to \neg G.\mathrm{Adj}uv\to Au\cdot Av=Av\cdot Au))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.Realization (✓ std3).

Citation. Daniel McNulty (2025). A Graph-Theoretic Approach to Quantum Measurement Incompatibility. URL: https://arxiv.org/abs/2511.15954.

Commentary.

McNulty, Definition 1, p. 3: “The anti-commutativity graph G = (V,E) of a set of observables 𝒜 is defined by {v,v′} ∈ E ⇔ A_v A_v′ = −A_v′ A_v, so that adjacent vertices correspond to anti-commuting observables, and non-adjacent vertices correspond to commuting ones.” The carrier is Matrix (Fin d) (Fin d) ℂ with 1 ≤ d. Every observable is Hermitian and squares to the identity. Vertices are zero-indexed; the graph is Mathlib’s pathGraph or cycleGraph.

Definition 1.2 (noisyObservable).

$$\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 (eta:\mathbb{R}),\\ \forall (v:\mathrm{Fin}m),\\ (\mathrm{noisyObservable}(m:=m)(d:=d)(A:=A)(eta:=eta)(v:=v):\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})=((eta:\mathbb{C})\cdot Av+((Av).\mathrm{trace}/(d:\mathbb{C})\cdot (1-(eta:\mathbb{C})))\cdot 1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.noisyObservable (✓ std3).

Citation. Daniel McNulty (2025). A Graph-Theoretic Approach to Quantum Measurement Incompatibility. URL: https://arxiv.org/abs/2511.15954.

Commentary.

McNulty, Eq. (9), p. 3: “A_v^η = η A_v + (tr[A_v]/d)(1−η) 𝟙”. The matrix expression retains the trace term. The definition uses TomiyamaDiagonalKPositivity.phi d (1−η) 0 at A v; expanding its scalar coefficients gives this expression.

Definition 1.3 (effect).

$$\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 (eta:\mathbb{R}),\\ \forall (v:\mathrm{Fin}m),\\ \forall (s:\mathrm{Bool}),\\ (\mathrm{effect}(m:=m)(d:=d)(A:=A)(eta:=eta)(v:=v)(s:=s):\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})=((1/2:\mathbb{C})\cdot (1+(\mathrm{if}s\mathrm{then}(1:\mathbb{C})\mathrm{else}-1)\cdot \mathrm{noisyObservable}Aetav))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.effect (✓ std3).

Citation. Daniel McNulty (2025). A Graph-Theoretic Approach to Quantum Measurement Incompatibility. URL: https://arxiv.org/abs/2511.15954.

Commentary.

McNulty, Eq. (3), p. 2: “M_v(±) = ½(𝟙 ± A_v).” The noisy binary effect replaces A_v by noisyObservable A η v. Bool true denotes +1 and false denotes −1.

Definition 1.4 (JM).

$$\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 (eta:\mathbb{R}),\\ \mathrm{JM}(m:=m)(d:=d)(A:=A)(eta:=eta)⟺(\exists (E:(\mathrm{Fin}m\to \mathrm{Bool})\to \mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),(\forall (a:\mathrm{Fin}m\to \mathrm{Bool}),(Ea).\mathrm{PosSemidef})\wedge (\sum a:\mathrm{Fin}m\to \mathrm{Bool},Ea=1)\wedge (\forall (v:\mathrm{Fin}m)(s:\mathrm{Bool}),(\sum a\in \mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}(a:\mathrm{Fin}m\to \mathrm{Bool})\mapsto av=s),Ea)=\mathrm{effect}Aetavs))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.JM (✓ std3).

Citation. Daniel McNulty (2025). A Graph-Theoretic Approach to Quantum Measurement Incompatibility. URL: https://arxiv.org/abs/2511.15954.

Commentary.

McNulty, Section II.C, p. 3: “A collection of measurements are jointly measurable if there exists a parent POVM such that each measurement can be recovered as one of its marginals, or equivalently, if their statistics can be obtained from the parent after classical post-processing [47, 48].” E is indexed by every Boolean assignment. Each E a is positive semidefinite, the total is the identity, and both sign marginals equal the noisy effects exactly.

Definition 1.5 (visibility).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ (\mathrm{visibility}(n:=n):\mathbb{R})=((2/(2\cdot (n:\mathbb{R})+2))\cdot ((\mathrm{Real}.\sin (\mathrm{Real}.\mathrm{pi}/(2\cdot (n:\mathbb{R})+2))){)}^{-1})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.visibility (✓ std3).

Citation. Daniel McNulty (2025). A Graph-Theoretic Approach to Quantum Measurement Incompatibility. URL: https://arxiv.org/abs/2511.15954.

Commentary.

The candidate threshold is (2/(2n+2)) csc(π/(2n+2)); every division in this formula is real division. It is shared by the two consecutive path sizes and the next even cycle.

Lemma 1.6 (signed product).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (a:R),\\ \forall (b:R),\\ \forall (x:R),\\ \forall (s:\mathbb{C}),\\ \forall (t:\mathbb{C}),\\ (a\cdot x=s\cdot (x\cdot a))\to \\ (b\cdot x=t\cdot (x\cdot b))\to \\ (a\cdot b)\cdot x=(s\cdot t)\cdot (x\cdot (a\cdot b))\end{array}$$

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

Source. Repository-derived.

Commentary.

This signed product identity is used in the CliffordPathRealizations construction.

Definition 1.7 (generatorSign).

$$\begin{array}{r}\forall (k:\mathbb{N}),\\ \forall (j:\mathbb{N}),\\ (\mathrm{generatorSign}(k:=k)(j:=j):\mathbb{C})=(\mathrm{if}k+1=j\vee j+1=k\mathrm{then}-1\mathrm{else}1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.generatorSign (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines generatorSign.

Definition 1.8 (prefixSign).

$$\begin{array}{r}\forall (k:\mathbb{N}),\\ \forall (j:\mathbb{N}),\\ (\mathrm{prefixSign}(k:=k)(j:=j):\mathbb{C})=(\mathrm{if}j+1=k\vee j=k\mathrm{then}-1\mathrm{else}1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.prefixSign (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines prefixSign.

Lemma 1.9 (prefixSign zero).

$$\begin{array}{r}\forall (j:\mathbb{N}),\\ \mathrm{prefixSign}0j=\mathrm{if}j=0\mathrm{then}-1\mathrm{else}1\end{array}$$

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

Source. Repository-derived.

Commentary.

This prefixSign zero identity is used in the CliffordPathRealizations construction.

Definition 1.10 (pathMajorana).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (A:\mathbb{N}\to R),\\ \forall (q:R),\\ \forall (k:\mathbb{N}),(\mathrm{pathMajorana}Aq0=q)\wedge (\mathrm{pathMajorana}Aq(k+1)=-\mathrm{Complex}.I\cdot (\mathrm{pathMajorana}Aqk\cdot Ak))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.pathMajorana (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pathMajorana.

Lemma 1.11 (anticommuting trace zero).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (A:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (B:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (B\cdot B=1)\to \\ (A\cdot B=-(B\cdot A))\to \\ A.\mathrm{trace}=0\end{array}$$

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

Source. Repository-derived.

Commentary.

This anticommuting trace zero identity is used in the CliffordPathRealizations construction.

Lemma 1.12 (noisy eq of trace zero).

$$\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 v,(Av).\mathrm{trace}=0)\to \\ \forall (t:\mathbb{R}),\\ \forall (v:\mathrm{Fin}m),\\ \mathrm{noisyObservable}Atv=(t:\mathbb{C})\cdot Av\end{array}$$

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

Source. Repository-derived.

Commentary.

This noisy eq of trace zero identity is used in the CliffordPathRealizations construction.

Definition 1.13 (outcomeSign).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),\\ (\mathrm{outcomeSign}(b:=b):\mathbb{C})=(\mathrm{if}b\mathrm{then}1\mathrm{else}-1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.outcomeSign (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines outcomeSign.

Lemma 1.14 (parent signed marginal).

$$\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 (t:\mathbb{R}),\\ (\forall v,(Av).\mathrm{trace}=0)\to \\ \forall (E:(\mathrm{Fin}m\to \mathrm{Bool})\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\forall vs,(\sum a\in \mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}a\mapsto av=s),Ea)=\mathrm{effect}Atvs)\to \\ \forall (v:\mathrm{Fin}m),\\ (\sum a,\mathrm{outcomeSign}(av)\cdot Ea)=(t:\mathbb{C})\cdot Av\end{array}$$

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

Source. Repository-derived.

Commentary.

This parent signed marginal identity is used in the CliffordPathRealizations construction.

Definition 1.15 (weightedHamiltonian).

$$\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 (w:\mathrm{Fin}m\to \mathbb{R}),\\ \forall (a:\mathrm{Fin}m\to \mathrm{Bool}),\\ (\mathrm{weightedHamiltonian}(m:=m)(d:=d)(A:=A)(w:=w)(a:=a):\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})=(\sum v,(\mathrm{outcomeSign}(av)\cdot (wv:\mathbb{C}))\cdot Av)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedHamiltonian (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines weightedHamiltonian.

Lemma 1.16 (weighted trace bound).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (0<d)\to \\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (w:\mathrm{Fin}m\to \mathbb{R}),\\ \forall (t:\mathbb{R}),\\ \forall (c:\mathbb{R}),\\ (\forall v,(Av).\mathrm{trace}=0)\to \\ (\forall v,Av\cdot Av=1)\to \\ (\mathrm{JM}At)\to \\ (\forall a,((c:\mathbb{C})\cdot (1:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))-\mathrm{weightedHamiltonian}Awa).\mathrm{PosSemidef})\to \\ t\cdot (\sum v,wv)\le c\end{array}$$

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

Source. Repository-derived.

Commentary.

This weighted trace bound identity is used in the CliffordPathRealizations construction.

Lemma 1.17 (path realization trace zero).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (2\le m)\to \\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{pathGraph}m)A)\to \\ \forall (v:\mathrm{Fin}m),\\ (Av).\mathrm{trace}=0\end{array}$$

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

Source. Repository-derived.

Commentary.

This path realization trace zero identity is used in the CliffordPathRealizations construction.

Lemma 1.18 (cycle realization trace zero).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (2\le m)\to \\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{cycleGraph}m)A)\to \\ \forall (v:\mathrm{Fin}m),\\ (Av).\mathrm{trace}=0\end{array}$$

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

Source. Repository-derived.

Commentary.

This cycle realization trace zero identity is used in the CliffordPathRealizations construction.

Definition 1.19 (liftPath).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (A:\mathbb{N}\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (k:\mathbb{N}),\\ (\mathrm{liftPath}(d:=d)(A:=A)(k:=k):\mathrm{Matrix}(\mathrm{Fin}d\times \mathrm{Fin}2)(\mathrm{Fin}d\times \mathrm{Fin}2)\mathbb{C})=(Ak(\mathrm{Matrix}.\mathrm{kronecker})(\mathrm{if}k=0\mathrm{then}\mathrm{qubitZ}\mathrm{else}1))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftPath (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines liftPath.

Definition 1.20 (liftSeed).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ (\mathrm{liftSeed}(d:=d):\mathrm{Matrix}(\mathrm{Fin}d\times \mathrm{Fin}2)(\mathrm{Fin}d\times \mathrm{Fin}2)\mathbb{C})=((1:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(\mathrm{Matrix}.\mathrm{kronecker})\mathrm{qubitX})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftSeed (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines liftSeed.

Lemma 1.21 (liftSeed square).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \mathrm{liftSeed}d\cdot \mathrm{liftSeed}d=1\end{array}$$

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

Source. Repository-derived.

Commentary.

This liftSeed square identity is used in the CliffordPathRealizations construction.

Lemma 1.22 (liftSeed relation).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (A:\mathbb{N}\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (j:\mathbb{N}),\\ \mathrm{liftSeed}d\cdot \mathrm{liftPath}Aj=\mathrm{prefixSign}0j\cdot (\mathrm{liftPath}Aj\cdot \mathrm{liftSeed}d)\end{array}$$

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

Source. Repository-derived.

Commentary.

This liftSeed relation identity is used in the CliffordPathRealizations construction.

Lemma 1.23 (arbitrary path majorana extension).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (m:\mathbb{N}),\\ \forall (A:\mathbb{N}\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\forall k,k<m\to Ak\cdot Ak=1)\to \\ (\forall k,k<m\to (Ak).\mathrm{IsHermitian})\to \\ (\forall kj,k<m\to j<m\to Ak\cdot Aj=\mathrm{generatorSign}kj\cdot (Aj\cdot Ak))\to \\ \mathrm{let}g:=\mathrm{pathMajorana}(\mathrm{liftPath}A)(\mathrm{liftSeed}d);(\forall k,k\le m\to gk\cdot gk=1)\wedge (\forall k,k\le m\to \mathrm{star}(gk)=gk)\wedge (\forall j,j\le m\to \forall i,i<j\to gi\cdot gj=-(gj\cdot gi))\wedge (\forall k,k<m\to \mathrm{Complex}.I\cdot (gk\cdot g(k+1))=\mathrm{liftPath}Ak)\end{array}$$

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

Source. Repository-derived.

Commentary.

One qubit ancilla gives a seed that anticommutes with the first path generator and commutes with all subsequent generators. The recursive Majorana family is Hermitian, squares to the identity, anticommutes pairwise, and has the exact consecutive bonds shown.

Definition 1.24 (totalPath).

$$\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{totalPath}(d:=d)(m:=m)(A:=A)(k:=k):\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})=(\mathrm{if}\mathrm{hk}:k<m\mathrm{then}A⟨k,\mathrm{hk}⟩\mathrm{else}1)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.totalPath (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines totalPath.

Lemma 1.25 (realization majoranas).

$$\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})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{pathGraph}m)A)\to \\ \mathrm{let}g:=\mathrm{pathMajorana}(\mathrm{liftPath}(\mathrm{totalPath}A))(\mathrm{liftSeed}d);(\forall k,k\le m\to gk\cdot gk=1)\wedge (\forall k,k\le m\to \mathrm{star}(gk)=gk)\wedge (\forall j,j\le m\to \forall i,i<j\to gi\cdot gj=-(gj\cdot gi))\wedge (\forall k,k<m\to \mathrm{Complex}.I\cdot (gk\cdot g(k+1))=\mathrm{liftPath}(\mathrm{totalPath}A)k)\end{array}$$

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

Source. Repository-derived.

Commentary.

This realization majoranas identity is used in the CliffordPathRealizations construction.

Lemma 1.26 (labeled parent suffices).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ \forall (Omega:\mathrm{Type}),\\ [\mathrm{Fintype}Omega],\\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (t:\mathbb{R}),\\ \forall (\mathrm{label}:Omega\to \mathrm{Fin}m\to \mathrm{Bool}),\\ \forall (P:Omega\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\forall \omega ,(P\omega ).\mathrm{PosSemidef})\to \\ (\sum \omega ,P\omega =1)\to \\ (\forall v,\sum \omega ,\mathrm{outcomeSign}(\mathrm{label}\omega v)\cdot P\omega =\mathrm{noisyObservable}Atv)\to \\ \mathrm{JM}At\end{array}$$

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

Source. Repository-derived.

Commentary.

This labeled parent suffices identity is used in the CliffordPathRealizations construction.

Definition 1.27 (qubitV).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{DecidableEq}\iota ],\\ (\mathrm{qubitV}(\iota :=\iota ):\mathrm{Matrix}(\iota \times \mathrm{Fin}2)\iota \mathbb{C})=((1:\mathrm{Matrix}(\iota \times \mathrm{Fin}2)(\iota \times \mathrm{Fin}2)\mathbb{C}).\mathrm{submatrix}\mathrm{id}(\mathrm{fun}v\mapsto (v,0)))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.qubitV (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines qubitV.

Lemma 1.28 (qubitV isometry).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ (\mathrm{qubitV}(\iota :=\iota )).\mathrm{conjTranspose}\cdot (\mathrm{qubitV}(\iota :=\iota ))=(1:\mathrm{Matrix}\iota \iota \mathbb{C})\end{array}$$

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

Source. Repository-derived.

Commentary.

This qubitV isometry identity is used in the CliffordPathRealizations construction.

Lemma 1.29 (qubitV compress).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (D:\mathrm{Matrix}(\mathrm{Fin}2)(\mathrm{Fin}2)\mathbb{C}),\\ (\mathrm{qubitV}(\iota :=\iota )).\mathrm{conjTranspose}\cdot (A(\mathrm{Matrix}.\mathrm{kronecker})D)\cdot (\mathrm{qubitV}(\iota :=\iota ))=D00\cdot A\end{array}$$

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

Source. Repository-derived.

Commentary.

This qubitV compress identity is used in the CliffordPathRealizations construction.

Lemma 1.30 (compressed parent).

$$\begin{array}{r}\forall (m:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ \forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (A:\mathrm{Fin}m\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ \forall (B:\mathrm{Fin}m\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (t:\mathbb{R}),\\ \forall (V:\mathrm{Matrix}\iota (\mathrm{Fin}d)\mathbb{C}),\\ (V.\mathrm{conjTranspose}\cdot V=1)\to \\ (\forall v,(Av).\mathrm{trace}=0)\to \\ (\forall v,V.\mathrm{conjTranspose}\cdot Bv\cdot V=Av)\to \\ \forall (E:(\mathrm{Fin}m\to \mathrm{Bool})\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ (\forall a,(Ea).\mathrm{PosSemidef})\to \\ (\sum a,Ea=1)\to \\ (\forall v,\sum a,\mathrm{outcomeSign}(av)\cdot Ea=(t:\mathbb{C})\cdot Bv)\to \\ \mathrm{JM}At\end{array}$$

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

Source. Repository-derived.

Commentary.

This compressed parent identity is used in the CliffordPathRealizations construction.

Definition 1.31 (paddedMajoranas).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{DecidableEq}\iota ],\\ \forall (m:\mathbb{N}),\\ \forall (g:\mathbb{N}\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (j:\mathrm{Fin}(m+2)),\\ (\mathrm{paddedMajoranas}(\iota :=\iota )(m:=m)(g:=g)(j:=j):\mathrm{Matrix}(\iota \times \mathrm{Fin}2)(\iota \times \mathrm{Fin}2)\mathbb{C})=(\mathrm{if}j.\mathrm{val}=0\mathrm{then}(1:\mathrm{Matrix}\iota \iota \mathbb{C})(\mathrm{Matrix}.\mathrm{kronecker})\mathrm{qubitX}\mathrm{else}g(j.\mathrm{val}-1)(\mathrm{Matrix}.\mathrm{kronecker})\mathrm{qubitZ})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.paddedMajoranas (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines paddedMajoranas.

Lemma 1.32 (paddedMajoranas relations).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (m:\mathbb{N}),\\ \forall (g:\mathbb{N}\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ (\forall k,k\le m\to gk\cdot gk=1)\to \\ (\forall k,k\le m\to \mathrm{star}(gk)=gk)\to \\ (\forall kl,k\le m\to l\le m\to k\ne l\to gk\cdot gl=-(gl\cdot gk))\to \\ (\forall j,\mathrm{paddedMajoranas}(m:=m)gj\cdot \mathrm{paddedMajoranas}gj=1)\wedge (\forall j,\mathrm{star}(\mathrm{paddedMajoranas}(m:=m)gj)=\mathrm{paddedMajoranas}gj)\wedge (\forall jk,j\ne k\to \mathrm{paddedMajoranas}(m:=m)gj\cdot \mathrm{paddedMajoranas}gk=-(\mathrm{paddedMajoranas}gk\cdot \mathrm{paddedMajoranas}gj))\end{array}$$

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

Source. Repository-derived.

Commentary.

This paddedMajoranas relations identity is used in the CliffordPathRealizations construction.

Lemma 1.33 (paddedMajoranas bond).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (m:\mathbb{N}),\\ \forall (g:\mathbb{N}\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (j:\mathrm{Fin}(m+2)),\\ (0<j.\mathrm{val})\to \\ \forall (\mathrm{hnext}:j.\mathrm{val}+1<m+2),\\ \mathrm{Complex}.I\cdot (\mathrm{paddedMajoranas}gj\cdot \mathrm{paddedMajoranas}g⟨j.\mathrm{val}+1,\mathrm{hnext}⟩)=(\mathrm{Complex}.I\cdot (g(j.\mathrm{val}-1)\cdot gj.\mathrm{val}))(\mathrm{Matrix}.\mathrm{kronecker})(1:\mathrm{Matrix}(\mathrm{Fin}2)(\mathrm{Fin}2)\mathbb{C})\end{array}$$

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

Source. Repository-derived.

Commentary.

This paddedMajoranas bond identity is used in the CliffordPathRealizations construction.

Definition 1.34 (Quadratic).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ \forall (g:\mathrm{Fin}M\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ \forall (C:\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C}),\\ (\mathrm{Quadratic}(M:=M)(\iota :=\iota )(g:=g)(C:=C):\mathrm{Matrix}\iota \iota \mathbb{C})=(\sum j,\sum k,Cjk\cdot (gj\cdot gk))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.Quadratic (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines Quadratic.

Lemma 1.35 (quadratic bound of positive split).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (g:\mathrm{Fin}M\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 (P:\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C}),\\ \forall (Q:\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C}),\\ \forall (K:\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C}),\\ (P.\mathrm{PosSemidef})\to \\ (Q.\mathrm{PosSemidef})\to \\ (K=P-Q)\to \\ (P.\mathrm{trace}\cdot (1:\mathrm{Matrix}\iota \iota \mathbb{C})-(1/2:\mathbb{C})\cdot \mathrm{Quadratic}gK).\mathrm{PosSemidef}\end{array}$$

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

Source. Repository-derived.

Commentary.

This quadratic bound of positive split identity is used in the CliffordPathRealizations construction.

Lemma 1.36 (sum fin next).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (S:\mathrm{Type}),\\ [\mathrm{AddCommMonoid}S],\\ \forall (j:\mathrm{Fin}M),\\ \forall (f:\mathrm{Fin}M\to S),\\ (\sum k,\mathrm{if}j.\mathrm{val}+1=k.\mathrm{val}\mathrm{then}fk\mathrm{else}0)=\mathrm{if}h:j.\mathrm{val}+1<M\mathrm{then}f⟨j.\mathrm{val}+1,h⟩\mathrm{else}0\end{array}$$

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

Source. Repository-derived.

Commentary.

This sum fin next identity is used in the CliffordPathRealizations construction.

Lemma 1.37 (sum fin prev).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (S:\mathrm{Type}),\\ [\mathrm{AddCommMonoid}S],\\ \forall (j:\mathrm{Fin}M),\\ \forall (f:\mathrm{Fin}M\to S),\\ (\sum k,\mathrm{if}k.\mathrm{val}+1=j.\mathrm{val}\mathrm{then}fk\mathrm{else}0)=\mathrm{if}h:0<j.\mathrm{val}\mathrm{then}f⟨j.\mathrm{val}-1,\mathrm{by}\mathrm{omega}⟩\mathrm{else}0\end{array}$$

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

Source. Repository-derived.

Commentary.

The previous-index sum selects the preceding coordinate when it exists, and is zero at the left endpoint.

Definition 1.38 (tridiagonal).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (d:\mathrm{Fin}M\to \mathbb{C}),\\ \forall (w:\mathrm{Fin}M\to \mathbb{C}),\\ (\mathrm{tridiagonal}(M:=M)(d:=d)(w:=w):\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C})=(\mathrm{Matrix}.\mathrm{diagonal}d+\mathrm{Matrix}.\mathrm{of}(\mathrm{fun}jk:\mathrm{Fin}M\mapsto \mathrm{if}j.\mathrm{val}+1=k.\mathrm{val}\mathrm{then}wj\mathrm{else}0)+\mathrm{Matrix}.\mathrm{transpose}(\mathrm{Matrix}.\mathrm{of}(\mathrm{fun}jk:\mathrm{Fin}M\mapsto \mathrm{if}j.\mathrm{val}+1=k.\mathrm{val}\mathrm{then}wj\mathrm{else}0)))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.tridiagonal (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines tridiagonal.

Lemma 1.39 (tridiagonal mul apply).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (N:\mathbb{N}),\\ \forall (d:\mathrm{Fin}M\to \mathbb{C}),\\ \forall (w:\mathrm{Fin}M\to \mathbb{C}),\\ \forall (F:\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}N)\mathbb{C}),\\ \forall (j:\mathrm{Fin}M),\\ \forall (r:\mathrm{Fin}N),\\ (\mathrm{tridiagonal}Mdw\cdot F)jr=dj\cdot Fjr+(\mathrm{if}h:j.\mathrm{val}+1<M\mathrm{then}wj\cdot F⟨j.\mathrm{val}+1,h⟩r\mathrm{else}0)+(\mathrm{if}0<j.\mathrm{val}\mathrm{then}w⟨j.\mathrm{val}-1,\cdot ⟩\cdot F⟨j.\mathrm{val}-1,\cdot ⟩r\mathrm{else}0)\end{array}$$

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

Source. Repository-derived.

Commentary.

This tridiagonal mul apply identity is used in the CliffordPathRealizations construction.

Lemma 1.40 (mul tridiagonal apply).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (N:\mathbb{N}),\\ \forall (d:\mathrm{Fin}M\to \mathbb{C}),\\ \forall (w:\mathrm{Fin}M\to \mathbb{C}),\\ \forall (F:\mathrm{Matrix}(\mathrm{Fin}N)(\mathrm{Fin}M)\mathbb{C}),\\ \forall (j:\mathrm{Fin}N),\\ \forall (r:\mathrm{Fin}M),\\ (F\cdot \mathrm{tridiagonal}Mdw)jr=Fjr\cdot dr+(\mathrm{if}h:r.\mathrm{val}+1<M\mathrm{then}Fj⟨r.\mathrm{val}+1,h⟩\cdot wr\mathrm{else}0)+(\mathrm{if}0<r.\mathrm{val}\mathrm{then}Fj⟨r.\mathrm{val}-1,\cdot ⟩\cdot w⟨r.\mathrm{val}-1,\cdot ⟩\mathrm{else}0)\end{array}$$

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

Source. Repository-derived.

Commentary.

This mul tridiagonal apply identity is used in the CliffordPathRealizations construction.

Definition 1.41 (edgeVector).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (r:\mathrm{Fin}M),\\ \forall (j:\mathrm{Fin}M),\\ (\mathrm{edgeVector}(M:=M)(r:=r)(j:=j):\mathbb{C})=((\mathrm{Pi}.\mathrm{single}r(1:\mathbb{C}):\mathrm{Fin}M\to \mathbb{C})j-(\mathrm{if}r.\mathrm{val}+1=j.\mathrm{val}\mathrm{then}1\mathrm{else}0))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.edgeVector (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines edgeVector.

Definition 1.42 (weightedLap).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (b:\mathrm{Fin}M\to \mathbb{R}),\\ (\mathrm{weightedLap}(M:=M)(b:=b):\mathrm{Matrix}(\mathrm{Fin}M)(\mathrm{Fin}M)\mathbb{C})=(\sum r,(br:\mathbb{C})\cdot \mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{edgeVector}Mr)(\mathrm{star}(\mathrm{edgeVector}Mr)))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedLap (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines weightedLap.

Lemma 1.43 (weightedLap psd).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (b:\mathrm{Fin}M\to \mathbb{R}),\\ (\forall r,0\le br)\to \\ (\mathrm{weightedLap}Mb).\mathrm{PosSemidef}\end{array}$$

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

Source. Repository-derived.

Commentary.

This weightedLap psd identity is used in the CliffordPathRealizations construction.

Lemma 1.44 (weightedLap apply).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ \forall (b:\mathrm{Fin}M\to \mathbb{R}),\\ \forall (j:\mathrm{Fin}M),\\ \forall (k:\mathrm{Fin}M),\\ \mathrm{weightedLap}Mbjk=(\mathrm{if}j=k\mathrm{then}((bj:\mathbb{C})+(\mathrm{if}0<j.\mathrm{val}\mathrm{then}(b⟨j.\mathrm{val}-1,\cdot ⟩:\mathbb{C})\mathrm{else}0))\mathrm{else}0)-(\mathrm{if}j.\mathrm{val}+1=k.\mathrm{val}\mathrm{then}(bj:\mathbb{C})\mathrm{else}0)-(\mathrm{if}k.\mathrm{val}+1=j.\mathrm{val}\mathrm{then}(bk:\mathbb{C})\mathrm{else}0)\end{array}$$

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

Source. Repository-derived.

Commentary.

This weightedLap apply identity is used in the CliffordPathRealizations construction.

References

• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.JM
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.Quadratic
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.Realization
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.anticommuting_trace_zero
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.arbitrary_path_majorana_extension
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.compressed_parent
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.cycle_realization_trace_zero
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.edgeVector
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.effect
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.generatorSign
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.labeled_parent_suffices
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftPath
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftSeed
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftSeed_relation
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.liftSeed_square
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.mul_tridiagonal_apply
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.noisyObservable
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.noisy_eq_of_trace_zero
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.outcomeSign
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.paddedMajoranas
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.paddedMajoranas_bond
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.paddedMajoranas_relations
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.parent_signed_marginal
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.pathMajorana
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.path_realization_trace_zero
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.prefixSign
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.prefixSign_zero
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.quadratic_bound_of_positive_split
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.qubitV
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.qubitV_compress
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.qubitV_isometry
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.realization_majoranas
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.signed_product
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.sum_fin_next
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.sum_fin_prev
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.totalPath
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.tridiagonal
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.tridiagonal_mul_apply
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.visibility
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedHamiltonian
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedLap
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedLap_apply
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weightedLap_psd
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations.weighted_trace_bound
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/Quantum/QuantumChannels/TomiyamaDiagonalKPositivity
• Dependency: D5/S3/QuantumBounds/MerminMeasurementDependence/Model