ProductMachineSemantics.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

The exact table lookups and field schedule consumed by the product machine. The table contains rows only: the three input header words have already been consumed, so each affine lookup has coefficient q+2 and no header offset.

theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.row_table_lookup line 23

Source documentation

Indexing a flattened constant-width row list preserves the literal field position, not merely the multiset of row contents.

theorem row_table_lookup (constraints : List (Constraint n q))
    (e : Fin constraints.length) (field : Fin (q + 2)) :
    (constraints.flatMap constraintWords)[(q + 2) * e.val + field.val]? =
      (constraintWords constraints[e])[field.val]? := by
…

def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable line 44
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable_source line 46
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable_target line 51
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable_image line 56
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.reverseDigits line 63
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.reverseDigits_at line 66
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.reverseDigits_words line 69
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.horner_ofFin line 82
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.sourceCommand line 88
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.targetCommand line 89
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.imageCommand line 90
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.commands line 95
Source documentation
The complete fixed-alphabet row schedule: two endpoints followed by every forward-table entry in increasing numeric label order.
```
def commands (q t : ℕ) : List (MachineProductRow.Command t) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Command
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.commands_length line 98
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.fields line 101
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.fieldValue line 105
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.source_fields line 110
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.target_fields line 115
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.image_fields line 120
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.selected line 130
Source documentation
Every scheduled lookup selects an actual word in the input table.
```
theorem selected (H : Instance q) (edges : Fin t → Fin H.constraints.length)
    (c : MachineProductRow.Command t) (hc : c ∈ commands q t) (i : Fin t) :
    (inputTable H)[(q + 2) * (edges i).val + c.2 i]? =
      some (fields H edges c i) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Command, OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.commands, OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.inputTable, OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.fields
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.command_offset_lt line 142
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.fields_lt line 153
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.source_value line 166
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.target_value line 173
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.image_value line 180
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.encodeWords_map line 190
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.rowBits_eq line 198
Source documentation
The controller's literal field-command output is the serialized semantic row, including every forward permutation-table entry.
```
theorem rowBits_eq (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t) (i : Fin (H.constraints.length ^ t)) :
    MachineProductRow.rowBits (fieldValue H (finFunctionFinEquiv.symm i)) (commands q t) =
      encodeWords (constraintWords (ProductPaddedOutput.outputRow H presentation t ht i)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.rowBits, OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.fieldValue, OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.commands, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.outputRow
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.encodeWords_flatMap line 224
def OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.allRowsBits line 232
Source documentation
Product rows are emitted in ascending radix address, exactly the literal order of the output constraint list.
```
def allRowsBits (H : Instance q) (t : ℕ) : List Bool :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.allRowsBits_eq line 236
theorem OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.gameBits_eq line 253
Source documentation
Concatenating the three computed headers and all physical row fields yields precisely the target serialization, including list order and full tables.
```
theorem gameBits_eq (H : Instance q) (presentation : SimpleBipartite H)
    (t : ℕ) (ht : 0 < t) :
    encodeWords [H.vertices ^ t, q ^ t, H.constraints.length ^ t] ++ allRowsBits H t =
      gameBits (ProductPaddedOutput.output H presentation t ht) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.ProductMachineSemantics.allRowsBits, OAI.UniqueGamesTheorem.Explicit.ProductPaddedOutput.output