Hardware Circuit Factors

Abstract

HardwareCircuitFactors describes the forced-twin mechanism for QPU-restricted IQP circuits.

Definition 1.1 (connector).

$$\forall (m:\mathbb{N}),(\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{connector}uv⟺\mathrm{val}((u.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=5\wedge \mathrm{val}((v.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=4\wedge \mathrm{val}((v.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{divNat})=\mathrm{Nat}.\mathrm{mod}(\mathrm{val}((u.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{divNat})+1)m)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.connector (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines connector. Fin.divNat and Fin.modNat give the quotient and remainder after the product-size cast. Nat.div and Nat.mod denote integer division and remainder; every cast displays its target or equality proof.

Definition 1.2 (hardwareAdj).

$$\forall (m:\mathbb{N}),(\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{hardwareAdj}uv⟺u\ne v\wedge ((\mathrm{val}((u.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{divNat})=\mathrm{val}((v.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{divNat})\wedge \neg ((\mathrm{val}((u.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=4\wedge \mathrm{val}((v.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=5)\vee (\mathrm{val}((u.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=5\wedge \mathrm{val}((v.\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=4)))\vee \mathrm{connector}uv\vee \mathrm{connector}vu))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardwareAdj (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines hardwareAdj.

Definition 1.3 (H).

$$\forall (m:\mathbb{N}),((Hm).\mathrm{Adj}=\mathrm{hardwareAdj})$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.H (✓ std3).

Source. Repository-derived.

Commentary.

The simple hardware graph has the displayed adjacency: each component is K6 without the edge between vertices 4 and 5, and consecutive blocks have the cyclic connector from 5 to 4.

Definition 1.4 (hardwareEdges).

$$\forall (m:\mathbb{N}),(\mathrm{hardwareEdges}m=\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}\mathrm{fun}e\mapsto e.1.\mathrm{val}<e.2.\mathrm{val}\wedge \mathrm{hardwareAdj}e.1e.2)$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardwareEdges (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines hardwareEdges.

Definition 1.5 (edgeDegree).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeDegree}Gv=(G.\mathrm{filter}\mathrm{fun}e\mapsto v\in s(e.1,e.2)).\mathrm{card})))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeDegree (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines edgeDegree.

Definition 1.6 (F4).

$$\forall (m:\mathbb{N}),(F4m=(\mathrm{hardwareEdges}m).\mathrm{powerset}.\mathrm{filter}\mathrm{fun}G\mapsto \forall v,\mathrm{edgeDegree}Gv=4)$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.F4 (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

Definition 1, p. 4, verbatim from the source TeX: “Let \mH_n=(\mV_{\mH},\mE_{\mH}) be a fixed simple D-regular hardware graph on n labeled vertices, and let 3\le d\le D be a fixed constant (n-independent). The \emph{d-factors} of a graph \mH are \mF_d(\mH) \equiv {\mG=(\mV,\mE_{\mG}) : \mE_{\mG}\subseteq \mE_{\mH},\deg_{\mG}(v)=d\ \forall v\in\mV}. The \emph{QPU-restricted graph ensemble} is the probability space \mathrm{Unif}[\mF_d(\mH_n)] in which, for each run of \UDAD, a graph \mG\in\mF_d(\mH_n) is drawn uniformly at random.” Here d is four; ordered endpoint pairs record each undirected edge once, and all four-factors are retained.

Definition 1.7 (randomLayer).

$$\forall (m:\mathbb{N}),\forall (\theta :((\mathrm{Fin}(6\cdot m))\to \mathbb{R})),\mathrm{randomLayer}m\theta =((\mathrm{tensorOp}(\mathrm{fun}i\mapsto (\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\theta i))))).\mathrm{submatrix}(\mathrm{fun}si\mapsto (\mathrm{if}((si))\mathrm{then}1\mathrm{else}0))(\mathrm{fun}zi\mapsto (\mathrm{if}((zi))\mathrm{then}1\mathrm{else}0)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.randomLayer (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

The displayed expression defines randomLayer.

Definition 1.8 (HZ).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{HZ}Gz=(\sum i,(\mathrm{Real}.\mathrm{pi}/7)\cdot D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}(zi))+(\mathrm{Real}.\mathrm{pi}/4)\cdot \sum e\in G,D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}(ze.1)\cdot D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}(ze.2))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.HZ (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

Equation (19) uses the Hamiltonian H prime Z from Eq. (19b): each single-qubit angle is fixed to pi/7, and every selected edge has coupling pi/4. The diagonal entries use the Z eigenvalues of the bit string.

Definition 1.9 (circuit).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}(\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m))),(\forall (\theta :\mathrm{Fin}(6\cdot m)\to \mathbb{R}),(\mathrm{circuit}G\theta =\mathrm{randomLayer}m\theta \cdot (\mathrm{Matrix}.\mathrm{diagonal}(\mathrm{fun}z\mapsto \mathrm{Complex}.\exp (-\mathrm{Complex}.I\cdot (\mathrm{HZ}Gz:\mathbb{C}))))\cdot (\mathrm{tensorOp}(\mathrm{fun}\cdot :\mathrm{Fin}(6\cdot m)\mapsto \mathrm{hadamard})).\mathrm{submatrix}(\mathrm{fun}(s:\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})i\mapsto (\mathrm{if}(si)\mathrm{then}1\mathrm{else}0))(\mathrm{fun}(z:\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})i\mapsto (\mathrm{if}(zi)\mathrm{then}1\mathrm{else}0)))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.circuit (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

Equation (19), verbatim: \UIQP^{(\theta)} = U_{\mathrm{R}}^{(\theta)} e^{-i H’_Z} W^{\otimes n}. The definition is this literal matrix product, with randomLayer the tensor product of hadamard times rotation 1 theta_i in Bool coordinates.

Definition 1.10 (outputProbability).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (\theta :(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),(\forall (s:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{outputProbability}G\theta s=\mathrm{Complex}.\mathrm{normSq}(\mathrm{circuit}G\theta s(\mathrm{fun}\cdot \mapsto \mathrm{false}))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.outputProbability (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

The probability is the squared modulus of the literal circuit matrix element from the all-false input to the output s.

Definition 1.11 (uniformAngles).

$$\forall (m:\mathbb{N}),(\mathrm{uniformAngles}m=\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot \mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.uniformAngles (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

The angle distribution is specified on p. 4, verbatim from the source TeX: “We choose i.i.d. angles {\theta_i}_{i=1}^n uniformly from [0,2\pi),”. The displayed product measure expresses the independence of all coordinates.

Definition 1.12 (joint).

$$\forall (m:\mathbb{N}),(\mathrm{joint}m=((\mathrm{ProbabilityTheory}.\mathrm{uniformOn}(F4m:\mathrm{Set}(\mathrm{Finset}(\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))))).\mathrm{prod}(\mathrm{uniformAngles}m))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.joint (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

The graph and angles are independent; their joint law is the product measure.

Definition 1.13 (tailProbability).

$$\forall (m:\mathbb{N}),(\forall (a:\mathbb{R}),(\forall (s:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{tailProbability}mas=(\mathrm{joint}m).\mathrm{real}\{\omega |a\cdot ((2:\mathbb{R}{)}^{6\cdot m}{)}^{-1}\le \mathrm{outputProbability}\omega .1\omega .2s\})))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.tailProbability (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

The displayed expression defines tailProbability.

Definition 1.14 (localEdges).

$$\mathrm{localEdges}=![(0,1),(0,2),(0,3),(0,4),(0,5),(1,2),(1,3),(1,4),(1,5),(2,3),(2,4),(2,5),(3,4),(3,5)]$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localEdges (✓ std3).

Source. Repository-derived.

Commentary.

The displayed table defines localEdges : Fin 14 → Fin 6 × Fin 6, the fourteen internal edges of K6 with the edge (4,5) removed.

Definition 1.15 (localDegree).

$$\forall (M:\mathrm{Fin}14\to \mathrm{Bool}),(\forall (v:\mathrm{Fin}6),(\mathrm{localDegree}Mv=\sum e:\mathrm{Fin}14,\mathrm{if}\mathrm{Bool}.\mathrm{and}(Me)(\mathrm{Bool}.\mathrm{or}(\mathrm{decide}((\mathrm{localEdges}e).1=v))(\mathrm{decide}((\mathrm{localEdges}e).2=v)))\mathrm{then}1\mathrm{else}0))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localDegree (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines localDegree.

Definition 1.16 (boundaryDegree).

$$\forall (\mathrm{incoming}:\mathrm{Bool}),(\forall (\mathrm{outgoing}:\mathrm{Bool}),(\forall (v:\mathrm{Fin}6),(\mathrm{boundaryDegree}\mathrm{incoming}\mathrm{outgoing}v=(\mathrm{if}\mathrm{Bool}.\mathrm{and}(\mathrm{decide}(v=4))\mathrm{incoming}\mathrm{then}1\mathrm{else}0)+(\mathrm{if}\mathrm{Bool}.\mathrm{and}(\mathrm{decide}(v=5))\mathrm{outgoing}\mathrm{then}1\mathrm{else}0))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.boundaryDegree (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines boundaryDegree.

Definition 1.17 (LocalMatching).

$$\forall (M:\mathrm{Fin}14\to \mathrm{Bool}),(\forall (\mathrm{incoming}:\mathrm{Bool}),(\forall (\mathrm{outgoing}:\mathrm{Bool}),(\mathrm{LocalMatching}M\mathrm{incoming}\mathrm{outgoing}⟺\forall v,\mathrm{localDegree}Mv+\mathrm{boundaryDegree}\mathrm{incoming}\mathrm{outgoing}v=1)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.LocalMatching (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines LocalMatching.

Definition 1.18 (blockEquiv).

$$\forall (m:\mathbb{N}),(\mathrm{blockEquiv}m=\mathrm{finProdFinEquiv}.\mathrm{trans}(\mathrm{finCongr}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}m6)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.blockEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines blockEquiv.

Theorem 1.19 (blockEquiv val).

$$\forall (m:\mathbb{N}),(\forall (i:\mathrm{Fin}m),(\forall (v:\mathrm{Fin}6),((\mathrm{blockEquiv}m(i,v)).\mathrm{val}=6\cdot i.\mathrm{val}+v.\mathrm{val})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.blockEquiv_val (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated blockEquiv val relation for the finite twin-pair calculation.

Theorem 1.20 (component encode).

$$\forall (m:\mathbb{N}),(\forall (i:\mathrm{Fin}m),(\forall (v:\mathrm{Fin}6),(\mathrm{val}(((\mathrm{blockEquiv}m(i,v)).\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{divNat})=i.\mathrm{val}\wedge \mathrm{val}(((\mathrm{blockEquiv}m(i,v)).\mathrm{cast}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}6m)).\mathrm{modNat})=v.\mathrm{val})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.block_encode (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated component encode relation for the finite twin-pair calculation.

Definition 1.21 (localNeighbours).

$$\forall (v:\mathrm{Fin}6),(\mathrm{localNeighbours}v=\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}\mathrm{fun}w\mapsto v\ne w\wedge \neg ((v=4\wedge w=5)\vee (v=5\wedge w=4)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localNeighbours (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines localNeighbours.

Theorem 1.22 (hardware adj encoded).

$$\forall (m:\mathbb{N}),(\forall (i:\mathrm{Fin}m),(\forall (j:\mathrm{Fin}m),(\forall (r:\mathrm{Fin}6),(\forall (t:\mathrm{Fin}6),(\mathrm{hardwareAdj}(\mathrm{blockEquiv}m(i,r))(\mathrm{blockEquiv}m(j,t))⟺(i=j\wedge t\in \mathrm{localNeighbours}r)\vee (r=5\wedge t=4\wedge j.\mathrm{val}=(i.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}m)\vee (t=5\wedge r=4\wedge i.\mathrm{val}=(j.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}m))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_adj_encoded (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated hardware adj encoded relation for the finite twin-pair calculation.

Theorem 1.23 (cyclic next val).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),((i+1).\mathrm{val}=(i.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}m))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_next_val (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated cyclic next val relation for the finite twin-pair calculation.

Theorem 1.24 (cyclic prev iff).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),(\forall (j:\mathrm{Fin}m),(i.\mathrm{val}=(j.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}m⟺j=i-1)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_prev_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated cyclic prev iff relation for the finite twin-pair calculation.

Theorem 1.25 (cyclic next iff).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),(\forall (j:\mathrm{Fin}m),(j.\mathrm{val}=(i.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}m⟺j=i+1)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_next_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated cyclic next iff relation for the finite twin-pair calculation.

Theorem 1.26 (hardware adj encoded cycle).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),(\forall (j:\mathrm{Fin}m),(\forall (r:\mathrm{Fin}6),(\forall (t:\mathrm{Fin}6),(\mathrm{hardwareAdj}(\mathrm{blockEquiv}m(i,r))(\mathrm{blockEquiv}m(j,t))⟺(i=j\wedge t\in \mathrm{localNeighbours}r)\vee (r=5\wedge t=4\wedge j=i+1)\vee (t=5\wedge r=4\wedge j=i-1))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_adj_encoded_cycle (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated hardware adj encoded cycle relation for the finite twin-pair calculation.

Theorem 1.27 (encoded neighbours card).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),(\forall (r:\mathrm{Fin}6),((\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}w:\mathrm{Fin}m\times \mathrm{Fin}6\mapsto \mathrm{hardwareAdj}(\mathrm{blockEquiv}m(i,r))(\mathrm{blockEquiv}mw))).\mathrm{card}=5)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.encoded_neighbours_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated encoded neighbours card relation for the finite twin-pair calculation.

Theorem 1.28 (orderedEdge hardware).

$$\forall (m:\mathbb{N}),(\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),((\mathrm{hardwareAdj}uv)\to ((Sym2.\mathrm{sortEquiv}s(u,v)).\mathrm{val}\in \mathrm{hardwareEdges}m))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.orderedEdge_hardware (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated orderedEdge hardware relation for the finite twin-pair calculation.

Theorem 1.29 (hardware incident card).

$$\forall (m:\mathbb{N}),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeDegree}(\mathrm{hardwareEdges}m)v=(\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}w\mapsto \mathrm{hardwareAdj}vw)).\mathrm{card}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_incident_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated hardware incident card relation for the finite twin-pair calculation.

Theorem 1.30 (hardware degree five).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeDegree}(\mathrm{hardwareEdges}m)v=5))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_degree_five (✓ std3). ∎

Source. Repository-derived.

Commentary.

For more than one component the hardware is five-regular, as required by Definition 1 with D=5.

Theorem 1.31 (factor complement matching).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((G\in F4m)\to (\forall v,\mathrm{edgeDegree}(\mathrm{hardwareEdges}m\setminus G)v=1)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.factor_complement_matching (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated factor complement matching relation for the finite twin-pair calculation.

Definition 1.32 (edgeAdj).

$$\forall (m:\mathbb{N}),(\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeAdj}Euv⟺(Sym2.\mathrm{sortEquiv}s(u,v)).\mathrm{val}\in E))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines edgeAdj.

Theorem 1.33 (edgeAdj hardware).

$$\forall (m:\mathbb{N}),(\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((E\subseteq \mathrm{hardwareEdges}m)\to (\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),((\mathrm{edgeAdj}Euv)\to (\mathrm{hardwareAdj}uv))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj_hardware (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated edgeAdj hardware relation for the finite twin-pair calculation.

Theorem 1.34 (edgeAdj symm).

$$\forall (m:\mathbb{N}),(\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (u:(\mathrm{Fin}(6\cdot m))),(\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeAdj}Euv⟺\mathrm{edgeAdj}Evu))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj_symm (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated edgeAdj symm relation for the finite twin-pair calculation.

Theorem 1.35 (subset incident card).

$$\forall (m:\mathbb{N}),(\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((E\subseteq \mathrm{hardwareEdges}m)\to (\forall (v:(\mathrm{Fin}(6\cdot m))),(\mathrm{edgeDegree}Ev=(\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}w\mapsto \mathrm{edgeAdj}Evw)).\mathrm{card}))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.subset_incident_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated subset incident card relation for the finite twin-pair calculation.

Theorem 1.36 (matching neighbour unique).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((G\in F4m)\to (\forall (v:(\mathrm{Fin}(6\cdot m))),(\exists !w,\mathrm{edgeAdj}(\mathrm{hardwareEdges}m\setminus G)vw))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.matching_neighbour_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated matching neighbour unique relation for the finite twin-pair calculation.

Definition 1.37 (localMatchingFlags).

$$\forall (m:\mathbb{N}),(\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (i:\mathrm{Fin}m),(\mathrm{localMatchingFlags}Ei=\mathrm{fun}e\mapsto \mathrm{decide}(\mathrm{edgeAdj}E(\mathrm{blockEquiv}m(i,(\mathrm{localEdges}e).1))(\mathrm{blockEquiv}m(i,(\mathrm{localEdges}e).2))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localMatchingFlags (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines localMatchingFlags.

Definition 1.38 (connectorFlag).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to (\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (i:\mathrm{Fin}m),(\mathrm{connectorFlag}Ei=\mathrm{decide}(\mathrm{edgeAdj}E(\mathrm{blockEquiv}m(i,5))(\mathrm{blockEquiv}m(i+1,4)))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.connectorFlag (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines connectorFlag.

Theorem 1.39 (subset degree local).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (E:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((E\subseteq \mathrm{hardwareEdges}m)\to (\forall (i:\mathrm{Fin}m),(\forall (r:\mathrm{Fin}6),(\mathrm{edgeDegree}E(\mathrm{blockEquiv}m(i,r))=\mathrm{localDegree}(\mathrm{localMatchingFlags}Ei)r+\mathrm{boundaryDegree}(\mathrm{connectorFlag}E(i-1))(\mathrm{connectorFlag}Ei)r)))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.subset_degree_local (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated subset degree local relation for the finite twin-pair calculation.

Theorem 1.40 (hardware internal vertex).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (i:\mathrm{Fin}m),(\forall (j:\mathrm{Fin}m),(\forall (r:\mathrm{Fin}6),(\forall (w:\mathrm{Fin}6),((r.\mathrm{val}<4)\to (\mathrm{hardwareAdj}(\mathrm{blockEquiv}m(i,r))(\mathrm{blockEquiv}m(j,w))⟺i=j\wedge w\ne r))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_internal_vertex (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated hardware internal vertex relation for the finite twin-pair calculation.

Theorem 1.41 (factor component twins).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((G\in F4m)\to (\forall (i:\mathrm{Fin}m),(\exists rt:\mathrm{Fin}6,r\ne t\wedge (\forall jw,\mathrm{edgeAdj}G(\mathrm{blockEquiv}m(i,r))(\mathrm{blockEquiv}m(j,w))⟺i=j\wedge w\ne r\wedge w\ne t)\wedge (\forall jw,\mathrm{edgeAdj}G(\mathrm{blockEquiv}m(i,t))(\mathrm{blockEquiv}m(j,w))⟺i=j\wedge w\ne r\wedge w\ne t)))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.factor_block_twins (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every four-factor contains, in each hardware component, two nonadjacent vertices with the other four component vertices as their exact common neighbourhood. This forces a positive density of twin pairs independently of the choice of factor.

Theorem 1.42 (angle integral eq).

$$\forall (f:\mathbb{R}\to \mathbb{R}),((\int x,fxd(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))=(2\cdot \mathrm{Real}.\mathrm{pi}{)}^{-1}\cdot \int x\mathrm{in}(0:\mathbb{R})..(2\cdot \mathrm{Real}.\mathrm{pi}),fx)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_integral_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

The conditional Lebesgue integral is the interval integral divided by the interval length.

Theorem 1.43 (angle integrable of continuous).

$$\forall (f:\mathbb{R}\to \mathbb{R}),((\mathrm{Continuous}f)\to (\mathrm{Integrable}f(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_integrable_of_continuous (✓ std3). ∎

Source. Repository-derived.

Commentary.

A continuous real function is integrable over the normalized finite angle interval.

Theorem 1.44 (angle cos mean).

$$(\int x,\mathrm{Real}.\cos xd(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_cos_mean (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalized cosine integral over a full period vanishes.

Definition 1.45 (pairAngle).

$$\mathrm{pairAngle}=(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))).\mathrm{prod}(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairAngle (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pairAngle.

Definition 1.46 (pairCos).

$$\forall (x:\mathbb{R}\times \mathbb{R}),(\mathrm{pairCos}x=\mathrm{Real}.\cos x.1\cdot \mathrm{Real}.\cos x.2)$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairCos (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pairCos.

Theorem 1.47 (fractional markov).

$$\forall (A:\mathrm{Type}),([\mathrm{MeasurableSpace}A]\to (\forall (\mu :\mathrm{Measure}A),([\mathrm{IsProbabilityMeasure}\mu ]\to (\forall (Z:A\to \mathbb{R}),((\forall x,0\le Zx)\to ((\mathrm{Integrable}(\mathrm{fun}x\mapsto \mathrm{Real}.\mathrm{sqrt}(Zx))\mu )\to (\forall (m:\mathbb{N}),(((\int x,\mathrm{Real}.\mathrm{sqrt}(Zx)d\mu )\le (47/48:\mathbb{R}{)}^m)\to (\forall (a:\mathbb{R}),((0<a)\to (\mu .\mathrm{real}\{x|a\le Zx\}\le (\mathrm{Real}.\mathrm{sqrt}a{)}^{-1}\cdot (47/48:\mathbb{R}{)}^m)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.fractional_markov (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated fractional markov relation for the finite twin-pair calculation.

Theorem 1.48 (eventual tail bound).

$$\forall (a:\mathbb{R}),(\forall (b:\mathbb{R}),((0<a)\to ((0<b)\to (\exists m:\mathbb{N},3\le m\wedge (\mathrm{Real}.\mathrm{sqrt}a{)}^{-1}\cdot (47/48:\mathbb{R}{)}^m<b))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.eventual_tail_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated eventual tail bound relation for the finite twin-pair calculation.

Theorem 1.49 (normalized periodic shift).

$$\forall (f:\mathbb{R}\to \mathbb{R}),((\mathrm{Function}.\mathrm{Periodic}f(2\cdot \mathrm{Real}.\mathrm{pi}))\to (\forall (d:\mathbb{R}),((\int x,f(x+d)d(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))=\int x,fxd(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.normalized_periodic_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated normalized periodic shift relation for the finite twin-pair calculation.

Theorem 1.50 (conditional fractional moment).

$$\forall (Y:\mathrm{Type}),([\mathrm{MeasurableSpace}Y]\to (\forall (\nu :\mathrm{Measure}Y),([\mathrm{IsProbabilityMeasure}\nu ]\to (\forall (m:\mathbb{N}),(\forall (Z:(\mathrm{Fin}m\to (\mathbb{R}\times \mathbb{R}))\times Y\to \mathbb{R}),((\forall w,0\le Zw)\to ((\forall x,\mathrm{Integrable}(\mathrm{fun}y\mapsto Z(x,y))\nu \wedge \mathrm{Integrable}(\mathrm{fun}y\mapsto \mathrm{Real}.\mathrm{sqrt}(Z(x,y)))\nu )\to ((\mathrm{Integrable}(\mathrm{fun}w\mapsto \mathrm{Real}.\mathrm{sqrt}(Zw))((\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}m\mapsto \mathrm{pairAngle}).\mathrm{prod}\nu ))\to ((\forall x,(\int y,Z(x,y)d\nu )=\prod i,(1+\mathrm{pairCos}(xi)))\to ((\int w,\mathrm{Real}.\mathrm{sqrt}(Zw)d((\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}m\mapsto \mathrm{pairAngle}).\mathrm{prod}\nu ))\le (47/48:\mathbb{R}{)}^m))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.conditional_fractional_moment (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated conditional fractional moment relation for the finite twin-pair calculation.

Theorem 1.51 (pi periodic shift).

$$\forall (n:\mathbb{N}),(\forall (f:(\mathrm{Fin}n\to \mathbb{R})\to \mathbb{R}),((\mathrm{Continuous}f)\to (\forall (C:\mathbb{R}),((\forall x,\Vert fx\Vert \le C)\to ((\forall xi,\mathrm{Function}.\mathrm{Periodic}(\mathrm{fun}t\mapsto f(\mathrm{Function}.\mathrm{update}xit))(2\cdot \mathrm{Real}.\mathrm{pi}))\to (\forall (d:\mathrm{Fin}n\to \mathbb{R}),((\int x,f(\mathrm{fun}i\mapsto xi+di)d\mathrm{Measure}.\mathrm{pi}(\mathrm{fun}\cdot \mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))=\int x,fxd\mathrm{Measure}.\mathrm{pi}(\mathrm{fun}\cdot \mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pi_periodic_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

A bounded continuous function that is periodic in each coordinate has the same normalized product-angle integral after any fixed coordinate shift. The proof integrates one coordinate at a time.

Theorem 1.52 (sign product).

$$\forall (b:\mathrm{Bool}),(\forall (c:\mathrm{Bool}),(\mathrm{Int}.\mathrm{negOnePow}((b.\mathrm{toNat}):\mathbb{Z})\times \mathrm{Int}.\mathrm{negOnePow}((c.\mathrm{toNat}):\mathbb{Z})=\mathrm{Int}.\mathrm{negOnePow}(((\mathrm{Bool}.\mathrm{xor}bc).\mathrm{toNat}):\mathbb{Z})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.sign_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated sign product relation for the finite twin-pair calculation.

Definition 1.53 (twinPhase).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to (\mathrm{Fin}4\to \mathrm{Bool}))\to \mathrm{Bool}),(\forall (x:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool}),(\forall (y:(\mathrm{Fin}m\to (\mathrm{Fin}4\to \mathrm{Bool}))),(\mathrm{twinPhase}m\mathrm{qC}xy=\mathrm{Int}.\mathrm{negOnePow}(((\mathrm{qC}y).\mathrm{toNat}):\mathbb{Z})\cdot \prod i,\mathrm{Int}.\mathrm{negOnePow}(((\mathrm{Bool}.\mathrm{and}(\mathrm{Bool}.\mathrm{xor}(xi).1(xi).2)(\mathrm{List}.\mathrm{foldl}\mathrm{Bool}.\mathrm{xor}((yi)0)[((yi)1),((yi)2),((yi)3)])).\mathrm{toNat}):\mathbb{Z})))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twinPhase (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines twinPhase. The three-element List.foldl starts with the first bit and applies Bool.xor to the remaining bits in order.

Definition 1.54 (twinAmplitude).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to (\mathrm{Fin}4\to \mathrm{Bool}))\to \mathrm{Bool}),(\forall (\mathrm{xy}:(\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool})\times (\mathrm{Fin}m\to (\mathrm{Fin}4\to \mathrm{Bool}))),(\mathrm{twinAmplitude}m\mathrm{qC}\mathrm{xy}=(({\left((2:\mathbb{R}{)}^{-1}\right)}^{3\cdot m}:\mathbb{R}):\mathbb{C})\cdot (\mathrm{twinPhase}m\mathrm{qC}\mathrm{xy}.1\mathrm{xy}.2:\mathbb{C}))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twinAmplitude (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines twinAmplitude.

Theorem 1.55 (twin density tensor).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to (\mathrm{Fin}4\to \mathrm{Bool}))\to \mathrm{Bool}),(\forall (x:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool}),(\forall (x^{\prime }:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool}),(\mathrm{partialTraceRight}(\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{twinAmplitude}m\mathrm{qC})(\mathrm{star}(\mathrm{twinAmplitude}m\mathrm{qC})))x{x}^{\prime }=\prod i,\mathrm{if}(\mathrm{Bool}.\mathrm{xor}(xi).1(xi).2)=(\mathrm{Bool}.\mathrm{xor}(x^{\prime }i).1(x^{\prime }i).2)\mathrm{then}(1/4:\mathbb{C})\mathrm{else}0))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twin_density_tensor (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complement phase cancels in the Gram sum. The retained density matrix is the exact product of the four-dimensional pair matrices (I4 + X tensor X)/4. The variable qC is a function of the entire complementary bit configuration, so its type is (Fin m -> Fin 4 -> Bool) -> Bool.

Lemma 1.56 (effect entry).

$$\forall (\alpha :\mathbb{R}),(\forall (r:\mathrm{Bool}),(\forall (r^{\prime }:\mathrm{Bool}),(\mathrm{effect}\alpha r{r}^{\prime }=\mathrm{if}r=r^{\prime }\mathrm{then}1/2\mathrm{else}((\mathrm{Real}.\cos \alpha :\mathbb{C})+(\mathrm{if}r\mathrm{then}-1\mathrm{else}1)\cdot \mathrm{Complex}.I\cdot (\mathrm{Real}.\sin \alpha :\mathbb{C}))/2)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect_entry (✓ std3). ∎

Source. Repository-derived.

Commentary.

The gate-row projector has the displayed trigonometric entries.

Definition 1.57 (effect).

$$\forall (\alpha :\mathbb{R}),\mathrm{effect}\alpha =(\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{fun}r\mapsto (\mathrm{star}((\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1(\alpha ))0(\mathrm{if}(r)\mathrm{then}1\mathrm{else}0))))(\mathrm{star}(\mathrm{fun}r\mapsto (\mathrm{star}((\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1(\alpha ))0(\mathrm{if}(r)\mathrm{then}1\mathrm{else}0))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines effect.

Lemma 1.58 (pair density entry).

$$\forall (x:\mathrm{Bool}\times \mathrm{Bool}),(\forall (x^{\prime }:\mathrm{Bool}\times \mathrm{Bool}),(\mathrm{pairDensity}x{x}^{\prime }=\mathrm{if}(\mathrm{Bool}.\mathrm{xor}x.1x.2)=(\mathrm{Bool}.\mathrm{xor}{x}^{\prime }.1x^{\prime }.2)\mathrm{then}1/4\mathrm{else}0))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pair_density_entry (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two-qubit density matrix retains exactly equal parity indices.

Definition 1.59 (pairDensity).

$$\mathrm{pairDensity}=(1/4:\mathbb{C})\cdot ((1:\mathrm{Matrix}(\mathrm{Bool}\times \mathrm{Bool})(\mathrm{Bool}\times \mathrm{Bool})\mathbb{C})+((\mathrm{tensorOp}(\mathrm{fun}(\cdot :(\mathrm{Fin}2))\mapsto \mathrm{qubitX})).\mathrm{submatrix}(\mathrm{fun}(x:(\mathrm{Bool}\times \mathrm{Bool}))\mapsto ![(\mathrm{if}(x.1)\mathrm{then}1\mathrm{else}0),(\mathrm{if}(x.2)\mathrm{then}1\mathrm{else}0)])(\mathrm{fun}(x:(\mathrm{Bool}\times \mathrm{Bool}))\mapsto ![(\mathrm{if}(x.1)\mathrm{then}1\mathrm{else}0),(\mathrm{if}(x.2)\mathrm{then}1\mathrm{else}0)])))$$

Formalization. D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairDensity (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pairDensity.

Theorem 1.60 (measurement tensor).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{alpha}:\mathrm{Fin}m\to \mathbb{R}),(\forall (\mathrm{beta}:\mathrm{Fin}m\to \mathbb{R}),((\sum x:(\mathrm{Fin}m\to (\mathrm{Bool}\times \mathrm{Bool})),\sum x^{\prime }:(\mathrm{Fin}m\to (\mathrm{Bool}\times \mathrm{Bool})),\prod i,\mathrm{pairDensity}(xi)(x^{\prime }i)\cdot \mathrm{effect}(\mathrm{alpha}i)(xi).1(x^{\prime }i).1\cdot \mathrm{effect}(\mathrm{beta}i)(xi).2(x^{\prime }i).2)=(\prod i,(((1+\mathrm{Real}.\cos (\mathrm{alpha}i)\cdot \mathrm{Real}.\cos (\mathrm{beta}i))/4:\mathbb{R}):\mathbb{C})))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.measurement_tensor (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the finite product measurement tensor used by the twin marginal calculation.

Theorem 1.61 (effect integrable).

$$\forall (r:\mathrm{Bool}),(\forall (r^{\prime }:\mathrm{Bool}),(\mathrm{Integrable}(\mathrm{fun}\mathrm{alpha}\mapsto \mathrm{effect}\mathrm{alpha}r{r}^{\prime })(\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The single-qubit effect is integrable under the normalized angle measure.

Theorem 1.62 (complementary effect mean).

$$\forall (k:\mathbb{N}),(\forall (z:\mathrm{Fin}k\to \mathrm{Bool}),(\forall (z^{\prime }:\mathrm{Fin}k\to \mathrm{Bool}),((\int \mathrm{alpha},(\prod i,(\mathrm{effect}(\mathrm{alpha}i)(zi)(z^{\prime }i)))d(\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}k\mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))=(\prod i,(\mathrm{if}(zi=z^{\prime }i)\mathrm{then}(1/2:\mathbb{C})\mathrm{else}0)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.complementary_effect_mean (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product angle integral of complementary single-qubit effects factors into the corresponding diagonal means.

References

• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.F4
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.H
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.HZ
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.LocalMatching
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_cos_mean
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_integrable_of_continuous
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.angle_integral_eq
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.blockEquiv
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.blockEquiv_val
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.block_encode
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.boundaryDegree
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.circuit
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.complementary_effect_mean
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.conditional_fractional_moment
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.connector
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.connectorFlag
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_next_iff
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_next_val
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.cyclic_prev_iff
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj_hardware
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeAdj_symm
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.edgeDegree
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect_entry
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.effect_integrable
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.encoded_neighbours_card
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.eventual_tail_bound
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.factor_block_twins
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.factor_complement_matching
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.fractional_markov
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardwareAdj
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardwareEdges
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_adj_encoded
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_adj_encoded_cycle
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_degree_five
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_incident_card
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.hardware_internal_vertex
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.joint
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localDegree
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localEdges
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localMatchingFlags
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.localNeighbours
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.matching_neighbour_unique
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.measurement_tensor
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.normalized_periodic_shift
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.orderedEdge_hardware
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.outputProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairAngle
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairCos
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pairDensity
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pair_density_entry
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.pi_periodic_shift
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.randomLayer
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.sign_product
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.subset_degree_local
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.subset_incident_card
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.tailProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twinAmplitude
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twinPhase
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.twin_density_tensor
• Truth anchor: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors.uniformAngles
• Dependency: D5/S3/Quantum/Entanglement/PrecessionSpinOneSeparableBound
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerLocalInequivalence
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/QuantumBounds/MerminMeasurementDependence/Model