OAI/Computability/UniqueGames/PCP/CleanupLemmas.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-stack cleanup. Each selected stack is drained using the checked pop loop, followed by one transition resetting the finite state. Repeated selections are allowed; they only reduce the cost upper bound.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet line 23
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.finish line 26

    Source documentation

    Reset both the ambient finite state and the drain register before exiting.

    def finish (initial : σ) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.instruction line 32

    Source documentation

    A concrete instruction for each of the n drain phases and the final reset.

    def instruction {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ) (phase : Fin (n + 1)) :
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.instruction_drain line 41
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.instruction_finish line 49
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes line 55

    Source documentation

    Actual tape family after the selected stacks have been drained in order.

    def clearTapes : {n : Nat} → (Fin n → K) → (K → List Bool) → K → List Bool
  | 0, _, base => base
  | n + 1, selected, base =>
      clearTapes (fun i : Fin n => selected i.succ) (Function.update base (selected 0) [])

/-- Exact number of transitions, including the final state-reset transition. -/
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.actualCost line 61

    Source documentation

    Exact number of transitions, including the final state-reset transition.

    def actualCost : {n : Nat} → (Fin n → K) → (K → List Bool) → Nat
  | 0, _, _ => 1
  | n + 1, selected, base =>
      actualCost (fun i : Fin n => selected i.succ) (Function.update base (selected 0) []) +
        ((base (selected 0)).length + 1)
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_apply line 67
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_selected line 80
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_unselected line 84
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.actualCost_le line 90
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.cleanupTrace line 108

    Source documentation

    The trace is derived solely from the actual drain instructions and final reset instruction. No execution of the entire cleanup is assumed.

    theorem cleanupTrace {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.cleanupInTime line 134

    Source documentation

    Actual cleanup execution, bounded using the original selected-stack lengths.

    def cleanupInTime {n : Nat} (selected : Fin n → K) (labels : Fin (n + 1) → Λ)
    (initial : σ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.program, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.program line 151

    Source documentation

    Concrete n+1-label program, terminating after resetting the finite state.

    def program {n : Nat} (selected : Fin n → K) (initial : σ) :
    Fin (n + 1) → TM2.Stmt (Alphabet (K := K)) (Fin (n + 1)) (σ × Option Bool) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.Alphabet

  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.machine line 156

    Source documentation

    A bundled finite machine. Its input/output tapes are designated explicitly.

    def machine [Fintype K] [Fintype σ] {n : Nat} (selected : Fin n → K)
    (input output : K) (initial : σ) : FinTM2 where
…
  16. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.machineInTime line 168
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_outputOnly line 181

    Source documentation

    Enumerating exactly the nonoutput stacks yields the standard final tape family. Repeated selected stacks are permitted.

    theorem clearTapes_outputOnly {n : Nat} (selected : Fin n → K)
    (output : K) (base : K → List Bool)
    (excludesOutput : ∀ i, selected i ≠ output)
    (coversOther : ∀ k, k ≠ output → ∃ i, selected i = k) :
    clearTapes selected base = fun k => if k = output then base output else [] := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.clearTapes

  18. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime line 195

    Source documentation

    Full cleanup reaches haltList, with all nonoutput stacks empty and the machine's actual initial finite state restored.

    def machineHaltInTime [Fintype K] [Fintype σ] {n : Nat} (selected : Fin n → K)
    (input output : K) (initial : σ) (base : K → List Bool)
    (ambient : σ) (register : Option Bool)
    (excludesOutput : ∀ i, selected i ≠ output)
    (coversOther : ∀ k, k ≠ output → ∃ i, selected i = k) :
    StateTransition.EvalsToInTime (machine selected input output initial).step
      ⟨some (0 : Fin (n + 1)), (ambient, register), base⟩
      (some (haltList (machine selected input output initial) (base output)))
      ((∑ i, (base (selected i)).length) + n + 1) := by
…

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

  19. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 222
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.skipBits line 227

    Source documentation

    A fixed finite chain skips Boolean unary words. A true head causes one additional delimiter pop; a false head is already the complete zero word. Only the one-bit head register is examined.

    def skipBits (source : K) : Nat →
    TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool) →
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 238
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 255
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 269
  24. inductive OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label line 277
  25. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label.enumList line 281
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_getElem?_ctorIdx_eq line 284
  27. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_nodup line 288
  28. instance OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.(instance at line 290) line 290
  29. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.statement line 296

    Source documentation

    Six fixed control labels implement row selection. q fixes the finite predicate parser; no data-dependent number is placed in the program syntax.

    def statement (q : Nat) (counter source destination : K) (labels : Label → Λ)
    (exit : Option Λ) : Label → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  30. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.program line 305
  31. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowBits line 309
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 311
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 316
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 319
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 321
  36. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.skipCost line 325
  37. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 328
  38. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 331
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 345

    Source documentation

    One skipped row: two actual unary scans followed by one finite predicate statement. All registers are reset and every other tape is untouched.

    theorem skipRowTrace (base : K → List Bool) (row : DartRow q n m) (suffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step P))^[row.tail.val + row.reverseIndex.val + 3]
      (some ⟨some (labels .skipTail), (ambient, register),
        Function.update base source (rowBits row ++ suffix)⟩) =
      some ⟨some (labels .guard), (ambient, none), Function.update base source suffix⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowBits

  40. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 374
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 388
  42. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 408

    Source documentation

    Exact successful row lookup. The only data premise is the literal table prefix; no lookup result or whole execution is postulated.

    theorem lookupTailTrace
    (hcs : counter ≠ source) (hcd : counter ≠ destination) (hsd : source ≠ destination)
    (base : K → List Bool) (prior : List (DartRow q n m)) (row : DartRow q n m)
    (counterSuffix suffix output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step P))^[lookupCost prior row]
      (some ⟨some (labels .guard), (ambient, register),
        MachineLookup.tapes counter source destination base
          (encodeWord prior.length ++ counterSuffix)
          (rowsBits prior ++ (rowBits row ++ suffix)) output⟩) =
      some ⟨exit, (ambient, none),
        MachineLookup.tapes counter source destination base
          (encodeWord 0 ++ counterSuffix)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupCost, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowBits

  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 478

    Source documentation

    The number of actual transitions is linear in the scanned encoding and the unary row index. Fixed predicate statements contribute one transition.

    theorem lookupCost_le {q n m : Nat} (prior : List (DartRow q n m)) (row : DartRow q n m) :
    lookupCost prior row ≤ (rowsBits prior ++ rowBits row).length +
      2 * (encodeWord prior.length).length + 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupCost, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowsBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.rowBits

  44. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 498

    Source documentation

    The exact row-selection trace packaged with its linear transition budget.

    def lookupTailInTime {q n m : Nat}
    (counter source destination : K) (labels : Label → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 523

    Source documentation

    The input's actual stored row vector determines the selected row. This specialization derives the literal lookup prefix from the checked codec.

    theorem tableTailTrace {q : Nat}
    (counter source destination : K) (labels : Label → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  46. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 558

    Source documentation

    Two real delimiter-scanning loops remove the header of the copied table before the row counter starts. The protected original table can occupy any other tape in base and is unchanged.

    theorem fullTableTailTrace {q : Nat}
    (counter source destination : K) (labels : Label → Λ) (exit : Option Λ)
    (headerVertices headerDarts : Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  47. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 598
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 604
  49. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 608
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headIndex line 631
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headValue line 634
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 639

    Source documentation

    The looked-up endpoint is the head of the actual graph semantics, including paired loop darts whose reverse index differs from their own index.

    theorem headValue_eq_semantics {q : Nat} (table : Table q) (e : Fin table.darts) :
    headValue table e = ((semantics table).head e).val := rfl

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headValue

  53. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 642
  54. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 644
  55. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 653
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 657
  57. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 666
  58. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 669
  59. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 761
  60. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 766
  61. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 772
  62. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 777
  63. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 783
  64. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 789
  65. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 795
  66. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 801
  67. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 804
  68. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 811
  69. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 823

    Source documentation

    Read both unary fields using actual copy loops, then execute the checked fixed predicate parser. Only the two field destinations must initially be empty; the cursor suffix and every unrelated tape are retained exactly.

    def readRowInTime {q n m : Nat} (source tail reverse : K)
    (hst : source ≠ tail) (hsr : source ≠ reverse) (htr : tail ≠ reverse)
    (tailStart tailLoop reverseStart reverseLoop readLabel exitLabel : Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (ReadRelation.State σ q))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.Alphabet, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.ReadRelation.State

  70. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Lookup.machine line 909

    Source documentation

    A concrete finite machine instance, with input-dependent unary values located only on its three tapes.

    def machine (q : Nat) : FinTM2 where
…