OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingFiniteGraph.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

A finite, decidable graph for one expanding-array stage. Its lookup examines the guarded local table and bounded integer stacks only. The injectivity theorem applies to every defined address, including addresses outside the initialized computation.

  1. def OAI.ForcedComputation.ExpandingDetector.localDisplacement line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.moveCode_localDisplacement line 16
  3. def OAI.ForcedComputation.ExpandingDetector.BoundedIntegerStep line 20
  4. instance OAI.ForcedComputation.ExpandingDetector.(instance at line 30) line 30
  5. theorem OAI.ForcedComputation.ExpandingDetector.boundedIntegerStep_iff line 50
  6. structure OAI.ForcedComputation.ExpandingDetector.RecorderAddress line 69
  7. def OAI.ForcedComputation.ExpandingDetector.RecorderAddress.toAddress line 76
  8. def OAI.ForcedComputation.ExpandingDetector.RecorderAddress.number line 82
  9. theorem OAI.ForcedComputation.ExpandingDetector.RecorderAddress.number_bounds line 86
  10. theorem OAI.ForcedComputation.ExpandingDetector.RecorderAddress.number_injective line 92
  11. def OAI.ForcedComputation.ExpandingDetector.stageEdge line 102
  12. instance OAI.ForcedComputation.ExpandingDetector.(instance at line 107) line 107
  13. theorem OAI.ForcedComputation.ExpandingDetector.stageEdge_integer line 114
  14. theorem OAI.ForcedComputation.ExpandingDetector.stageEdge_source_unique line 121
  15. theorem OAI.ForcedComputation.ExpandingDetector.stageEdge_target_unique line 129
  16. def OAI.ForcedComputation.ExpandingDetector.recorderAddresses line 137
  17. theorem OAI.ForcedComputation.ExpandingDetector.mem_recorderAddresses line 143
  18. def OAI.ForcedComputation.ExpandingDetector.lookupTarget line 150
  19. theorem OAI.ForcedComputation.ExpandingDetector.lookupTarget_eq_some_iff line 155
  20. theorem OAI.ForcedComputation.ExpandingDetector.lookupTarget_injective line 173