OAI/Computability/QuantumFactoring/TotientCircuit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   A division-based totient step. Redundant prime entries do nothing.

   def totientPair {k w : ℕ} (q v a : BooleanNetwork k w) : BooleanNetwork k (w+w) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientPair_value line 26
3. def OAI.ExactQuantumFactoring.BitArithmetic.totientStepBound line 71

   Source documentation

   A loose but explicit uniform polynomial bound; the residual, prime and accumulator subcircuits are evaluated a constant number of times per step.

   def totientStepBound (w c : ℕ) : ℕ := 30*c+3000*w*w+3000*w+300

4. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientPair_count line 73
5. def OAI.ExactQuantumFactoring.BitArithmetic.totientUpdate line 88

   Source documentation

   Carry the input unchanged and update two finite-word accumulators.

   def totientUpdate {k w : ℕ} (q : BooleanNetwork k w) :
       BooleanNetwork (k+(w+w)) (k+(w+w)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

6. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientUpdate_value line 94
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientUpdate_count line 114
8. def OAI.ExactQuantumFactoring.BitArithmetic.totientScanNet line 119
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientScanNet_count line 123
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.totientScanNet_value line 134