OAI/Computability/MaxCut/Machines/MachineTableIteration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial-time iteration of the concrete graph-table round. A certificate for that one body is the only supplied machine input. Counter preparation, repeated calls, tape handoffs, and final cleanup are all proved.

  1. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.finalTable line 15
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.counterCertificate line 18
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.countedCertificate line 28

    Source documentation

    The generic repeat machine executes only the actual successive graph words. Its polynomial bound uses the proved linear growth of their semantic sizes.

    noncomputable def countedCertificate :
    TM2ComputableInPolyTime countedBits GraphTables.tableBits (finalTable H) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.finalTable

  4. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.computableInPolyTime line 66

    Source documentation

    One actual finite machine computes the complete logarithmic iteration.

    noncomputable def computableInPolyTime :
    TM2ComputableInPolyTime inputBits GraphTables.tableBits (finalTable H) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.finalTable

  5. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.initialCertificate line 70
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.tableCertificate line 78

    Source documentation

    The initial graph and entire repeated table transformation have concrete finite-machine executions with the same formula and table encodings.

    noncomputable def tableCertificate :
    TM2ComputableInPolyTime formulaBits GraphTables.tableBits (TableIteration.outputTable H) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.formulaBits

  7. def OAI.MaxCutGames.Foundations.Complexity.MachineTableIteration.gapMapCertificate line 87

    Source documentation

    Actual 3SAT gap-map runtime follows from the one concrete round certificate; initialization, variable repetition, and the final CNF converter are supplied.

    noncomputable def gapMapCertificate :
    TM2ComputableInPolyTime formulaBits formulaBits (TableIteration.gapMap H) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.formulaBits

  8. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.initial line 99
  9. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.finalCNF line 104
  10. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.counter line 109
  11. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.counted line 121
  12. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.iteration line 124
  13. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.table line 128
  14. theorem OAI.MaxCutGames.Foundations.Complexity.TableIterationFiniteAlphabet.gapMap line 132