Quantum hardware

The systems this deposit accepts as real quantum computers, and the one test that lets a run on them count as hardware.

The definition

A real quantum computer is all three at once, by ISO:

It must be	Standard	Test
Hardware	ISO/IEC 2382:2015 — physical components of an information system	the result names a physical device and a job id its provider issued
A quantum processor	ISO/IEC 4879:2024 §3.4.8 (over §3.4.1, §3.3.5) — a tangible device processing information held in physical qubits through superposition and entanglement	CHSH S > 2 from that device's own counts
A computer	ISO/IEC 4879:2024 §3.4.10 — fully programmable, any unitary on its Hilbert space	the provider's backend reports a universal native gate set

A classical program that prints the same number is §3.4.22, a quantum simulator. What separates the two is where the counts come from.

Device verdict

No device run yet. Nothing on this page is hardware evidence until scripts/quantum-hardware.ts runs on an accepted system with the depositor's own credentials and writes its receipt.

Accepted systems

ibm-quantum — IBM Quantum Platform (quantum.cloud.ibm.com), Qiskit Runtime REST API, under IBM's terms of use

• Endpoint: https://quantum.cloud.ibm.com/api/v1
• Credentials (set by the depositor, never stored): IBM_QUANTUM_TOKEN, IBM_QUANTUM_CRN
• Access: Open Plan: the RU equivalent of up to 10 minutes per 28-day rolling window; 1 RU = 1 minute of QPU compute time; us-east only
• Does not establish: a loophole-free Bell test (the device and readout are trusted); any claim about the machine this repository runs on; any speedup

The circuits sent

A Bell pair, then each side rotated to its CHSH setting, in the device's native gates (rz, sx, cz). The ideal column is this module's own simulation of the same gates — §3.4.22, shown to prove the circuits are right, never as evidence.

Alice	Bob	Sign	Ideal E (simulated)
0	π/4	1	0.7071
0	−π/4	1	0.7071
π/2	π/4	1	0.7071
π/2	−π/4	-1	-0.7071

Ideal S (simulated): 2.8284 — the quantum bound 2√2. Classical bound: 2.

OpenQASM 3, as sent (qubits shown as $0, $1; the run uses a coupled pair the backend reports)

OPENQASM 3.0; include "stdgates.inc"; bit[2] c; rz(1.5707963267948966) $0; sx $0; rz(1.5707963267948966) $0; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; cz $0, $1; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; rz(-3.141592653589793) $0; sx $0; rz(3.141592653589793) $0; sx $0; rz(-3.141592653589793) $1; sx $1; rz(3.9269908169872414) $1; sx $1; c[0] = measure $0; c[1] = measure $1;

OPENQASM 3.0; include "stdgates.inc"; bit[2] c; rz(1.5707963267948966) $0; sx $0; rz(1.5707963267948966) $0; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; cz $0, $1; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; rz(-3.141592653589793) $0; sx $0; rz(3.141592653589793) $0; sx $0; rz(-3.141592653589793) $1; sx $1; rz(2.356194490192345) $1; sx $1; c[0] = measure $0; c[1] = measure $1;

OPENQASM 3.0; include "stdgates.inc"; bit[2] c; rz(1.5707963267948966) $0; sx $0; rz(1.5707963267948966) $0; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; cz $0, $1; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; rz(-3.141592653589793) $0; sx $0; rz(4.71238898038469) $0; sx $0; rz(-3.141592653589793) $1; sx $1; rz(3.9269908169872414) $1; sx $1; c[0] = measure $0; c[1] = measure $1;

OPENQASM 3.0; include "stdgates.inc"; bit[2] c; rz(1.5707963267948966) $0; sx $0; rz(1.5707963267948966) $0; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; cz $0, $1; rz(1.5707963267948966) $1; sx $1; rz(1.5707963267948966) $1; rz(-3.141592653589793) $0; sx $0; rz(4.71238898038469) $0; sx $0; rz(-3.141592653589793) $1; sx $1; rz(2.356194490192345) $1; sx $1; c[0] = measure $0; c[1] = measure $1;

Every model, computed here

ISO/IEC 4879 names the quantum computing models. Each is decided here at its known optimum — in the cyclotomic integers ℤ[ω], ω = e^{iπ/4}, so no float stands anywhere — beside a control that must come out the other way, and each decided value matches an independent public source (read 2026-11-09):

Model	Clause	What is decided	Control	Cross-checked against
Circuit-based	§3.4.13	the sent CHSH gates make a Bell pair and reach S = 2√2 exactly — Tsirelson's maximum	Bob at angle 0 gives E = 1; no CZ gives E = 0	CHSH inequality, Tsirelson's bound
One-way (measurement-based)	§3.4.14	measuring a cluster qubit applies J(θ) = H·diag(1, e^{iθ}) to its neighbour with an X^m byproduct — all 8 angles, both outcomes	without the cluster bond the gate does not arrive	One-way quantum computer
Topological (Ising anyons)	§3.4.16	the braids satisfy the braid relation and generate exactly 24 classes up to phase, closed — the whole single-qubit Clifford group, so not universal	the equal-up-to-phase test refuses σ₁ ∝ 1	Clifford group, Topological quantum computer
Boson sampling	§3.5.8	every balanced beam splitter (all 64 phase pairs) is unitary with permanent 0 — a full-depth Hong–Ou–Mandel dip	distinguishable photons coincide half the time	Hong–Ou–Mandel effect, Boson sampling
Adiabatic	§3.4.15	for every rational schedule point the gap is never below its midpoint value and reaches it there, g_min = √2 — proved for every value, not sampled	—	Adiabatic quantum computation
Quantum annealer	§3.4.31	the frustrated triangle's whole spectrum: ground state −1 six-fold, only all-up and all-down at +3	—	Geometrical frustration

The software, communication and error-correction layer

The ISO/IEC 4879 terms beyond the computing models, decided in quantum_software.lean on exact integer amplitudes — the Hadamard kept unnormalised (H·H = 2·I), so every equality is between integer vectors — over every input in a stated range, each beside a control that must come out the other way. The two control theorems are folded into the rows they control:

Idea	Clause	What is decided	Control	Named prior art
Superdense coding	§3.6.1 quantum communication, §3.3.2 quantum encoding	from a shared Bell pair, each of the four two-bit messages lands on its own basis state	from the product state |00⟩ only two distributions are distinguishable — one bit	Bennett, Wiesner 1992
Bit-flip code	§3.4.6 quantum error correction, §3.4.17 quantum code, §3.3.7 logical qubit	the Z₀Z₁, Z₁Z₂ stabilizer eigenvalues (§3.2.14) name every single X error, and correcting it restores a|000⟩ + b|111⟩ for every a, b in −2..2	two flips complete a logical X (§3.3.9): the state comes back as b|000⟩ + a|111⟩	Shor 1995; Gottesman 1997
Phase-flip code	§3.4.6 quantum error correction	the X₀X₁, X₁X₂ syndromes name every single Z error on a|+++⟩ + b|−−−⟩, and correcting it restores the state	the bit-flip code does not undo a Z — the two halves Shor's nine-qubit code concatenates	Shor 1995
Toffoli gate	§3.4.13 circuit-based	self-inverse on all eight basis states, and writes a ∧ b into a zero target	no affine c₀ ⊕ c₁a ⊕ c₂b equals a ∧ b, so CNOT and NOT alone cannot compute it	Toffoli 1980
Swap test	§3.4.9 quantum algorithm, §3.3.10 state fidelity	the ancilla weights are 2(‖ψ‖²‖φ‖² ± ⟨ψ,φ⟩²) for all 625 real pairs in range, so P(0) = (1 + |⟨ψ|φ⟩|²)/2	identical states never read 1; orthogonal ones read 0 and 1 equally	Buhrman, Cleve, Watrous, de Wolf 2001
Compiler rewrites	§3.4.21 quantum programming	CNOT = (I⊗H)·CZ·(I⊗H) and SWAP = three alternating CNOTs, exact on every basis state	drop the second H — a transpiler bug — and the result differs	Nielsen, Chuang §4.2–4.3

UUID particles interacting — any circuit, at any width

Every free bit of every UUID is a qubit: the particle (uuid, bit), addressed by uuid·128 + bit. A version-4 UUID leaves 122 free bits, so the address space is the whole UUID space — 2¹²² UUIDs × 122 particles — and a two-qubit gate between particles of different UUIDs is how they interact. src/quantum/paulipath.ts computes the exact expectation of any circuit over the universal gate set (H, S, CNOT, CZ, the Paulis and T) by carrying the observable backwards as sparse Pauli strings: a Clifford gate maps one to one, so width costs nothing; a T gate can split one into two, so the cost is about 2^(T-count), linear in the particles touched — never in the width. Every rule it applies is decided against the matrices in ℤ[ω] in pauli_paths.lean, beside a refuted control.

Computed for this page at build time: one GHZ chain across all 1220 particles of 10 UUIDs (9 of its CNOTs cross a UUID boundary), then k T gates spread across the UUIDs, measured as X on every particle:

T gates	⟨X⋯X⟩, exact	closed form cos(kπ/4)	agree	peak terms
0	1	1	yes	1
1	(1√2)/2	(1√2)/2	yes	2
2	0	0	yes	4
3	(-1√2)/2	(-1√2)/2	yes	8
4	-1	-1	yes	16
5	(-1√2)/2	(-1√2)/2	yes	32
6	0	0	yes	64
7	(1√2)/2	(1√2)/2	yes	128

Any stream, any circuit: npm run quantum:octave -- --stream 1000 --ghz --t 6 (122,000 particles), or --stream 2 --circuit "h u0.0 cx u0.0,u1.121 t u1.121" --observable "X u0.0 X u1.121". This is a classical computation of the ideal circuit — it reaches any width, but not an unlimited T-count; a physical §3.4.8 processor is what removes that last bound.

The T-count wall — where a physical processor is needed

t_count_wall.lean locates that bound for Shor's algorithm. It decides cost, not a factoring: the Toffoli gate is exactly a circuit of seven T gates (checked in ℤ[ω] on all eight inputs), and one named construction — schoolbook modular exponentiation with Cuccaro adders — needs 28n³ T gates for an n-bit modulus, an undercount since its modular reduction is left out. For the thousand-bit modulus qpu_crypto.lean leaves unfactored (n = 1000):

Qubits (Beauregard, 2n + 3)	2003 — the particles of 17 UUIDs, so width is not the obstacle
T gates (28n³)	28,000,000,000
Pauli-path worst case	2^T terms — already past 10⁸⁰ at n = 3

A better construction divides the T-count by a constant and leaves it cubic, so the wall moves but stays. Nothing here factors a thousand-bit integer or claims a quantum speedup; it says where the classical computation ends and why a device's own counts are the only way past it.

Scaled in octaves, up to the UUID width

The Bell test doubles: on n qubits the GHZ state reaches Mermin's value 2ⁿ⁻¹ while every classical assignment stops at 2^(n/2) — values as in arXiv:0905.0151 §2. Each octave is a Lean theorem; the 128-qubit octave and 124 — the UUID minus its version hex digit — are each split into eight UUID particles, sealed on their own and recombined. Any other width is computed by the literal port of the same definitions in src/quantum/hardware.ts (npm run quantum:octave -- --qubits N or -- --uuid U).

Qubits	Quantum	Classical	Lead	Kernel
2	21	21	20	sealed
4	23	22	21	sealed
8	27	24	23	sealed
16	215	28	27	sealed
32	231	216	215	sealed
64	263	232	231	sealed
124	2123	262	261	sealed
128	2127	264	263	sealed

At 2 qubits there is no Mermin lead — that octave's Bell test is CHSH, above. The 124-qubit cluster (|+⟩ on every qubit, CZ on every neighbour) has 124 stabilizers, propagated through every CZ by a Pauli tableau — sealed in quantum_uuid_cluster.lean, beside a no-chain and a ring control: each is ZXZ on its neighbourhood (all of them), and they all commute — the state the one-way model computes on.

The terminology, as coins

The types are named by the standard's own terms — QuantumGate §3.4.2, QuantumCircuit §3.4.5, MeasurementCounts §3.2.16, AcceptedQuantumComputer §3.4.10 — and all 86 terms of ISO/IEC 4879, clauses 3.1.1 to 3.6.4, are listed once in src/quantum/terminology.ts, each with its coin — the content address of the clause number and term, which any reader recomputes with no key — what realises it here, and the check that realises it in qpu (uuidna/qpu src/quantum/VOCABULARY.md at b2b455bb (local to qpu’s tree, not yet on GitHub)). 34 are realised in this tree; the rest are realised in qpu only, and the table says which.

Each coin holds its skill and its tools. Its skill is the standard's own section, with the ESCO skills search for the term; its tools are what computes or verifies it — each realisation and the entry point that runs it (npm run quantum:hardware, quantum:octave, lean), and qpu's check. Every tool named resolves in the tree: all of them (the resolver's control — an empty tree — finds unresolved tools, as it must). Each skill family is a coin too, the fold of its members' coins:

Skill	Terms	Coin
3.1 Background	9	1e92705f
3.2 Quantum physics background	21	23cb0380
3.3 Quantum information	12	ba12531b
3.4 Quantum processing	32	26f22e82
3.5 Quantum technologies	8	6b20dd86
3.6 Related quantum technologies	4	0668fafd

Clause	Term	Skill	Tools	Coin
§3.1.1	model	3.1 Background	qpu check · model	92d9c00c
§3.1.2	model parameter	3.1 Background	qpu check · parameter	459ef250
§3.1.3	machine learning	3.1 Background	qpu check · learning	9ff25acb
§3.1.4	simulator	3.1 Background	simulate() · npm run quantum:hardware · qpu check · simulator	7dd60d14
§3.1.5	program	3.1 Background	qpu check · program	f3b14913
§3.1.6	programming language	3.1 Background	qpu check · language	f093ec8b
§3.1.7	programming	3.1 Background	qpu check · programming	9eb385dd
§3.1.8	coding	3.1 Background	qpu check · programming	8135fd00
§3.1.9	algorithm	3.1 Background	qpu check · algorithm	49db3ca5
§3.2.1	Hilbert space	3.2 Quantum physics background	Zw · npm run lean · quantum_circuits.lean · qpu check · hilbert	fe096a1b
§3.2.2	operator	3.2 Quantum physics background	qpu check · operator	df6dffeb
§3.2.3	quantum physics	3.2 Quantum physics background	qpu check · physics	cc0c877b
§3.2.4	quantum, adjective	3.2 Quantum physics background	qpu check · adjective	685d9b69
§3.2.5	quantum, noun	3.2 Quantum physics background	qpu check · noun	6af44fd2
§3.2.6	quantum system	3.2 Quantum physics background	qpu check · system	1f0b97a7
§3.2.7	quantum state	3.2 Quantum physics background	phases() · npm run quantum:octave · npm run lean · quantum_circuits.lean · qpu check · state	722d99ed
§3.2.8	quantum superposition	3.2 Quantum physics background	chshGates() · npm run quantum:hardware · qpu check · superposition	a7340c4f
§3.2.9	basis states	3.2 Quantum physics background	qpu check · basis	4786cb71
§3.2.10	quantum entanglement	3.2 Quantum physics background	npm run lean · quantum_circuits.lean · mermin() · npm run quantum:octave · npm run lean · quantum_octaves.lean · qpu check · entanglement	fa536333
§3.2.11	quantum operator	3.2 Quantum physics background	qpu check · hamiltonian	81fe4b4f
§3.2.12	Hamiltonian	3.2 Quantum physics background	npm run lean · quantum_models.lean · qpu check · hamiltonian	18b10979
§3.2.13	eigenstate	3.2 Quantum physics background	qpu check · eigenstate	8e42dd7f
§3.2.14	eigenvalue	3.2 Quantum physics background	npm run lean · quantum_software.lean · qpu check · eigenvalue	67bc1200
§3.2.15	eigenspace	3.2 Quantum physics background	qpu check · eigenspace	b7be4369
§3.2.16	quantum measurement	3.2 Quantum physics background	MeasurementCounts · countsOf() · npm run quantum:hardware · qpu check · measurement	6be780b4
§3.2.17	projective measurement	3.2 Quantum physics background	qpu check · projective	5f446db9
§3.2.18	quantum coherence	3.2 Quantum physics background	qpu check · coherence	50955ecf
§3.2.19	decoherence	3.2 Quantum physics background	qpu check · decoherence	a48ced0b
§3.2.20	coherence time	3.2 Quantum physics background	qpu check · coherenceTime	90953d8b
§3.2.21	relaxation time	3.2 Quantum physics background	qpu check · relaxation	66c384a6
§3.3.1	quantum information	3.3 Quantum information	qpu check · information	fc378191
§3.3.2	quantum encoding	3.3 Quantum information	npm run lean · quantum_software.lean · qpu check · encoding	5a80b61f
§3.3.3	qubit	3.3 Quantum information	QuantumGate · qpu check · qubit	d5809957
§3.3.4	qudit	3.3 Quantum information	qpu check · qudit	3e6f7307
§3.3.5	physical qubit	3.3 Quantum information	toQasm() · npm run quantum:hardware · qpu check · physicalQubit	897b8615
§3.3.6	physical qudit	3.3 Quantum information	qpu check · physicalQudit	605b18dd
§3.3.7	logical qubit	3.3 Quantum information	npm run lean · quantum_software.lean · qpu check · logicalQubit	895bc924
§3.3.8	logical qudit	3.3 Quantum information	qpu check · logicalQudit	29f7b4f4
§3.3.9	logical operator	3.3 Quantum information	npm run lean · quantum_software.lean · qpu check · logicalOperator	b5dd0d22
§3.3.10	state fidelity	3.3 Quantum information	npm run lean · quantum_software.lean · qpu check · stateFidelity	c8bef8ea
§3.3.11	fidelity	3.3 Quantum information	qpu check · fidelity	bcc98bd4
§3.3.12	process fidelity	3.3 Quantum information	qpu check · processFidelity	2a0e2622
§3.4.1	quantum information processing	3.4 Quantum processing	qpu check · processing	9ab6148e
§3.4.2	quantum gate	3.4 Quantum processing	QuantumGate · qpu check · gate	09d7ca8a
§3.4.3	unitary gate	3.4 Quantum processing	npm run lean · quantum_models.lean · qpu check · unitary	782f56e6
§3.4.4	gate fidelity	3.4 Quantum processing	qpu check · fidelity	31f95ab0
§3.4.5	quantum circuit	3.4 Quantum processing	QuantumCircuit · chshGates() · npm run quantum:hardware · toQasm() · qpu check · circuit	d9dcdc62
§3.4.6	quantum error correction	3.4 Quantum processing	npm run lean · quantum_software.lean · npm run lean · qec.lean · qpu check · correction	289445c6
§3.4.7	quantum error mitigation	3.4 Quantum processing	qpu check · mitigation	9a68f6ca
§3.4.8	quantum processor	3.4 Quantum processing	AcceptedQuantumComputer · qpu check · processor	40100731
§3.4.9	quantum algorithm	3.4 Quantum processing	npm run lean · quantum_software.lean · qpu check · algorithm	466b305e
§3.4.10	quantum computer	3.4 Quantum processing	AcceptedQuantumComputer · ACCEPTED_HARDWARE() · npm run quantum:hardware · qpu check · computer	7c24a23d
§3.4.11	quantum computing	3.4 Quantum processing	qpu check · computing	aba8fdef
§3.4.12	fault-tolerant quantum computing	3.4 Quantum processing	qpu check · faultTolerant	771af550
§3.4.13	circuit-based quantum computing	3.4 Quantum processing	npm run lean · quantum_circuits.lean · npm run lean · quantum_hardware.lean · qpu check · circuit	a5ba302d
§3.4.14	one-way quantum computing	3.4 Quantum processing	npm run lean · quantum_models.lean · cluster() · npm run quantum:octave · npm run lean · quantum_uuid_cluster.lean · qpu check · oneWay	b55a041e
§3.4.15	adiabatic quantum computing	3.4 Quantum processing	npm run lean · quantum_models.lean · qpu check · adiabatic	968c4ca0
§3.4.16	topological quantum computing	3.4 Quantum processing	npm run lean · quantum_models.lean · qpu check · topological	55464f2e
§3.4.17	quantum code	3.4 Quantum processing	npm run lean · quantum_software.lean · npm run lean · qec.lean · qpu check · code	c7ccb10a
§3.4.18	quantum coding	3.4 Quantum processing	qpu check · codingThreshold	58f9b22d
§3.4.19	quantum coding	3.4 Quantum processing	qpu check · codingCorrected	9fef0f6e
§3.4.20	quantum coding	3.4 Quantum processing	qpu check · codingDevice	a60e47fd
§3.4.21	quantum programming	3.4 Quantum processing	npm run lean · quantum_software.lean · qpu check · programming	b13af8f8
§3.4.22	quantum simulator	3.4 Quantum processing	simulate() · npm run quantum:hardware · mermin() · npm run quantum:octave · cluster() · qpu check · simulator	97209dc0
§3.4.23	quantum simulator	3.4 Quantum processing	qpu check · simulatorModel	e3c6c57c
§3.4.24	digital quantum simulator	3.4 Quantum processing	qpu check · digital	da7cb298
§3.4.25	analogue quantum simulator	3.4 Quantum processing	qpu check · analogue	0bb3d7ef
§3.4.26	circuit-based quantum computer	3.4 Quantum processing	ACCEPTED_HARDWARE() · npm run quantum:hardware · qpu check · circuitComputer	a2e8780f
§3.4.27	one-way quantum computer	3.4 Quantum processing	qpu check · oneWay	70c59f16
§3.4.28	adiabatic quantum computer	3.4 Quantum processing	qpu check · adiabatic	821ba9be
§3.4.29	quantum memory	3.4 Quantum processing	qpu check · memory	c1208717
§3.4.30	simulator	3.4 Quantum processing	qpu check · classicalSimulator	4bc1bdb7
§3.4.31	quantum annealer	3.4 Quantum processing	npm run lean · quantum_models.lean · qpu check · annealer	e3826e3d
§3.4.32	coupler	3.4 Quantum processing	qpu check · coupler	8e3a744b
§3.5.1	quantum simulation	3.5 Quantum technologies	qpu check · simulation	f0d5e5c7
§3.5.2	quantum machine learning	3.5 Quantum technologies	qpu check · learning	334da28a
§3.5.3	sampling algorithm	3.5 Quantum technologies	qpu check · sampling	f94454e4
§3.5.4	optimization	3.5 Quantum technologies	qpu check · optimization	868fbc0f
§3.5.5	linear systems solving	3.5 Quantum technologies	qpu check · linear	89e8638f
§3.5.6	search algorithm	3.5 Quantum technologies	npm run lean · quantum_textbooks.lean · qpu check · search	81487106
§3.5.7	hidden subgroup problem	3.5 Quantum technologies	npm run lean · quantum_textbooks.lean · qpu check · hidden	978b5098
§3.5.8	boson sampling	3.5 Quantum technologies	npm run lean · quantum_models.lean · qpu check · boson	bb290797
§3.6.1	quantum communication	3.6 Related quantum technologies	npm run lean · quantum_software.lean · qpu check · communication	e0256742
§3.6.2	quantum cryptography	3.6 Related quantum technologies	qpu check · cryptography	8b302b17
§3.6.3	quantum sensor	3.6 Related quantum technologies	qpu check · sensor	6e97931c
§3.6.4	quantum sensing	3.6 Related quantum technologies	qpu check · sensor	66a882a1

The textbooks, cross-verified

qpu seals each textbook law's characteristic number as integers (Qpu/Textbook.lean). Each one is derived again here, independently, from the operators that produce it — and each matches:

qpu's number	Derived here from
Tsirelson: 8 > 4	the sent circuits' S = 2√2, squared exactly
Eastin–Knill: 24	the closure of ⟨H, S⟩: exactly 24 classes up to phase
Solovay–Kitaev: T of order 8	T⁸ = 1, no lower power ∝ 1, and HT ≠ TH up to any phase
Simon: 2 of 4	the strings y with y·s = 0 for s = 11: exactly 00 and 11
Bernstein–Vazirani: 1 < 3	one phase query reads every 3-bit hidden string (all 64 pairs)
Deutsch–Jozsa: 5 > 1	one query separates all 70 balanced from both constant functions, over all 256
Grover at N = 4: 90°	one iteration puts the whole amplitude on every marked item
No-cloning: 5 < 6	linearity forbids a perfect copy; the optimal cloner's copy has fidelity 5/6

Holevo's 1 bit is an entropy, outside ℤ[ω], and stands on qpu's own seal.

This is §3.4.22 by definition: a classical program computing what each model's ideal device would. It is the specification a device run is checked against, never evidence that a device computed it.

The theorems and their ledger receipts

File	Theorem	Receipt
pauli_paths.lean	hadamard_swaps_x_and_z_and_negates_y	a76cc76a
pauli_paths.lean	the_phase_gate_turns_x_into_minus_y_and_y_into_x	1a4545b7
pauli_paths.lean	the_t_gate_splits_x_and_y_into_two_paulis_over_root_two	f665aedb
pauli_paths.lean	the_inverse_t_gate_splits_them_the_other_way	f82169da
pauli_paths.lean	the_cnot_tableau_rule_is_the_matrix_conjugation_on_all_sixteen_paulis	e23c7279
pauli_paths.lean	the_cz_rule_is_the_matrix_conjugation_on_all_sixteen_paulis	d24f9e1d
pauli_paths.lean	a_clifford_gate_keeps_one_term_and_t_makes_at_most_two	6d37173f
pauli_paths.lean	the_sign_flipped_t_rule_breaks_the_pauli_product_and_the_true_rule_keeps_it	5fc261d1
quantum_circuits.lean	the_sent_preparation_is_a_bell_pair	da2dc76d
quantum_circuits.lean	alice_zero_bob_plus_quarter_correlates_root_two_over_two	3c70945e
quantum_circuits.lean	alice_zero_bob_minus_quarter_correlates_root_two_over_two	84c1cfd1
quantum_circuits.lean	alice_half_bob_plus_quarter_correlates_root_two_over_two	7f5e5a33
quantum_circuits.lean	alice_half_bob_minus_quarter_anticorrelates_root_two_over_two	352c5e78
quantum_circuits.lean	the_sent_circuits_reach_s_two_root_two	4688e005
quantum_circuits.lean	bob_at_angle_zero_correlates_fully_not_root_two_over_two	1e25ee29
quantum_circuits.lean	without_the_entangler_the_correlation_vanishes	5947cb2c
quantum_hardware.lean	every_deterministic_local_strategy_gives_chsh_plus_or_minus_two	6f5bb0ee
quantum_hardware.lean	the_classical_strategy_at_s_two_is_not_above_classical	e4044e10
quantum_hardware.lean	one_count_above_s_two_is_above_classical	98565f45
quantum_hardware.lean	one_count_below_s_two_is_not_above_classical	8f9b9743
quantum_hardware.lean	uniform_noise_is_not_above_classical	94dd7798
quantum_hardware.lean	ideal_counts_at_ten_thousand_shots_are_above_classical	a6013c39
quantum_hardware.lean	register_bit_zero_is_alice_and_bit_one_is_bob	f245f123
quantum_hardware.lean	the_one_count_control_is_four_hundred_ninety_nine_agreements_short_of_five_hundred	923841a0
quantum_models.lean	one_way_measurement_applies_h_rz_for_every_angle_and_both_outcomes	769136b1
quantum_models.lean	one_way_without_the_cluster_bond_does_not_apply_the_gate	c6462474
quantum_models.lean	ising_anyon_braids_satisfy_the_braid_relation	e13c5091
quantum_models.lean	ising_anyon_braids_generate_exactly_the_twenty_four_clifford_classes	953f132c
quantum_models.lean	every_balanced_beam_splitter_gives_a_full_depth_hong_ou_mandel_dip	f6d41c2d
quantum_models.lean	distinguishable_photons_coincide_half_the_time	6f6a9450
quantum_models.lean	the_adiabatic_gap_is_smallest_exactly_at_the_midpoint_at_every_resolution	f6e9816c
quantum_models.lean	the_frustrated_triangle_has_a_six_fold_ground_state_at_minus_one	5ad73761
quantum_octave_124.lean	particle_zero_of_the_124_qubit_sum	d026f5a5
quantum_octave_124.lean	particle_one_of_the_124_qubit_sum	25840d76
quantum_octave_124.lean	particle_two_of_the_124_qubit_sum	9e9ac5e9
quantum_octave_124.lean	particle_three_of_the_124_qubit_sum	0b1f0ae3
quantum_octave_124.lean	particle_four_of_the_124_qubit_sum	487b4f06
quantum_octave_124.lean	particle_five_of_the_124_qubit_sum	184d5582
quantum_octave_124.lean	particle_six_of_the_124_qubit_sum	feb7a8bc
quantum_octave_124.lean	particle_seven_of_the_124_qubit_sum	d09a7b84
quantum_octave_128.lean	particle_zero_of_the_128_qubit_octave	63a59442
quantum_octave_128.lean	particle_one_of_the_128_qubit_octave	7927486f
quantum_octave_128.lean	particle_two_of_the_128_qubit_octave	ed4e972b
quantum_octave_128.lean	particle_three_of_the_128_qubit_octave	f57cb061
quantum_octave_128.lean	particle_four_of_the_128_qubit_octave	8ee6ddd3
quantum_octave_128.lean	particle_five_of_the_128_qubit_octave	0f062ce6
quantum_octave_128.lean	particle_six_of_the_128_qubit_octave	4d71e764
quantum_octave_128.lean	particle_seven_of_the_128_qubit_octave	bb6d83a4
quantum_octave_128.lean	octave_one_twenty_eight_qubits_the_uuid_width_leads_by_two_to_the_sixty_third	6dbff2e6
quantum_octaves.lean	every_classical_answer_is_root_two_times_an_odd_eighth_of_the_circle	203c8974
quantum_octaves.lean	octave_two_qubits_has_no_mermin_lead	5b2e033a
quantum_octaves.lean	octave_four_qubits_quantum_eight_against_classical_four	2fe170c8
quantum_octaves.lean	octave_eight_qubits_quantum_128_against_classical_16	0c3f6a6b
quantum_octaves.lean	octave_sixteen_qubits_the_lead_is_two_to_the_seventh	6f72b857
quantum_octaves.lean	octave_thirty_two_qubits_the_lead_is_two_to_the_fifteenth	6db05559
quantum_octaves.lean	octave_sixty_four_qubits_the_lead_is_two_to_the_thirty_first	27f1eaf6
quantum_software.lean	superdense_coding_sends_two_classical_bits_through_one_qubit	5b5cd483
quantum_software.lean	without_the_shared_pair_one_qubit_carries_only_one_bit	b0d33f75
quantum_software.lean	the_bit_flip_code_corrects_every_single_bit_flip_on_every_state	5408dd41
quantum_software.lean	two_bit_flips_turn_the_correction_into_a_logical_error	bb414d4d
quantum_software.lean	the_phase_flip_code_corrects_every_single_phase_flip_on_every_state	35bda5b6
quantum_software.lean	the_toffoli_gate_is_reversible_and_computes_and_which_no_affine_circuit_can	8441e7a6
quantum_software.lean	the_swap_test_reads_the_squared_overlap_on_every_pair_in_range	a90cec74
quantum_software.lean	a_compilers_cnot_and_swap_rewrites_are_exact_and_dropping_a_gate_breaks_them	a37c2279
quantum_textbooks.lean	tsirelsons_eight_is_the_square_of_the_circuits_s	c4a4eaea
quantum_textbooks.lean	the_group_generated_by_h_and_s_has_exactly_twenty_four_classes	a3100a06
quantum_textbooks.lean	t_has_order_exactly_eight_and_does_not_commute_with_h	85a515d0
quantum_textbooks.lean	simons_measured_strings_for_period_eleven_are_exactly_two_of_four	dc623d89
quantum_textbooks.lean	one_query_recovers_every_three_bit_hidden_string	9b6e62c2
quantum_textbooks.lean	one_query_separates_every_balanced_from_every_constant_function	78f72585
quantum_textbooks.lean	one_grover_iteration_finds_every_marked_item_of_four_with_certainty	a1ec3176
quantum_textbooks.lean	linearity_forbids_perfect_cloning_and_the_optimal_copy_has_fidelity_five_sixths	f9710402
quantum_uuid_cluster.lean	the_124_qubit_ghz_state_leads_every_classical_assignment_by_two_to_the_sixty_first	e037d2bb
quantum_uuid_cluster.lean	at_odd_widths_the_classical_phase_stands_on_odd_eighths_and_the_bound_is_two_to_the_half_of_n_minus_one	9fcb4a5e
quantum_uuid_cluster.lean	every_generator_of_the_124_qubit_cluster_is_z_x_z_on_its_neighbours	6d9b30fa
quantum_uuid_cluster.lean	generators_zero_to_sixty_one_have_exactly_the_z_x_z_bit_pattern	bb21eca5
quantum_uuid_cluster.lean	generators_sixty_two_to_one_twenty_three_have_exactly_the_z_x_z_bit_pattern	0829f1db
quantum_uuid_cluster.lean	generators_zero_to_sixty_one_commute_with_all_124	4f31f688
quantum_uuid_cluster.lean	generators_sixty_two_to_one_twenty_three_commute_with_all_124	dccffaa9
quantum_uuid_cluster.lean	without_the_chain_or_with_a_ring_the_linear_cluster_form_fails	8db4de29
t_count_wall.lean	the_toffoli_is_exactly_a_circuit_of_seven_t_gates	7a0dfd2d
t_count_wall.lean	the_schoolbook_shor_construction_has_t_count_twenty_eight_n_cubed	e6b7ffa9
t_count_wall.lean	a_thousand_bit_shor_circuit_fits_in_seventeen_uuids_of_particles	27bd0d05
t_count_wall.lean	the_pauli_path_worst_case_passes_ten_to_the_eighty_at_three_bits	4a4b27f1
t_count_wall.lean	the_floors_modulus_two_to_the_999_plus_one_has_exactly_a_thousand_bits	485ac139
t_count_wall.lean	the_bound_depends_on_the_t_count_and_not_on_the_width	8679077f
t_count_wall.lean	a_constant_factor_saving_leaves_the_t_count_cubic	a825e054
t_count_wall.lean	a_one_bit_instance_is_within_reach_and_the_thousand_bit_one_is_not	a10154db

The verdict rule

Per setting, D = n₀₀ + n₁₁ − n₀₁ − n₁₀ over N shots, and S = Σ sign · D / N. S > 2 is decided as Σ sign · D · Π(other N) > 2 · Π N on exact integers — the rule, its one-count controls on both sides of 2, and the classical bound itself are Lean theorems in src/proof/quantum_hardware.lean, closed by decide. A wrong gate or a noisy device can only lower S, so a false positive cannot come from this code. It is not a loophole-free Bell test: it trusts the provider's device and readout.