OAI/Computability/QuantumFactoring/ListSamplerCircuit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.ListSampler.work line 18
  2. abbrev OAI.ExactQuantumFactoring.ListSampler.width line 19
  3. def OAI.ExactQuantumFactoring.ListSampler.word line 21
  4. lemma OAI.ExactQuantumFactoring.ListSampler.word_input line 26
  5. lemma OAI.ExactQuantumFactoring.ListSampler.word_mask line 30
  6. lemma OAI.ExactQuantumFactoring.ListSampler.word_sample line 36
  7. lemma OAI.ExactQuantumFactoring.ListSampler.word_work line 43
  8. lemma OAI.ExactQuantumFactoring.ListSampler.packed_word line 48
  9. def OAI.ExactQuantumFactoring.ListSampler.maskRegister line 54
  10. lemma OAI.ExactQuantumFactoring.ListSampler.maskRegister_val line 63
  11. lemma OAI.ExactQuantumFactoring.ListSampler.word_register line 65
  12. lemma OAI.ExactQuantumFactoring.ListSampler.word_replace line 74
  13. def OAI.ExactQuantumFactoring.ListSampler.circuit line 102

    Source documentation

    A single family (depending only on n) prepares the manuscript's exact runtime-b(n,m) fair sample. No Hadamard is chosen by a metalevel value of m.

    def circuit (n : ℕ) : List (Instruction (width n)) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ListSampler.width

  14. lemma OAI.ExactQuantumFactoring.ListSampler.circuit_length line 107
  15. lemma OAI.ExactQuantumFactoring.ListSampler.circuit_state line 114
  16. lemma OAI.ExactQuantumFactoring.ListSampler.word_injective line 129
  17. lemma OAI.ExactQuantumFactoring.ListSampler.circuit_mass line 137

    Source documentation

    Born events in the actual prepared register are exactly the b(n,m)-bit fair events, retaining the original input, mask and all clean work wires.

    lemma circuit_mass (n : ℕ) (m : Basis n) (P : Basis (width n)→Prop) :
    outcomeMass P ((programMatrix (circuit n)).mulVec
      (basisVector (word m (fun _ => false) (fun _ => false))))=
    outcomeMass (fun y => P (word m ((listMaskNet n).eval m)
      (padBits (Nat.clog_le_of_le_pow (bitsValue m).isLt.le) y)))
      (fairState (Nat.clog 2 (bitsValue m).toNat)) := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.ListSampler.width, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.ListSampler.circuit, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.ListSampler.word, OAI.ExactQuantumFactoring.listMaskNet, OAI.ExactQuantumFactoring.padBits, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.fairState