OAI/Computability/UniqueGames/Machines/MachineRegularMetadata.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Actual metadata preparation for an original regularized vertex. The shared 27-tape row interface is preserved, with two explicit extra outputs for padding count and geometric level. Family generation is a subsequent stage and owns the rotor tape.

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Extra line 20
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Extra.enumList line 24
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_getElem?_ctorIdx_eq line 26
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_nodup line 30
  5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.(instance at line 32) line 32
  6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Tape line 36
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Alphabet line 37
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.State line 38
  9. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Label line 40
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 52

    Source documentation

    Original table, affine query, copied scan, owner output, and scratch.

    def ownerTapes : Fin 5 → Tape := ![.inl 0, .inl 9, .inl 10, .inl 2, .inl 11]

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Tape

  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankTape line 54
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixTape line 62
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudTape line 77
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program line 93

    Source documentation

    Fixed finite code. Original graph/global-index inputs are never replaced by specification values; owner and rank queries are produced on the tapes.

    def program : Label → TM2.Stmt Alphabet Label (State σ)
  | .owner l => MachineAffineLookup.instruction (.inl 1) ownerTapes 4098 2
      Label.owner (some .ownerClearQuery) l
  | .ownerClearQuery => MachineDrain.drain (.inl 9) .ownerClearQuery (some .ownerClearWork)
  | .ownerClearWork => MachineDrain.drain (.inl 10) .ownerClearWork (some .copyXFirst)
  | .copyXFirst => Reduction.MachineTransfer.loopAt (.inl 1) (.inl 10) id false
      .copyXFirst (some .copyXSecond)
  | .copyXSecond => MachineCopy.forkLoop (.inl 10) (.inl 1) (.inl 9) false
      .copyXSecond (some .copyOwnerFirst)
  | .copyOwnerFirst => Reduction.MachineTransfer.loopAt (.inl 2) (.inl 10) id false
      .copyOwnerFirst (some .copyOwnerSecond)
  | .copyOwnerSecond => MachineCopy.forkLoop (.inl 10) (.inl 2) (.inl 9) false
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAffineLookup.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drain, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCopy.forkLoop

  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankView line 119
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixView line 130
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudView line 148
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankView_left line 162
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankView_right line 164
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 170
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 176
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 182
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 184
  24. structure OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data line 192

    Source documentation

    Boundary data is a specification of physical tape contents, never part of the machine's finite control state. All eighteen core work tapes are empty.

    structure Data where
…
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.frame line 205
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.frame_index line 220
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 223
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg line 226
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudData line 230
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 238

    Source documentation

    Common owner-based stage for original and dummy vertices. The count, padding, and level are actual outputs of the checked physical cloud scan.

    theorem cloudTrace (t : GraphTables.Table) (v : Fin t.vertices) (data : Data)
    (htable : data.table = GraphTables.tableBits t) (howner : data.owner = encodeWord v.val)
    (hcount : data.count = []) (hpadding : data.padding = []) (hlevel : data.level = [])
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[MachineCloudPadding.totalTime t v]
      (some (cfg (some (.cloud .init)) data ambient register)) =
      some (cfg none (cloudData t v data) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudData

  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.join_trace line 274
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.drainAt line 278
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixData line 288
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 292
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 297

    Source documentation

    The actual padding-prefix scan, followed by removal of its copied query and exhausted fuel. Every other core field is preserved.

    theorem prefixTrace (t : GraphTables.Table) (v : Fin t.vertices) (data : Data)
    (htable : data.table = GraphTables.tableBits t) (howner : data.owner = encodeWord v.val)
    (hoffset : data.offset = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[prefixSteps t v]
      (some (cfg (some (.prefixCode .init)) data ambient register)) =
      some (cfg (some (.cloud .init)) (prefixData t v data) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.prefixData

  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.selected_owner line 349
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerData line 357
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 360
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 363
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 369

    Source documentation

    The owner is read from its actual field at 4098*x+2; arithmetic, table copy, lookup, and cleanup all execute in the finite machine.

    theorem ownerTrace (t : GraphTables.Table) (e : Fin t.darts) (data : Data)
    (htable : data.table = GraphTables.tableBits t)
    (hindex : data.globalIndex = encodeWord e.val) (howner : data.owner = [])
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[ownerSteps t e]
      (some (cfg (some (.owner .seed)) data ambient register)) =
      some (cfg (some .copyXFirst) (ownerData t e data) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerData

  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankQuery line 415
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.queryFrame line 417
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.querySteps line 421
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.queryTrace line 425

    Source documentation

    Two preserving copy loops physically create [owner,x]; a transition then initializes the unary result counter.

    theorem queryTrace (data : Data) (v x : Nat)
    (howner : data.owner = encodeWord v) (hindex : data.globalIndex = encodeWord x)
    (hrank : data.localRank = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[querySteps v x]
      (some (cfg (some .copyXFirst) data ambient register)) =
      some ⟨some (.rank .queryFirst), ((ambient, false), none), queryFrame data v x⟩ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.querySteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.queryFrame

  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankData line 462
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 466
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankSteps line 470
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankTrace line 478

    Source documentation

    Rank is computed by physically scanning earlier original rows, with the fresh query and copied scan/fuel all removed before the next phase.

    theorem rankTrace (t : GraphTables.Table) (v : Fin t.vertices)
    (e : DegreeReplacement.Cloud (GraphTables.semantics t) v) (data : Data)
    (htable : data.table = GraphTables.tableBits t)
    (howner : data.owner = encodeWord v.val) (hindex : data.globalIndex = encodeWord e.val.val)
    (hrank : data.localRank = []) (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[rankSteps t v e]
      (some (cfg (some .copyXFirst) data ambient register)) =
      some (cfg (some (.prefixCode .init)) (rankData t v e data) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankSteps, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankData

  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalMember line 543

    Source documentation

    Membership is a statement about the actual stored tail, used only to identify the numeric answer of the physical rank routine.

    def originalMember (t : GraphTables.Table) (e : Fin t.darts) :
    DegreeReplacement.Cloud (GraphTables.semantics t) t.rows[e].tail := ⟨e, rfl⟩
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalData line 546
  51. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.totalTime line 550
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalTrace line 557

    Source documentation

    Full original-vertex metadata preparation. Inputs and all row/output fields are preserved, results occupy their agreed physical tapes, and every one of the eighteen core work tapes is empty at return.

    theorem originalTrace (t : GraphTables.Table) (e : Fin t.darts) (data : Data)
    (htable : data.table = GraphTables.tableBits t)
    (hindex : data.globalIndex = encodeWord e.val)
    (howner : data.owner = []) (hrank : data.localRank = []) (hcount : data.count = [])
    (hoffset : data.offset = []) (hpadding : data.padding = []) (hlevel : data.level = [])
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step program))^[totalTime t e]
      (some (cfg (some (.owner .seed)) data ambient register)) =
      some (cfg none (originalData t e data) ambient none) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.totalTime, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalData

  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le line 578
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 585
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 589
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 600
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.overhead line 604
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.overhead_le line 608
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 613
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalInTime line 664

    Source documentation

    Concrete timed execution certificate, with no runtime premise.

    def originalInTime (t : GraphTables.Table) (e : Fin t.darts) (data : Data)
    (htable : data.table = GraphTables.tableBits t)
    (hindex : data.globalIndex = encodeWord e.val)
    (howner : data.owner = []) (hrank : data.localRank = []) (hcount : data.count = [])
    (hoffset : data.offset = []) (hpadding : data.padding = []) (hlevel : data.level = [])
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      (cfg (some (.owner .seed)) data ambient register)
      (some (cfg none (originalData t e data) ambient none))
      (timePolynomial.eval (GraphTables.tableBits t).length) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.originalData

  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 681

    Source documentation

    The common dummy-owner path also carries the checked physical scan's polynomial certificate; the caller's existing rank, prefix, and rotor survive.

    def cloudInTime (t : GraphTables.Table) (v : Fin t.vertices) (data : Data)
    (htable : data.table = GraphTables.tableBits t) (howner : data.owner = encodeWord v.val)
    (hcount : data.count = []) (hpadding : data.padding = []) (hlevel : data.level = [])
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      (cfg (some (.cloud .init)) data ambient register)
      (some (cfg none (cloudData t v data) ambient none))
      (MachineCloudPadding.timePolynomial.eval (MachineCloudPadding.inputLength t v [])) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.Data, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRegularMetadata.cloudData, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.inputLength