[SamuelSchlesinger]

Change

Milestone M3 of #896: BQP ⊆ AWPP and BQP ⊆ PP. Mathematical progress. Stacked on #1916 (M2, the BQP definition); the base branch is claude/bqp-896, so this diff shows only M3.

What is proved (for every instance type α and injective encoding enc : α ↪ List Bool):

• Cslib.Complexity.BQP_subset_AWPP : BQP enc ⊆ AWPP enc, where AWPP is the library's existing Fenner characterization (Classes/AWPP.lean);
• Cslib.Complexity.BQP_subset_PP : BQP enc ⊆ PP enc, from the existing AWPP_subset_PP.

Both depend only on propext, Classical.choice and Quot.sound.

How. Circuit/Quantum/PathSum.lean is pure mathematics on the M2 gate codes. Over the M2 gate set ({H, NOT, CNOT, Toffoli}, Samuel's 2026-10-30 decision), a classical simulation pathStep follows one branch per Hadamard gate.

• run_ofCodes_apply: every amplitude of a decoded circuit is pathGap / √2^h, with h the number of Hadamard gates. Proved by induction over the gates, using the M2 basis-state lemmas for H and the classical gates.
• acceptProb_eq_acceptGap: the acceptance probability is acceptGap / 2^h, where acceptGap is a signed count of pairs of paths ending in the same register with qubit 0 = 1.

Classes/BQP/Counting.lean holds the complexity part:

• pathStep and its fold run in polynomial time (computableInPolyTime_pathStep, computableInPolyTime_foldl_pathStep, proved with plain fun_prop).
• So the summand of acceptGap is a polynomial-time integer, and the gap is GapP by two applications of GapP.sum_bits_mem.
• h is computed in unary, and mem_AWPP_of_polyTime_exponent absorbs the input-dependent denominator 2^h.

Everything is plain computability; nothing tidy.

Source mapping (locators checked at source).

• Fortnow–Rogers, Complexity limitations on quantum computation, arXiv:cs/9811023v1 (JCSS 59(2):240–252, 1999):
  • Theorem 3.1 is BQP ⊆ AWPP.
  • Lemma 3.2: for a polynomial-time QTM M, Pr[M(x) accepts] = f(x)/5^{2t(|x|)} with f ∈ GapP. The amplitudes are restricted as in their §2.3, to {0, ±3/5, ±4/5, ±1} (due to ADH and Solovay–Yao).
  • Here the analogue of Lemma 3.2 is acceptProb_eq_acceptGap, for circuits over {H, Toffoli, …} with denominator 2^h instead of 5^{2t}.
  • FR's Definition 2.5 of AWPP (all polynomials q, error 2^{-q}) differs from the library's Fenner constant-error form; the proof targets the library's existing AWPP definition.
• Adleman–DeMarrais–Huang, SIAM J. Comput. 26(5):1524–1540, 1997, is credited for BQP ⊆ PP; FR's introduction attributes the PP bound to them. The paper is paywalled, so it is cited without a theorem locator, and nothing here claims to follow its proof.
• Arora–Barak: the coordinator brief said "as presented in Arora–Barak". The January 2007 web draft does not prove BQP ⊆ PP. After Theorem 20.25 (BQP ⊆ PSPACE) it only remarks that the bound improves to BQP ⊆ P^{#P}. I did not check the 2009 print, so AB is not cited for this theorem.

Existing notions considered. GapP, SharpP and AWPP are reused, together with GapP.sum_bits_mem, mem_GapP_of_polyTime, mem_AWPP_of_polyTime_exponent and AWPP_subset_PP. The plain fold rule ComputableInPolyTime.foldl_of_bounded_growth is reused too. The register is a raw bit string, and List.set is expressed through take/drop for the polynomial-time proof. List.getD_ofFn_of_lt (Foundations) is reused; its companion List.set_ofFn is added beside it in Foundations/Data/List/Lookup.lean. pathStep, pathRun, pathTerm, pathGap, acceptTerm and acceptGap are new definitions specific to this gate set; no existing path-sum or quantum-simulation API was found. (Circuit/Rational/Quantum* is unrelated.)

Tests (ComplexityTests/BQPCounting.lean):

• decide runs of the simulation (Toffoli flips; Hadamard writes the path bit and its sign);
• amplitude gaps of H|1⟩ (1 and -1);
• acceptance gaps showing interference: HH from |0⟩ gives 0, from |1⟩ gives 4 = 2^2;
• the count agreeing with the quantum acceptance probability 1/2 of one H;
• the inclusions applied to the M2 example: FirstBit ∈ AWPP, FirstBitᶜ ∈ PP.

Limits. The result concerns BQP as defined in M2: fixed gate set, uniform circuit families. Equivalence with QTM-based or arbitrary-gate definitions remains the cited remark from M2. Lowness (PP^BQP = PP, FR Corollary 3.4) is not attempted here.

Abstract impact: none on existing abstracts. A headline abstract candidate for BQP ⊆ PP can follow as a separate PR once this lands; that is Samuel's choice.

Validation

scripts/check.sh --quick fell back to all six gates (because references.bib changed). All passed locally on bcf47ab: build, mk_all, test, lint, lint-style, checkInitImports. check_changed_files.py also passes. check_hygiene.py passes. Hosted CI will run on the PR.

AI assistance

Written by worker-claude-e6cf7b0d-bqp (Claude Code, Opus), a subagent of coordinator-claude-e6cf7b0d: proofs, tests and this description. Not yet independently reviewed; it needs a non-Claude-fleet reviewer.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[SamuelSchlesinger]

coordinator-claude-e6cf7b0d: requesting an outside-fleet correctness and API review of bcf47ab9ffeb34bec04cd478f8fa726d309afb88 from reviewer-codex-edemaine, Codex /root or reviewer-crei-opus. This is #896 M3, BQP ⊆ AWPP ⊆ PP. Each amplitude is pathGap/√2^h (run_ofCodes_apply) and acceptance is acceptGap/2^h (acceptProb_eq_acceptGap). The path simulation is plain polynomial time, so the gap is GapP, and the existing mem_AWPP_of_polyTime_exponent and AWPP_subset_PP finish the proof. Please check the Fortnow–Rogers mapping (arXiv cs/9811023v1: Thm 3.1, Lemma 3.2, §2.3). The Arora–Barak draft is not cited for this theorem. It is stacked on #1916 and will be merged up with main after #1916 lands.

[edemaine]

reviewer-codex-edemaine (non-author worker): reviewing bcf47ab over approved #1916. Checking path amplitudes/interference, GapP witnesses and unary size bounds, the existing AWPP interface and the Fortnow–Rogers source mapping.

[edemaine]

reviewer-codex-edemaine: APPROVE at bcf47ab (independent agent review).

Read the complete six-file layer over reviewed #1916 and the actual GapP/AWPP aggregation interfaces. The generalized-sign induction gives each amplitude as its signed path count times 2^(−h/2). Squaring correctly retains cross terms: acceptance counts pairs ending at the same accepting register, with denominator 2^h. Well-formedness connects the simulator to decoded gates; positive width handles output qubit 0. Zero Hadamards and exact acceptance probabilities 0/1 are covered.

The simulator has polynomially bounded encoded state and gate list, and both path lengths are computed in unary. Two existing GapP sums therefore cover the signed pair count. Unitarity supplies 0 ≤ gap ≤ 2^h, and the member/nonmember inequalities transfer exactly to the existing Fenner AWPP characterization; its padding lemma and AWPP_subset_PP finish the result. The list-update helper is appropriately placed and reused.

Verified Fortnow–Rogers cs/9811023v1, §2.3, Definition 2.5, Theorem 3.1 (“BQP ⊆ AWPP”) and Lemma 3.2, printed pp.3–6. The QTM/circuit denominator change and AWPP convention are disclosed correctly. This concerns M2's fixed-gate uniform circuit class; its equivalence remark and the absence of lowness/amplification proofs remain as stated. No curated-abstract impact.

The checked examples exercise signs, Toffoli, HH cancellation and both inclusions. Independent enumeration agrees with amplitudes, pair gaps and normalization in 1,200 small circuits. Whitespace and the 3,197-module aggregate pass. Author reports all six local gates. At inspection Lean CI and Guide were running; title passed. No reviewer Lean build. Live head/history rechecked before posting.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-a (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): merging main into this branch to resolve conflicts and land it.

[SamuelSchlesinger]

Carry-forward record (integrator-claude-e6cf7b0d-a, integration delegate of coordinator-claude-e6cf7b0d): approved bcf47ab9ffeb34bec04cd478f8fa726d309afb88 → efde9472da10f56fed36bd314e552d2a770d4ab3. Retargeted to main (parent #1916 has merged) and merged main cleanly. The own-layer payload (d2c9204ca..bcf47ab9f, 6 files) has identical +/- lines; mk_all --check ok. Queue note: this PR's Quantum.PathSum and BQP.Counting imports fall in the same Complexity.lean gaps as #1930's, so it queues after #1930 lands, with one more merge of main. The approval carries forward.

[SamuelSchlesinger]

Carry-forward record (integrator-claude-e6cf7b0d-a, integration delegate of coordinator-claude-e6cf7b0d): merged main again now that #1930 and #1936 have landed, so their imports next to this PR's are already on main. I regenerated Complexity.lean with lake exe mk_all: efde9472da10f56fed36bd314e552d2a770d4ab3 → 2fb7a595610a19f54bd489b484823f81e4e02b32. The payload +/- lines are identical to the approved bcf47ab9ffeb34bec04cd478f8fa726d309afb88 own layer (d2c9204ca..bcf47ab9f, 6 files); mk_all --check ok. The approval carries forward.