OAI/Computability/QuantumFactoring/TotientAccumulator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.totientStepNat line 18

   Source documentation

   The finite-word accumulator semantics. Only the multiplicative accumulator is reduced; division of the residual never overflows.

   def totientStepNat (B p : ℕ) (s : ℕ×ℕ) : ℕ×ℕ :=
   …

2. def OAI.ExactQuantumFactoring.totientFoldNat line 21
3. lemma OAI.ExactQuantumFactoring.totientStepNat_bound line 25
4. lemma OAI.ExactQuantumFactoring.totientFoldNat_score line 33
5. lemma OAI.ExactQuantumFactoring.totientFoldNat_exact line 50