OAI/Computability/QuantumFactoring/BooleanProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.programMatrix_nil line 13
  2. lemma OAI.ExactQuantumFactoring.programMatrix_cons line 15
  3. lemma OAI.ExactQuantumFactoring.programMatrix_singleton line 20
  4. inductive OAI.ExactQuantumFactoring.BooleanOp line 27

    Source documentation

    A Boolean node is implemented by at most two of the named fixed gates. The target is excluded from the sources, but repeated sources are permitted. Its action toggles the target, so the semantics are reversible on all states.

    inductive BooleanOp (q : ℕ) (t : Fin q) where
…
  5. def OAI.ExactQuantumFactoring.BooleanOp.value line 35
  6. def OAI.ExactQuantumFactoring.BooleanOp.eval line 41
  7. def OAI.ExactQuantumFactoring.BooleanOp.compile line 44
  8. lemma OAI.ExactQuantumFactoring.BooleanOp.compile_length line 52
  9. lemma OAI.ExactQuantumFactoring.BooleanOp.eval_at line 60
  10. lemma OAI.ExactQuantumFactoring.BooleanOp.eval_away line 63
  11. lemma OAI.ExactQuantumFactoring.BooleanOp.eval_fresh line 66
  12. lemma OAI.ExactQuantumFactoring.BooleanOp.compile_basis line 70
  13. abbrev OAI.ExactQuantumFactoring.BooleanProgram line 101

    Source documentation

    The classical network explicitly retains all values already computed. In a fresh-output DAG each node's target is a previously zero ancilla.

    abbrev BooleanProgram (q : ℕ) := List ((t : Fin q) × BooleanOp q t)

    Mentions: OAI.ExactQuantumFactoring.BooleanOp

  14. def OAI.ExactQuantumFactoring.BooleanProgram.eval line 103
  15. def OAI.ExactQuantumFactoring.BooleanProgram.compile line 106
  16. lemma OAI.ExactQuantumFactoring.BooleanProgram.compile_basis line 109
  17. lemma OAI.ExactQuantumFactoring.BooleanProgram.compile_length line 118
  18. lemma OAI.ExactQuantumFactoring.BooleanProgram.uncompute line 130

    Source documentation

    Reversing the actual compiled gate list erases the complete retained trace, not only its output. No irreversible erasure is used.

    lemma BooleanProgram.uncompute {q : ℕ} (p : BooleanProgram q) (x : Basis q) :
    (programMatrix (p.compile.reverse.map Instruction.reverse)).mulVec
      (basisVector (p.eval x)) = basisVector x := by
…

    Mentions: OAI.ExactQuantumFactoring.BooleanProgram, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.Instruction.reverse, OAI.ExactQuantumFactoring.basisVector