OAI/Computability/MaxCut/Machines/MachineRegularLift.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

The outer construction uses independent finite registers for its existing subprograms. This transport combines tape placement, an untouched register frame, and a static register equivalence, without adding any machine steps.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.statement line 20
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.configuration line 26
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.stepAux line 34
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.step line 47
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.trace line 69
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.update_memory_spare line 95
  7. inductive OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.RankLabel line 100
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankSkip line 106
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram line 109
  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 128
  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 133
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 144
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 152
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankRowTrace line 168

    Source documentation

    One actual row comparison consumes one unit of fuel and restores the entire vertex query before discarding the remaining fixed row fields.

    theorem rankRowTrace (r : Row) (hwidth : r.2.length = 4097) (v k : Nat)
    (original suffix targetSuffix fuelSuffix count : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (rankProgram (σ := σ))))^[rowTime v r]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram

  15. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.prefixTime line 205

    Source documentation

    Specification of the trace length; this function is not part of control.

    def prefixTime (v : Nat) : List Row → Nat
  | [] => 2
  | r :: rs => prefixTime v rs + rowTime v r

/-- The row loop runs for the unary fuel on spare, not until the input ends. -/
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.prefixTrace line 210

    Source documentation

    The row loop runs for the unary fuel on spare, not until the input ends.

    theorem prefixTrace (rs : List Row) (hwidth : ∀ r ∈ rs, r.2.length = 4097) (v : Nat)
    (original suffix targetSuffix fuelSuffix count : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (rankProgram (σ := σ))))^[prefixTime v rs]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram, OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.prefixTime

  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.prefixTime_le line 237
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.queryWord line 247
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 250
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankSteps line 258
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankTrace line 265

    Source documentation

    The full finite trace copies the query, extracts its unary row fuel, preserves the graph while copying it, skips both headers, and counts a prefix.

    theorem rankTrace (n m v k : Nat) (rs : List Row) (hk : k ≤ rs.length)
    (hwidth : ∀ r ∈ rs, r.2.length = 4097) (querySuffix count : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (rankProgram (σ := σ))))^[rankSteps n m v k rs querySuffix]
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram, OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankSteps

  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankSteps_le line 324

    Source documentation

    The concrete trace has a linear bound in the two preserved input words.

    theorem rankSteps_le (n m v k : Nat) (rs : List Row) (querySuffix : List Bool) :
    rankSteps n m v k rs querySuffix ≤
      5 * (inputWord n m rs).length + 3 * (queryWord v k querySuffix).length + 6 := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankSteps, OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.queryWord

  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 339

    Source documentation

    In a filtered list, the rank of a retained entry is the number of retained entries preceding its first original occurrence. This is a specification lemma.

    theorem idxOf_filter_prefix {α : Type*} [BEq α] [LawfulBEq α]
    (p : α → Bool) (a : α) (hp : p a = true) :
    ∀ xs : List α, a ∈ xs →
      (xs.filter p).idxOf a = ((xs.take (xs.idxOf a)).filter p).length := by
…
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.tableRows_length line 358
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 362

    Source documentation

    The executable cloud rank is exactly the count of matching earlier rows.

    theorem cloudRank_eq_prefix_count (t : GraphTables.Table) (v : Fin t.vertices)
    (e : DegreeReplacement.Cloud (GraphTables.semantics t) v) :
    (PreprocessingCloudIndex.cloudRank t v e).val =
      rowsHits v.val ((tableRows t).take e.val.val) := by
…
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 377

    Source documentation

    Full trace on a genuine stored graph and a genuine member of its cloud. The complete input table and the entire vertex/dart query remain unchanged.

    theorem cloudRankTrace (t : GraphTables.Table) (v : Fin t.vertices)
    (e : DegreeReplacement.Cloud (GraphTables.semantics t) v)
    (querySuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (rankProgram (σ := σ))))^[
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram

  27. def OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 402

    Source documentation

    A genuine timed execution witness with a polynomial (indeed linear) transition budget. Neither the result nor a body trace is a premise.

    def cloudRankInTime (t : GraphTables.Table) (v : Fin t.vertices)
    (e : DegreeReplacement.Cloud (GraphTables.semantics t) v)
    (querySuffix countSuffix : List Bool) (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (rankProgram (σ := σ)))
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCloudRank.rankProgram

  28. inductive OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Label line 430
  29. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Label.enumList line 435
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Label.enumList_getElem?_ctorIdx_eq line 438
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Label.enumList_nodup line 442
  32. instance OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.(instance at line 444) line 444
  33. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.Alphabet line 450
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.routine line 454

    Source documentation

    fields 0, fields 1, and fields 2 are the tail, reverse index, and encoded relation tapes. Every instruction reads or writes a single tape head.

    def routine (fields : Fin 3 → K) (row output scratch : K)
    (labels : Label → Λ) (exit : Option Λ) :
    Label → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool)
…

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

  35. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.fieldBits line 477

    Source documentation

    Exact row field concatenation at the level of stored bits.

    def fieldBits (fields : Fin 3 → K) (base : K → List Bool) : List Bool :=
…
  36. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.fieldSize line 480
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.fieldBits_length line 484
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.prefixTapes line 488
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.prefixTrace line 492

    Source documentation

    The three actual preserving-copy phases, with exact tape handoffs.

    theorem prefixTrace (fields : Fin 3 → K) (row output scratch : K)
    (hfields : ∀ i, fields i ≠ row ∧ fields i ≠ scratch)
    (hrowScratch : row ≠ scratch) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.appendTrace line 544
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.rowBits_eq line 589

    Source documentation

    The full existing graph codec, including all 4096 unary predicate fields.

    theorem rowBits_eq {n m : Nat} (r : DartRow n m) :
    encodeWords (rowWords r) = encodeWord r.tail.val ++
      encodeWord r.reverseIndex.val ++ encodeWords (relationWords r.relation) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 595
  43. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.timePolynomial line 603
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 606
  45. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.rowAppendInTime line 615

    Source documentation

    A composable actual execution certificate for a correctly encoded row. The program is fixed; row data occur only in the input-tape equalities.

    def rowAppendInTime {n m : Nat} (r : DartRow n m)
    (fields : Fin 3 → K) (row output scratch : K)
    (hfields : ∀ i, fields i ≠ row ∧ fields i ≠ scratch)
    (hrowOutput : row ≠ output) (hrowScratch : row ≠ scratch)
    (houtputScratch : output ≠ scratch) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (σ × Option Bool))
…

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

  46. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.machine line 642

    Source documentation

    A fixed nine-label six-stack finite machine implementing the routine. Its inputs may be supplied in a caller's distributed tape configuration.

    def machine : FinTM2 where
…
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.machineRowInTime line 655

    Source documentation

    Direct execution of the concrete finite machine on caller-supplied unary fields. This instantiates all program equations; no execution premise remains.

    def machineRowInTime {n m : Nat} (r : DartRow n m) (base : Fin 6 → List Bool)
    (hrow : base 3 = []) (hscratch : base 5 = [])
    (htail : base 0 = encodeWord r.tail.val)
    (hreverse : base 1 = encodeWord r.reverseIndex.val)
    (hrelation : base 2 = encodeWords (relationWords r.relation)) (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      ⟨some .relationRead, ((), register), base⟩
      (some ⟨none, ((), none),
        Function.update base (4 : Fin 6) (base 4 ++ encodeWords (rowWords r))⟩)
      (timePolynomial.eval ((encodeWords (rowWords r)).length + (base 4).length)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.encodeWords

  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTableRows.outputFrame line 684
  49. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 707
  50. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 712
  51. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 717
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 725
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 730
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 743
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 756
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 763
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 766
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 769
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 774
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 786
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 792
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 799
  63. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Tape line 806
  64. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 807
  65. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.State line 808
  66. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 809
  67. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 811
  68. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 813
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 815
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 822
  71. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.fields line 828
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 830
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 831
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 832
  75. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 834
  76. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 837
  77. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Label line 843
  78. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 849
  79. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.instruction line 854
  80. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.machine line 866
  81. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.looked line 877
  82. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copied line 881
  83. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined line 886
  84. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 891
  85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 896
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 900
  87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 910
  88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 922
  89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 928

    Source documentation

    Reusable identity copy of exactly the physically read 4096 unary Boolean fields. The fixed register is reset; every other state component is retained.

    theorem relationCopy_step {K Λ σ : Type} [DecidableEq K]
    (src dst : K) (hne : src ≠ dst) (label : Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State σ))
    (code : program label = relationCopyAt src dst exit)
    (relation : RelationTable) (suffix : List Bool) (base : K → List Bool)
    (input : base src = encodeWords (relationWords relation) ++ suffix)
    (ambient : σ) (buffer : Buffer) (register : Option Bool) :
    TM2.step program ⟨some label, ((ambient, buffer), register), base⟩ =
      some ⟨exit, ((ambient, zeroBuffer), register),
        Function.update (Function.update base src suffix) dst
          (encodeWords (relationWords relation) ++ base dst)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer

  90. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 957
  91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 962
  92. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 968
  93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 973
  94. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 977
  95. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 982
  96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 986
  97. structure OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Input line 991

    Source documentation

    The input graph and dart index occur only as physically stored tape data.

    structure Input (t : Table) (e : Fin t.darts) (base : Tape → List Bool) : Prop where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Tape

  98. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 1000
  99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 1003
  100. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 1013
  101. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.steps line 1016
  102. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 1020
  103. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.join_trace_inline_MachineRegularOriginalRow line 1028
  104. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTrace line 1032
  105. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.copyTrace line 1046
  106. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affineTrace line 1061
  107. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.emitTrace line 1082
  108. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.traceAt line 1109

    Source documentation

    All four phases are derived from their concrete instructions.

    theorem traceAt (q : Nat) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State σ))
    (code : ∀ l, program (labels l) = instruction q labels exit l)
    (t : Table) (e : Fin t.darts) (base : Tape → List Bool) (input : Input t e base)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[steps q t e base]
      (some ⟨some (labels (.lookup .seed)), ((ambient, zeroBuffer), register), base⟩) =
      some ⟨exit, ((ambient, zeroBuffer), none), finalTapes q t e base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Input, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.steps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes

  109. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.timeBound line 1125
  110. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.steps_le line 1128
  111. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.machineInTime line 1146

    Source documentation

    Concrete finite-machine execution for the actual regularized input row.

    def machineInTime (H : BaseTable) (t : Table) (e : Fin t.darts)
    (base : Tape → List Bool) (input : Input t e base) (register : Option Bool) :
    StateTransition.EvalsToInTime (machine internalDegree).step
      ⟨some (.lookup .seed), (((), zeroBuffer), register), base⟩
      (some ⟨none, (((), zeroBuffer), none),
        Function.update (affined internalDegree t e base) (9 : Tape)
          (base (9 : Tape) ++ encodeWords (rowWords (inheritedRow H t e)))⟩)
      (timeBound internalDegree (tableBits t).length (base (9 : Tape)).length) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.Input, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.machine, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.affined, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalRow.timeBound