OAI/Computability/QuantumFactoring/FactoringCircuit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedLength_pos line 19
2. lemma OAI.ExactQuantumFactoring.PhysicalTree.finalRegister_bound line 21
3. def OAI.ExactQuantumFactoring.PhysicalTree.finalRegister line 28
4. def OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit line 35
5. lemma OAI.ExactQuantumFactoring.PhysicalTree.final_input line 40
6. lemma OAI.ExactQuantumFactoring.PhysicalTree.final_register_output line 48
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.final_output line 54
8. lemma OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit_qubits line 83
9. theorem OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit_exact line 90
10. theorem OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit_spec line 118

    Source documentation

    Discharges exactly the input/output clause for one explicit length-only family. This does NOT assert the outstanding resource or TM2-uniformity clauses.

    theorem finalCircuit_spec (ℓ N : ℕ) (hN : 2≤N) (hs : N.size=ℓ) :
        ℓ+(paddedLength ℓ)^2≤(finalCircuit ℓ).qubits ∧
          (finalCircuit ℓ).correctProbability ℓ N=1 := by
    …

    Mentions: OAI.ExactQuantumFactoring.paddedLength, OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit

11. lemma OAI.ExactQuantumFactoring.PhysicalTree.finalCircuit_length line 125