OAI/Computability/UniqueGames/PCP/PortTableEncoding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.HasPortTails line 12

    Source documentation

    The flat graph's stored tails agree with its fixed regular-port ordering.

    def HasPortTails (rows : GraphTables.Rows n (n * d)) : Prop :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows

  2. instance OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.(instance at line 15) line 15
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.flatRows_hasPortTails line 19
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.ofRows line 24

    Source documentation

    The actual reverse and predicate vectors extracted from validated flat rows.

    def ofRows (rows : GraphTables.Rows n (n * d)) (valid : GraphTables.Valid rows) : Table n d where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Valid, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table

  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.table_ext line 36
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.ofRows_flatRows line 46

    Source documentation

    Recovering the implicit-tail representation loses none of its stored data.

    @[simp] theorem ofRows_flatRows (table : Table n d) :
    ofRows (flatRows table) (flatRows_valid table) = table := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.ofRows, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.flatRows, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.flatRows_valid

  7. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.extractInput line 57

    Source documentation

    Port-family checks applied after the full existing graph-table validation.

    def extractInput (ports : Nat) : GraphTables.Table → Option (Input ports)
  | ⟨vertices, darts, rows, valid⟩ =>
      if count_ok : darts = vertices * ports then
        let rows' : GraphTables.Rows vertices (vertices * ports) := count_ok ▸ rows
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Input, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Rows

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.extractInput_graphTable line 69
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.decodeInputBits line 73
  10. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.decodeInputBits_inputBits line 76
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.encoding line 82

    Source documentation

    A genuine roundtripping encoding of the fixed-port executable input family.

    def encoding (ports : Nat) : Computability.Encoding (Input ports) Bool where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Input

  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.inputBits_injective line 87