OAI/Computability/QuantumFactoring/LabelRecoveryCircuit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.OrderTrial.scanPairs line 15

    Source documentation

    A bounded scan; either the sole valid label, or the distinguished zero pair.

    def scanPairs (Q B k : ℕ) : ℕ → ℕ×ℕ
  | 0 => (0,0)
  | i+1 => let a := checkedPair Q B k i
…

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.checkedPair

  2. lemma OAI.ExactQuantumFactoring.OrderTrial.scanPairs_success line 20
  3. lemma OAI.ExactQuantumFactoring.OrderTrial.scanPairs_sound line 37
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.scanPairs_complete line 47
  5. def OAI.ExactQuantumFactoring.OrderTrial.pairChoice line 57

    Source documentation

    Choose the left nonzero-denominator pair, otherwise the right. The costly candidate and recursive scan are paired ONCE before this inexpensive mux.

    def pairChoice (w : ℕ) : BooleanNetwork ((w+w)+(w+w)) (w+w) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  6. lemma OAI.ExactQuantumFactoring.OrderTrial.pairChoice_eval line 64
  7. lemma OAI.ExactQuantumFactoring.OrderTrial.pairChoice_count line 76
  8. def OAI.ExactQuantumFactoring.OrderTrial.recoveryNet line 83
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.recoveryNet_value line 87