OAI/Computability/MaxCut/Games/FinalCNFOutput.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

The final machine's complete output stream is the exact serialization of its actual formula. This identity includes the two size fields, every clause and literal field, and all unary delimiters. No desired output equality is assumed.

  1. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 17
  2. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 20
  3. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 26
  4. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 32
  5. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 51
  6. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 57
  7. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 67

    Source documentation

    Reversing the finished stack accumulator restores the required output order.

    theorem reversed_accumulator_output (table : GraphTables.Table) :
    (formulaHeader table ++ outputStream rowPlan table (List.finRange table.darts)).reverse.reverse =
      formulaBits (FinalTableFormula.output table) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.formulaBits

  8. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 72
  9. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 84
  10. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 88
  11. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 93
  12. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 98

    Source documentation

    Header, at most N rows with guards, and the final output reversal.

    noncomputable def phaseTimePolynomial : Polynomial Nat :=
…
  13. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 103
  14. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 110
  15. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 116
  16. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 125

    Source documentation

    The bound specialized to the actual table and actual formula serialization.

    theorem table_phaseTime_le (table : GraphTables.Table) :
    headerTimePolynomial.eval (GraphTables.tableBits table).length +
      (table.darts * (rowTime rowPlan (GraphTables.tableBits table).length + 1) + 1) +
      ((formulaBits (FinalTableFormula.output table)).length + 1) ≤
        phaseTimePolynomial.eval (GraphTables.tableBits table).length :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.formulaBits

  17. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 135

    Source documentation

    Twelve private stacks are drained, then the finite state is reset. C is the fixed maximum number of pushes in a raw-program transition.

    noncomputable def finalTimePolynomial (C : Nat) : Polynomial Nat :=
…
  18. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 139
  19. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 146

    Source documentation

    Pure budget composition; the drain implementation supplies its own trace.

    theorem finalTime_le (C N workLength : Nat)
    (workBound : workLength ≤ N + phaseTimePolynomial.eval N * C) :
    phaseTimePolynomial.eval N + 12 * (workLength + 1) + 1 ≤
      (finalTimePolynomial C).eval N := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial

  20. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 166
  21. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 170
  22. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 175

    Source documentation

    Structural redirection changes only the destinations of goto and halt.

    def redirectStmt (labels : Λ → Λ') (haltTarget : Option Λ') :
    TM2.Stmt Γ Λ σ → TM2.Stmt Γ Λ' σ
  | .push k f next => .push k f (redirectStmt labels haltTarget next)
  | .peek k f next => .peek k f (redirectStmt labels haltTarget next)
  | .pop k f next => .pop k f (redirectStmt labels haltTarget next)
  | .load f next => .load f (redirectStmt labels haltTarget next)
  | .branch test yes no => .branch test
      (redirectStmt labels haltTarget yes) (redirectStmt labels haltTarget no)
  | .goto label => .goto (fun state => labels (label state))
  | .halt => match haltTarget with
    | none => .halt
    | some label => .goto (fun _ => label)
  23. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 188
  24. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.chosen line 209

    Source documentation

    The raw machine has thirteen tapes. These are precisely the twelve non-output tapes, including the original input and retained archive.

    def chosen : List Tape :=
…
  25. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.chosen_length line 213
  26. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 215
  27. abbrev OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.Label line 218
  28. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 222
  29. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.resetLabel line 225
  30. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 227
  31. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedProgram line 230
  32. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedMachine line 238
  33. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 249
  34. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.step_simulation line 254
  35. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.embedded_init line 273
  36. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 277
  37. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 287
  38. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 294

    Source documentation

    Actual drains followed by a real state-reset instruction reach canonical halt.

    def cleanupExecution (headerPlan rowPlan : Plan) (state : State Unit) (base : Tape → List Bool) :
    StateTransition.EvalsToInTime (completedMachine headerPlan rowPlan).step
      ⟨cleanupEntry headerPlan rowPlan, state, base⟩
      (some (haltList (completedMachine headerPlan rowPlan) (base .output)))
      (MachineDrainMany.steps chosen base + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedMachine, OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps, OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.chosen

  39. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 327

    Source documentation

    The extra cost is bounded from the actual raw execution, independently of the contents of its dirty private tapes and finite state.

    def outputsInTime (headerPlan rowPlan : Plan) (input output : List Bool)
    (state : State Unit) (base : Tape → List Bool) (budget : Nat)
    (raw : StateTransition.EvalsToInTime
      (FinalCNFMachine.Program.machine headerPlan rowPlan).step
      (initList (FinalCNFMachine.Program.machine headerPlan rowPlan) input)
      (some ⟨none, state, base⟩) budget)
    (correctOutput : base .output = output) :
    TM2OutputsInTime (completedMachine headerPlan rowPlan) input (some output)
      (budget + 12 * (input.length + budget *
        Runtime.programPushBound (FinalCNFMachine.Program.machine headerPlan rowPlan) + 1) + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.machine, OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedMachine, OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

  40. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedTime line 360

    Source documentation

    For fixed raw plans, polynomial raw time gives polynomial cleanup time.

    noncomputable def completedTime (headerPlan rowPlan : Plan) (rawTime : Polynomial Nat) : Polynomial Nat :=
…
  41. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 364
  42. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes_eq_formulaBits line 382
  43. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget_le_phaseTime line 386
  44. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.computableInPolyTime line 394

    Source documentation

    A concrete finite machine computes the complete CNF serialization from the exact unary graph-table serialization, with a proved polynomial bound.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime GraphTables.tableBits formulaBits FinalTableFormula.output where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.formulaBits