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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Decision corollaries for the prescribed forces and their actual classical solutions. The observation predicates mention neither machines nor halting.

  1. def OAI.ForcedComputation.VelocityDetector.TorusVelocityEvent line 15
  2. def OAI.ForcedComputation.VelocityDetector.compiledTorusDetectorForce line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.torus_velocity_event_iff line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.torus_velocity_undecidable line 42

    Source documentation

    The compact-chart velocity event is undecidable on the finite source inputs.

    theorem torus_velocity_undecidable (hT : FiniteMachineHaltingUndecidable)
    (hE : TorusScalarExistence) (hK : TorusHeatInput)
    (hv : ∀ I hI Ω,
      IsPlanarTransition (planarSlice (Recorder.Planar.normalizedHamiltonian I hI)) Ω →
      PlanarVariations (planarSlice (Recorder.Planar.normalizedHamiltonian I hI)) Ω)
    (hback : ∀ I hI Ω,
      IsPlanarTransition (planarSlice (Recorder.Planar.normalizedHamiltonian I hI)) Ω →
      ContDiff ℝ ∞ (fun y : ℝ × Plane => Ω y.1 (-y.1) y.2))
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      TorusVelocityEvent ν (compiledTorusDetectorForce ν I hI)) := by
…

    Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.VelocityDetector.TorusScalarExistence, OAI.ForcedComputation.VelocityDetector.TorusHeatInput, OAI.ForcedComputation.IsPlanarTransition, OAI.ForcedComputation.planarSlice, OAI.ForcedComputation.Recorder.Planar.normalizedHamiltonian, OAI.ForcedComputation.PlanarVariations, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.VelocityDetector.TorusVelocityEvent, OAI.ForcedComputation.VelocityDetector.compiledTorusDetectorForce

  5. def OAI.ForcedComputation.VelocityDetector.PlaneVelocityEvent line 60
  6. theorem OAI.ForcedComputation.VelocityDetector.plane_velocity_event_iff line 64
  7. theorem OAI.ForcedComputation.VelocityDetector.plane_velocity_undecidable line 78

    Source documentation

    The whole-plane integral event is undecidable for every positive viscosity.

    theorem plane_velocity_undecidable (hT : FiniteMachineHaltingUndecidable)
    (hE : PlaneScalarExistence) (hEnergy : CylinderLocalEnergyIdentity) :
    ∃ C : ℕ, 1 ≤ C ∧ ∀ (ν : ℝ), 0 < ν → ∀ (a : ℕ → ℚ), IsFastRealName a ν →
      NoCompiledInputDecider (fun I hI =>
        PlaneVelocityEvent ν (ExpandingDetector.compiledExpandingForce C I hI a ν)) := by
…

    Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.VelocityDetector.PlaneScalarExistence, OAI.ForcedComputation.VelocityDetector.CylinderLocalEnergyIdentity, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.VelocityDetector.PlaneVelocityEvent, OAI.ForcedComputation.ExpandingDetector.compiledExpandingForce