OAI/Computability/UniqueGames/PCP/EmitRows.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

The actual alphabet-reduction row template. The old predicate and the loop flag are finite registers. All unbounded quantities reside in five preserved unary tapes. The fixed event/slot/orientation order is retained without deduplication.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.Context line 18
  2. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 19
  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 21
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn line 26
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn line 31
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 40
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 49

    Source documentation

    Two actual affine fields followed by the 4096 stored relation entries.

    def rowCommands (q : Nat) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (orientation : Bool) : List (RowCommand q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.RowCommand

  8. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 58
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 62
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.encodedRow line 68
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 76

    Source documentation

    The executable command semantics equals the precise stored row, including the orientation-specific tail, reverse index, and every predicate bit.

    theorem rowCommands_bits {q : Nat} (input : GenericGraphTables.Table q)
    (edge : Fin input.darts) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (orientation : Bool) :
    (rowCommands q event slot orientation).flatMap
      (commandBits (rowValues input edge) (rowContext input edge)) =
      encodeWords (GraphTables.rowWords
        (Table.rowFromDart input (((edge, event), slot), orientation))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowCommands, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowValues, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowContext, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.rowWords, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.rowFromDart

  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 109

    Source documentation

    One old dart emits every local event, then all six slots, false orientation before true. These loops are fixed by q and form part of the finite template.

    def blockCommands (q : Nat) : List (RowCommand q) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.RowCommand

  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 114
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 121
  15. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 134

    Source documentation

    Headers use only the preserved n and m tapes; all relation registers may still have their initial values.

    def headerCommands (q : Nat) (σ : Type) : List (Command 2 σ (Addresses.fieldBound q)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound

  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 140
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 154
  18. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 158
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap line 183
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 189
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 196
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le line 204
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 215
  24. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 229

    Source documentation

    Actual execution of all rows belonging to one old dart. The finite relation register is supplied by the checked row parser; only code equations are assumed about the enclosing program. The trace restores the five operand tapes.

    def blockInTime {K Λ : Type} [DecidableEq K] {q : Nat}
    (input : GenericGraphTables.Table q) (edge : Fin input.darts)
    (sources : Fin 5 → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label (blockCommands q).length (Addresses.fieldBound q) → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State (Context q)))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommands, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.Context

  25. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 259

    Source documentation

    Preserve additional finite parser/driver registers through a projection.

    def blockCommandsIn {σ : Type} (q : Nat) (context : σ → Context q) :
    List (Command 5 σ (Addresses.fieldBound q)) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.Context, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Addresses.fieldBound

  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 263
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 272