MachineRegularTable.lean`

211 declarations, 0 contain sorry, 0 declared as axioms

Actual regular-table construction

The header subroutine reads the two original graph headers, computes the padding total by the actual prefix machine, performs unary addition and constant multiplication, and appends both resulting header fields. The outer vertex routines are assembled from actual metadata and row programs.

inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Extra line 29
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList line 33
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_getElem?_ctorIdx_eq line 36
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_nodup line 40
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.(instance at line 42) line 42
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Tape line 46
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 47
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.State line 48
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.tableTape line 50
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.nTape line 51
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.queryTape line 52
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 53
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.sumTape line 54
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.mTape line 55
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.indexTape line 56
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.workTape line 57
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 58
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 59
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 60
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.emitTape line 61
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.outputTape line 62
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.memory line 64
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame line 76
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_table line 79
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_n line 81
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_query line 83
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 85
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 87
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_m line 89
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_index line 91
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_work line 93
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 95
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 97
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 99
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 101
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame_output line 103
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 106
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 119
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 132
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 145
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 158
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 171
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 184
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 197
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 210
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 223
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 236
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 249
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 262
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Field line 275
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Field.enumList line 279
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_getElem?_ctorIdx_eq line 281
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_nodup line 285
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.(instance at line 287) line 287
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 291
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList line 295
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_getElem?_ctorIdx_eq line 297
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_nodup line 301
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.(instance at line 303) line 303
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Label line 307
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 317
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 321
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 325
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 328
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.copySource line 333
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 338
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.copyExit line 342
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.prefixView line 347
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 351
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 353
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 357
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.program line 368
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.appendTrace line 398
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 402
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 405
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 408
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 410
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.initStep line 415
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 424
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 433
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.readTime line 442

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.readTrace line 447

Source documentation

Both original header numbers are produced by physical preserving lookups.

theorem readTrace (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program q)))^[readTime t]
      (some ⟨some .init, ((ambient, false), register),
        frame (GraphTables.tableBits t) [] [] [] [] [] [] [] [] [] [] [] output⟩) =
      some ⟨some (.prefix .init), ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] []
          (encodeWord t.darts) [] [] [] [] [] [] output⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.readTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 496

Source documentation

The original vertex count is the physical bound supplied to the checked padding-prefix machine. Its complement tapes preserve the original dart count.

theorem prefixTrace (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program q)))^[MachineCloudPrefix.totalTime t t.vertices []]
      (some ⟨some (.prefix .init), ((ambient, false), register),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] []
          (encodeWord t.darts) [] [] [] [] [] [] output⟩) =
      some ⟨some (.copyFirst .count), ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) (encodeWord t.vertices)
          (encodeWord 0) (encodeWord (paddingTotal t)) (encodeWord t.darts)
          [] [] [] [] [] [] output⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPrefix.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.paddingTotal

def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.computeTime line 516
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 519
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.headerBits line 557
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 560
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 564
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 570
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.emitTime line 579
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 583
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.totalTime line 646
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.trace line 649
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 662
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 669
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 672
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.inTime line 715
Source documentation
A genuine finite-machine execution with a cubic input-length budget.
```
def inTime (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some .init, ((ambient, false), register),
        frame (GraphTables.tableBits t) [] [] [] [] [] [] [] [] [] [] [] output⟩
      (some ⟨none, ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] [] (encodeWord t.darts)
          [] [] [] (encodeWord (vertexTotal t)) (encodeWord (dartTotal q t)) []
          (output ++ headerBits q t)⟩)
      ((timePolynomial q).eval ((GraphTables.tableBits t).length + output.length)) where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.vertexTotal, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.dartTotal, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.headerBits, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.timePolynomial
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.guard line 737
Source documentation
The outer loop consumes one real unary fuel bit. The zero delimiter is consumed on exit; its temporary finite register is reset on both branches.
```
def guard (fuel : K) (body : Λ) (exit : Option Λ) :
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool) :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 745
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 752
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.increment line 760
Source documentation
Unary successor needs one physical push and no unbounded register.
```
def increment (counter : K) (next : Λ) : TM2.Stmt (fun _ : K => Bool) Λ σ :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 763
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Body line 773
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Tape line 774
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 775
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.State line 776
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Data line 777
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 778
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq line 780
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 791
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 806
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 809
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 813
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.coreTape line 821
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 822
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 823
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 824
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.scratch line 825
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerTape line 827
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerView line 833
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 844
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 853
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.bodyView line 872
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 876
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 877
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 883
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerView line 887
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 895
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 901
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerStates line 910
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.readyState line 918
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 920
abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList line 924
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_getElem?_ctorIdx_eq line 926
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_nodup line 930
instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.(instance at line 932) line 932
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copySource line 936
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 939
inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Label line 943
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyExit line 958
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.clearTape line 962
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 966
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.program line 971
Source documentation
All graph-dependent loop counts remain on tapes. The code contains only the fixed expander base and the finite subprogram labels.
```
def program (H : BaseTable) : Label → TM2.Stmt Alphabet Label State
  | .header l => Lift.statement headerTape Label.header (some .oldSeed) headerStates
      (Header.program PreprocessingRegularTables.internalDegree l)
  | .oldSeed => .push (coreTape 1) (fun _ => false) (.goto fun _ => Label.copyFirst CopyPhase.old)
  | .copyFirst phase => Reduction.MachineTransfer.loopAt (copySource phase) scratch id false
      (.copyFirst phase) (some (.copySecond phase))
  | .copySecond phase => MachineCopy.forkLoop scratch (copySource phase) (copyTarget phase) false
      (.copySecond phase) (some (copyExit phase))
  | .oldGuard => Fuel.guard oldFuel (Label.oldBody MachineRegularOriginalBody.entry) (some Label.ownerSeed)
  | .oldBody l => Lift.statement Sum.inl Label.oldBody (some .oldIncrement) (Equiv.refl _)
      (MachineRegularOriginalBody.program H l)
  | .oldIncrement => Fuel.increment (coreTape 1) Label.oldGuard
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Lift.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerStates, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.coreTape, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copySource, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.scratch, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyTarget, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyExit, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.guard, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldFuel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Fuel.increment
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.machine line 991
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame line 1004
Source documentation
These are mathematical descriptions of the physical stacks at loop boundaries. They are never loaded into the machine's finite control.
```
def frame (data : Data) (header : Header.Tape → List Bool) (counters : Fin 4 → List Bool) :
    Tape → List Bool
  | .inl k => MachineRegularOriginalBody.frame data k
  | .inr (.inl k) => header k
  | .inr (.inr i) => counters i
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.frame
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cfg line 1010
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_core line 1015
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 1019
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerAux line 1028
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 1034
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 1038
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.inputData line 1065
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerData line 1078
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 1081
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 1085
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldData line 1104
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 1107
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 1112
Source documentation
The actual old-vertex body is transported with all outer counters and header words untouched. No body-execution hypothesis occurs in this lemma.
```
theorem oldBodyTrace (H : BaseTable) (t : GraphTables.Table) (e : Fin t.darts)
    (output : List Bool) (header : Header.Tape → List Bool) (counters : Fin 4 → List Bool) :
    (advance (TM2.step (program H)))^[MachineRegularOriginalBody.totalSteps H t e output]
      (some (cfg H (some (Label.oldBody MachineRegularOriginalBody.entry))
        (oldData t e.val output) header counters)) =
      some (cfg H (some .oldIncrement)
        (oldData t e.val (output ++ MachineRegularOriginalBody.emittedBits H t e)) header counters) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.totalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularOriginalBody.emittedBits
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 1127
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 1130
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 1134
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 1138
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 1149
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 1160
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 1173
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 1186
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 1200
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 1211
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 1225
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 1228
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 1235
Also declared: OAI/Computability/UniqueGames/Machines/MachineRegularTableTrace.lean:10 (same declaration text).
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 1241
Source documentation
Each actual fuel/body/increment segment appends exactly the next original vertex block. This induction is over a specification index, not a register.
```
theorem oldPrefixTrace (H : BaseTable) (t : GraphTables.Table) (output : List Bool)
    (header : Header.Tape → List Bool) (k : Nat) : k ≤ t.darts →
    (advance (TM2.step (program H)))^[oldElapsed H t output k]
      (some (cfg H (some .oldGuard) (oldData t 0 output) header
        (counterStacks (encodeWord t.darts) [] [] []))) =
      some (cfg H (some .oldGuard) (oldData t k (output ++ oldPrefix H t k)) header
        (counterStacks (encodeWord (t.darts-k)) [] [] [])) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldElapsed, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.counterStacks, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldPrefix
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 1272
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 1284
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 1288
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 1291
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 1295
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 1308
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 1323
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 1333
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerData line 1346
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 1354
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 1372
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 1386
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 1398
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 1401
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 1417
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 1431
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 1442
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 1462
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 1465
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 1472
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 1502
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 1514
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 1524
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleaned line 1540
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 1545
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 1550
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 1558
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 1572
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 1578
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 1581
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 1601
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 1615
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 1631
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 1695
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 1698
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 1701
def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.totalTime line 1704
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 1710
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 1715