OAI/Computability/MaxCut/Machines/MachineDummyRows.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Actual finite control for the dummy self-loop rows of one padded vertex. The port count is a fixed program parameter. Vertex and reverse-dart indices remain on unary tapes, and each row advances the reverse index by one actual push. The all-true relation is a fixed literal field, initialized once.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueRelation line 20

    Source documentation

    The actual 64-by-64 always-accepting relation.

    def trueRelation : RelationTable := Vector.replicate 4096 true
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueBits line 22
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueBits_length line 24
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits line 29
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits_length line 31
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 35
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits line 41

    Source documentation

    Ordered serialized rows with successive physically stored reverse indices.

    def rowsBits (v e : Nat) : Nat → List Bool
  | 0 => []
  | count + 1 => rowBits v e ++ rowsBits v (e + 1) count

/-- One initialization label and ten labels per fixed port. -/

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits

  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Label line 46

    Source documentation

    One initialization label and ten labels per fixed port.

    abbrev Label (d : Nat) := Unit ⊕ (Fin d × (MachineTableRows.Label ⊕ Unit))

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Label

  9. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start line 48
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowLabel line 49
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.bumpLabel line 51
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fields line 53
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.afterPort line 57

    Source documentation

    The only data-changing index operation is a tape push, below. This function chooses a finite continuation among the fixed port-control labels.

    def afterPort {d : Nat} (p : Fin d) : Option (Label d) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Label

  14. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.entry line 60
  15. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Alphabet line 65
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.continueAt line 67
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 73
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program line 79

    Source documentation

    No input-dependent natural number occurs in the finite program.

    def program (d : Nat) : Label d → TM2.Stmt Alphabet (Label d) (σ × Option Bool)
  | .inl () => pushWord 2 trueBits.reverse
      (.load (fun state => (state.1, none)) (continueAt (entry d)))
  | .inr (p, .inl stage) => MachineTableRows.routine fields 3 4 5
      (rowLabel p) (some (bumpLabel p)) stage
  | .inr (p, .inr ()) => .push 1 (fun _ => true) (continueAt (afterPort p))

/-- The three unary row fields, two empty work tapes, and accumulated output. -/

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Label, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.continueAt, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.entry, OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.routine, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fields, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.bumpLabel, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.afterPort

  19. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes line 87

    Source documentation

    The three unary row fields, two empty work tapes, and accumulated output.

    def fieldTapes (v e : Nat) (output : List Bool) : Fin 6 → List Bool :=
…
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes line 91

    Source documentation

    Before initialization, the fixed-relation tape is empty.

    def initialTapes (v e : Nat) (output : List Bool) : Fin 6 → List Bool :=
…
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initializeStep line 95

    Source documentation

    The fixed literal relation is actually emitted by a finite push chain.

    theorem initializeStep (d v e : Nat) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    TM2.step (program d) ⟨some (start d), (ambient, register), initialTapes v e output⟩ =
      some ⟨entry d, (ambient, none), fieldTapes v e output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.entry, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes

  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowTrace line 108
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.bumpStep line 131

    Source documentation

    The reverse index advances by pushing a real unary bit. The delimiter, all input fields, output, and work tapes have their exact stated contents.

    theorem bumpStep {d : Nat} (p : Fin d) (v e : Nat) (output : List Bool) (ambient : σ) :
    TM2.step (program d) ⟨some (bumpLabel p), (ambient, none), fieldTapes v e output⟩ =
      some ⟨afterPort p, (ambient, none), fieldTapes v (e + 1) output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.bumpLabel, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.afterPort

  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 144

    Source documentation

    The concrete row body and its actual index increment are consecutive phases of one fixed program; no whole-body trace is supplied as a premise.

    theorem rowAndBumpTrace {d : Nat} (p : Fin d) (v e : Nat) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[
        4 * (v + e + 8194) + 2 * output.length + 10]
      (some ⟨some (rowLabel p .relationRead), (ambient, register), fieldTapes v e output⟩) =
      some ⟨afterPort p, (ambient, none), fieldTapes v (e + 1) (output ++ rowBits v e)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.afterPort, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits

  25. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps line 157

    Source documentation

    Exact sum of actual row-and-increment costs. This recurrence is matched to the program by suffixTrace, rather than postulated as a runtime.

    def steps (v e : Nat) (output : List Bool) : Nat → Nat
  | 0 => 0
  | count + 1 => (4 * (v + e + 8194) + 2 * output.length + 10) +
      steps v (e + 1) (output ++ rowBits v e) count

/-- Actual execution from any port boundary to the final halt. The finite
control index fixes the remaining number of rows; all unbounded values are
physically stored in `fieldTapes`. -/

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes

  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.suffixTrace line 165

    Source documentation

    Actual execution from any port boundary to the final halt. The finite control index fixes the remaining number of rows; all unbounded values are physically stored in fieldTapes.

    theorem suffixTrace {d : Nat} (count : Nat) (p : Fin d) (hp : p.val + count = d)
    (v e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[steps v e output count]
      (some ⟨some (rowLabel p .relationRead), (ambient, register), fieldTapes v e output⟩) =
      some ⟨none, (ambient, none), fieldTapes v (e + count) (output ++ rowsBits v e count)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowLabel, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits

  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.allTrace line 190

    Source documentation

    One fixed-relation initialization transition followed by all actual rows. At zero ports initialization itself halts; no row is spuriously produced.

    theorem allTrace (d v e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program d)))^[steps v e output d + 1]
      (some ⟨some (start d), (ambient, register), initialTapes v e output⟩) =
      some ⟨none, (ambient, none), fieldTapes v (e + d) (output ++ rowsBits v e d)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineComposition.advance, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits

  28. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.graphRows line 206

    Source documentation

    Actual finite graph rows in increasing reverse-index order.

    def graphRows {n m : Nat} (v : Fin n) (e : Nat) :
    (count : Nat) → e + count ≤ m → List (DartRow n m)
  | 0, _ => []
  | count + 1, h =>
      ⟨v, ⟨e, by omega⟩, trueRelation⟩ ::
        graphRows v (e + 1) count (by omega)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueRelation

  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.graphRows_length line 213
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 221

    Source documentation

    The machine's bit stream is exactly the existing codec on the actual ordered row list, including both index fields and every predicate entry.

    theorem rowsBits_eq_graphRows {n m : Nat} (v : Fin n) (e count : Nat)
    (h : e + count ≤ m) :
    rowsBits v.val e count = encodeWords ((graphRows v e count h).flatMap rowWords) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.graphRows

  31. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.dummyRows line 233

    Source documentation

    For one vertex of an n-vertex degree-d graph, every dummy dart is its own reverse. The caller's initial index is the actual unary value d * v.

    def dummyRows {n : Nat} (d : Nat) (v : Fin n) : List (DartRow n (n * d)) :=
…
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.dummyRows_length line 238
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 241
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps_le_bound line 255

    Source documentation

    Every actual row cost is bounded by the largest row and accumulated output encountered during this finite loop.

    theorem steps_le_bound (v e : Nat) (output : List Bool) (count : Nat) :
    steps v e output count ≤ count *
      (4 * (v + e + count + 8194) +
        2 * (output.length + count * (v + e + count + 8194)) + 10) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps

  35. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.inputSize line 289

    Source documentation

    The variable-size input is exactly the two physical unary fields and existing output. The relation field is a fixed program constant.

    def inputSize (v e : Nat) (output : List Bool) : Nat :=
…
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.timePolynomial line 293

    Source documentation

    A linear polynomial for each fixed port count d.

    noncomputable def timePolynomial (d : Nat) : Polynomial Nat :=
…
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 299
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machine line 322

    Source documentation

    A fixed finite machine. Its control stores only the fixed port position; vertex and reverse-index values reside on the tapes.

    def machine (d : Nat) : FinTM2 where
…
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machineInTime line 335

    Source documentation

    The full actual finite-machine execution, including initialization and all rows. No body trace or runtime hypothesis is an input to this certificate.

    def machineInTime (d v e : Nat) (output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine d).step
      ⟨some (start d), ((), register), initialTapes v e output⟩
      (some ⟨none, ((), none), fieldTapes v (e + d) (output ++ rowsBits v e d)⟩)
      ((timePolynomial d).eval (inputSize v e output)) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machine, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowsBits, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.timePolynomial, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.inputSize

  40. def OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 347

    Source documentation

    The same actual machine on the padding invariant e = d * v, with its exact existing-codec graph-row output.

    def machineDummyInTime {n : Nat} (d : Nat) (v : Fin n)
    (output : List Bool) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine d).step
      ⟨some (start d), ((), register), initialTapes v.val (d * v.val) output⟩
      (some ⟨none, ((), none), fieldTapes v.val (d * v.val + d)
        (output ++ encodeWords ((dummyRows d v).flatMap rowWords))⟩)
      ((timePolynomial d).eval (inputSize v.val (d * v.val) output)) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.machine, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.dummyRows, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.timePolynomial, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.inputSize

  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.finalFrame line 361

    Source documentation

    Input tail and both work tapes retain their required contents. The relation tape keeps the one initialized fixed field for subsequent use.

    theorem finalFrame (v e : Nat) (output : List Bool) :
    fieldTapes v e output 0 = encodeWord v ∧
    fieldTapes v e output 2 = trueBits ∧
    fieldTapes v e output 3 = [] ∧ fieldTapes v e output 5 = [] :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.trueBits

  42. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Tape line 384
  43. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 385
  44. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.State line 386
  45. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Label line 388
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 394
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 396
  48. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.instruction line 400

    Source documentation

    The row subprogram is a static label placement of the checked emitter.

    def instruction {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt Alphabet Λ (State σ)
  | .affine .seed => MachineUnaryAffineAt.seed 1 q (labels (.affine .scan))
  | .affine .scan => MachineUnaryAffineAt.scan 0 3 1 (q + 1)
      (labels (.affine .scan)) (labels (.affine .restore))
  | .affine .restore => Reduction.MachineTransfer.loopAt 3 0 id false
      (labels (.affine .restore)) (some (labels (.row (MachineDummyRows.start 1))))
  | .row stage => MachineCloudPadding.Placement.statement (id : Tape → Tape)
      (fun l => labels (.row l)) (some (labels .reverse))
      (MachineDummyRows.program 1 stage)
  | .reverse => MachineDrain.drain 1 (labels .reverse) (some (labels .relation))
  | .relation => MachineDrain.drain 2 (labels .relation) exit

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.seed, OAI.MaxCutGames.Foundations.Complexity.MachineUnaryAffineAt.scan, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.program, OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drain

  49. structure OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Input line 413
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.memory line 420
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.memory_input line 423
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.join_trace_inline_MachineRegularDummyRow line 426
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 430
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 438
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 448

    Source documentation

    The existing one-port emitter executes under the caller's actual labels.

    theorem rowTraceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[MachineDummyRows.steps x e output 1 + 1]
      (some ⟨some (labels (.row (MachineDummyRows.start 1))), (ambient, register),
        MachineDummyRows.initialTapes x e output⟩) =
      some ⟨some (labels .reverse), (ambient, none),
        MachineDummyRows.fieldTapes x (e + 1) (output ++ MachineDummyRows.rowBits x e)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.start, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.rowBits

  56. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 471

    Source documentation

    Both cleanup loops pop their entire physical fields.

    theorem cleanupTraceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x e : Nat) (output : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[
        ((encodeWord e).length + 1) + (MachineDummyRows.trueBits.length + 1)]
      (some ⟨some (labels .reverse), (ambient, register),
        MachineDummyRows.fieldTapes x e output⟩) =
      some ⟨exit, (ambient, none),
        Function.update (Function.update (MachineDummyRows.fieldTapes x e output) 1 []) 2 []⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineDummyRows.fieldTapes

  57. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.steps line 497

    Source documentation

    Sum of the actual arithmetic, row-emission, and cleanup transition counts.

    def steps (q x : Nat) (output : List Bool) : Nat :=
…
  58. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.timeBound line 503

    Source documentation

    For each fixed degree, the exact cost is linear in index and prior output.

    def timeBound (q x outputLength : Nat) : Nat :=
…
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 506
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.traceAt line 513

    Source documentation

    Exact physical execution; only the accumulated output changes at the boundary.

    theorem traceAt {σ Λ : Type} (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (x : Nat) (base : Tape → List Bool) (input : Input x base)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps q x (base 4)]
      (some ⟨some (labels (.affine .seed)), (ambient, register), base⟩) =
      some ⟨exit, (ambient, none), Function.update base 4 (base 4 ++ emittedBits q x)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.Input, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits

  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.machine line 541

    Source documentation

    A canonical finite machine over six Boolean stacks.

    def machine (q : Nat) : FinTM2 where
…
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 552
  63. inductive OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Control line 570
  64. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList line 573
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_getElem?_ctorIdx_eq line 575
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_nodup line 579
  67. instance OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.(instance at line 581) line 581
  68. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Tape line 585
  69. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Label line 586
  70. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.Alphabet line 587
  71. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.State line 589
  72. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.bodyEntry line 591
  73. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.extra line 594
  74. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.program line 605
  75. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.tapes line 608
  76. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.cfg line 612
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.bodyTrace line 616
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.guard_succ line 634
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.guard_zero line 645
  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.bump_step line 656
  81. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.paddingBits line 668
  82. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.steps line 672
  83. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.loopTrace line 679

    Source documentation

    The entire varying-length padding loop is proved from its actual guards, actual row bodies and actual vertex increments.

    theorem loopTrace (d : Nat) (hd : 0 < d) (count v e : Nat) (output : List Bool) :
    (advance (TM2.step (program d hd)))^[steps d v e output count]
      (some (cfg d (some (.inr .guard)) v e count output)) =
      some (cfg d none (v + count) (e + count * d) 0
        (output ++ paddingBits d v e count)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.program, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.steps, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.cfg, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.paddingBits

  84. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.initialTapes line 701
  85. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.initialize_step line 704
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.paddingTrace line 719
  87. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.machine line 726
  88. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.execution line 739

    Source documentation

    The exact time count is the sum of the physically executed row loops. Its polynomial bound is derived separately from this recurrence.

    def execution (d : Nat) (hd : 0 < d) (count v e : Nat) (output : List Bool) :
    StateTransition.EvalsToInTime (machine d hd).step
      ⟨some (.inr .initialize), (((), none), ()), initialTapes v e count output⟩
      (some (cfg d none (v + count) (e + count * d) 0
        (output ++ paddingBits d v e count)))
      (steps d v e output count + 1) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.machine, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.cfg, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.paddingBits, OAI.MaxCutGames.Foundations.Complexity.MachinePaddingRows.steps