OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedPlanarOrbit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The same machine-only body processes every input point. Quantitative orbit bounds make the all-time cube guard independent of the choice of compact vertical cutoff.

  1. def OAI.ForcedComputation.BalancedPlanar.inputPosition line 14

    Source documentation

    The input point is rational and can be used as the loading target.

    def inputPosition (I : Alternating.MachineInput) (hI : Alternating.ValidInput I) : Fin 2 → ℚ :=
…

    Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput

  2. theorem OAI.ForcedComputation.BalancedPlanar.inputCode_rational line 17
  3. theorem OAI.ForcedComputation.BalancedPlanar.inputCode_bounds line 26
  4. theorem OAI.ForcedComputation.BalancedPlanar.inputCode_in_unit line 45
  5. theorem OAI.ForcedComputation.BalancedPlanar.inputCode_loader_guard line 57
  6. theorem OAI.ForcedComputation.BalancedPlanar.body_periodic line 64
  7. theorem OAI.ForcedComputation.BalancedPlanar.body_nonhalting_corridor line 68
  8. theorem OAI.ForcedComputation.BalancedPlanar.body_halting_clearance line 108