OAI/Computability/QuantumFactoring/ZeroOutside.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.zeroOutside line 18

    Source documentation

    A linear-size clean-work flag, leaving every protected input bit alone.

    def zeroOutside {q : ℕ} (I : Finset (Fin q)) : BooleanNetwork q 1 :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  2. lemma OAI.ExactQuantumFactoring.zeroOutside_value line 21
  3. lemma OAI.ExactQuantumFactoring.zeroOutside_count line 34
  4. lemma OAI.ExactQuantumFactoring.zeroOutside_sector line 46
  5. lemma OAI.ExactQuantumFactoring.tensorLayout_zero line 59
  6. lemma OAI.ExactQuantumFactoring.PhysicalTree.launchZero_suffix line 71
  7. lemma OAI.ExactQuantumFactoring.PhysicalTree.paddedZero_suffix line 76
  8. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterZero_clean line 87
  9. def OAI.ExactQuantumFactoring.PhysicalTree.zeroNet line 113

    Source documentation

    The zero reflection's flag depends only on the length and the actual clean work coordinates, never on the unknown integer or its factorization.

    def zeroNet (n : ℕ) : BooleanNetwork (quarterWidth n) 1 := zeroOutside (inputWires n)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.PhysicalTree.quarterWidth, OAI.ExactQuantumFactoring.zeroOutside, OAI.ExactQuantumFactoring.PhysicalTree.inputWires

  10. lemma OAI.ExactQuantumFactoring.PhysicalTree.zeroNet_count line 115
  11. lemma OAI.ExactQuantumFactoring.PhysicalTree.zeroNet_sector line 118