MachineUnaryAffine.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

A real finite program for uniform whole-instance copying. It reads three headers, physically multiplies the occurrence count by the fixed constant, copies the header-free body the same fixed number of times, and clears all working tapes. No input-dependent data are placed in finite control.

abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 16
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.finish line 18
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan line 21
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.seed line 31
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes line 35
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 39
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 45
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 50
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.update_source_inline_MachineUnaryAffineAt line 55
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.update_scratch_inline_MachineUnaryAffineAt line 69
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.update_destination_inline_MachineUnaryAffineAt line 80
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 86
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 91
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 111
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 128
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 158
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 177
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 213
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 235
Source documentation
Include the literal offset prefix. The caller supplies an arbitrary output suffix, not a precomputed address; all runtime arithmetic occurs on the tapes.
```
theorem seededAffineTrace (source scratch destination : K)
    (hs : source ≠ scratch) (hd : source ≠ destination) (hsd : scratch ≠ destination)
    (coefficient offset : Nat) (seedLabel scanLabel restoreLabel : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.program, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet
inductive OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Label line 269
abbrev OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList line 273
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_getElem?_ctorIdx_eq line 275
theorem OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_nodup line 279
instance OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.(instance at line 281) line 281
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.program line 285
def OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.machine line 291
inductive OAI.MaxCutGames.Explicit.MachineUniformProgram.Tape line 314
abbrev OAI.MaxCutGames.Explicit.MachineUniformProgram.Tape.enumList line 319
theorem OAI.MaxCutGames.Explicit.MachineUniformProgram.Tape.enumList_getElem?_ctorIdx_eq line 322
theorem OAI.MaxCutGames.Explicit.MachineUniformProgram.Tape.enumList_nodup line 326
instance OAI.MaxCutGames.Explicit.MachineUniformProgram.(instance at line 328) line 328
abbrev OAI.MaxCutGames.Explicit.MachineUniformProgram.State line 332
def OAI.MaxCutGames.Explicit.MachineUniformProgram.initialState line 334
def OAI.MaxCutGames.Explicit.MachineUniformProgram.headerField line 336
def OAI.MaxCutGames.Explicit.MachineUniformProgram.emitField line 341
def OAI.MaxCutGames.Explicit.MachineUniformProgram.tokens line 347
def OAI.MaxCutGames.Explicit.MachineUniformProgram.clearKeys line 350
inductive OAI.MaxCutGames.Explicit.MachineUniformProgram.Label line 354
def OAI.MaxCutGames.Explicit.MachineUniformProgram.headerNext line 363
def OAI.MaxCutGames.Explicit.MachineUniformProgram.emitEntry line 366
def OAI.MaxCutGames.Explicit.MachineUniformProgram.program line 369
def OAI.MaxCutGames.Explicit.MachineUniformProgram.machine line 385
theorem OAI.MaxCutGames.Explicit.MachineUniformProgram.covers line 396
theorem OAI.MaxCutGames.Explicit.MachineUniformProgram.accumulator_not_mem_clearKeys line 400
theorem OAI.MaxCutGames.Explicit.MachineUniformProgram.output_not_mem_clearKeys line 401
def OAI.MaxCutGames.Explicit.MachineUniformHeaders.inputTapes line 414
def OAI.MaxCutGames.Explicit.MachineUniformHeaders.afterVertices line 417
def OAI.MaxCutGames.Explicit.MachineUniformHeaders.afterAlphabet line 420
def OAI.MaxCutGames.Explicit.MachineUniformHeaders.resultTapes line 424
theorem OAI.MaxCutGames.Explicit.MachineUniformHeaders.initList_eq line 429
theorem OAI.MaxCutGames.Explicit.MachineUniformHeaders.first_result line 435
theorem OAI.MaxCutGames.Explicit.MachineUniformHeaders.second_result line 443
theorem OAI.MaxCutGames.Explicit.MachineUniformHeaders.third_result line 451
def OAI.MaxCutGames.Explicit.MachineUniformHeaders.headersInTime line 461
Source documentation
The input headers are consumed literally; all unread constraint bits retain their original order and no tape contains an implicit runtime number.
```
def headersInTime (C q n Q : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime (machine C).step
      (initList (machine C) (encodeWords [n, q, Q] ++ body))
      (some ⟨some (.scale 0), initialState, resultTapes n q Q body⟩)
      (n + q + Q + 6) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineUniformHeaders.resultTapes
theorem OAI.MaxCutGames.Explicit.MachineUniformHeaders.headers_budget line 496