OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/RapidMachineHaltingDischarge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

All three rapid-forcing decision inputs follow from Mathlib's halting theorem. The universal machine is fixed; its program argument is encoded in the finite input word.

  1. theorem OAI.ForcedComputation.list_val_computable line 16
  2. theorem OAI.ForcedComputation.rapidMachineHaltingUndecidable line 21
  3. theorem OAI.ForcedComputation.alternatingMachineHaltingUndecidable line 37
  4. theorem OAI.ForcedComputation.lattice_constructor_computable line 56
  5. theorem OAI.ForcedComputation.lattice_input_computable line 62
  6. theorem OAI.ForcedComputation.lattice_input_valid line 67
  7. theorem OAI.ForcedComputation.lattice_undecidable_of_universal line 74
  8. theorem OAI.ForcedComputation.latticeMachineHaltingUndecidable line 95