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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A machine-only planar body for the Euclidean box test. Normalize using one fixed empty input, then encode every other input at its own point in the same body. The one-period realization theorems hold for every configuration.

  1. def OAI.ForcedComputation.BalancedPlanar.referenceInput line 15

    Source documentation

    The empty input fixes the spatial normalization of the repeated body.

    def referenceInput (M : Alternating.Machine) : Alternating.MachineInput := (M, [])

    Mentions: OAI.Alternating.Machine, OAI.Alternating.MachineInput

  2. theorem OAI.ForcedComputation.BalancedPlanar.referenceValid line 17
  3. def OAI.ForcedComputation.BalancedPlanar.bodyHamiltonian line 23
  4. def OAI.ForcedComputation.BalancedPlanar.bodyVelocity line 26
  5. def OAI.ForcedComputation.BalancedPlanar.bodyCode line 29
  6. def OAI.ForcedComputation.BalancedPlanar.inputCode line 33
  7. def OAI.ForcedComputation.BalancedPlanar.referenceShift line 36
  8. theorem OAI.ForcedComputation.BalancedPlanar.referenceShift_small line 39
  9. theorem OAI.ForcedComputation.BalancedPlanar.body_step line 44
  10. theorem OAI.ForcedComputation.BalancedPlanar.body_step_safe line 51
  11. theorem OAI.ForcedComputation.BalancedPlanar.body_step_corridor line 59
  12. theorem OAI.ForcedComputation.BalancedPlanar.body_observation line 67