OAI/Computability/QuantumFactoring/AIGBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.AIGBounds.cached_go_size line 15
  2. lemma OAI.ExactQuantumFactoring.AIGBounds.cached_size line 25
  3. lemma OAI.ExactQuantumFactoring.AIGBounds.atom_size line 30
  4. lemma OAI.ExactQuantumFactoring.AIGBounds.and_size line 35
  5. lemma OAI.ExactQuantumFactoring.AIGBounds.or_size line 38
  6. lemma OAI.ExactQuantumFactoring.AIGBounds.xor_size line 41
  7. lemma OAI.ExactQuantumFactoring.AIGBounds.fullAdderOut_size line 51
  8. lemma OAI.ExactQuantumFactoring.AIGBounds.fullAdderCarry_size line 59
  9. lemma OAI.ExactQuantumFactoring.AIGBounds.fullAdder_size line 71
  10. lemma OAI.ExactQuantumFactoring.AIGBounds.add_go_size line 79
  11. theorem OAI.ExactQuantumFactoring.AIGBounds.add_size line 95

    Source documentation

    A verified native ripple circuit has linear declaration count. The cache can only decrease this upper bound.

    theorem add_size {w : ℕ} (aig : AIG α) (input : AIG.BinaryRefVec aig w) :
    (blastAdd aig input).aig.decls.size ≤ aig.decls.size + 12*w := by
…
  12. lemma OAI.ExactQuantumFactoring.AIGBounds.if_size line 100
  13. lemma OAI.ExactQuantumFactoring.AIGBounds.ite_go_size line 110
  14. lemma OAI.ExactQuantumFactoring.AIGBounds.ite_size line 124
  15. lemma OAI.ExactQuantumFactoring.AIGBounds.shift_go_size line 128
  16. lemma OAI.ExactQuantumFactoring.AIGBounds.shift_size line 137
  17. lemma OAI.ExactQuantumFactoring.AIGBounds.mul_go_size line 140
  18. lemma OAI.ExactQuantumFactoring.AIGBounds.mul_blast_size line 164
  19. theorem OAI.ExactQuantumFactoring.AIGBounds.mul_size line 177

    Source documentation

    The native shift-and-add multiplier has quadratic declaration count.

    theorem mul_size {w : ℕ} (aig : AIG α) (input : AIG.BinaryRefVec aig w) :
    (blastMul aig input).aig.decls.size ≤ aig.decls.size + 15*w*w := by
…