OAI/Computability/QuantumFactoring/ComponentPhiCircuit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.componentPhiNet line 21

   Source documentation

   Euler's prime-power formula, implemented by n-bit arithmetic on the computed gcd component. Divisibility by p is a verified-call precondition.

   def componentPhiNet {k n : ℕ} (m p : BooleanNetwork k n) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentPhiNet_value line 25
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentPhiNet_ne_zero line 39
4. def OAI.ExactQuantumFactoring.BitArithmetic.componentPhiBound line 46
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentPhiNet_count line 47
6. def OAI.ExactQuantumFactoring.BitArithmetic.componentLevelNet line 58
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentLevelNet_value line 62
8. def OAI.ExactQuantumFactoring.BitArithmetic.componentLevelBound line 78
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentLevelNet_count line 80