OAI/Computability/QuantumFactoring/RetainedTotient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.retainedTotient line 22

   Source documentation

   The totient network reads only the actual retained rectangular table.

   def retainedTotient (t : ℕ) (v : BooleanNetwork (M.width t) n) :
       BooleanNetwork (M.width t) n := tableTotient v (M.fieldRows t)

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedTotient_exact line 25
3. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedTotient_count line 43
4. def OAI.ExactQuantumFactoring.NodeMachine.retainedOrderPhi line 54

   Source documentation

   The numerator of the exact order-trial success probability, with no recovery of an exponent record and no factorization call at runtime.

   def retainedOrderPhi (t : ℕ) (a m : BooleanNetwork (M.width t) n) :
       BooleanNetwork (M.width t) n := M.retainedTotient t (M.retainedOrder t a m)

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

5. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedOrderPhi_exact line 57