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.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 22
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 24
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 28
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits line 35
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.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 39
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 49
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 53
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 58
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.joinTrace_inline_MachineRegularVertexBlock line 66

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 72

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.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 101
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 117
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView line 120
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 125
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 128
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 133
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 141
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 148
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 152
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 156
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 160

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 168

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.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalClean.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory

def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 200
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 202
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 207
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 210
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 215
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 221
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 226
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 232
inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.Label line 261
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 268
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 271
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.instruction line 274
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 283
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 286
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 290
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap_inline_MachineRegularVertexBlock line 301
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair_inline_MachineRegularVertexBlock line 307
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 310
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 323

theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 332

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.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud

def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 375
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 382
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 425
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.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 427
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 433
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 447
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 455
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 459
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 491
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 496
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 500
theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 530
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 549
Source documentation
A concrete finite program for original vertex blocks.
```
def originalMachine (q : Nat) (positive : 0 < q) : FinTM2 where
…
```
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 561
Source documentation
The same fixed instructions, entered at the dummy-vertex port loop.
```
def dummyMachine (q : Nat) (positive : 0 < q) : FinTM2 where
…
```
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 572
def OAI.MaxCutGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 592