OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarDormantZero.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Every pulse that does not belong to the tracked branch vanishes at its current sparse anchor. The proof uses the actual order of the compiled list.

  1. theorem OAI.ForcedComputation.PlanarRouting.notMem_collar_of_gap line 13
  2. theorem OAI.ForcedComputation.PlanarRouting.extract_before_arithmetic line 18
  3. theorem OAI.ForcedComputation.PlanarRouting.extract_after_arithmetic line 21
  4. theorem OAI.ForcedComputation.PlanarRouting.scale_before_arithmetic line 25
  5. theorem OAI.ForcedComputation.PlanarRouting.scale_after_arithmetic line 29
  6. theorem OAI.ForcedComputation.PlanarRouting.insert_before_arithmetic line 33
  7. theorem OAI.ForcedComputation.PlanarRouting.insert_after_arithmetic line 37
  8. theorem OAI.ForcedComputation.Recorder.Planar.sourceRank_injective line 46
  9. theorem OAI.ForcedComputation.Recorder.Planar.targetRank_injective line 52
  10. theorem OAI.ForcedComputation.Recorder.Planar.centers_before_parking line 58
  11. theorem OAI.ForcedComputation.Recorder.Planar.ordered_source_collar_gap line 70
  12. theorem OAI.ForcedComputation.Recorder.Planar.ordered_target_collar_gap line 84
  13. theorem OAI.ForcedComputation.Recorder.Planar.extractHorizontal_sparse_zero line 101
  14. theorem OAI.ForcedComputation.Recorder.Planar.extractVertical_sparse_zero line 155
  15. theorem OAI.ForcedComputation.Recorder.Planar.scale_sparse_zero line 207
  16. theorem OAI.ForcedComputation.Recorder.Planar.insertVertical_sparse_zero line 260
  17. theorem OAI.ForcedComputation.Recorder.Planar.insertHorizontal_sparse_zero line 311
  18. theorem OAI.ForcedComputation.Recorder.Planar.action_sparseAnchor_notMem_collar line 363
  19. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_notMem_collar line 377