OAI/MathematicalPhysics/RapidForcing/Detector.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.addressPath_smooth line 11
  2. lemma OAI.RapidForcing.materialFlow_loading line 15
  3. lemma OAI.RapidForcing.materialFlow_addressPath line 31
  4. lemma OAI.RapidForcing.ScaleData.history_zero line 68
  5. lemma OAI.RapidForcing.ScaleData.history_succ line 71
  6. lemma OAI.RapidForcing.runAddress_center line 76
  7. lemma OAI.RapidForcing.runAddress_mod line 82
  8. lemma OAI.RapidForcing.runAddress_le_D line 86
  9. lemma OAI.RapidForcing.runAddress_nonterminal_end line 90
  10. lemma OAI.RapidForcing.runAddress_nonterminal_first line 103
  11. lemma OAI.RapidForcing.runAddress_terminal_first line 112
  12. theorem OAI.RapidForcing.materialFlow_at_codeTime line 122
  13. lemma OAI.RapidForcing.materialFlow_run_slot line 140
  14. lemma OAI.RapidForcing.materialFlow_nonhalting_first line 149
  15. theorem OAI.RapidForcing.materialFlow_halting_iff line 165
  16. theorem OAI.RapidForcing.addressed_particle_detection line 186