OAI/Computability/QuantumFactoring/PhysicalCompletionOutput.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.Completion.totalWidth line 18
  2. def OAI.ExactQuantumFactoring.Completion.rareWires line 20
  3. def OAI.ExactQuantumFactoring.Completion.ordinaryWires line 22
  4. def OAI.ExactQuantumFactoring.Completion.guessWires line 24
  5. def OAI.ExactQuantumFactoring.Completion.retentionWires line 26
  6. lemma OAI.ExactQuantumFactoring.Completion.rareWires_eval line 29
  7. lemma OAI.ExactQuantumFactoring.Completion.ordinaryWires_eval line 34
  8. lemma OAI.ExactQuantumFactoring.Completion.guessWires_eval line 39
  9. lemma OAI.ExactQuantumFactoring.Completion.retentionWires_eval line 44
  10. def OAI.ExactQuantumFactoring.Completion.rareNet line 50
  11. lemma OAI.ExactQuantumFactoring.Completion.rareNet_eval line 52
  12. lemma OAI.ExactQuantumFactoring.Completion.rareNet_count line 56
  13. def OAI.ExactQuantumFactoring.Completion.outputNet line 65

    Source documentation

    Runtime output selection retains the entire unused ordinary computation even on the rare branch. Neither success statistics nor future auxiliary data enter this network.

    def outputNet {q W : ℕ} (ordinary : BooleanNetwork q W) (t d : ℕ) :
    BooleanNetwork (totalWidth q W t d) W :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Completion.totalWidth

  14. lemma OAI.ExactQuantumFactoring.Completion.outputNet_eval line 69
  15. lemma OAI.ExactQuantumFactoring.Completion.outputNet_count line 74
  16. def OAI.ExactQuantumFactoring.Completion.zeros line 83

    Source documentation

    Constant-zero fresh blocks are explicit gates, rather than analytical initialization assumptions about the raw sampler layout.

    def zeros (k m : ℕ) : BooleanNetwork k m := vector (fun _ => constant false)

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  17. lemma OAI.ExactQuantumFactoring.Completion.zeros_eval line 84
  18. lemma OAI.ExactQuantumFactoring.Completion.zeros_count line 87
  19. def OAI.ExactQuantumFactoring.Completion.initialNet line 90
  20. lemma OAI.ExactQuantumFactoring.Completion.initialNet_eval line 93
  21. lemma OAI.ExactQuantumFactoring.Completion.initialNet_count line 97