← QBP consequence · Complete narrative · Source map →
The repository uses executable checks to test the conventions and constructions that are easiest to get wrong: column labels, chronological order, relative phases, coherent routing, work-register cleanup, and simultaneous resource peaks. The asymptotic theorem itself is established analytically.
| Level | Meaning in this repository |
|---|---|
| analytic proof | a dimension-independent operator or resource argument |
| explicit construction | a complete reversible or logical-gate schedule is supplied |
| imported exact synthesis | an elementary compiler theorem is used under its stated model |
| finite regression check | independently constructed matrices, states, schedules, or ledgers are compared |
These levels are kept distinct. A matrix test does not prove an asymptotic bound, and an asymptotic bound does not certify an implementation's bit order.
The selected Results A–D are analytic theorems. Their finite fixtures check conventions, literal phases, work return, and resource accounting under the individual recorded contracts.
| Claim | Analytic proof | Principal executable evidence | Boundary |
|---|---|---|---|
| A: exact complete frame | Compiler theorem | Exact-frame, strict-zero, decoder, router, and resource suites in §§2–8 below | UCG and multi-controlled-X elementary synthesis are imported |
| B: sufficient-clean matching T count | Fault-tolerant compiler | Four exact receipt suites, resource ledgers, and full-input approximation checks | Finite kernels and analytic resource proxies; no general native frame emitter |
| C: one-clean frame and corollaries | One-clean compiler, grouped extension | Operator-source checks, one-clean word, amplification, grouped residual and bank-allocation fixtures | Small emitted words and matrices; operator-core return error is included in the joint norm |
| D: uniform count and T-depth | Uniform-precision theorem | Unary-source, blocked-query, dirty-indicator, arithmetic, and uniform allocation suites | Same-circuit analytic schedule; finite fixtures do not emit every variable-size frame |
The verification catalogue preserves the complete per-fixture descriptions, negative controls, and software boundaries, including separate state-based QBP coverage and optional research diagnostics. Its detailed records are not additional claims of A–D.
| Component | Local representation | Principal executable check | Imported ingredient |
|---|---|---|---|
| Hopf states and frames | dense matrices from independent recursive and addressed-layer constructions | complete equality, orthogonality, state and marker columns, chart domains, singular coordinates | Hopf geometry inherited from the earlier work |
| strict-zero echo | dense logical gates and exact reversible permutations | all four sectors, every nonfinal depth, full frames, inverse, and complex composition | UCG and ancilla-free MCT resource theorems |
| binary–one-hot decoder | explicit X/CNOT/Toffoli layers | basis action, arbitrary-basis reversibility, disjoint layers, counts, and clean return | constant-cost elementary decompositions |
| coherent router | explicit CNOT-fanout and Fredkin layers with sparse complex-state simulation | basis routing, entangled inputs, tail direct sum, complete cut, and zero leakage | coherent copy and constant-cost controlled gates |
| controlled subtree frames | exact logical token/flag-controlled rotations | equality to the ideal block-diagonal tail and flag cleanup | UCG and MCT synthesis |
| leaf-phase diagonal | exact block-diagonal UCG matrix | complete diagonal, inverse, common phase, and complex magnitude composition | UCG synthesis |
| resource theorem | integer and exact-rational ledgers | workspace peaks, schedule dispatch, endpoints, geometric sums, and cut inequalities | asymptotic primitive bounds |
| gradient records | parity, signed-histogram, and fast Walsh–Hadamard decoders | agreement of routes, empirical means, and deterministic record norms | QBP record identities |
The repository does not reproduce the elementary UCG or multi-controlled-X compiler. Those exact results are imported from the all-workspace state-preparation framework. Toffoli, Fredkin, controlled one-qubit gates, and fixed-width controlled Givens rotations have exact constant-size, constant-depth decompositions in the declared arbitrary-one-qubit+CNOT model.
The frame suite checks:
- equality of the recursive and addressed-layer frames;
- real-frame orthogonality;
- phase-dressed complex magnitude-frame unitarity;
- the breadth-first marker convention;
-
$g_{j,j}=a_j^2$ for unrestricted angles; -
$a_j=\sqrt{g_{j,j}}$ on the canonical domains; - tolerance-aware regularity at floating-point chart boundaries;
- zero raw derivative and a unit chart-selected marker continuation at a singular coordinate.
The compiler-boundary fixtures check:
- two unitaries with the same prepared state but different marker columns;
- the resulting gradient change
$$(2,0,0)\longmapsto(0,\sqrt2,0);$$ - a checkpoint suffix that preserves one state but changes a derivative;
- an active-interface-safe suffix that preserves designated means without preserving the complete distribution.
Additional boundary tests exercise the sharp worst-observable sensitivity, common-phase cancellation, projected marker error versus physical leakage, and singular-marker ambiguity across all two-qubit Pauli observables.
Files:
- frame implementation
- frame tests
- complex geometry tests
- compiler-boundary implementation
- compiler-boundary tests
The strict-zero suite checks:
-
$C^2=R_y(\theta)$ and$XCX=C^{-1}$ ; - all four
$(h,b)$ sectors; - exact restoration of the borrowed logical suffix bit;
- absence of hidden workspace;
- every nonfinal addressed depth through
$n=8$ ; - complete real frames through
$n=8$ ; - inverse frames and phase-dressed complex magnitude frames;
- the endpoints
$n=1$ ,$d=0$ ,$d=n-2$ , and the final depth.
The resource audit checks, using exact arithmetic,
and the absorption of the polynomial predicate terms into
Files:
The decoder is tested as a complete reversible permutation, not only on its intended clean input. The suite verifies:
-
$\lvert x\rangle\lvert0\rangle$ maps to$\lvert0\rangle\lvert e_x\rangle\lvert0\rangle$ and returns under the inverse; - arbitrary computational-basis contents return after forward and inverse;
- every declared layer has disjoint wire support;
- the exact workspace formula
3\,2^t-2-t; - the exact gate and depth formulas;
- the one-hot Givens network equals the complete prefix Hopf frame on the code.
Files:
The router is supplied as an explicit schedule. The tests cover:
- branch-data, token, copy, and reusable-flag register allocation;
- balanced prefix fanout and exact uncopy;
- disjoint Fredkin layers;
- every clean basis input routed to its prefix-selected branch;
- forward route followed by inverse route on arbitrary complex inputs;
- prefix–suffix-entangled inputs;
- token-controlled action of all subtree frames;
- cleanup of every branch flag before inverse routing;
- equality to
$$\bigoplus_r W_s^{(r)};$$ - equality of the complete routed cut to the direct Hopf frame;
- zero probability outside the clean-workspace subspace.
The explicit schedule is cross-checked against
The simulator iterates over branches for convenience. The circuit-depth claim uses the declared parallel schedule: branch data, tokens, flags, and subtree frames have disjoint physical support.
Files:
The ledgers use integer or exact-rational checks rather than fitted slopes. They cover:
- strict zero workspace;
- the one-clean-flag endpoint;
- the direct-to-routed transition;
- maximal feasible cuts over broad
$n,m$ grids; - copy-pool reuse as branch flags;
- the
$s=1$ routed endpoint; - arbitrarily large workspace;
- matching real-state parameter and light-cone lower bounds.
Representative checked implications are
and
for the maximal routed cut, including the saturated endpoint
Files:
The decoder suite compares:
- direct record-wise parity averages;
- dense Walsh transforms;
- the fast Walsh–Hadamard implementation;
- direct phase-stream signed one-hot records.
It verifies the deterministic norm-two record property used by the coordinatewise concentration statement.
Files:
Use Python 3.11 or 3.13. From the repository root:
python -m venv .venv
source .venv/bin/activate
python -m pip install --upgrade pip
python -m pip install -r requirements.txt
python scripts/reviewer_walkthrough.py
python validate.py
python scripts/verify_fault_tolerant.pyThe last two commands run the deterministic unittest collection and the four separate exact receipt suites. Resource ledgers and offline provenance:
python scripts/unified_resource_ledger.py --n 12
python scripts/strict_zero_echo_ledger.py --n 12
python scripts/check_upstream_sync.py --offlineThe rendering guide covers diagrams, Markdown, MathJax, and native MathML; detailed coverage records its limits. Local previews do not reproduce GitHub's private renderer.
The repository does not use finite experiments to establish asymptotic optimality. It also does not test:
- device connectivity or routing overhead;
- a hardware-native gate set;
- a general elementary-gate emitter for the full asymptotic Clifford+T compiler;
- noisy execution or readout mitigation;
- application-specific controlled-observable implementations;
- arbitrary non-Hopf differential frames.
The proof should be assessed in four separate steps:
- the Hopf operator identities;
- the logical circuits and workspace cleanup;
- the imported synthesis bounds and resource sums;
- the matched QBP output and access conventions.
The fault-tolerant theorem separates the analytic
resource proof from the focused finite checks.
Run python scripts/verify_fault_tolerant.py from the repository root. Four
stdlib-only suites reproduce the retained exact Gray-source, shift-kernel,
resource, and reflection receipts without changing their saved reference files.
The runner compares scientific receipt fields and separately verifies the
deterministic source-file hashes, whose values changed when the sources were
relocated into this repository.
| Standalone receipt suite | What it checks | Evidence boundary |
|---|---|---|
| Gray geometric source | Emitted logical source words, actual inverse, scratch return, reference witnesses, and gate-count recurrences | Finite clean-scratch fixtures; the full source is not emitted as an elementary Clifford+T circuit |
| Shift kernel | Complete finite kernel columns, actual inverses, source defects, failure tracking, and negative controls | Small fixed parameters, without the production residual construction or emitted outer amplification |
| Shift resource | Exact rational scales, coefficient rounding, scalar error budgets, and resource ledgers | Analytic proxies and inequalities; the rows are not measured gate counts |
| Geometric reflection | Small source/reflection matrices, exact Pauli-transfer arithmetic, and algebraic norm separation | Supporting source-cost evidence and a kernel-suite dependency; no additive lower bound follows from these fixtures |
The receipt map records the exact fixture ranges, source dependencies, and provenance for all four suites.
The approximation bridge has tests for full-input error, actual-adjoint transfer, leakage, reference-entangled borrowed inputs, and bounded estimator bias. These validate the finite examples behind the general proof, not differentiation of a synthesized family.
The approximation suite also checks the complex phase stream directly, reflection-term sampling, pathwise finite-weight error, and a two-shot measurement instrument whose retained dirty state changes the next-shot law. The last fixture tests the conditional-mean premise of the martingale proof; it is not a fitted statistical scaling experiment.