OAI/Computability/UniqueGames/Machines/MachinePaddingTable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact table-codec endpoint of the polynomial padding-row routine. The caller supplies the physical unary counters and copied old-row buffer with the updated headers. This theorem executes every added row and proves that the resulting output is exactly the existing full table encoding.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingTable.initialOutput line 17
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddingTable.execution line 20