PortTableEncoding.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Foundations.PCP.PortTables.HasPortTails line 11
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.MaxCutGames.Foundations.PCP.GraphTables.Rows
instance OAI.MaxCutGames.Foundations.PCP.PortTables.(instance at line 14) line 14
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.flatRows_hasPortTails line 18
def OAI.MaxCutGames.Foundations.PCP.PortTables.ofRows line 23
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.MaxCutGames.Foundations.PCP.GraphTables.Rows, OAI.MaxCutGames.Foundations.PCP.GraphTables.Valid, OAI.MaxCutGames.Foundations.PCP.PortTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.table_ext_inline_PortTableEncoding line 35
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.ofRows_flatRows line 45
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.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.ofRows, OAI.MaxCutGames.Foundations.PCP.PortTables.flatRows, OAI.MaxCutGames.Foundations.PCP.PortTables.flatRows_valid
def OAI.MaxCutGames.Foundations.PCP.PortTables.extractInput line 56
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.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.Input, OAI.MaxCutGames.Foundations.PCP.GraphTables.Rows
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.extractInput_graphTable line 68
def OAI.MaxCutGames.Foundations.PCP.PortTables.decodeInputBits line 72
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.decodeInputBits_inputBits line 75
def OAI.MaxCutGames.Foundations.PCP.PortTables.encoding line 81
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.MaxCutGames.Foundations.PCP.PortTables.Input
theorem OAI.MaxCutGames.Foundations.PCP.PortTables.inputBits_injective line 86