OAI/Computability/QuantumFactoring/WideSplitCircuit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.halfPowerBits line 19

    Source documentation

    The exponent word may be the entire completion-guess width. In particular an arbitrary rare-branch guess is NOT silently truncated to n bits.

    def halfPowerBits {k w e : ℕ} (a m : BooleanNetwork k w) (d : BooleanNetwork k e) : BooleanNetwork k w :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.halfPowerBits_value line 21
  3. def OAI.ExactQuantumFactoring.BitArithmetic.shiftedHalfBits line 33
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.shiftedHalfBits_value line 36
  5. def OAI.ExactQuantumFactoring.BitArithmetic.candidateBits line 58
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.candidateBits_value line 61
  7. def OAI.ExactQuantumFactoring.BitArithmetic.ordersBits line 73
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.ordersBits_value line 76
  9. def OAI.ExactQuantumFactoring.BitArithmetic.suppliedBits line 87
  10. theorem OAI.ExactQuantumFactoring.BitArithmetic.suppliedBits_value line 91