ParticleDecisionCorollaries.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Undecidability of the compiled particle experiments, conditional only on the separately cited finite-machine halting input.

theorem OAI.ForcedComputation.initialized_particle_undecidable line 12
Source documentation
379-01, the undecidability corollary for the initialized experiment.
```
theorem initialized_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (machineVelocity I hI) ![1 / 8, 3 / 8, 1 / 2] particleRightHalf) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.machineVelocity, OAI.ForcedComputation.particleRightHalf
theorem OAI.ForcedComputation.fixed_particle_undecidable line 19
Source documentation
379-02, the fixed-particle undecidability corollary.
```
theorem fixed_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (fixedParticleVelocity I hI) ![1 / 8, 3 / 8, 0] particleRightHalf) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.fixedParticleVelocity, OAI.ForcedComputation.particleRightHalf
theorem OAI.ForcedComputation.stationary_particle_undecidable line 26
Source documentation
379-03, eventual stationarity does not make the particle event decidable.
```
theorem stationary_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (stationaryVelocity I hI) stationaryStartingPoint
        stationaryObserver) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.stationaryVelocity, OAI.ForcedComputation.stationaryStartingPoint, OAI.ForcedComputation.stationaryObserver
theorem OAI.ForcedComputation.slow_particle_undecidable line 34
Source documentation
379-08, the logarithmic-clock particle event remains undecidable.
```
theorem slow_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (torusSlowVelocity I hI) ![1 / 4, 1 / 2, 1 / 2] particleRightHalf) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.torusSlowVelocity, OAI.ForcedComputation.particleRightHalf
theorem OAI.ForcedComputation.prefix_particle_undecidable line 41
Source documentation
The interspersed-history prefix experiment has no total decision algorithm.
```
theorem prefix_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (prefixVelocity I hI) ![1 / 8, 1 / 4, 1 / 4] particleRightHalf) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.prefixVelocity, OAI.ForcedComputation.particleRightHalf
theorem OAI.ForcedComputation.periodic_particle_undecidable line 48
Source documentation
Repeating the initializer does not make the material observation decidable.
```
theorem periodic_particle_undecidable (hT : FiniteMachineHaltingUndecidable)
    {ν : ℝ} (hν : 0 < ν) :
    NoCompiledInputDecider (fun I hI =>
      MaterialEvent (periodicVelocity I hI) ![1 / 4, 1 / 2, 1 / 4]
        {x | 1 / 2 < x 0 ∧ x 0 < 7 / 8}) :=
…
```
Mentions: OAI.ForcedComputation.FiniteMachineHaltingUndecidable, OAI.ForcedComputation.NoCompiledInputDecider, OAI.ForcedComputation.MaterialEvent, OAI.ForcedComputation.periodicVelocity