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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite planar addresses for the expanding velocity detector. The index is computed from a state and two bounded stacks; it never requires executing the selected run. The next layer can enumerate every address.

  1. structure OAI.ForcedComputation.ExpandingDetector.Address line 11
  2. def OAI.ForcedComputation.ExpandingDetector.Address.index line 17
  3. theorem OAI.ForcedComputation.ExpandingDetector.Address.index_positive line 20
  4. theorem OAI.ForcedComputation.ExpandingDetector.Address.index_le line 24
  5. theorem OAI.ForcedComputation.ExpandingDetector.Address.index_injective line 35
  6. def OAI.ForcedComputation.ExpandingDetector.Address.finIndex line 57
  7. theorem OAI.ForcedComputation.ExpandingDetector.Address.finIndex_injective line 60