OAI/Computability/MaxCut/Machines/Lookup.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

The finite registers and physical tape roles of the alphabet-table machine. Input-sized numbers occur only on unary tapes. The comparison and emitter register layouts are related by explicit, executable product rearrangements.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 14
  2. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.skipBits line 19

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  3. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 30
  4. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 47
  5. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 61
  6. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label line 69
  7. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList line 73
  8. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_getElem?_ctorIdx_eq line 76
  9. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_nodup line 80
  10. instance OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.(instance at line 82) line 82
  11. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.statement line 88

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  12. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.program line 97
  13. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits line 101
  14. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 103
  15. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 108
  16. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 111
  17. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 113
  18. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.skipCost line 117
  19. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 120
  20. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 123
  21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 137

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits

  22. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 166
  23. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 180
  24. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 200

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits

  25. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 270

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits

  26. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 290

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  27. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 315

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  28. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 350

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet

  29. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 390
  30. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 396
  31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 400
  32. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headIndex line 423
  33. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headValue line 426
  34. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 431

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headValue

  35. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 434
  36. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 436
  37. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 445
  38. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 449
  39. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 458
  40. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 461
  41. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 553
  42. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 558
  43. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 564
  44. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 569
  45. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 575
  46. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 581
  47. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 587
  48. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 593
  49. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 596
  50. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 603
  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 615

    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.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.State

  52. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Lookup.machine line 701

    Source documentation

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

    def machine (q : Nat) : FinTM2 where
…
  53. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 725
  54. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList line 731
  55. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_getElem?_ctorIdx_eq line 735
  56. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape.enumList_nodup line 739
  57. instance OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 741) line 741
  58. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 745
  59. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 748

    Source documentation

    Self-loop flag, comparison mismatch flag, and second head register.

    abbrev Flags := Bool × Bool × Option Bool
  60. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 749
  61. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.State line 750
  62. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 752
  63. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 755
  64. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.context line 757
  65. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 760
  66. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 767
  67. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 772
  68. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 778
  69. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 781
  70. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 785
  71. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 788
  72. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 792
  73. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 793
  74. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 794
  75. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 796
  76. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 800
  77. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 803
  78. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 825
  79. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 830
  80. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 836

    Source documentation

    Store the result chosen by the actual comparison's equal/different exit. This does not compare tape contents in a register transition.

    def storeLoop (value : Bool) (next : Λ) : TM2.Stmt Alphabet Λ (State q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.State

  81. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 839
  82. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 844
  83. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 848
  84. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 858

    Source documentation

    One-step simulations transport complete timed executions through the explicit finite register permutations.

    def transportInTime {K τ υ : Type} [DecidableEq K] {Γ : K → Type}
    (e : τ ≃ υ) (p : Λ → TM2.Stmt Γ Λ τ)
    {start finish : TM2.Cfg Γ Λ τ} {budget : Nat}
    (run : StateTransition.EvalsToInTime (TM2.step p) start (some finish) budget) :
    StateTransition.EvalsToInTime (TM2.step (MachineControl.program (Equiv.refl Λ) e p))
      (MachineControl.configuration id e start)
      (some (MachineControl.configuration id e finish)) budget := by
…