OAI/Computability/UniqueGames/PCP/PreprocessingTablesLemmas.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Concrete preprocessing table algorithm

Given one fixed expander base table, this function computes regularized cloud rows, pads the whole vertex set, overlays a stored family table, and adds the half-lazy rows. It is total even on zero-dart input tables. The bounds below concern actual output data; an actual TM2 execution certificate is a separate theorem and is not inferred from these size bounds.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.BaseTable line 33
  2. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.degree line 35
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.degree_eq line 37
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.regularVertices line 42
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices line 43
  6. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.padded line 45
  7. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.overlayFamily line 50
  8. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.preprocess line 55
  9. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.output line 60
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.graphTable line 63
  11. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.outputBits line 66
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 69
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.regularVertices_le line 73
  14. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices_positive line 76
  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 79
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 89
  17. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices_le line 95

    Source documentation

    The total algorithm also has a uniform data bound on empty inputs.

    theorem vertices_le (t : GraphTables.Table) :
    vertices t ≤ ExpanderFamily.growth ^ 2 * (t.darts + 1) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth

  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.darts_eq line 105
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.darts_le line 108
  20. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 116
  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 121
  22. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 146
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 160
  24. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 174
  25. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 182
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 192

    Source documentation

    The concrete generated rows have the required absolute contraction.

    theorem spectral_certificate (H : BaseTable)
    (certificate : SpectralCertificate (ExpanderTables.graph H) (1 / 100 : ℝ))
    (t : GraphTables.Table) :
    SpectralCertificate (PortTables.portGraph (preprocess H t)) (31 / 32 : ℝ) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph

  27. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 200
  28. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 205
  29. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.roundLabels line 213
  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.soundness line 217
  31. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.completeness line 225
  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 238
  33. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.inputLength line 282
  34. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.cloudSize_le_input line 284
  35. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.cloudTotal_le_input line 288
  36. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.level_le_input line 294
  37. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.regularVertices_le_input line 298
  38. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.offset_le_sum line 303
  39. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.prefix_le_input line 314
  40. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.tablePolynomial line 323

    Source documentation

    A two-parameter bound for the complete unary graph codec.

    noncomputable def tablePolynomial (a b : Nat) : Polynomial Nat :=
…
  41. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.tableBits_le_of_counts line 328
  42. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.regularPolynomial line 338
  43. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.regularBits_le line 341
  44. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.rotorPolynomial line 355
  45. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingMachineBounds.cloudRotorBits_le line 359
  46. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.BaseTable line 386
  47. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.regular line 388
  48. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.padding line 391
  49. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.familyAt line 395
  50. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.paddedOverlay line 400
  51. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.lazy line 405
  52. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.output_eq line 410

    Source documentation

    Exact equality with the original executable constructor, including all chosen row coordinates and the actual fixed base table.

    theorem output_eq (H : BaseTable) (t : GraphTables.Table) :
    PreprocessingTables.output H t =
      lazy ((internalDegree + 1) + internalDegree)
        (paddedOverlay H (internalDegree + 1) (regular H t)) := rfl
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.output, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.lazy, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.paddedOverlay, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingStageMaps.regular

  53. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundGap.poweredLower line 430
  54. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundGap.poweredLower_nonnegative line 434
  55. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundGap.powered_count_gap line 442
  56. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundGap.amplifies line 470