MachineRegularVertexBlock.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Actual regularized vertex-block execution

The finite internal-port loop invokes the checked row machine for every port in order. Each invocation restores the shared 27-tape frame. Inherited-row stages use fixed tape placements and finite state permutations.

abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 23
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 25
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 29
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portBits line 36
Source documentation
A prefix of the emitted rows, defined without any execution hypothesis.
```
def portBits {q : Nat} (bits : Fin q → List Bool) : Nat → List Bool
  | 0 => []
  | k + 1 => portBits bits k ++ if h : k < q then bits ⟨k, h⟩ else []
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 40
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 50
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 54
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 59
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.joinTrace line 67

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 73

Source documentation

Every body is an actual invocation of coreTrace; the code hypothesis only states the fixed placement into the caller's program.

theorem portPrefixTrace (q : Nat) (positive : 0 < q)
    (labels : PortLabel q → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q))
    (code : ∀ l, program (labels l) = portInstruction q positive labels exit l)
    (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (cloudSize t v + padding v) q)
    (v : Fin t.vertices) (x : PaddedCloud t padding v) (output : List Bool) (ambient : σ)
    (k : Nat) (hk : k ≤ q) :
    (advance (TM2.step program))^[portSteps t padding tables v x output.length k]
      (some ⟨portEntry q labels exit 0, coreInitialState q positive ambient,
        coreInputTapes t padding tables v x output⟩) =
      some ⟨portEntry q labels exit k, coreInitialState q positive ambient,
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.PortLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portEntry

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 102
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 118
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalView line 121
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 126
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 129
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 134
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 142
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 149
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 153
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 157
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 161

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 169

Source documentation

The inherited old relation is physically copied by the checked original-row machine, with a static tape placement and state permutation.

theorem originalCoreTrace (q : Nat) (positive : 0 < q)
    (labels : MachineRegularOriginalClean.Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q))
    (code : ∀ l, program (labels l) = originalCoreInstruction q labels exit l)
    (t : GraphTables.Table) (e : Fin t.darts) (v i k o m : Nat)
    (rotor output : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[MachineRegularOriginalClean.steps q t e
        (originalMemory (GraphTables.tableBits t) e.val output)]
      (some ⟨some (labels (.row (.lookup .seed))), coreInitialState q positive ambient,
        coreMemory (GraphTables.tableBits t) e.val v i k o m rotor output [] [] [] [] [] []⟩) =
      some ⟨exit, coreInitialState q positive ambient,
        coreMemory (GraphTables.tableBits t) e.val v i k o m rotor
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalClean.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMemory

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 201
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 203
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 208
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 211
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 216
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 222
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 227
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 233
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.Label line 262
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 269
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 272
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.instruction line 275
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 284
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 287
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 291
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap line 302
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair line 308
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 311
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 324

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 333

Source documentation

The full old-vertex block uses every internal port, then physically copies the original relation and reverse index. The output is the actual table block.

theorem originalTraceAt (q : Nat) (positive : 0 < q)
    (labels : Label q → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : CoreTape => Bool) Λ (CoreState σ q))
    (code : ∀ l, program (labels l) = instruction q positive labels exit l)
    (t : GraphTables.Table) (padding : Fin t.vertices → Nat)
    (tables : ∀ v, ExpanderTables.Table (cloudSize t v + padding v) q)
    (e : Fin t.darts) (output : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[originalSteps t padding tables e output.length]
      (some ⟨some (labels (originalEntry q positive)), coreInitialState q positive ambient,
        coreInputTapes t padding tables t.rows[e].tail (oldCloud t padding e) output⟩) =
      some ⟨exit, coreInitialState q positive ambient,
        coreInputTapes t padding tables t.rows[e].tail (oldCloud t padding e)
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.oldCloud

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 376
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 383
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 426
Source documentation
Uniform bound on a serialized row in the actual output table.
```
def rowSizeBound (q vertices : Nat) : Nat := vertices + vertices * (q + 1) + 8192
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 428
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 434
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 448
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 456
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 460
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 492
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 497
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 501
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 531
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 550
Source documentation
A concrete finite program for original vertex blocks.
```
def originalMachine (q : Nat) (positive : 0 < q) : FinTM2 where
…
```
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 562
Source documentation
The same fixed instructions, entered at the dummy-vertex port loop.
```
def dummyMachine (q : Nat) (positive : 0 < q) : FinTM2 where
…
```
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 573
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 593