OAI/Computability/MaxCut/Machines/Input.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Serialization boundaries and direct row lookup for the shared executable fixed-alphabet graph codec. The alphabet is a fixed parameter. Rows remain in their stored order, including repeated darts and loops. Word offsets are fixed; bit offsets are represented by actual encoded prefixes because unary fields have data-dependent lengths. These are data identities, not runtime certificates.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowWidth line 32
  2. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowOffset line 35

    Source documentation

    Offset measured in natural-word fields, including the two header fields.

    def rowOffset (q e : Nat) : Nat := 2 + rowWidth q * e

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowWidth

  3. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowsWords_split line 38

    Source documentation

    Exact decomposition before, at, and after a selected stored row.

    theorem rowsWords_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) :
    rows.flatMap rowWords = (rows.take e).flatMap rowWords ++
      (rowWords rows[e] ++ (rows.drop (e + 1)).flatMap rowWords) := by
…
  4. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowsBits_split line 49

    Source documentation

    The unary serialization keeps exactly the same row boundaries, with separate encoded prefixes rather than an assumed constant bit offset.

    theorem rowsBits_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) :
    encodeWords (rows.flatMap rowWords) =
      encodeWords ((rows.take e).flatMap rowWords) ++
        (encodeWords (rowWords rows[e]) ++
          encodeWords ((rows.drop (e + 1)).flatMap rowWords)) := by
…
  5. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowsBits_append_split line 59

    Source documentation

    A selected row can be followed by an arbitrary caller-owned suffix.

    theorem rowsBits_append_split (rows : List (DartRow q n m)) (e : Nat)
    (he : e < rows.length) (suffix : List Bool) :
    encodeWords (rows.flatMap rowWords) ++ suffix =
      encodeWords ((rows.take e).flatMap rowWords) ++
        (encodeWords (rowWords rows[e]) ++
          (encodeWords ((rows.drop (e + 1)).flatMap rowWords) ++ suffix)) := by
…
  6. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.prefixWords line 68
  7. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.suffixWords line 71
  8. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.prefixWords_length line 74
  9. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_at_row line 79
  10. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableBits_at_row line 88
  11. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableBits_header line 95

    Source documentation

    Removing precisely the two encoded header words exposes the stored rows.

    theorem tableBits_header (table : Table q) :
    tableBits table = encodeWord table.vertices ++
      (encodeWord table.darts ++ encodeWords ((rowList table).flatMap rowWords)) := by
…
  12. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_row line 100
  13. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_take_row line 107
  14. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_tail line 113
  15. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_reverse line 118
  16. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_relation line 123
  17. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.relationWords_get line 129
  18. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_relation line 134
  19. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_predicate line 144
  20. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.rowOffset_lt_length line 151
  21. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Input.relationOffset_lt_length line 159
  22. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Alphabet line 179
  23. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Ports line 181
  24. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label line 183
  25. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList line 188
  26. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_getElem?_ctorIdx_eq line 191
  27. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_nodup line 195
  28. instance OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.(instance at line 197) line 197
  29. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.statement line 201
  30. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.resultTapes line 220
  31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.resultTapes_other line 229
  32. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.setupInTime line 237

    Source documentation

    Actual program placement is the only execution premise. Header values and unread row bits specify the input, and every auxiliary role starts empty.

    def setupInTime (ports : Ports K) (distinct : Function.Injective ports)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Ports, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Alphabet

  33. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.tableSetupInTime line 329

    Source documentation

    Specialization to the checked graph-table codec. The bound follows from the actual copy and delimiter-scan traces above.

    def tableSetupInTime {q : Nat} (ports : Ports K) (distinct : Function.Injective ports)
    (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Ports, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.Alphabet

  34. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.program line 356
  35. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Setup.machine line 360

    Source documentation

    This stage itself has only seven tapes and nine control labels.

    def machine : FinTM2 where
…
  36. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 388
  37. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.State line 389
  38. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 392

    Source documentation

    The relation register is a finite tuple of bits, with no unbounded storage.

    def relationEquiv (q : Nat) : RelationTable q ≃ (Fin (q * q) → Bool) where
…
  39. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 399

    Source documentation

    Executable enumeration used when assembling the finite machine state.

    @[instance_reducible] def relationFintype (q : Nat) : Fintype (RelationTable q) :=
…
  40. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 402
  41. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 408

    Source documentation

    Read one encoded Boolean into a fixed slot of the finite relation register.

    def readSlot (source : K) (i : Fin (q * q))
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q)) :
…

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

  42. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 418
  43. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 428
  44. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 434
  45. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 437
  46. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 443
  47. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 455
  48. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 468
  49. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 475
  50. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 488

    Source documentation

    Each stored register bit is obtained from its actual serialized field.

    theorem stepAux_readSlots (source : K) (indices : List (Fin (q * q)))
    (relation : RelationTable q)
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q))
…

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

  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 505

    Source documentation

    Fixed finite program fragment; it can be inserted before any continuation.

    def readRelation (source : K)
    (next : TM2.Stmt (Alphabet (K := K)) Λ (State σ q)) :
…

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

  52. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 510
  53. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 521
  54. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 535
  55. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 545
  56. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.parser line 551
  57. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 556
  58. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 561
  59. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 576

    Source documentation

    One transition executes the fixed chain of q*q slot readers.

    theorem parserTrace (source : K) (readLabel exitLabel : Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ q))
…

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

  60. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 588
  61. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer line 622
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 624
  63. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.readSlots line 630
  64. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill line 640

    Source documentation

    Proof-level description of the finite register updates.

    def fill (slots : List (Fin N)) (bits buffer : Buffer N) : Buffer N :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer

  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 643
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill_all line 654
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 662

    Source documentation

    The input symbols are physically popped; the remaining suffix is exact.

    theorem stepAux_readSlots (src : K) (slots : List (Fin N))
    (next : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N))
    (ambient : σ) (bits buffer : Buffer N) (tapes : K → List Bool)
    (suffix : List Bool) :
    TM2.stepAux (readSlots src slots next) (ambient, buffer)
        (Function.update tapes src (slots.map bits ++ suffix)) =
      TM2.stepAux next (ambient, fill slots bits buffer)
        (Function.update tapes src suffix) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.readSlots, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.fill

  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 678
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 692
  70. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 702

    Source documentation

    The slot list is a fixed part of the syntax; each instruction reads only the finite internal state. Push order is reversed on the stack.

    def writeSlots {M : Nat} (dst : K) (emit : σ → Buffer M) : List (Fin M) →
    TM2.Stmt (fun _ : K => Bool) Λ σ → TM2.Stmt (fun _ : K => Bool) Λ σ
  | [], next => next
  | i :: slots, next => .push dst (fun state => emit state i) (writeSlots dst emit slots next)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer

  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 707
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 722
  73. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 740

    Source documentation

    Read a fixed block, write its fixed finite transformation, reset the local register, and execute the next finite statement.

    def blockStmt (src dst : K) (F : Buffer N → Buffer M)
    (next : TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N)) :
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer

  74. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.finishAt line 747
  75. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 752
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 756
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 763
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 771
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 787

    Source documentation

    The suffix and all unmentioned tapes are preserved, and the local register is reset, in the actual transition semantics.

    theorem stepAux_blockMapAt (src dst : K) (F : Buffer N → Buffer M)
    (exit : Option Λ) (hne : src ≠ dst) (bits : Buffer N) (suffix : List Bool)
    (state : σ × Buffer N) (tapes : K → List Bool)
    (hinput : tapes src = List.ofFn bits ++ suffix) :
    TM2.stepAux (blockMapAt src dst F exit) state tapes =
      { l := exit, var := (state.1, emptyBuffer N),
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer

  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 799

    Source documentation

    Placement in an arbitrary program gives one actual TM2 transition.

    theorem step_blockMapAt (src dst : K) (F : Buffer N → Buffer M)
    (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Buffer N))
    (label : Λ) (hprogram : program label = blockMapAt src dst F exit)
    (hne : src ≠ dst) (bits : Buffer N) (suffix : List Bool)
    (state : σ × Buffer N) (tapes : K → List Bool)
    (hinput : tapes src = List.ofFn bits ++ suffix) :
    TM2.step program { l := some label, var := state, stk := tapes } =
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer, OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt

  81. def OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.machine line 818

    Source documentation

    The fixed block map is also a concrete machine with two Boolean tapes and a finite register, independently of any ambient placement.

    def machine {N M : Nat} (F : Buffer N → Buffer M) : FinTM2 where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer

  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 829