OAI/Computability/QuantumFactoring/PhysicalMachine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.oracleOn_encode line 18
  2. lemma OAI.ExactQuantumFactoring.appendPrepared_state_dependent line 27
  3. structure OAI.ExactQuantumFactoring.SplitMachine line 42

    Source documentation

    A bit-level finite-state controller. Both transition functions are literal Boolean networks; this structure does not grant any classical computation oracle.

    structure SplitMachine (n c : ℕ) where
…
  4. abbrev OAI.ExactQuantumFactoring.SplitMachine.initWork line 49
  5. abbrev OAI.ExactQuantumFactoring.SplitMachine.updateWork line 50
  6. abbrev OAI.ExactQuantumFactoring.SplitMachine.width line 52
  7. def OAI.ExactQuantumFactoring.SplitMachine.current line 56
  8. def OAI.ExactQuantumFactoring.SplitMachine.currentNet line 60
  9. def OAI.ExactQuantumFactoring.SplitMachine.initNet line 61
  10. lemma OAI.ExactQuantumFactoring.SplitMachine.initNet_count line 63
  11. def OAI.ExactQuantumFactoring.SplitMachine.updateNet line 66
  12. lemma OAI.ExactQuantumFactoring.SplitMachine.updateNet_count line 69
  13. def OAI.ExactQuantumFactoring.SplitMachine.program line 72
  14. def OAI.ExactQuantumFactoring.SplitMachine.initial line 78
  15. abbrev OAI.ExactQuantumFactoring.SplitMachine.Trace line 82
  16. instance OAI.ExactQuantumFactoring.SplitMachine.traceFintype line 85
  17. def OAI.ExactQuantumFactoring.SplitMachine.next line 90
  18. def OAI.ExactQuantumFactoring.SplitMachine.config line 92
  19. def OAI.ExactQuantumFactoring.SplitMachine.encoded line 96
  20. def OAI.ExactQuantumFactoring.SplitMachine.state line 101
  21. lemma OAI.ExactQuantumFactoring.SplitMachine.current_encoded line 105
  22. lemma OAI.ExactQuantumFactoring.SplitMachine.initNet_encoded line 110
  23. lemma OAI.ExactQuantumFactoring.SplitMachine.updateNet_encoded line 113
  24. theorem OAI.ExactQuantumFactoring.SplitMachine.program_state line 122

    Source documentation

    The actual adaptive quantum history, not a table of independent counterfactual branches. Every update and next modulus comes from this run.

    theorem program_state (x : Basis c) (t : ℕ) :
    (programMatrix (M.program t)).mulVec (basisVector (M.initial t x))=
      encodeState (M.encoded x t) (M.state x t) := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.encodeState

  25. lemma OAI.ExactQuantumFactoring.SplitMachine.encoded_injective line 150
  26. lemma OAI.ExactQuantumFactoring.SplitMachine.width_eq line 168
  27. lemma OAI.ExactQuantumFactoring.SplitMachine.program_length line 173