MachineExpanderRow.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Complete execution of one expander-table row

The actual finite program performs both stored-table lookups, splits their results by its fixed degree, emits the resulting square/zigzag reverse index, and clears its work tapes. Its transition bound is linear in the unary input table length. The output accumulator and finite caller state are arbitrary.

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.concatenate line 19
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowSteps line 24
Source documentation
The actual number of transitions, retaining both concrete lookup costs.
```
def rowSteps {v d : Nat} (r : RowData v d) (output : List Bool) : Nat :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowTraceAt line 44
Source documentation
The complete execution follows the concrete program. The only code premise places its instructions in a caller; every lookup is derived from oldTable.
```
theorem rowTraceAt :
    (advance (TM2.step target))^[rowSteps r output]
      (some ⟨some (labels .initialize), divisionState positive ambient r.control0 none,
        frame0 r output⟩) =
      some ⟨exit, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowSteps_le line 168
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowInTimeAt line 188
Source documentation
The actual row program has a linear transition bound, with all temporary tapes empty at return. The bound holds for every valid finite input table.
```
def rowInTimeAt {v d : Nat} {ρ Λ : Type} [Fintype ρ]
    (positive : 0 < d) (r : RowData v d) (output : List Bool) (ambient : ρ)
    (labels : Label d → Λ) (exit : Option Λ)
    (target : Λ → TM2.Stmt (fun _ : Tape => Bool) Λ (State ρ d))
    (code : ∀ l, target (labels l) = statement positive r.smallTable id labels exit l) :
    StateTransition.EvalsToInTime (TM2.step target)
      ⟨some (labels .initialize), divisionState positive ambient r.control0 none,
        frame0 r output⟩
      (some ⟨exit, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩)
      (80 * (r.tableLength + 1)) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.rowInTime line 204
Source documentation
Specialization to the standalone finite row program.
```
def rowInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (r : RowData v d) (output : List Bool) (ambient : ρ) :
    StateTransition.EvalsToInTime (TM2.step (program positive r.smallTable))
      ⟨some .initialize, divisionState positive ambient r.control0 none, frame0 r output⟩
      (some ⟨none, divisionState positive ambient r.control2 none,
        emittedWord .output (frame0 r output) r.finalValue⟩)
      (80 * (r.tableLength + 1)) :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.RowData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.divisionState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.frame0, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderRow.emittedWord