OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PeriodicLoaderGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

A small loading rectangle at the unused initial checkpoint. The incoming checkpoint row is removed; all remaining target rectangles stay separated from the loader, and all sources stay below its fixed source.

  1. theorem OAI.ForcedComputation.Recorder.stateBox_second_bounds line 17
  2. theorem OAI.ForcedComputation.Recorder.codedPoint_second_bounds line 27
  3. theorem OAI.ForcedComputation.Recorder.bandScale_le_real line 46
  4. theorem OAI.ForcedComputation.Recorder.centerY_bounds_real line 50
  5. theorem OAI.ForcedComputation.Recorder.codedPoint_in_compiledCenters line 58
  6. def OAI.ForcedComputation.Recorder.periodicLoaderStart line 83
  7. def OAI.ForcedComputation.Recorder.periodicLoaderRadius line 85
  8. def OAI.ForcedComputation.Recorder.periodicLoaderInstruction line 87
  9. theorem OAI.ForcedComputation.Recorder.periodicLoaderInstruction_image line 92
  10. theorem OAI.ForcedComputation.Recorder.periodicLoader_source_separated line 101
  11. theorem OAI.ForcedComputation.Recorder.periodicLoader_target_separated line 121
  12. def OAI.ForcedComputation.Recorder.filteredGeometricBranches line 151
  13. def OAI.ForcedComputation.Recorder.loadedInput line 156
  14. def OAI.ForcedComputation.Recorder.freshGeometricBranches line 162
  15. def OAI.ForcedComputation.Recorder.periodicLoadedInput line 166
  16. theorem OAI.ForcedComputation.Recorder.periodicLoader_single_valid line 170
  17. theorem OAI.ForcedComputation.Recorder.loadedInput_valid line 183
  18. theorem OAI.ForcedComputation.Recorder.periodicLoadedInput_valid line 201
  19. theorem OAI.ForcedComputation.Recorder.periodicLoadedInput_geometric_mem line 205
  20. theorem OAI.ForcedComputation.Recorder.periodicLoadedInput_used_mem line 218
  21. def OAI.ForcedComputation.Recorder.periodicInitializedInput line 235
  22. theorem OAI.ForcedComputation.Recorder.periodicInitializedInput_valid line 239
  23. theorem OAI.ForcedComputation.Recorder.periodicInitializedInput_height line 243
  24. theorem OAI.ForcedComputation.Recorder.periodicInitializedInput_period line 247