OAI/Computability/UniqueGames/PCP/FinalTableFormula.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The exact table-to-formula converter used by the final CNF machine. Its semantic count premise is explicit; amplification supplies that premise elsewhere. The converter chooses no vertex or dart numbering.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.output line 17
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.satisfiable_iff line 20
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.variable_count line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.clause_count line 31
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.nonempty line 35
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 40

    Source documentation

    Boolean labels and numeric labels have exactly the same rejected darts.

    theorem tableGraph_rejectionCount (table : GraphTables.Table)
    (labeling : Fin table.vertices → FinalBooleanVerifier.Label) :
    (FinalCNFPattern.tableGraph table).rejectionCount labeling =
      (GraphTables.semantics table).rejectionCount
        (fun v => FinalCNFPattern.labelEquiv (labeling v)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics

  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 51

    Source documentation

    A uniform numeric-label count bound transfers to the machine's Boolean-label graph.

    theorem tableGraph_count_lower (table : GraphTables.Table) (walkLength : Nat)
    (hgap : ∀ labeling : Fin table.vertices → GraphTables.Label,
      table.darts ≤ walkLength * (GraphTables.semantics table).rejectionCount labeling)
    (labeling : Fin table.vertices → FinalBooleanVerifier.Label) :
    Fintype.card (Fin table.darts) ≤
      walkLength * (FinalCNFPattern.tableGraph table).rejectionCount labeling := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.FinalBooleanVerifier.Label

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.clauseGap line 60
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.total_size_le line 70
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.sizePolynomial line 78

    Source documentation

    A fixed quadratic in the full serialized input length.

    noncomputable def sizePolynomial : Polynomial Nat :=
…
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 83
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 87