QuantumVerifier.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The promise-QMA interface for the Heisenberg source. The verifier uses the fixed H,T,CNOT gate set, complex quantum witnesses, ancillas initialized to zero, one output measurement and a polynomial-time TM2 circuit generator. There is no condition outside either promise set.

inductive OAI.ContinuumCoulomb.QMAGate line 18
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:203 (same declaration text).
def OAI.ContinuumCoulomb.qmaGateEquiv line 24
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:209 (same declaration text).
def OAI.ContinuumCoulomb.qmaGateCodec line 36
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:221 (same declaration text).
structure OAI.ContinuumCoulomb.QMACircuit line 39
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:224 (same declaration text).
def OAI.ContinuumCoulomb.qmaCircuitEquiv line 46
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:230 (same declaration text).
def OAI.ContinuumCoulomb.qmaCircuitCodec line 52
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:236 (same declaration text).
def OAI.ContinuumCoulomb.QMAGate.WellFormed line 55
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:239 (same declaration text).
def OAI.ContinuumCoulomb.QMACircuit.WellFormed line 60
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:244 (same declaration text).
def OAI.ContinuumCoulomb.qmaHadamard line 66
Source documentation
Exact algebraic Hadamard gate.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:247 (same declaration text).
```
def qmaHadamard : Matrix (Fin 2) (Fin 2) ℂ :=
…
```
def OAI.ContinuumCoulomb.qmaPhaseT line 70
Source documentation
T=diag(1,exp(i*pi/4)), written with its exact algebraic entries.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:250 (same declaration text).
```
def qmaPhaseT : Matrix (Fin 2) (Fin 2) ℂ :=
…
```
def OAI.ContinuumCoulomb.qmaQubit line 73
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:253 (same declaration text).
def OAI.ContinuumCoulomb.qmaControlledNot line 76
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:256 (same declaration text).
def OAI.ContinuumCoulomb.qmaGateMatrix line 80
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:260 (same declaration text).
def OAI.ContinuumCoulomb.qmaCircuitMatrix line 89
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:269 (same declaration text).
def OAI.ContinuumCoulomb.qmaInitialState line 95
Source documentation
The witness occupies the first witness qubits; every remaining qubit, including the measured final qubit, starts in the zero state.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:273 (same declaration text).
```
def qmaInitialState (c : QMACircuit) (hc : c.WellFormed)
    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) :
    SourceSpinBasis (c.work + 1) → ℂ :=
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis
def OAI.ContinuumCoulomb.qmaAcceptance line 103
Source documentation
Born probability of measuring one on the output qubit.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:280 (same declaration text).
```
def qmaAcceptance (c : QMACircuit) (hc : c.WellFormed)
    (psi : EuclideanSpace ℂ (SourceSpinBasis c.witness)) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.QMACircuit, OAI.ContinuumCoulomb.SourceSpinBasis
structure OAI.ContinuumCoulomb.QuantumVerifier line 109
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:286 (same declaration text).
structure OAI.ContinuumCoulomb.PromiseProblem line 116
Distinct definitions of this name: ComparatorChallenges/ContinuumCoulombHardness.lean:293 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.PromiseProblem@path.
theorem OAI.ContinuumCoulomb.inQMA_two_atLeastTwo line 123
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:312 (same declaration text).
theorem OAI.ContinuumCoulomb.inQMA_three_atLeastTwo line 126
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:315 (same declaration text).
def OAI.ContinuumCoulomb.InQMA line 132
Source documentation
Promise-QMA with completeness 2/3 and soundness 1/3.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:320 (same declaration text).
```
def InQMA (P : PromiseProblem BitString) : Prop :=
…
```
structure OAI.ContinuumCoulomb.PolynomialManyOne line 142
Source documentation
Actual polynomial-time many-one reduction with both promise maps.
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:329 (same declaration text).
```
structure PolynomialManyOne {α β : Type} (ea : α → BitString) (eb : β → BitString)
    (P : PromiseProblem α) (Q : PromiseProblem β) where
…
```
def OAI.ContinuumCoulomb.QMAHard line 149
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:336 (same declaration text).
def OAI.ContinuumCoulomb.PolynomialManyOne.refl line 153
Source documentation
The machine-based definition includes the identity reduction.
```
def PolynomialManyOne.refl {α : Type} (ea : α → BitString) (P : PromiseProblem α) :
    PolynomialManyOne ea ea P P where
…
```
Mentions: OAI.ContinuumCoulomb.PolynomialManyOne