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

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The actual finite rational pulse compiler: ordered extraction, four anisotropic shears in each isolated parking column, and ordered insertion.

  1. def OAI.ForcedComputation.PlanarRouting.separationMinimum line 16
  2. theorem OAI.ForcedComputation.PlanarRouting.separationMinimum_pos line 20
  3. theorem OAI.ForcedComputation.PlanarRouting.separationMinimum_le line 34
  4. def OAI.ForcedComputation.Recorder.Planar.branchAt line 50
  5. def OAI.ForcedComputation.Recorder.Planar.branchIndex line 54
  6. theorem OAI.ForcedComputation.Recorder.Planar.branchAt_index line 59
  7. def OAI.ForcedComputation.Recorder.Planar.sourceFamily line 63
  8. def OAI.ForcedComputation.Recorder.Planar.targetFamily line 67
  9. theorem OAI.ForcedComputation.Recorder.Planar.sourceFamily_separation line 71
  10. theorem OAI.ForcedComputation.Recorder.Planar.targetFamily_separation line 78
  11. def OAI.ForcedComputation.Recorder.Planar.routingCollar line 85
  12. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_pos line 89
  13. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_parking_bound line 98
  14. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_source_gap line 105
  15. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_target_gap line 115
  16. inductive OAI.ForcedComputation.Recorder.Planar.Phase line 125
  17. structure OAI.ForcedComputation.Recorder.Planar.Action line 132
  18. def OAI.ForcedComputation.Recorder.Planar.actions line 136
  19. def OAI.ForcedComputation.Recorder.Planar.parkingFor line 141
  20. def OAI.ForcedComputation.Recorder.Planar.Action.primitive line 145
  21. def OAI.ForcedComputation.Recorder.Planar.phaseRectangle line 160
  22. def OAI.ForcedComputation.Recorder.Planar.Action.rectangle line 170
  23. def OAI.ForcedComputation.Recorder.Planar.compiledPulse line 176
  24. theorem OAI.ForcedComputation.Recorder.Planar.compiledPulse_valid line 184
  25. def OAI.ForcedComputation.Recorder.Planar.compiledHamiltonian line 188
  26. theorem OAI.ForcedComputation.Recorder.Planar.compiledHamiltonian_valid line 191
  27. theorem OAI.ForcedComputation.Recorder.Planar.compiledHamiltonian_noTime line 194
  28. theorem OAI.ForcedComputation.Recorder.Planar.compiledHamiltonian_unitPeriods line 197