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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite Hamiltonian data for the prescribed initial particle. All branches are translated by the same rational normalization, after adjoining the fresh nonhalting initial state.

  1. def OAI.ForcedComputation.Recorder.Planar.normalizedPulse line 13
  2. theorem OAI.ForcedComputation.Recorder.Planar.normalizedPulse_valid line 18
  3. theorem OAI.ForcedComputation.Recorder.Planar.normalizedPulse_inUnit line 23
  4. def OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian line 47
  5. theorem OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian_valid line 50
  6. theorem OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian_noTime line 54
  7. theorem OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian_unitPeriods line 58
  8. theorem OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian_periodic line 62