OAI/Computability/QuantumFactoring/WordBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.wordBlocks line 16

    Source documentation

    Consecutive fixed-width words; construction duplicates a word network at most w times and so has a direct polynomial-size bound.

    def wordBlocks {n s w : ℕ} (f : Fin s → BooleanNetwork n w) : BooleanNetwork n (s*w) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  2. def OAI.ExactQuantumFactoring.BitArithmetic.block line 20
  3. def OAI.ExactQuantumFactoring.BitArithmetic.blockNet line 23
  4. lemma OAI.ExactQuantumFactoring.BitArithmetic.blockNet_eval line 26
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.blockNet_count line 28
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordBlocks_eval line 30
  7. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordBlocks_count line 35
  8. def OAI.ExactQuantumFactoring.BitArithmetic.addMod line 43

    Source documentation

    One extra carry bit before reduction avoids overflow even on noncanonical coefficient representatives; all arrays use exactly as many bits as specified.

    def addMod {n w : ℕ} (a b m : BooleanNetwork n w) : BooleanNetwork n w :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  9. lemma OAI.ExactQuantumFactoring.BitArithmetic.addMod_count line 47
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.addMod_value line 55
  11. def OAI.ExactQuantumFactoring.BitArithmetic.sumMod line 72

    Source documentation

    Linear-length modular accumulation, not a repeated expanded expression.

    def sumMod {n w : ℕ} (m : BooleanNetwork n w) : List (BooleanNetwork n w) → BooleanNetwork n w
  | [] => wordConstant 0
  | a::as => addMod a (sumMod m as) m

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BitArithmetic.wordConstant, OAI.ExactQuantumFactoring.BitArithmetic.addMod

  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.sumMod_value line 76
  13. lemma OAI.ExactQuantumFactoring.BitArithmetic.sumMod_count line 86