QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Structure before circuit tricks

Uncompute: digesting discovered reversible circuits

A circuit can output correct bits yet fail coherently through a wrong phase or dirty workspace. Explain the reusable construction before exposing the implementation proof forest.

research target setting:pinned-kickmix-clean-phase-trajectory

\[\text{reachable invariant}\;\land\;\text{branch decoder}\;\land\;\text{circuit refinement}\;\Longrightarrow\;\text{clean reversible implementation}\]

Choose your reading depth

Question → mechanism → mathematical suppliers → evidence. Open only the level you need; the contract and unproved boundaries remain visible below.

01 · The question

How can an automatically proposed circuit become a trustworthy SP/BE construction?

  • Follow data, phase and garbage separately. Start with the contract, not theorem names.
  • The planned laboratory follows a visible loop: freeze the contract -> propose a circuit -> independently check and cost it -> prove its symbolic guarantees -> compare -> mutate or cross over a named mechanism.
02 · The mechanisms

Route data through a shared kernel; recover history from a proved invariant; account for permitted failure.

  • These are techniques to audit under their own promises, not automatic substitutions into a state-preparation route.
  • Conditional routing shares an arithmetic kernel; branch recovery reconstructs a decision from a proved reachable-state invariant; measurement-based cleanup needs its own feedback and phase semantics.
  • A mutation changes one specified mechanism. A crossover combines compatible verified interfaces; concatenating two proposals does not transfer a certificate.
03 · The mathematical suppliers

Read the source construction and its complete AND dependencies.

  • Appendix A: initialization and step -> determinant/parity and window invariant -> decoder -> finite-dependence/depth-two consumers.
  • Termination is a separate certificate branch; it is not a prerequisite for the local decoder.
  • SP/diagonal BE needs function evaluation AND amplitude transduction AND uncomputation AND the relevant error/success guarantees. LCU needs PREPARE AND SELECT AND unprepare, with coefficient/phase and normalization conventions. These are planned integration chains, not newly certified graph edges.
04 · The evidence

Open upstream Lean first, then the local compatibility and independent acceptance records as they become available.

  • Upstream 4.32.2/4.33.1 is not local 4.33.0 acceptance. An isolated compatibility compile is not local publication admission or a circuit certificate.
  • Circuit refinement, statistical confidence, instance constants and resource counts retain separate open gates.
  • Correctness is a gate before resource comparison. Record oracle construction/calls, classical preprocessing/storage, Toffoli and other gates, depth, peak qubits, cleanup, precision and SP success/amplification. TQ alone is not the objective.
  • Compare only matched domains, error norms, precision, failure budgets and oracle assumptions. Preserve failed candidates, lineage and available wall-clock/model-call/token telemetry; unknown measurements stay unknown.

Frozen target and input model

First research priority: digest the whole pinned paper and its existing proofs into readable, audited mechanisms, then use them in controlled SP/BE construction-evolution experiments. Start with Appendix A branch recovery and the DQI theorem boundary, then connect real circuit semantics, error and resources; do not stop at a toy arithmetic identity or claim a resource improvement before a matched-contract comparison.

Access model: Pinned paper v1 and author code commit 64b5a13aa249f1360846657392e6c66817b26d0f. Explicit bit widths, registers, signed arithmetic, phase, measurement records, allowed input subspace, failure distribution and actual emitted operations. Each SP/BE experiment additionally freezes the target state/operator, oracle access, error norm, precision, success probability and comparison baseline before proposing circuits.

  • Keep Lean 4.33.0 locally; upstream 4.32.2 and 4.33.1 proofs need explicit compatibility checks.
  • Reachable-state invariants must be proved from initialization, not added as convenient final circuit hypotheses.
  • Do not replace phase and cleanup checks by output-bit tests, or random tests by universal certificates.
  • Retain separate native-certificate trust, primality, code-distance, collision, statistical and circuit-to-oracle obligations.
  • Workers never modify the trusted verifier, acceptance anchors, scoring, benchmark split or historical logs. Workflow variants require controlled experiments.
  • A distribution-dependent failure allowance or small error on one initial state is not a uniform operator-norm block-encoding guarantee.

Desired result, not an achieved bound

First deliver a source-faithful, independently reviewed 4.33.0 adaptation and exact source-to-Lean crosswalk; subsequently certify the missing gate/record/cleanup and cost bridges. Then evaluate actual SP/BE candidates under matched contracts and preserve both improvements and negative results. Author results remain author results; no new best-known circuit is promised.

No new ASPBE Lean closure yet. Upstream recurrence/DQI proofs do not certify all eight circuit tasks. A 590-step worst-case result does not accept the 533-step failure-budget circuit. TQ is a paper objective, not a replacement for ASPBE correctness-first resource contracts.

Dependency-ready execution route

01

Pin and audit the actual upstream theorem interfaces before adapting them to Lean4.33.0.

Acceptance: Compile exact adapted modules; audit axioms, binders, definitions, licenses and source graph; preserve author credit and publish the compatibility delta.

planned; no claimed closure

02

Close the Appendix A reachability-to-decoder chain, then its actual reversible register implementation.

Acceptance: Initialization/step, determinant/parity and window suppliers discharge the decoder premises. Include zero/frozen/signed cases and exact cleanup; no arbitrary-state strengthening.

planned; no claimed closure

03

Audit DQI strict-distance and boundary regimes and connect the implementation to their oracle hypotheses.

Acceptance: Keep strict inequality, clean relocation, record leakage, collision and profile residual distinct. Prove the circuit-to-oracle refinement instead of assuming the desired output.

planned; no claimed closure

04

Digest numerical evaluation, chemistry SELECT/QROM and lattice-group constructions in dependency-ready batches.

Acceptance: Every claimed result has source coverage, exact finite-bit/error/resource contract, checked Lean scope and independently reproduced executable evidence.

planned; no claimed closure

05

Planned first construction loop: finite-bit function oracle -> controlled amplitude transduction -> uncompute -> state preparation or diagonal block encoding. Choose one source-backed HHL, Gaussian or Coulomb case after checking existing library interfaces.

Acceptance: Prove the actual output action, coherent relative phase, domain/scaling and workspace restoration. Charge finite-bit arithmetic and rotation synthesis; for SP also retain normalization, success probability and amplification cost. A function evaluator alone does not close SP or BE.

planned; no claimed closure

06

Planned second construction loop: proof-guided LCU PREPARE-SELECT optimization, using the paper's alias-SELECT case as a source-backed entry point rather than assuming an entire chemistry algorithm is certified.

Acceptance: Freeze coefficients, normalization, oracle contracts and error; compare real alias/QROM/selection/cleanup variants without changing that target. Supply PREPARE, SELECT and unprepare dependencies internally and retain the full resource tuple.

planned; no claimed closure

07

Publish a compressed construction spine with lossless source and proof drill-down.

Acceptance: Independent reader can recover registers, phases, cleanup, error, cost tier and remaining obligations; no declaration-count or sample-pass proxy.

planned; no claimed closure

Next bounded advance: Complete independent source-topology and source/formal reconciliation for the fixed upstream modules, retaining separate compatibility-build evidence. Freeze one dependency-ready SP/BE experiment and its baseline before proposal search; no production proof-tree changes until the current bindings are stable.

Reusable mathematics

Recoverable history on reachable statesFinite matrices, norms and registersCharged access and finite-precision compilation

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Lower-bound comparison contract

model-definition-pending

Paper resource improvements are instance/model comparisons, not universal optimality or a poly(n) state-preparation theorem.

Same-model key: setting:pinned-kickmix-clean-phase-trajectory

Diagnostic examples, not proofs

  • Appendix A: reachable negative-counter nonswap, including frozen and signed cases
  • DQI: strict dual distance versus the Reed-Solomon boundary; no global-isometry shortcut
  • Methods: correct bits with incorrect phase or dirty record must fail

Primary-source ledger

Discovering state-of-the-art quantum circuits with large language models

primary-text-checked v1: design principles; Methods Eqs. (10)-(22); Appendix A, A.1-A.8 (PDF pp. 44-46). Other case studies remain a queued source audit.

Priority intake for reversible computation and proof digestion. First batch audits existing branch-recovery and DQI proof interfaces; full paper and circuit/resource closure remain open.

uncompute: pinned author circuit, evaluator and Lean artifacts

primary-text-checked Commit 64b5a13aa249f1360846657392e6c66817b26d0f; lean/divsteps/README.md, lean/dqi/README.md; selected Recovery.lean and Complete.lean theorem interfaces; not yet a whole-module audit or local build.

Observed pins: divsteps Lean/Mathlib4.32.2; DQI Lean/Mathlib4.33.1. Apache-2.0 repository; divsteps also retains MIT safegcd-bounds attribution. Upstream source and claimed builds are not ASPBE acceptance.

Download bounded agent / contributor packet

python3 website/scripts/research_atlas.py context --route spw-uncompute