OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarInitialShift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The rational normalization of the planar initial condition. The fresh machine starts in a nonhalting band, so the normalization preserves the fixed halting strip and the unit-speed spatial clock on all coding rectangles.

  1. theorem OAI.ForcedComputation.Recorder.Planar.compression_le_real line 17
  2. theorem OAI.ForcedComputation.Recorder.Planar.point_horizontal_bound line 22
  3. theorem OAI.ForcedComputation.Recorder.Planar.point_vertical_bound line 36
  4. def OAI.ForcedComputation.Recorder.Planar.initialShift line 51
  5. def OAI.ForcedComputation.Recorder.Planar.shiftPoint line 54
  6. theorem OAI.ForcedComputation.Recorder.Planar.initialShift_spec line 56
  7. theorem OAI.ForcedComputation.Recorder.Planar.initialShift_small line 63
  8. theorem OAI.ForcedComputation.Recorder.Planar.fresh_initial_nonhalting line 83
  9. theorem OAI.ForcedComputation.Recorder.Planar.initialShift_small_rat line 90
  10. theorem OAI.ForcedComputation.Recorder.Planar.shifted_nonhalting_height line 100
  11. theorem OAI.ForcedComputation.Recorder.Planar.shifted_halting_clearance line 117

    Source documentation

    Halting points have the paper's fixed clearance from both edges of the observer, including the rational initial normalization.

    theorem shifted_halting_clearance (M : Alternating.Machine) (hM : M.WellFormed)
    (C : Configuration (State M) (Alphabet M)) (δ : Fin 2 → ℚ)
    (hh : recorderHalting M C.control = true) (hδ : |(δ 1 : ℝ)| ≤ 3 / 1024) :
    1 / 16 ≤ shiftPoint δ (point M hM C) 1 ∧
      shiftPoint δ (point M hM C) 1 ≤ 3 / 32 := by
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.Configuration, OAI.ForcedComputation.Recorder.State, OAI.ForcedComputation.Recorder.Alphabet, OAI.ForcedComputation.Recorder.recorderHalting, OAI.ForcedComputation.Recorder.Planar.shiftPoint, OAI.ForcedComputation.Recorder.Planar.point

  12. theorem OAI.ForcedComputation.Recorder.Planar.shifted_point_observer_iff line 132
  13. theorem OAI.ForcedComputation.Recorder.Planar.shifted_coding_rectangle_clock line 154
  14. theorem OAI.ForcedComputation.Recorder.Planar.shifted_instruction_source_clock line 175
  15. theorem OAI.ForcedComputation.Recorder.Planar.shifted_instruction_target_clock line 183
  16. theorem OAI.ForcedComputation.Recorder.Planar.shifted_run_observer_iff line 191
  17. theorem OAI.ForcedComputation.Recorder.Planar.normalized_run_observer_iff line 203