OAI/Computability/UniqueGames/Machines/PoweringGlobalEnumerationLemmas.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Explicit executable enumeration of the global powering tapes

The four header tapes come first, followed by the eleven shared roles, the bounded trajectory tapes, and the final output tape. Both directions use constructor cases and arithmetic sum encodings. No enumeration is selected from a cardinality theorem.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 24
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 36

    Source documentation

    The single extra output tape occupies its unique local index.

    def unitTapeEquiv : Unit ≃ Fin 1 where
…
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 42
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 45
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 49

    Source documentation

    Exact arithmetic numbering of every physical global tape.

    def globalTapeEquiv (max : Nat) : GlobalTape max ≃ Fin (4 + (11 + max + 1)) :=
…
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 53

    Source documentation

    The executable equivalence consumed by Finish and DrainMany.

    def enumeration (max : Nat) : Fin (4 + (11 + max + 1)) ≃ GlobalTape max :=
…
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 56
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 60
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 64
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 67
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 70
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 73
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 76
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 79
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 82
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 86

    Source documentation

    The exact cardinality follows from the explicit executable bijection.

    theorem card_globalTape (max : Nat) :
    Fintype.card (GlobalTape max) = 4 + (11 + max + 1) := by
…
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 90
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 95

    Source documentation

    A fixed finite list of all tape names is available without ambient search.

    def allTapes (max : Nat) : List (GlobalTape max) := List.ofFn (enumeration max)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.enumeration

  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 97
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 100
  21. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 121
  22. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.State line 122
  23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.Label line 123
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 125
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 129
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 135
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.endpoint line 145
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 148
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.bit line 155
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.instruction line 159
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.afterWord line 168
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 174
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.steps line 182
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 188
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 205

    Source documentation

    Table, start, scratch and both comparison stacks satisfy these numerical inequalities, so their contents are preserved without an emptiness premise.

    theorem finalTapes_frame (placement : PoweringMachineTapes.Tape max → K) (distinct : Function.Injective placement)
    (path : List (Fin d)) (lengthBound : path.length ≤ max)
    (port : Fin d) (left right : PortTables.Label)
    (table : PortTables.Table n d) (vertex : Fin n) (base : K → List Bool)
    (role : Fin 11) (h₂ : role ≠ 2) (h₃ : role ≠ 3) (h₄ : role ≠ 4)
    (h₆ : role ≠ 6) (h₁₀ : role ≠ 10) :
    finalTapes placement path lengthBound port left right table vertex base (placement (.inl role)) =
      base (placement (.inl role)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.finalTapes

  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 224

    Source documentation

    Any caller tape outside the shared placement is preserved, including a separate accumulator for already completed output rows.

    theorem finalTapes_other (placement : PoweringMachineTapes.Tape max → K)
    (path : List (Fin d)) (lengthBound : path.length ≤ max)
    (port : Fin d) (left right : PortTables.Label)
    (table : PortTables.Table n d) (vertex : Fin n) (base : K → List Bool)
    (k : K) (outside : ∀ i, k ≠ placement i) :
    finalTapes placement path lengthBound port left right table vertex base k = base k := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.finalTapes

  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 237
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRelationField.steps_le line 294
  39. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.Tape line 312
  40. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.State line 313
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.Label line 315
  42. instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.labelFintype line 319
  43. instance OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.labelDecidableEq line 322
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.entry line 325
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.instruction line 329
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.finalTapes line 338
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.steps line 348
  48. structure OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.Ready line 352
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.finalTapes_role line 360
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.ready_finalTapes line 375
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.finalTapes_other line 392
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.fieldTrace line 405
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.finalTapes_output line 427
  54. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Command line 463
  55. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 464
  56. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Label line 465
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.entry line 467
  58. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.instruction line 471
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.result line 478
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.finalTapes line 482
  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.steps line 486
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.planTrace line 491
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 517
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 530
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 552

    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.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Command

  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 559
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 564
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement line 590

    Source documentation

    The existing word placement, with its result directed to row-output 10.

    def headerPlacement {t max : Nat} (h : t ≤ max) : PoweringMachineWord.Tape t → Tape max :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.Tape

  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_injective line 593
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_table line 597
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_query line 601
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scan line 605
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_reverse line 609
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scratch line 613
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_output line 617
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_start line 621
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_succ line 625
  78. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.Label line 629
  79. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.entry line 632
  80. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry line 634
  81. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction line 637
  82. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.instruction line 645

    Source documentation

    Only the coefficient, word, and direction are built into finite control.

    def instruction (n : Nat) (h : n + 1 ≤ max) (placement : Tape max → K)
    (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (labels : Label n → Λ) (exit : Option Λ) :
    Label n → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
  | .inl q => affineInstruction (placement (start max)) (placement (scratch max))
      (placement (rowOutput max)) (blockSize d n) (reverseOffset d n ports direction)
      (fun z => labels (.inl z)) (some (labels (tailEntry n direction))) q
  | .inr (.inl q) => PoweringMachineWord.copyInstruction
      (placement (start max)) (placement (scratch max)) (placement (rowOutput max))
      (fun z => labels (.inr (.inl z))) exit q
  | .inr (.inr q) => PoweringMachineWord.instruction (n + 1)
      (placement ∘ headerPlacement h) ports (fun z => labels (.inr (.inr z))) exit q

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.copyInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineWord.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement

  83. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.afterReverse line 658
  84. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes line 663
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.steps line 672
  86. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.headerTrace line 680

    Source documentation

    Compose the actual affine and word/copy instructions. The trace and both header values are derived; the only data premises describe the physical input.

    theorem headerTrace (input : PortTables.Table vertices d) (n : Nat) (h : n + 1 ≤ max)
    (placement : Tape max → K) (distinct : Function.Injective placement)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (labels : Label n → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
    (atLabels : ∀ l, program (labels l) = instruction n h placement ports direction labels exit l)
    (base : K → List Bool) (tableWord : base (placement (table max)) = PortTables.tableBits input)
    (scratchEmpty : base (placement (scratch max)) = []) (suffix : List Bool)
    (sourceWord : base (placement (start max)) = encodeWord vertex.val ++ suffix)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps input n vertex ports direction]
      (some ⟨some (labels (entry n)), (ambient, register), base⟩) =
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.entry

  87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_other line 752
  88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_shared line 777

    Source documentation

    In particular, table 0, start 1, scratch 5, and saved endpoint/copy tapes 6--9 survive the header phase. Only roles 2, 3, 4, 10 and trajectory tapes may change.

    theorem finalTapes_shared (input : PortTables.Table vertices d) (n : Nat) (h : n + 1 ≤ max)
    (placement : Tape max → K) (distinct : Function.Injective placement)
    (vertex : Fin vertices) (ports : Fin (n + 1) → Fin d)
    (direction : Bool) (base : K → List Bool) (i : Fin 11)
    (hquery : i ≠ 2) (hscan : i ≠ 3) (hreverse : i ≠ 4) (houtput : i ≠ 10) :
    finalTapes input n h placement vertex ports direction base (placement (.inl i)) =
      base (placement (.inl i)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes

  89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.steps_le line 792

    Source documentation

    Linear in the serialized input length for the fixed word length.

    theorem steps_le (input : PortTables.Table vertices d) (n : Nat) (vertex : Fin vertices)
    (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    steps input n vertex ports direction ≤
      (14 * (n + 1) + 4) * (PortTables.tableBits input).length + 12 * (n + 1) + 6 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.steps

  90. def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRowHeaders.machine line 810

    Source documentation

    A closed finite-control instance. Embedded uses instantiate instruction on the caller's common tapes and preserve its larger ambient register.

    def machine (degree n : Nat) (ports : Fin (n + 1) → Fin degree) (direction : Bool) : FinTM2 where
…