OAI/Computability/QuantumFactoring/RetainedCanonical.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NodeMachine.retainedCanonical line 23
  2. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedCanonical_exact line 26
  3. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedCanonical_count line 47
  4. def OAI.ExactQuantumFactoring.TransitionWords.readNet line 62
  5. lemma OAI.ExactQuantumFactoring.TransitionWords.readNet_eval line 64
  6. def OAI.ExactQuantumFactoring.TransitionWords.firstOnly line 69

    Source documentation

    A polynomial-size literal shape check, including the otherwise-unused last word. It does not construct the unknown canonical CRT residue.

    def firstOnly {k n K : ℕ} (a : BooleanNetwork k n) : BooleanNetwork k (n*(K+1)) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  7. lemma OAI.ExactQuantumFactoring.TransitionWords.firstOnly_eval line 71
  8. def OAI.ExactQuantumFactoring.NodeMachine.retainedCanonicalList line 85
  9. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedCanonicalList_exact line 90