OAI/Computability/QuantumFactoring/BinLabelCircuit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.binCheckExpr line 17

   Source documentation

   Input order Q,B,k,d,j; coprimality is already guaranteed by the convergent recurrence and does not require a second gcd computation.

   def binCheckExpr : NatExpr (Fin 5) :=
   …

   Mentions: OAI.ExactQuantumFactoring.NatExpr

2. lemma OAI.ExactQuantumFactoring.OrderTrial.binCheckExpr_eval line 29
3. def OAI.ExactQuantumFactoring.OrderTrial.checkedConvergent line 37
4. def OAI.ExactQuantumFactoring.OrderTrial.checkedPair line 45
5. lemma OAI.ExactQuantumFactoring.OrderTrial.checkedConvergent_value line 49
6. lemma OAI.ExactQuantumFactoring.OrderTrial.checkedPair_nonzero_iff line 100
7. lemma OAI.ExactQuantumFactoring.OrderTrial.checkedPair_sound line 107