RapidDecisionCorollaries.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The four undecidable material experiments in paper 379-06. Their events refer only to actual material paths and fixed open observation sets.

def OAI.ForcedComputation.RapidMaterialEvent line 16
theorem OAI.ForcedComputation.rapid_material_event_iff line 20
theorem OAI.ForcedComputation.rapid_particle_undecidable line 30
Source documentation
The compact Euclidean rapid-force experiment has no total decider.
```
theorem rapid_particle_undecidable (hT : RapidMachineHaltingUndecidable) :
    ¬ ∃ d : ℕ → Bool, Computable d ∧
      ∀ (M : RapidForcing.Machine) (w : M.Input),
        d (M.inputDescription w) = true ↔
          RapidMaterialEvent (RapidForcing.addressedVelocity M w) := by
…
```
Mentions: OAI.ForcedComputation.RapidMachineHaltingUndecidable, OAI.RapidForcing.Machine, OAI.ForcedComputation.RapidMaterialEvent, OAI.RapidForcing.addressedVelocity
def OAI.ForcedComputation.AlternatingMaterialEvent line 38
theorem OAI.ForcedComputation.alternating_material_event_iff line 43

theorem OAI.ForcedComputation.alternating_particle_undecidable line 56

Source documentation

The alternating-memory rapid-force experiment has no total decider.

theorem alternating_particle_undecidable (hT : AlternatingMachineHaltingUndecidable) :
    ¬ ∃ d : AlternatingNS.Machine × List ℕ → Bool, Computable d ∧
      ∀ (M : AlternatingNS.Machine) (w : List ℕ), M.WellFormed → M.ValidInput w →
        (d (M,w) = true ↔ AlternatingMaterialEvent (AlternatingNS.Construction.velocity M w)) := by
…

Mentions: OAI.ForcedComputation.AlternatingMachineHaltingUndecidable, OAI.AlternatingNS.Machine, OAI.ForcedComputation.AlternatingMaterialEvent, OAI.AlternatingNS.Construction.velocity

def OAI.ForcedComputation.LatticeMaterialEvent line 64
def OAI.ForcedComputation.RapidTorusMaterialEvent line 67
theorem OAI.ForcedComputation.lattice_material_event_iff line 71
theorem OAI.ForcedComputation.rapid_torus_material_event_iff line 81
theorem OAI.ForcedComputation.lattice_particle_undecidable line 98
Source documentation
Both general and solenoidal lattice forces drive this same material event.
```
theorem lattice_particle_undecidable (hT : LatticeMachineHaltingUndecidable) :
    ¬ ∃ d : PeriodicLattice.Input → Bool, Computable d ∧
      ∀ I : PeriodicLattice.Input, I.WellFormed → (d I = true ↔ LatticeMaterialEvent (PeriodicLattice.FluidLift.velocity I)) := by
…
```
Mentions: OAI.ForcedComputation.LatticeMachineHaltingUndecidable, OAI.PeriodicLattice.Input, OAI.ForcedComputation.LatticeMaterialEvent, OAI.PeriodicLattice.FluidLift.velocity
theorem OAI.ForcedComputation.rapid_torus_particle_undecidable line 105
Source documentation
The solenoidal mean-zero rapid-force experiment on the torus is undecidable.
```
theorem rapid_torus_particle_undecidable (hT : LatticeMachineHaltingUndecidable) :
    ¬ ∃ d : PeriodicLattice.Input → Bool, Computable d ∧
      ∀ I : PeriodicLattice.Input, I.WellFormed → (d I = true ↔ RapidTorusMaterialEvent
        (PeriodicLattice.RapidTorus.transformedField (PeriodicLattice.FluidLift.velocity I))) := by
…
```
Mentions: OAI.ForcedComputation.LatticeMachineHaltingUndecidable, OAI.PeriodicLattice.Input, OAI.ForcedComputation.RapidTorusMaterialEvent, OAI.PeriodicLattice.RapidTorus.transformedField, OAI.PeriodicLattice.FluidLift.velocity