OAI/Computability/UniqueGames/Machines/MachineSubdivisionBody.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

One whole occurrence iteration of the actual subdivision controller. The proved trace includes both endpoint loads, the dynamic full-table reader, the four-row template, all three local drains, and private-index increments.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.tableBits line 21
  2. structure OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.Ready line 24
  3. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterU line 33
  4. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterV line 37
  5. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterTable line 41
  6. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.rowPayload line 45
  7. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterRows line 50
  8. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterDrainU line 55
  9. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterDrainV line 59
  10. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.afterDrainTable line 63
  11. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.incrementTapes line 67
  12. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.bodyResult line 73
  13. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.bodyBudget line 77
  14. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.rowField_ne_scratch line 86
  15. theorem OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.rowField_ne_accumulator line 89
  16. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.incrementInTime line 92
  17. def OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.bodyInTime line 103

    Source documentation

    Complete actual .startU → .guard execution, without a phase-run premise.

    def bodyInTime {q : Nat} (base : Tape → List Bool) (u v : Nat)
    (table : Target.PermutationTable q) (suffix : List Bool)
    (ready : Ready base u v table suffix) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some .startU, initialState, base⟩
      (some ⟨some .guard, initialState, bodyResult base u v table suffix⟩)
      (bodyBudget base u v table suffix) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.Ready, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.bodyResult, OAI.UniqueGamesTheorem.Explicit.MachineSubdivisionBody.bodyBudget