OAI/Computability/QuantumFactoring/PhysicalTreeMachine.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.NodeMachine line 20

    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 NodeMachine (n c : ℕ) where
…
  2. abbrev OAI.ExactQuantumFactoring.NodeMachine.initWork line 27
  3. abbrev OAI.ExactQuantumFactoring.NodeMachine.updateWork line 28
  4. abbrev OAI.ExactQuantumFactoring.NodeMachine.width line 30
  5. def OAI.ExactQuantumFactoring.NodeMachine.current line 34
  6. def OAI.ExactQuantumFactoring.NodeMachine.currentNet line 38
  7. def OAI.ExactQuantumFactoring.NodeMachine.initNet line 39
  8. lemma OAI.ExactQuantumFactoring.NodeMachine.initNet_count line 41
  9. def OAI.ExactQuantumFactoring.NodeMachine.updateNet line 44
  10. lemma OAI.ExactQuantumFactoring.NodeMachine.updateNet_count line 47
  11. def OAI.ExactQuantumFactoring.NodeMachine.program line 50
  12. def OAI.ExactQuantumFactoring.NodeMachine.initial line 56
  13. abbrev OAI.ExactQuantumFactoring.NodeMachine.Trace line 60
  14. instance OAI.ExactQuantumFactoring.NodeMachine.traceFintype line 63
  15. def OAI.ExactQuantumFactoring.NodeMachine.next line 68
  16. def OAI.ExactQuantumFactoring.NodeMachine.config line 70
  17. def OAI.ExactQuantumFactoring.NodeMachine.encoded line 74
  18. def OAI.ExactQuantumFactoring.NodeMachine.state line 79
  19. lemma OAI.ExactQuantumFactoring.NodeMachine.current_encoded line 83
  20. lemma OAI.ExactQuantumFactoring.NodeMachine.initNet_encoded line 88
  21. lemma OAI.ExactQuantumFactoring.NodeMachine.updateNet_encoded line 91
  22. theorem OAI.ExactQuantumFactoring.NodeMachine.program_state line 100

    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

  23. lemma OAI.ExactQuantumFactoring.NodeMachine.encoded_injective line 128
  24. lemma OAI.ExactQuantumFactoring.NodeMachine.width_eq line 146
  25. lemma OAI.ExactQuantumFactoring.NodeMachine.program_length line 151