OAI/Computability/QuantumFactoring/BitStackPrograms.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

A literal finite Boolean-stack compiler for circuit descriptions. Branches inspect and consume one symbol, not an entire encoded word. Operational derivations below count actual finite-state TM2 transitions.

  1. inductive OAI.ExactQuantumFactoring.BitStackProgram.Program line 16
  2. def OAI.ExactQuantumFactoring.BitStackProgram.Node line 23
  3. instance OAI.ExactQuantumFactoring.BitStackProgram.nodeFintype line 29
  4. def OAI.ExactQuantumFactoring.BitStackProgram.entry line 41
  5. abbrev OAI.ExactQuantumFactoring.BitStackProgram.Store line 46
  6. abbrev OAI.ExactQuantumFactoring.BitStackProgram.Config line 47
  7. def OAI.ExactQuantumFactoring.BitStackProgram.configured line 48
  8. def OAI.ExactQuantumFactoring.BitStackProgram.jump line 49
  9. def OAI.ExactQuantumFactoring.BitStackProgram.dispatch line 51
  10. def OAI.ExactQuantumFactoring.BitStackProgram.statement line 56
  11. inductive OAI.ExactQuantumFactoring.BitStackProgram.Runs line 77
  12. lemma OAI.ExactQuantumFactoring.BitStackProgram.iterate_step line 94
  13. lemma OAI.ExactQuantumFactoring.BitStackProgram.iterate_comp line 96
  14. lemma OAI.ExactQuantumFactoring.BitStackProgram.dispatch_nil line 102
  15. lemma OAI.ExactQuantumFactoring.BitStackProgram.dispatch_false line 108
  16. lemma OAI.ExactQuantumFactoring.BitStackProgram.dispatch_true line 114
  17. theorem OAI.ExactQuantumFactoring.BitStackProgram.compile_runs line 121
  18. def OAI.ExactQuantumFactoring.BitStackProgram.machine line 194
  19. lemma OAI.ExactQuantumFactoring.BitStackProgram.machine_alphabets_finite line 208
  20. def OAI.ExactQuantumFactoring.BitStackProgram.singletonStore line 212
  21. def OAI.ExactQuantumFactoring.BitStackProgram.machine_outputs line 215