MachineOverlayRows.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

The fixed-degree vertex loop has one finite label block per port, plus one terminal boundary. The stored row values do not occur in its program.

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.State line 15
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.Label line 17
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.bodyIndex line 24
Source documentation
The row body's nine tapes retain their numbering; tape 9 is the stream.
```
def bodyIndex (i : Fin 9) : Fin 10 := i.castSucc
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.bodyIndex_injective line 26
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.trueBits line 30
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.instruction line 32
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowBits line 47
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowSteps line 50
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.resultTapes line 54
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.joinTrace line 59

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowTrace line 65

Source documentation

Load the actual next expander index, execute the arithmetic and complete 4096-bit row emitter, then clear the three isolated temporary fields.

theorem rowTrace (d e : Nat) (positive : 0 < e) (tape : Fin 10 → K)
    (distinct : Function.Injective tape) (labels : Label e → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State A e))
    (atLabels : ∀ l, program (labels l) = instruction d e positive tape labels exit l)
    (base : K → List Bool) (v j : Nat) (suffix : List Bool)
    (tailWord : base (tape 0) = encodeWord v)
    (inputWord : base (tape 9) = encodeWord j ++ suffix)
    (empty : ∀ i : Fin 10, i ≠ 0 → i ≠ 7 → i ≠ 9 → base (tape i) = [])
    (ambient : A) :
    (advance (TM2.step program))^[rowSteps d e v j (base (tape 7))]
      (some ⟨some (labels .loadStart), MachinePortReindex.clean e positive ambient, base⟩) =
      some ⟨exit, MachinePortReindex.clean e positive ambient,
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.clean

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowBits_eq_expanderRow line 207
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.machine line 221
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.VertexLabel line 235
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexInstruction line 237
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.streamFrame line 247
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.streamOutput line 252
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSteps line 255
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.valueBound line 260
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowSizeBound line 261
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowCostBound line 262
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.value_le line 265
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowBits_length line 273
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowBits_length_le line 279
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowSteps_le line 286
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSteps_le_capacity line 296
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSteps_le line 323
Source documentation
Explicit polynomial budget for the finite port loop, including repeated output append costs and all real loader and cleanup transitions.
```
theorem vertexSteps_le (d e v B : Nat) (words : List Nat)
    (bounded : ∀ j ∈ words, j ≤ B) (output : List Bool) :
    vertexSteps d e v words output ≤
      words.length * (rowCostBound d e v B +
        2 * (output.length + words.length * rowSizeBound d e v B) + 1) + 1 :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowCostBound, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.rowSizeBound
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.streamFrame_afterRow line 330

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSuffixTrace line 348

Source documentation

A suffix of the actual fixed-degree port loop. Each row execution is derived from rowTrace; no row-execution premise is accepted.

theorem vertexSuffixTrace (d e : Nat) (positive : 0 < e) (tape : Fin 10 → K)
    (distinct : Function.Injective tape) (labels : VertexLabel e → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State A e))
    (atLabels : ∀ l, program (labels l) = vertexInstruction d e positive tape labels exit l)
    (base : K → List Bool) (v : Nat) (values : Fin e → Nat)
    (tailWord : base (tape 0) = encodeWord v)
    (empty : ∀ i : Fin 10, i ≠ 0 → i ≠ 7 → i ≠ 9 → base (tape i) = [])
    (ambient : A) (remaining : Nat) (i : Fin (e + 1)) (count : i.val + remaining = e)
    (output : List Bool) :
    (advance (TM2.step program))^[vertexSteps d e v ((List.ofFn values).drop i.val) output]
      (some ⟨some (labels (i, none)), MachinePortReindex.clean e positive ambient,
        streamFrame tape base ((List.ofFn values).drop i.val) output⟩) =
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.VertexLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePortReindex.clean, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.streamFrame

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexTrace line 422
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexInTime line 438
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.encodeWords_flatMap line 460
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.streamOutput_expanderRows line 466
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.expanderValues_bounded line 479
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineOverlayRows.vertexMachine line 486