QECTOR Decoder v3 - Certified Proof Suite

Executable proof suite certifying qector-decoder-v3==1.0.0 against the normative QECTOR Decoder v3 Reference Manual v1.0.0 (DOI 10.5281/zenodo.21941046).

The implementation under test is the live wheel from PyPI. The specification is a pure-Python math layer that runs without the wheel. No MCP server, no plugin manifests, no Workbench app, no hardcoded machine paths.

---

Quick start

Prerequisites: Python 3.9+ and internet access to pypi.org.

python -m venv .venv

Windows (PowerShell):

.venv\Scripts\Activate.ps1

Windows (cmd):

.venv\Scripts\activate.bat

macOS / Linux:

source .venv/bin/activate

Hermetic one-shot (todo2 P2.1 / G10):

python -m venv .venv
# Windows: .venv\Scripts\Activate.ps1
# POSIX:   source .venv/bin/activate
python -m pip install --require-hashes -r requirements.lock
python -m pip install -r requirements-formal.txt   # Git pin for symproof
python qector_proof_suite.py
# POSIX:   CERT_STRICT=1 python preflight.py
# Windows: $env:CERT_STRICT='1'; python preflight.py
python -m pytest tests -q -m "not gpu"

Verify the public AIO zip (todo2 P0.4):

# POSIX:   sha256sum -c QECTOR-PROOF-SUITE-v1.2.1-AIO.zip.sha256
# Windows: Get-FileHash QECTOR-PROOF-SUITE-v1.2.1-AIO.zip -Algorithm SHA256

Quick unhashed install (not the certification path):

python -m pip install -r requirements.txt
python qector_proof_suite.py

That is the entire certified workflow. The process:

1. Runs the math-proofs layer (pure Python; no wheel required).
2. Runs v1.0 theorems T1-T16 against the live wheel.
3. Runs v1.1 claim classes T17-T26.
4. Runs coverage upgrades (Stim round-trip, large-distance surface, CSS negative control, streaming telescope, golden vectors, threads).
5. Writes hash-anchored JSON + .sha256 sidecars to proof_artifacts/.

Exit 0 only when every layer passes, every sidecar matches the on-disk bytes, every artifact validates against the structural schema, and the bundled manual SHA-256 matches. Otherwise the process exits non-zero.

---

Repository layout

Path	Purpose
qector_proof_suite.py	Thin CLI entrypoint
certification/	Banner, artifacts, environment, schema, wording lint, sidecars
math_proofs/	Pure-Python algebraic identities
theorems_v10/	T1-T16
claims_v11/	T17-T26 plus coverage upgrades
goldens/vectors.json	Frozen (H, s, c_expected_coset) vectors
schemas/	JSON Schema documents for published artifacts
QectorDecoder_v3_Reference_Manual_v1.0.0.pdf	Bundled reference manual
requirements.txt	Public PyPI pins
formal_verification/	SMT, provably, paranoid, sympy, Lean/Coq/Isabelle bridges
.github/workflows/ci.yml	CPU matrix + GPU release gate

---

CLI and environment

Flag / variable	Effect
python qector_proof_suite.py	Full certified run
python preflight.py	One-shot pre-flight check (deps, bridges, tests)
qector-preflight	Same, after pip install -e . (console script)
python -m formal_verification hashes --print	List the proof-assistant artifact SHA-256s to stdout (D1→D2 wire)
python -m formal_verification hashes --write	Update each proof_artifact bridge JSON + sidecar
qector-proof-hashes --print	Same as above, after pip install -e . (console script)
QECTOR_PROOF_OUTPUT_DIR	Artifact directory (relative or absolute)
QECTOR_PROOF_SEED	RNG seed for property-based tests (default 20260829)
QECTOR_MIN_FRACTION	SparseBlossom near-optimality floor (default 0.99)
QECTOR_SILENT=1	Suppress the wheel licence banner
QECTOR_ALLOW_MANUAL_DRIFT=1	Diagnostic only; do not use for certification
QECTOR_PROOF_HASHES_CLI_TESTS=1	Enable subprocess CLI tests in tests/test_proof_hashes.py
pytest -m "not gpu and not slow"	Selective run

MIN_FRACTION is 0.99 because every audited small code in this suite historically scored 1.0; the 1% slack covers degeneracy-induced weight ties, not a performance claim.

The proof_hashes subcommand walks the repo tree from its own file location (no hardcoded absolute paths), computes the SHA-256 of the Lean / Coq / Isabelle source files, and wires the result into proof_artifacts/lean4_mathlib_overview.json, proof_artifacts/coq_bridge.json, and proof_artifacts/isabelle_blossom_mapping.json. Compiled-artifact hashes (.olean, .vo, .thy.ML) are only recorded when those files actually exist; otherwise the record carries compiled_sha256: null and pending_compile: true — no fake hashes.

Dependencies

The full dependency policy is in requirements.txt (minimum pins) and requirements.lock (fully pinned with SHA-256 digests for reproducible certification). The split is:

Layer	Packages	Install command
Hard runtime	qector-decoder-v3, numpy, sympy, paranoid-scientist, stim, pytest	pip install -r requirements.txt
Optional formal	z3-solver, cvc5, provably, symproof	pip install -r requirements-formal.txt or pip install -e .[formal]
Developer / CI	nox	pip install nox

preflight.py checks every hard dep is installed at the pinned version, every optional dep is either installed or honestly reported as missing, every proof_artifact bridge has a real source SHA-256 + an honest pending_compile: true flag, every sidecar SHA-256 matches its file, and the proof-hash test suite passes.

---

Pytest markers

Marker	Meaning
gpu	CUDA / OpenCL bit-identity (host-skips without the device)
slow	Stim round-trip and d=5/d=7 surface sweeps
colour	ColourCodeDecoder DEM-string path

---

What the suite will not claim

The suite certifies only the contracts in Reference Manual Table 4.1: syndrome faithfulness H c = s, coset/logical partition, dual/tight-edge theory as stated, and the per-decoder contracts in §J. It never certifies LER, p_th, wall-clock/latency, or “universally faster / exact Sparse MWPM on every instance” (Reference Manual Table 4.1, ch. 20 / 22.5, §3.4 non-goals, §6.6). A banned-phrase lint (certification/wording.py, BANNED_NOTE_PHRASES + T7 sparse.*exact regex) fails the process if a test note ever contains those claims. GPU tests skip on CPU-only hosts; a CUDA CI job is required to be green before a freeze (QECTOR_REQUIRE_GPU=1 on a CUDA runner).

Per-decoder formal contracts (J section, todo J)

Every Reference Manual Table 4.1 backend has a formal DecoderContract defined in formal_verification/decoder_contracts.py. Each contract has a Python predicate and an optional Z3 SMT encoding; the registry is recorded in proof_artifacts/decoder_contracts.json. The SparseBlossomDecoder contract carries the T7-split text: faithful + near-optimal on tested families per §6.6; mwpm_exact=false until T7-exact has a compiled proof hash. The wording linter fails if "exact MWPM" is asserted for the Sparse backend without T7-exact.

Z3 / CVC5 cross-check (L section, todo L)

formal_verification/cross_check.py runs two independent SMT encoders (Z3, CVC5) on the same Hc = s claim; the cross-check is part of the formal verification layer and is reported in the master cert's formal_verification block as all_agree: true (or the failure mode is reported, not swallowed). An exhaustive weight-≤t sweep is also available for Steane / small codes.

Evidence index and attributions

• proof_artifacts/EVIDENCE_INDEX.md maps every formal claim to its proof object (Lean, Coq, Isabelle, Z3, CVC5, Python regression).
• ATTRIBUTIONS.md records the licence of every PyPI dependency, every proof-assistant toolchain (Lean + Mathlib, Coq, Isabelle + Graph Library), and the referenced but-not-vendored CoqQ / Veri-QEC / Lean-QEC / QECLean materials.

Public label: algebraically green · formally executable · research Props non-cited. Exit 0 is executable + SMT + packaging. Coq QectorCoq.vo and Lean QectorLean.olean (when present) back Theorems 1, 3, 8 only. T2 full ker\im, T5–T7 weighted dual, and Table 4.1 backends stay tested-only. Isabelle attic is not part of the cert. Canonical out-of-scope list: docs/OUT_OF_SCOPE.md.

Distance parameters ([[90,8,10]] etc.) live alongside the cert as a side-channel (manual Ch. 27.2, proof_artifacts/distance_certificates.json), never inside theorem notes. GPU/OpenCL bit-identity is “on tested configurations” only; Streaming/SlidingWindow is a simulation workflow, not hardware-control certification (Table 4.1). SparseBlossomDecoder is faithful + near-optimal on tested families per §6.6; exact MWPM (T7-exact) requires Thm 5–7 + Edmonds correspondence and is tracked as faithful=true, mwpm_exact=false until a compiled proof exists (see formal_verification/phases.py:t7_split_claims, proof Artifacts §6.6).

---

Certified evidence

proof_artifacts/ contains per-theorem JSON + sidecars, combined layer records, certified_master_proof.json, and claim_class_matrix.json. Every JSON embeds the identity block (DOI, ORCID, licence, author).

Verify a sidecar:

sha256sum -c proof_artifacts/certified_master_proof.json.sha256

Get-FileHash proof_artifacts\certified_master_proof.json -Algorithm SHA256

Bundled manual SHA-256 (bytes on disk, canonical Zenodo):

ebb77e6462b1fd8672e5f5a61cf381e184dab6073f7590b85427a1d0e3382ddc (2206237 bytes, LF) CRLF alias (same content, normalized): 962c04a27ed181863b3e323b1fe433d770cc42db0dbfbc9ff8b8ec143bc4794d

---

Platform support

• Windows / macOS / Linux - pathlib only, UTF-8 with ASCII fallback, no C:\Users\... or /home/... literals, no os.sep branching.
• Drop the folder anywhere and run. Override the output directory with QECTOR_PROOF_OUTPUT_DIR.
• Certification of the live wheel requires a compatible qector-decoder-v3==1.0.0 binary. The math-proofs layer still runs without it.

---

Citation

@techreport{qector_decoder_v3_manual_1_0_0,
  title       = {QECTOR Decoder v3 Reference Manual},
  version     = {1.0.0},
  author      = {Lessard, Guillaume},
  institution = {iD01t Productions},
  year        = {2026},
  doi         = {10.5281/zenodo.21941046},
  url         = {https://doi.org/10.5281/zenodo.21941046}
}

Author: Guillaume Lessard - ORCID 0009-0000-3465-3753 · iD01t Productions

License

Source-available. Free for academic, personal and non-commercial research. Commercial use requires a paid licence: https://qector.store/pricing

Contact: admin@qector.store · https://www.qector.store