OAI/Computability/QuantumFactoring/CyclicCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.decodeCyclic line 16
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.decodeCyclic_coeff line 19
  3. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicTerm line 22
  4. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulNet line 26
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulNet_value line 30
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulNet_correct line 48
  7. abbrev OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulBound line 57
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicTerm_count line 60
  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulNet_count line 67
  10. def OAI.ExactQuantumFactoring.BitArithmetic.CanonicalCyclic line 81

    Source documentation

    Canonical representatives permit exact word comparison of arrays.

    def CanonicalCyclic {s w : ℕ} (m : ℕ) (x : Basis (s*w)) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.Basis

  11. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicMulNet_canonical line 84
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.decodeCyclic_injective line 91