OAI/Computability/UniqueGames/Machines/MachineCloudRankLemmas.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Actual inverse cloud numbering. The input table and query are copied preservingly. A unary working rank decreases only on equal stored tail fields; a separate unary row position increases on every skipped row. Only finite phase flags and symbol registers occur in the control state.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.update_memory_spare line 14
  2. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.RankLabel line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankSkip line 25
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram line 28
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 47
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 52
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 63
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 71
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankRowTrace line 87

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram

  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.prefixTime line 124

    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. -/
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.prefixTrace line 129

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.prefixTime

  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.prefixTime_le line 156
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.queryWord line 166
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 169
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankSteps line 177
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankTrace line 184

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankSteps

  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankSteps_le line 243

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.queryWord

  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 258

    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
…
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.tableRows_length line 277
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 281

    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
…
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 296

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram

  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 321

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCloudRank.rankProgram

  23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.BaseTape line 354
  24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 355
  25. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.BaseState line 356
  26. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.BaseLabel line 358
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.skipLabel line 364
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.baseProgram line 369
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 389
  30. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Phase line 394
  31. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Phase.enumList line 398
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Phase.enumList_getElem?_ctorIdx_eq line 400
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Phase.enumList_nodup line 404
  34. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.(instance at line 406) line 406
  35. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Control line 409
  36. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Control.enumList line 413
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Control.enumList_getElem?_ctorIdx_eq line 415
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Control.enumList_nodup line 419
  39. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.(instance at line 421) line 421
  40. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Tape line 425
  41. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Alphabet line 426
  42. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Label line 427
  43. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.State line 428
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.go line 430
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.dispatcher line 435

    Source documentation

    Pop the one-bit match result. Only a match pops the remaining local rank. Every completed skipped row separately pushes the global position.

    def dispatcher : TM2.Stmt Alphabet Label (State σ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.State

  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.extra line 448
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program line 452
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.memory line 455
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.memory_inl line 460
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.memory_position line 462
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 465
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 471
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.update_memory_position line 477
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg line 484
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.liftTrace line 489
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.compareTrace line 502
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 525
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 532
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 541
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.advanceStep line 549
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.finishStep line 558
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.initializeStep line 564
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.skipTrace line 572

    Source documentation

    The rest of a row is skipped field by field by the actual fixed program.

    theorem skipTrace (fields : List Nat) (hwidth : fields.length = 4097)
    (original suffix target rank position : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[(encodeWords fields).length + 1]
      (some (cfg (some (.inl (skipLabel 0))) .advancing original
        (encodeWords fields ++ suffix) target [] rank position ambient none)) =
      some (cfg (some (.inr .dispatch)) .advancing
        original suffix target [] rank position ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.skipLabel

  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 598

    Source documentation

    One nonselected row, with enough remaining rank to pass this row when it matches. Its global position is incremented on the output tape.

    theorem rowSkipTrace (r : Row) (hwidth : r.2.length = 4097) (v rank position : Nat)
    (original suffix targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[rowTime v r + 3]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (rowWords r) ++ suffix) (encodeWord v ++ targetSuffix) []
        (encodeWord (rank + if r.1 = v then 1 else 0) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg (some (.inl .field)) .checking original suffix
        (encodeWord v ++ targetSuffix) [] (encodeWord rank ++ rankSuffix)
        (encodeWord (position + 1) ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixTime line 642
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixTrace line 648

    Source documentation

    A preceding consumes precisely its number of matching tails from unary rank, while physically counting every original row on the position tape.

    theorem prefixTrace (rs : List Row) (hwidth : ∀ r ∈ rs, r.2.length = 4097)
    (v rank position : Nat) (original suffix targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prefixTime v rs]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (rs.flatMap rowWords) ++ suffix) (encodeWord v ++ targetSuffix) []
        (encodeWord (rowsHits v rs + rank) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg (some (.inl .field)) .checking original suffix
        (encodeWord v ++ targetSuffix) [] (encodeWord rank ++ rankSuffix)
        (encodeWord (position + rs.length) ++ outputSuffix) ambient
        (if rs = [] then register else none)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 678

    Source documentation

    Both copied workspaces are physically drained after finding the row; the original table, complete query, and position output are retained.

    theorem cleanupTrace (original work target rank position : List Bool) (ambient : σ) :
    (advance (TM2.step program))^[work.length + rank.length + 4]
      (some (cfg (some (.inl .clearWork)) .finishing
        original work target [] rank position ambient none)) =
      some (cfg none .checking original [] target [] [] position ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg

  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.selectedTrace line 712
  69. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.queryWord line 729
  70. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prepareSteps line 731
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prepareTrace line 737

    Source documentation

    Preserve the complete query and table while making the two working copies; extract the rank and skip the two actual table header fields.

    theorem prepareTrace (n m v rank : Nat) (rs : List Row)
    (querySuffix position : List Bool) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prepareSteps n m v rank rs querySuffix]
      (some (cfg (some (.inl .queryFirst)) .checking (MachineCloudCount.inputWord n m rs)
        [] (queryWord v rank querySuffix) [] [] position ambient register)) =
      some (cfg (some (.inl .field)) .checking (MachineCloudCount.inputWord n m rs)
        (encodeWords (rs.flatMap rowWords)) (queryWord v rank querySuffix) []
        (encodeWord rank ++ querySuffix) position ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prepareSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.inputWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.queryWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 798

    Source documentation

    A selected matching field is reached after precisely the matching count of its actual preceding rows has been consumed from the copied query.

    theorem prefixSelectedTrace (preceding : List Row)
    (hwidth : ∀ r ∈ preceding, r.2.length = 4097) (v position : Nat)
    (original work targetSuffix rankSuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prefixTime v preceding + 2 * v + work.length + rankSuffix.length + 8]
      (some (cfg (some (.inl .field)) .checking original
        (encodeWords (preceding.flatMap rowWords) ++ (encodeWord v ++ work))
        (encodeWord v ++ targetSuffix) [] (encodeWord (rowsHits v preceding) ++ rankSuffix)
        (encodeWord position ++ outputSuffix) ambient register)) =
      some (cfg none .checking original [] (encodeWord v ++ targetSuffix) [] []
        (encodeWord (position + preceding.length) ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.totalSteps line 820
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.fullTrace line 827

    Source documentation

    Complete execution for the actual encoded preceding decomposition. The decomposition is semantic data; every machine phase is proved above.

    theorem fullTrace (n m v rank : Nat) (rs preceding : List Row) (work : List Bool)
    (hwidth : ∀ r ∈ preceding, r.2.length = 4097)
    (hword : encodeWords (rs.flatMap rowWords) =
      encodeWords (preceding.flatMap rowWords) ++ (encodeWord v ++ work))
    (hrank : rank = rowsHits v preceding) (querySuffix outputSuffix : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[totalSteps n m v rank rs preceding work querySuffix]
      (some (cfg (some (.inr .initialize)) .checking (MachineCloudCount.inputWord n m rs)
        [] (queryWord v rank querySuffix) [] [] outputSuffix ambient register)) =
      some (cfg none .checking (MachineCloudCount.inputWord n m rs) []
        (queryWord v rank querySuffix) [] [] (encodeWord preceding.length ++ outputSuffix) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.totalSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudCount.inputWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.queryWord

  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 851
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 863
  77. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.remainder line 882

    Source documentation

    Bytes remaining after the selected row's actual tail field.

    def remainder (t : GraphTables.Table) (e : Fin t.darts) : List Bool :=
…
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 886
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.tableWord_split line 898

    Source documentation

    Canonical dart indexing yields the literal byte decomposition consumed by the actual preceding scan and final matching-field test.

    theorem tableWord_split (t : GraphTables.Table) (v : Fin t.vertices) (e : Fin t.darts)
    (owner : t.rows[e].tail = v) :
    encodeWords ((tableRows t).flatMap rowWords) =
      encodeWords (((tableRows t).take e.val).flatMap rowWords) ++
        (encodeWord v.val ++ remainder t e) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWords, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.remainder

  80. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 911
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 917
  82. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 941
  83. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.timePolynomial line 951
  84. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 954
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.machine line 970
  86. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.machineInTime line 983

    Source documentation

    A concrete finite-machine certificate, with neither a runtime nor a selection oracle among its hypotheses.

    def machineInTime (t : GraphTables.Table) (v : Fin t.vertices)
    (i : Fin (PreprocessingCloudIndex.cloudSize t v)) (querySuffix outputSuffix : List Bool)
    (register : Option Bool) :
    StateTransition.EvalsToInTime machine.step
      (cfg (some (.inr .initialize)) .checking (GraphTables.tableBits t)
        [] (queryWord v.val i.val querySuffix) [] [] outputSuffix () register)
      (some (cfg none .checking (GraphTables.tableBits t) [] (queryWord v.val i.val querySuffix)
        [] [] (encodeWord (PreprocessingCloudIndex.cloudSelect t v i).val.val ++ outputSuffix)
        () none))
      (timePolynomial.eval ((GraphTables.tableBits t).length + (queryWord v.val i.val querySuffix).length)) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudSelect.queryWord, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord