OAI/Computability/MaxCut/Machines/MachineSubdivisionEmission.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Literal output-header emission and the initial occurrence-loop frame.

  1. def OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.headerBits line 15
  2. def OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.resultTapes line 17
  3. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.header_template line 21
  4. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.header_copiedLength line 29
  5. theorem OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.header_result line 37
  6. def OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.headerInTime line 43
  7. def OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.prepareInTime line 62

    Source documentation

    From raw input headers to the running occurrence loop, including all finite arithmetic phases and literal output-header emission.

    def prepareInTime (q n Q : Nat) (body : List Bool) :
    StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) (encodeWords [n, q, Q] ++ body))
      (some ⟨some .guard, initialState, resultTapes n q Q body⟩)
      (n + q + Q + 6 + 9 * MachineSubdivisionInit.stageCost n Q +
        (3 * (n + 7 * Q + 2) + 10)) := by
…

    Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.resultTapes, OAI.MaxCutGames.Explicit.MachineSubdivisionInit.stageCost