OAI/Computability/MaxCut/Machines/PoweringMachineField.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The concrete finite program that produces an entire powered-row input block. Its static control executes the field plan backwards, so prepending each computed unary Boolean field leaves the canonical serialized block in order.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.Tape line 13
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.State line 14
  3. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.Label line 16
  4. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.labelFintype line 20
  5. instance OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.labelDecidableEq line 23
  6. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.entry line 26
  7. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.instruction line 30
  8. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.finalTapes line 39
  9. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.steps line 49
  10. structure OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.Ready line 53
  11. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.finalTapes_role line 61
  12. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.ready_finalTapes line 76
  13. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.finalTapes_other line 93
  14. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.fieldTrace line 106
  15. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachineField.finalTapes_output line 128
  16. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.Command line 164
  17. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 165
  18. abbrev OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.Label line 166
  19. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.entry line 168
  20. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.instruction line 172
  21. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.result line 179
  22. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.finalTapes line 183
  23. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.steps line 187
  24. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.planTrace line 192
  25. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 218
  26. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 231
  27. def OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 253

    Source documentation

    Each command of the actual row plan has a fixed bound of twice the radius.

    def boundedRowPlan (n : Nat) (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    List (Command d (2 * (n + 1))) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.Command

  28. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 260
  29. theorem OAI.MaxCutGames.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 265