OAI/Computability/UniqueGames/PCP/DriverLemmas.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The actual final driver phases: reverse the accumulated output, drain all fifteen nonoutput stacks, reset the finite state, and reach haltList. Polynomial resource bounds below require an actual preceding execution.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.headerPlan line 17
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.rowPlan line 18
  3. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.Label line 20
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.headerEntry line 32
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.rowEntry line 35
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.clearNext line 38
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program line 41
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine line 77

    Source documentation

    Every state component is finite; the q-dependent relation register is enumerated by the explicit vector/function equivalence of the parser.

    def machine (q : Nat) : FinTM2 := by
…
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program_setup line 90
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program_guard line 94
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 97
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program_compare line 101
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program_increment line 104
  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.afterReversal line 119
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 122
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 126
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.finishBudget line 130
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 134

    Source documentation

    The actual driver's reversal loop enters its first cleanup label.

    def reverseInTime (q : Nat) (base : Tape → List Bool) (word : List Bool)
    (state : State q) (hreversed : base .reversed = word.reverse)
    (houtput : base .output = []) :
    StateTransition.EvalsToInTime (Driver.machine q).step
      ⟨some .reverseOutput, state, base⟩
      (some ⟨some (.cleanup 0), (state.1, none), afterReversal base word⟩)
      (word.length + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.afterReversal

  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 148
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 157

    Source documentation

    All remaining driver stacks are actually popped, and the exact initial finite state is restored before the halting configuration is reached.

    def cleanupInTime (q : Nat) (base : Tape → List Bool) (state : State q) :
    StateTransition.EvalsToInTime (Driver.machine q).step
      ⟨some (.cleanup 0), state, base⟩
      (some (haltList (Driver.machine q) (base .output)))
      ((∑ i : Fin 15, (base (cleanupPorts i)).length) + 16) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine

  21. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.finishInTime line 173
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 194
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 202

    Source documentation

    Every stack bound here is derived from the actual preceding driver trace.

    theorem stackLength_after_prefix (q : Nat) (input : List Bool)
    (base : Tape → List Bool) (state : State q) (budget : Nat)
    (prefixRun : StateTransition.EvalsToInTime (Driver.machine q).step
      (initList (Driver.machine q) input) (some ⟨some .reverseOutput, state, base⟩) budget)
    (k : Tape) :
    (base k).length ≤ input.length + budget * Runtime.programPushBound (Driver.machine q) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine

  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 214
  25. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 238

    Source documentation

    A polynomial time allowance for the whole prefixRun followed by actual reversal and cleanup. The fixed push bound belongs to the concrete driver.

    noncomputable def completedPolynomial (q : Nat) (prefixTime : Polynomial Nat) : Polynomial Nat :=
…
  26. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 243
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 259