OAI/Computability/UniqueGames/Machines/MachineProductHeadersFrameLemmas.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Concrete header and initialized work-tape frames for the product machine.

  1. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame line 18

    Source documentation

    All permanent input fields and fixed Horner digits are explicit tape words. The argument is the forward-order emitted already emitted.

    def frame {q : Nat} (H : Instance q) (t : Nat) (emitted : List Bool) : Tape t → List Bool
  | .formula => encodeWords (ProductMachineSemantics.inputTable H)
  | .extra (.inl i) =>
      if i = 0 then encodeWord H.vertices
      else if i = 7 then encodeWord q
      else if i = 8 then encodeWord H.constraints.length
      else if i = 6 then emitted.reverse else []
  | .extra (.inr i) => encodeWord (MachineProductPower.digits i.val)
  | _ => []

    Mentions: OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable, OAI.UniqueGamesTheorem.Explicit.MachineProductPower.digits

  2. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.headerBits line 28
  3. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.baseTapes line 32

    Source documentation

    Canonical frame before the odometer digits are filled.

    def baseTapes {q : Nat} (H : Instance q) (t : Nat) : Tape t → List Bool :=
…
  4. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_accumulator line 35
  5. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_output line 38
  6. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_radix line 41
  7. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_digit line 47
  8. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.power_outside line 52
  9. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_power_clean line 58
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_power_output line 62
  11. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.frame_append line 66
  12. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.initialized_eq line 79

    Source documentation

    The generic odometer initializer has exactly the scheduler's concrete digit frame; all permanent headers and output-emitted bits retain their identity.

    theorem initialized_eq {q : Nat} (H : Instance q) (t : Nat) :
    MachineOdometerInit.stageTapes (initRole t) H.constraints.length (baseTapes H t) t =
      SourceOdometerSchedule.setDigits H.constraints.length (fun _ : Fin t => 0) (baseTapes H t) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.baseTapes

  13. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.powerExit line 107
  14. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.powerInTime line 110
  15. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.alphabetInTime line 126
  16. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.powersInTime line 137
  17. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.inputTapes line 176
  18. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.afterVertices line 180
  19. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.afterAlphabet line 185
  20. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.rawResultTapes line 190
  21. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.resultTapes line 196
  22. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.initList_eq line 202
  23. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.first_result line 210
  24. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.second_result line 223
  25. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.third_result line 236
  26. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.rawHeadersInTime line 249
  27. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.headersInTime line 288

    Source documentation

    The exact runtime machine starts on the complete ordinary target game codec and reaches the seed phase with its untouched row table and three unary headers.

    def headersInTime {q : Nat} (H : Target.Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some ⟨some .seedStart, (((), ()), none), resultTapes H t⟩)
      (H.vertices + q + H.constraints.length + 6) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.resultTapes

  28. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeadersRead.headers_budget line 302
  29. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.seedCommands_nodup line 323
  30. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.seed_result line 329
  31. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.seedBridge line 357
  32. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.seedInTime line 372
  33. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.initializeInTime line 404
  34. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.steps line 418
  35. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.prepareInTime line 425

    Source documentation

    Header reading, literal seed setup, actual Horner power computation, and all odometer digits are supplied by real execution traces of the same program.

    def prepareInTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length)
…
  36. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.timePolynomial line 441
  37. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.steps_le line 446
  38. def OAI.UniqueGamesTheorem.Explicit.MachineProductHeaders.inPolynomialTime line 462

    Source documentation

    Polynomial initialization in the literal incoming instance-code length.

    def inPolynomialTime {q : Nat} (H : Instance q) (t : Nat) :
    StateTransition.EvalsToInTime (machine q t).step
      (initList (machine q t) (gameBits H))
      (some (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length)
…
  39. structure OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.BaseReady line 492
  40. def OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.tupleTapes line 498
  41. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.tupleTapes_frame line 503
  42. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.tupleTapes_current line 515
  43. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.tupleTapes_accumulator line 520
  44. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.tupleTapes_ready line 525
  45. def OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.rowBits line 576
  46. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.input_length line 580
  47. def OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.bodyBound line 587
  48. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.bodyTrace line 592

    Source documentation

    The actual row execution supplies the local obligation of the generic odometer schedule. Its cost is uniformly polynomial in the original bits.

    theorem bodyTrace (H : Target.Instance q) (base : Tape t → List Bool) (ready : BaseReady H base) :
    SourceOdometerSchedule.BodyTrace (program q t) (rowMain q t) (nextCheck q t 0)
      ((), ()) (Sum.inl (6 : Fin 10)) base (rowBits (t := t) H) (bodyBound H t) := by
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.BaseReady, OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.rowBits, OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.bodyBound

  49. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.traversalInTime line 645

    Source documentation

    Complete positive-radix tuple traversal with actual row bodies discharged.

    theorem traversalInTime (H : Target.Instance q) (base : Tape t → List Bool) (ready : BaseReady H base) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step (program q t))
      (SourceOdometerSchedule.initialConfiguration (m := H.constraints.length) t (rowMain q t) ((), ()) base)
…

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductLoop.BaseReady

  50. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.base_ready line 684
  51. def OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.afterRows line 694
  52. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.afterRows_output line 698
  53. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.allRows_eq line 705
  54. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.afterRows_accumulator line 711
  55. def OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.finishInTime line 724

    Source documentation

    The entry hop reaches the actual cleanup list, then all work is drained, the accumulator is reversed, and the final finite register is reset.

    def finishInTime (base : Tape t → List Bool) (emptyOutput : base (output t) = []) :
    StateTransition.EvalsToInTime (TM2.step (program q t))
      ⟨some .finishStart, (((), ()), none), base⟩
      (some ⟨none, (((), ()), none),
        SourceRuntimeFinish.canonicalTapes (output t) (base (accumulator t)).reverse⟩)
      (1 + SourceRuntimeFinish.finishCost (clearKeys t) (accumulator t) base) := by
…
  56. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.finishCost_le_uniform line 746

    Source documentation

    A uniform bound on the real cleanup work, from bounds on actual stacks.

    theorem finishCost_le_uniform (base : Tape t → List Bool) (bound : Nat)
    (bounded : ∀ k, (base k).length ≤ bound) :
    SourceRuntimeFinish.finishCost (clearKeys t) (accumulator t) base ≤
      ((clearKeys t).length + 1) * bound + (clearKeys t).length + 2 := by
…
  57. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductFinish.finish_afterRows line 757