feat: Deutsch-Jozsa and GHZ quantum algos#1
Draft
tannerduve wants to merge 14 commits into
Draft
Conversation
tannerduve
force-pushed
the
quantum-algos
branch
from
March 27, 2026 19:49
a7e9686 to
24d1b8e
Compare
tannerduve
force-pushed
the
quantum-models
branch
from
March 27, 2026 19:50
26e715f to
733804b
Compare
tannerduve
force-pushed
the
quantum-algos
branch
from
March 27, 2026 19:50
24d1b8e to
7e23885
Compare
tannerduve
force-pushed
the
quantum-models
branch
from
March 27, 2026 20:48
733804b to
ba1be07
Compare
tannerduve
force-pushed
the
quantum-algos
branch
from
March 27, 2026 20:48
7e23885 to
314b5b0
Compare
tannerduve
force-pushed
the
quantum-algos
branch
from
April 7, 2026 02:20
d5cc501 to
34762e5
Compare
tannerduve
force-pushed
the
quantum-algos
branch
from
April 7, 2026 03:36
34762e5 to
65eceee
Compare
tannerduve
force-pushed
the
quantum-algos
branch
2 times, most recently
from
April 18, 2026 16:17
6d590a6 to
04401a9
Compare
tannerduve
force-pushed
the
quantum-models
branch
from
April 18, 2026 16:24
7764f87 to
d546faf
Compare
Replaces the hand-rolled amplitude-vector machinery with a syntactic query layer that denotes into QuantumInfo's CPTPMap. - QuantumQuery carries only syntactic data (gate tags, Fin n indices, rational phase); unitaryOf maps each constructor to its genuine 𝐔[Fin n → Fin 2] via embedQubitGate / cnotUnitary / phaseGate. - QuantumCircuit's toCPTP interprets the tree into CPTPMap via ofUnitary / compose / prod, with par threading through finFunSplitEquiv. - Retires QState, IsUnitary, tensorGate, measureDistribution, every gateX function and gateX_isUnitary lemma, QuantumCircuit.eval. - Adds UniformFamily to Complexity/Basic.lean and defines BQP/EQP/QNC against it with SingleTapeTM as the classical generator model. - Files live in Algolean/Models/Quantum/ (model layer) and Algolean/Complexity/BQP.lean (complexity classes). - Adds Physlib dependency in lakefile.
tannerduve
force-pushed
the
quantum-models
branch
from
April 18, 2026 16:30
d546faf to
0ac3504
Compare
tannerduve
force-pushed
the
quantum-algos
branch
from
April 18, 2026 16:30
04401a9 to
33df54c
Compare
tannerduve
force-pushed
the
quantum-models
branch
from
April 18, 2026 17:03
0ac3504 to
31151e5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Deutsch-Jozsa (query model) and GHZ state preparation (circuit model) using Prog. Correctness theorems stated with sorry (WIP)