OAI/Computability/MaxCut/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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Extra line 16
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList line 19
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_getElem?_ctorIdx_eq line 21
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_nodup line 25
  5. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.(instance at line 27) line 27
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Tape line 31
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Alphabet line 32
  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.State line 33
  9. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Label line 35
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 47

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Tape

  11. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankTape line 49
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixTape line 57
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudTape line 72
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program line 88

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.State, OAI.MaxCutGames.Foundations.Complexity.MachineAffineLookup.instruction, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes, OAI.MaxCutGames.Foundations.Complexity.MachineDrain.drain, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop

  15. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankView line 114
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixView line 125
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudView line 143
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankView_left line 157
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankView_right line 159
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 165
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 171
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 177
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 179
  24. structure OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data line 187

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.frame line 200
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.frame_index line 215
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 218
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg line 221
  29. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudData line 225
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 233

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudData

  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.join_trace_inline_MachineRegularMetadata line 269
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.drainAt_inline_MachineRegularMetadata line 273
  33. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixData line 283
  34. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 287
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 292

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.prefixData

  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.selected_owner line 344
  37. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerData line 352
  38. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 355
  39. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 358
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 364

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerData

  41. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankQuery line 410
  42. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.queryFrame line 412
  43. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.querySteps line 416
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.queryTrace line 420

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.querySteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.queryFrame

  45. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankData line 459
  46. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 463
  47. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankSteps line 467
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankTrace line 475

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankSteps, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankData

  49. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalMember line 540

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalData line 543
  51. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.totalTime line 547
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalTrace line 554

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalData

  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le_inline_MachineRegularMetadata line 575
  54. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 582
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 586
  56. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 597
  57. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.overhead line 601
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.overhead_le line 605
  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 610
  60. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalInTime line 661

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.originalData

  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 678

    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.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.Data, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cfg, OAI.MaxCutGames.Foundations.Complexity.MachineRegularMetadata.cloudData, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.inputLength