OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/VelocityDecisionDischarge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The velocity-decision main results with machine undecidability, smooth flow dependence and localized energy identity discharged.

  1. theorem OAI.ForcedComputation.VelocityDetector.torus_velocity_undecidable_parabolic line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.torus_velocity_undecidable_scalar line 30

    Source documentation

    Only the scalar advection-diffusion existence input remains.

    theorem torus_velocity_undecidable_scalar
    (hE : TorusScalarExistence) {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      TorusVelocityEvent ν (compiledTorusDetectorForce ν I hI)) :=
…

    Mentions: OAI.ForcedComputation.VelocityDetector.TorusScalarExistence, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.VelocityDetector.TorusVelocityEvent, OAI.ForcedComputation.VelocityDetector.compiledTorusDetectorForce

  3. theorem OAI.ForcedComputation.VelocityDetector.plane_velocity_undecidable_scalar line 36