OAI/Computability/UniqueGames/Machines/FinalCNFOutputLemmas.lean

GitHub source file

22 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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 26
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 29
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 35
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 41
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 60
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 66
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 76

    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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.outputStream, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 81
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 89
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 93
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 98
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 103

    Source documentation

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

    noncomputable def phaseTimePolynomial : Polynomial Nat :=
…
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 108
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 115
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 121
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 130

    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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowTime, OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits

  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 140

    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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 144
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 151

    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.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial

  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes_eq_formulaBits line 168
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.rawBudget_le_phaseTime line 172
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.FinalCNFMachine.Program.computableInPolyTime line 180

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