OAI/Computability/UniqueGames/Machines/GraphCounterStartLemmas.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Actual archive-copy and unary-header addition before the embedded logarithm machine. The two header values stay on tapes; they never enter finite control.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startExtra line 22
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startMemory line 27
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startMemory_input_update line 31
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startMemory_sum_update line 39
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.headerStep_zero line 47
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.headerStep_succ line 61
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.headerTrace line 78
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.headerInTime line 95
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.initialMemory line 107
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockInitialMemory line 117
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startInTime line 132

    Source documentation

    Exact handoff from the genuine machine input to the actual logarithm machine, with the original graph word protected in the archive.

    def startInTime (n m : Nat) (rest : List Bool) :
    StateTransition.EvalsToInTime machine.step
      (initList machine (encodeWords [n, m] ++ rest))
      (some (clockConfiguration (startExtra rest (encodeWords [n, m] ++ rest)) none
        (initList MachineLogCounter.machine (encodeWord (n + m)))))
      (2 * ((encodeWords [n, m] ++ rest).length + 1) + 1 + (n + 1) + (m + 1)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.clockConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterModel.startExtra, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineLogCounter.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.rawOutput line 201
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.rawInTime line 204
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.count line 228
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.output line 230
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.rowsBits line 233
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 236
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 240
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 246
  20. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.Tape line 271
  21. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.Label line 275
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.labelAt line 282
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.statement line 287

    Source documentation

    Place one of finitely many actual statements into an arbitrary ambient Boolean-tape program, preserving the ambient state component.

    def statement (tape : Tape k → K) (labels : Label k → Λ) (exit : Option Λ) :
    Label k → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
  | .seed j => .push (tape (.current j)) (fun _ => false)
      (.goto (fun _ => labels (.copyOut j)))
  | .copyOut j => Reduction.MachineTransfer.loopAt (tape .radix) (tape .scratch)
      id false (labels (.copyOut j)) (some (labels (.copyBack j)))
  | .copyBack j => MachineCopy.forkLoop (tape .scratch) (tape .radix) (tape (.remaining j))
      false (labels (.copyBack j)) (some (labels (.trim j)))
  | .trim j => .pop (tape (.remaining j)) (fun state _ => state)
      (.goto (fun _ => labelAt labels (j.val+1)))
  | .done => .load (fun state => (state.1,none))
      (Reduction.MachineTransfer.exitAt (tape .radix) exit)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.Label, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.exitAt

  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.digitOutput line 300
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.digitOutput_frame line 305
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.digitInTime line 315
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes line 366
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes_frame line 371
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes_current line 383
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes_remaining line 406
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.prefixInTime line 429

    Source documentation

    Place the actual finite initialization prefix inside an ambient program.

    def prefixInTime (m : Nat) (hm : 0 < m) (base : K → List Bool)
    (hradix : base (tape .radix) = encodeWord m)
    (hcurrent : ∀j, base (tape (.current j)) = [])
    (hremaining : ∀j, base (tape (.remaining j)) = [])
    (hscratch : base (tape .scratch) = []) (ambient : σ) (r : Nat) (hr : r ≤ k) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labelAt labels 0),(ambient,none),base⟩
      (some ⟨some (labelAt labels r),(ambient,none),stageTapes tape m base r⟩)
      (r*(2*m+6)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes

  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.initializeInTime line 463

    Source documentation

    Complete actual initialization, including width zero and the optional continuation. The radix, scratch, ambient state and unrelated tapes survive.

    def initializeInTime (m : Nat) (hm : 0 < m) (base : K → List Bool)
    (hradix : base (tape .radix) = encodeWord m)
    (hcurrent : ∀j, base (tape (.current j)) = [])
    (hremaining : ∀j, base (tape (.remaining j)) = [])
    (hscratch : base (tape .scratch) = []) (ambient : σ) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labelAt labels 0),(ambient,none),base⟩
      (some ⟨exit,(ambient,none),stageTapes tape m base k⟩)
      (k*(2*m+6)+1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.labelAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.stageTapes

  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.output_current line 486
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.output_remaining line 492
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.output_radix line 498
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOdometerInit.output_scratch line 504
  37. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.Alphabet line 518
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.finish line 520
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.emitStatement line 526

    Source documentation

    The fixed literal push chain executes in one TM2 transition.

    def emitStatement (destination : K) (offset : Nat) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.Alphabet

  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.emitStep line 530
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.prefix_encodeWord line 541
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.registerEmitTrace line 546

    Source documentation

    Caller-program form of the full exact trace. No execution premise is used.

    theorem registerEmitTrace (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch) (offset : Nat)
    (firstLabel secondLabel emitLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.Alphabet

  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.registerEmitInTime line 576

    Source documentation

    Timed witness retaining the exact 2*n+5-transition execution.

    def registerEmitInTime (source destination scratch : K)
    (sourceDestination : source ≠ destination) (sourceScratch : source ≠ scratch)
    (destinationScratch : destination ≠ scratch) (offset : Nat)
    (firstLabel secondLabel emitLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.Alphabet

  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.program line 600

    Source documentation

    The three labels are transfer, restore-and-copy, and fixed-offset emission.

    def program (source destination scratch : K) (offset : Nat) (exit : Option (Fin 3)) :
    Fin 3 → TM2.Stmt (Alphabet (K := K)) (Fin 3) (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.Alphabet

  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.programInTime line 608
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.machine line 624

    Source documentation

    Three Boolean stacks, three labels, and one optional Boolean register.

    def machine (offset : Nat) : FinTM2 where
…
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.machineInTime line 635
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.emitStatement_pushes line 647
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.program_pushes_le line 653
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.machine_pushes_le line 667

    Source documentation

    The fixed offset is included in the finite program's push bound.

    theorem machine_pushes_le (offset : Nat) :
    Runtime.programPushBound (machine offset) ≤ max 2 offset := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.Runtime.programPushBound, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegisterEmit.machine

  51. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.Tape line 693
  52. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.Symbols line 694
  53. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.Label line 697
  54. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.Register line 698
  55. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.State line 699
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstStates line 701
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondStates line 708
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondLabels line 715
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.bridgeLabel line 721
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstStatement line 724
  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondStatement line 729
  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.program line 737
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.machine line 753
  64. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstConfiguration line 780
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondConfiguration line 786
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstStep line 795
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondStep line 825
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstConfiguration_init line 850
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondConfiguration_halt line 867
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.temporaryTapes line 885
  71. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.temporaryConfiguration line 891
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstTransfer_tapes line 896
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondTransfer_tapes line 915
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.firstTransfer line 938
  75. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.secondTransfer line 959
  76. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.execute line 977

    Source documentation

    An execution of each component yields an actual execution of the combined machine. The two transfer loops add exactly twice the intermediate length plus two.

    def execute (first second : FinTM2)
    (relabel : first.Γ first.k₁ → second.Γ second.k₀)
    (fallback : second.Γ second.k₀)
    (input : List (first.Γ first.k₀)) (middle : List (first.Γ first.k₁))
    (output : List (second.Γ second.k₁)) (firstBudget secondBudget : Nat)
    (runFirst : TM2OutputsInTime first input (some middle) firstBudget)
    (runSecond : TM2OutputsInTime second (middle.map relabel) (some output) secondBudget) :
    TM2OutputsInTime (machine first second relabel fallback) input (some output)
      (firstBudget + 2 * (middle.length + 1) + secondBudget) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.machine

  77. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.compose line 1010

    Source documentation

    General sequential composition with an explicit symbol of the intermediate alphabet to totalize the bridge's unused empty-register expression. Its time polynomial uses the transition-derived output-length bound of the first machine.

    noncomputable def compose {α β γ αΓ βΓ γΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {ec : γ → List γΓ}
    {f : α → β} {g : β → γ}
    (first : TM2ComputableInPolyTime ea eb f)
    (second : TM2ComputableInPolyTime eb ec g) (fallback : βΓ) :
    TM2ComputableInPolyTime ea ec (fun a => g (f a)) := by
…
  78. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.composeBits line 1057