OAI/Computability/QuantumFactoring/PrimeComponentCircuit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.prime_component_gcd line 18
  2. def OAI.ExactQuantumFactoring.BitArithmetic.componentWidth line 35

    Source documentation

    A polynomial-width, polynomial-size component modulus circuit. It uses p as an input prime, not an oracle or enumeration of prime factors of m.

    def componentWidth (n : ℕ) : ℕ := n*n+1
  3. def OAI.ExactQuantumFactoring.BitArithmetic.primeComponent line 37
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.primeComponent_value line 43
  5. def OAI.ExactQuantumFactoring.BitArithmetic.primeComponentBound line 63
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.primeComponent_count line 67