OAI/Computability/QuantumFactoring/PhysicalSplitDecoder.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.FixedSplit.launchWires line 20
  2. def OAI.ExactQuantumFactoring.FixedSplit.allOrderWires line 22
  3. def OAI.ExactQuantumFactoring.FixedSplit.modulusNet line 24
  4. def OAI.ExactQuantumFactoring.FixedSplit.actualBaseNet line 25
  5. def OAI.ExactQuantumFactoring.FixedSplit.actualOrderRawNet line 27
  6. def OAI.ExactQuantumFactoring.FixedSplit.actualOrderNet line 29
  7. lemma OAI.ExactQuantumFactoring.FixedSplit.launchWires_eval line 32
  8. lemma OAI.ExactQuantumFactoring.FixedSplit.allOrderWires_eval line 34
  9. lemma OAI.ExactQuantumFactoring.FixedSplit.modulusNet_eval line 36
  10. lemma OAI.ExactQuantumFactoring.FixedSplit.actualBaseNet_eval line 39
  11. lemma OAI.ExactQuantumFactoring.FixedSplit.actualOrderRawNet_eval line 42
  12. lemma OAI.ExactQuantumFactoring.FixedSplit.actualOrderNet_eval line 46
  13. def OAI.ExactQuantumFactoring.FixedSplit.liftedModulus line 53
  14. def OAI.ExactQuantumFactoring.FixedSplit.actualPairs line 55
  15. def OAI.ExactQuantumFactoring.FixedSplit.divisorNet line 61

    Source documentation

    Supplied divisor computed from exactly this run's retained quantum bits. All guarded arithmetic is explicit, including full rare-branch order guesses.

    def divisorNet (n : ℕ) : BooleanNetwork (width n) (n+1) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.FixedSplit.width

  16. theorem OAI.ExactQuantumFactoring.FixedSplit.divisorNet_value line 64