OAI/Computability/SolenoidalRecorder/Checkpoints.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Recording cycles and finite simulation of machine prefixes.

  1. def OAI.Solenoidal.Recorder.checkpoint line 11
  2. theorem OAI.Solenoidal.Recorder.recording_cycle line 16
  3. theorem OAI.Solenoidal.Recorder.checkpoint_next line 112
  4. theorem OAI.Solenoidal.Recorder.checkpoint_count_ge_six line 134
  5. def OAI.Solenoidal.Recorder.initial line 139
  6. theorem OAI.Solenoidal.Recorder.simulate_prefix line 144