MachineSubdivisionRows.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.identityTable line 14
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.inverseTable line 20
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rows line 28
Source documentation
The saved fields are ordered u,p,q,r,v. All four edges are oriented left-to-right; hence the last permutation is inverted.
```
def rows {n q : Nat} (vertices : Fin 5 → Fin n) (p : PermutationTable q) :
    List (Constraint n q) :=
…
```
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rows_length line 35
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.tokens line 40
Source documentation
The program copies saved endpoint words and emits complete forward tables.
```
def tokens (identity inverse : List Bool) : List (MachineFieldTemplate.Token 5) :=
…
```
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.tokens_length line 46
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.fields line 49
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.rowBits line 52
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.templateOutput_rows line 55
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.field line 65
Source documentation
A finite stack layout: five preserved fields, scratch, and reversed output.
```
def field (j : Fin 5) : Fin 7 := ⟨j.val, by omega⟩
```
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.scratch line 67
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.output line 68
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.field_ne_scratch line 70
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.field_ne_output line 76
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.scratch_ne_output line 82
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.machine line 84
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.machine_finiteAlphabet line 95

def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.phaseInTime line 103

Source documentation

Exact physical row execution, preserving the five saved fields and restoring scratch. This is a phase theorem; it does not assume its own execution.

def phaseInTime (identity inverse : List Bool) (base : Fin 7 → List Bool)
    (emptyScratch : base scratch = []) (state : MachineFieldTemplate.State Unit) :
    StateTransition.EvalsToInTime (machine identity inverse).step
      ⟨some (MachineFieldTemplate.startAt (tokens identity inverse).length 0), state, base⟩
      (some ⟨none, MachineFieldTemplate.reset state,
        MachineFieldTemplate.outputTapes base output
          (MachineFieldTemplate.templateOutput (tokens identity inverse)
            (fun j => base (field j)))⟩)
      (3 * MachineFieldTemplate.copiedLength (tokens identity inverse)
        (fun j => base (field j)) + 37) := by
…

Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionRows.scratch, OAI.MaxCutGames.Explicit.MachineSubdivisionRows.machine, OAI.MaxCutGames.Explicit.MachineSubdivisionRows.tokens, OAI.MaxCutGames.Explicit.MachineSubdivisionRows.output, OAI.MaxCutGames.Explicit.MachineSubdivisionRows.field

theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.phase_budget line 118
def OAI.MaxCutGames.Explicit.MachineSubdivisionRows.subdivisionVertexWords line 129
Source documentation
The semantic subdivision numbering: originals and middle vertices on the left, then two private right vertices for each occurrence.
```
def subdivisionVertexWords (n Q u v e : Nat) : Fin 5 → Nat
  | 0 => u
  | 1 => n + Q + 2 * e
  | 2 => n + e
  | 3 => n + Q + 2 * e + 1
  | 4 => v
```
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRows.subdivisionVertexWords_bounded line 136