OAI/Computability/UniqueGames/PCP/LoopState.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Exact tape invariant for the old-dart loop. The cursor stores the remaining input rows, while the reversed tape stores precisely the output headers and the blocks already emitted. The scan and index-scan tapes are unconstrained: the next lookup prefixes fresh copies and retains old residues as suffixes. Finite control state is specified by the actual execution theorems using this tape invariant.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.inputBits line 24
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixWords line 28

    Source documentation

    The output headers are included even before the first old row is read.

    def prefixWords (input : GenericGraphTables.Table q) (e : Nat) : List Nat :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table

  3. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits line 33
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorWords line 36
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorBits line 39
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixWords_zero line 42
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits_zero line 48
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixWords_succ line 54
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits_succ line 67
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits_reverse_succ line 74
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixWords_full line 81
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits_full line 91

    Source documentation

    At the terminal guard the stored prefix is the complete concrete output encoding.

    theorem prefixBits_full (input : GenericGraphTables.Table q) :
    prefixBits input input.darts = GraphTables.tableBits (Table.build input) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.prefixBits, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build

  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorBits_zero line 96
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorWords_succ line 101
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorBits_succ line 112
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.cursorBits_full line 120
  17. structure OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready line 129

    Source documentation

    Guard-to-guard tape contract. Only scan and indexScan may contain residues.

    structure Ready (input : GenericGraphTables.Table q) (e : Nat)
    (base : Tape → List Bool) : Prop where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.of_agree line 148

    Source documentation

    Changing only lookup residues preserves the complete loop contract.

    theorem Ready.of_agree {input : GenericGraphTables.Table q} {e : Nat}
    {base next : Tape → List Bool} (ready : Ready input e base)
    (agree : ∀ tape, tape ≠ .scan → tape ≠ .indexScan → next tape = base tape) :
    Ready input e next where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready

  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.update_scan line 168
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.update_indexScan line 175
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_succ line 182
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.counter_at_end line 189
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.cursor_at_end line 194
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready.reversed_at_end line 198