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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Decision corollaries for the actual compiled fluid experiments. The sole new premise is the separately cited finite-machine halting input. The particle events and their equivalence to halting are proved from the compiled Navier–Stokes main results, including uniqueness of material flow.

  1. def OAI.ForcedComputation.MaterialEvent line 22

    Source documentation

    The designated particle of the prescribed fluid enters the open set.

    def MaterialEvent (V : Velocity) (a : Space) (O : Set Space) : Prop :=
…
  2. theorem OAI.ForcedComputation.materialEvent_iff line 25
  3. def OAI.ForcedComputation.particleRightHalf line 36
  4. theorem OAI.ForcedComputation.initialized_material_event_iff line 38
  5. theorem OAI.ForcedComputation.fixed_particle_material_event_iff line 46
  6. theorem OAI.ForcedComputation.stationary_material_event_iff line 54
  7. theorem OAI.ForcedComputation.slow_material_event_iff line 61
  8. theorem OAI.ForcedComputation.prefix_material_event_iff line 69
  9. theorem OAI.ForcedComputation.periodic_material_event_iff line 77