OAI/Computability/MaxCut/PCP/TableIteration.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Iteration of the concrete stored-table round, with the original formula's actual initial graph size controlling the number of rounds.

  1. def OAI.MaxCutGames.Foundations.PCP.TableIteration.run line 15
  2. def OAI.MaxCutGames.Foundations.PCP.TableIteration.runTables line 19

    Source documentation

    The same data computation on all validated tables; positivity is an invariant, and is erased from the runtime path.

    def runTables (H : BaseTable) : Nat → GraphTables.Table → GraphTables.Table :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table

  3. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.run_val line 22
  4. def OAI.MaxCutGames.Foundations.PCP.TableIteration.iterationCount line 30
  5. def OAI.MaxCutGames.Foundations.PCP.TableIteration.output line 32
  6. def OAI.MaxCutGames.Foundations.PCP.TableIteration.outputTable line 34
  7. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_val line 37
  8. def OAI.MaxCutGames.Foundations.PCP.TableIteration.gapMap line 40
  9. opaque OAI.MaxCutGames.Foundations.PCP.TableIteration.degreeData line 44

    Source documentation

    A checked initialized degree avoids evaluating enormous fixed logarithms while applying polynomial identities. Its bound is part of the stored data.

    opaque degreeData : {n : Nat // sizeFactor ≤ 2 ^ n} :=
…
  10. def OAI.MaxCutGames.Foundations.PCP.TableIteration.polynomialDegree line 47
  11. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 49
  12. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.run_completeness line 52
  13. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_completeness line 56
  14. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.gapMap_completeness line 60
  15. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_darts_positive line 66
  16. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.gapMap_nonempty line 70
  17. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.run_size line 73
  18. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_size line 77
  19. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.initial_size_le line 82
  20. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_size_le_input line 85
  21. def OAI.MaxCutGames.Foundations.PCP.TableIteration.tableSizePolynomial line 93
  22. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 96
  23. def OAI.MaxCutGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 101
  24. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.output_bits_le line 104
  25. def OAI.MaxCutGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 109
  26. theorem OAI.MaxCutGames.Foundations.PCP.TableIteration.gapMap_bits_le line 112
  27. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 131
  28. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 137
  29. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 140
  30. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 147

    Source documentation

    Pull target raw labels back to old port coordinates; this is a bijection.

    def labelEquiv (ports : D ≃ E) (t : Nat) : PaddedLabel E t A ≃ PaddedLabel D t A where
…
  31. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 159
  32. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 167
  33. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.reach_iff line 171
  34. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 182
  35. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 188
  36. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.pullSelector line 195

    Source documentation

    Use the target selector, including its concrete enumeration choices.

    def pullSelector {t : Nat} {v : V} (S : AddressSelector H t v) :
    AddressSelector G t v where
…
  37. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 203
  38. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.decode_transport line 209
  39. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 219
  40. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 232
  41. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 240
  42. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 255
  43. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 258
  44. def OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 284
  45. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 287
  46. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 300
  47. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 321
  48. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.pullReverse line 338
  49. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 344
  50. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 354
  51. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 383

    Source documentation

    The generic lazy-graph gap survives a genuine rotation-preserving port change and the target's chosen selectors, for every raw target labeling.

    theorem uniform_count_gap
    [Fintype V] [Fintype D] [Fintype E] [Nonempty V] [Nonempty D]
    [Fintype A] [Nonempty A]
    (G : PortGraph V D) (H : PortGraph V E) (ports : (Bool × D) ≃ E)
    (rotation : ∀ v d, H.rot (v, ports d) =
      (((lazyGraph G).rot (v,d)).1, ports ((lazyGraph G).rot (v,d)).2))
    (lambda : ℝ) (certificate : SpectralCertificate (lazyGraph G) lambda)
    (accepts : Edge V E → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts (H.rot e) b a = accepts e a b)
    (M : Nat) (hM : 1 ≤ M)
    (selectors : ∀v, AddressSelector H (2*center (Fintype.card A) M+1) v)
    (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.accepts

  52. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 423

    Source documentation

    Gap bound for the actual numbered power table built from a lazified port table. The spectral certificate is on the genuine Boolean-flag lazy graph.

    theorem lazy_table_uniform_count_gap {vertices d : Nat}
    (input : PortTables.Table vertices d) (hv : 0 < vertices) (hd : 0 < d)
    (lambda : ℝ)
    (certificate : SpectralCertificate (lazyGraph (PortTables.portGraph input)) lambda)
    (M : Nat) (hM : 1 ≤ M) (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
    (hgap : ∀ assignment : Fin vertices → Fin 64,
      epsilon * (Fintype.card (Fin vertices × Fin (2*d)) : ℝ) ≤
        ((PortTables.baseGraph (PreprocessingOverlayTables.lazy input)).rejectionCount assignment : ℝ)) :
    ∀ labels : PoweringTableSemantics.EncodedLabeling vertices (2*d) (2*center 64 M),
    (gain 64 M lambda * min epsilon (1 / ((2*center 64 M+1 : Nat) : ℝ))) *
      ((PoweringTables.table (PreprocessingOverlayTables.lazy input) (2*center 64 M)).darts : ℝ) ≤
      ((GenericGraphTables.semantics
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics

  53. theorem OAI.MaxCutGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 463

    Source documentation

    The same exact table bound with a separately stored walk parameter. Its proved equality may be used without evaluating a huge closed alphabet size.

    theorem lazy_table_uniform_count_gap_at {vertices d : Nat}
    (input : PortTables.Table vertices d) (hv : 0 < vertices) (hd : 0 < d)
    (lambda : ℝ)
    (certificate : SpectralCertificate (lazyGraph (PortTables.portGraph input)) lambda)
    (M : Nat) (hM : 1 ≤ M) (n : Nat) (hn : n = 2*center 64 M)
    (epsilon : ℝ) (hepsilon : 0 ≤ epsilon)
    (hgap : ∀ assignment : Fin vertices → Fin 64,
      epsilon * (Fintype.card (Fin vertices × Fin (2*d)) : ℝ) ≤
        ((PortTables.baseGraph (PreprocessingOverlayTables.lazy input)).rejectionCount
          assignment : ℝ)) :
    ∀ labels : PoweringTableSemantics.EncodedLabeling vertices (2*d) n,
    (gain 64 M lambda * min epsilon (1 / ((n+1 : Nat) : ℝ))) *
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.MaxCutGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling

  54. theorem OAI.MaxCutGames.Foundations.PCP.RoundTableGap.powered_count_gap line 500
  55. theorem OAI.MaxCutGames.Foundations.PCP.RoundTableGap.build_count_gap line 531
  56. theorem OAI.MaxCutGames.Foundations.PCP.RoundTableGap.step_gap line 546
  57. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.run_gap line 570
  58. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.output_gap line 575
  59. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.output_satisfiable_iff line 583
  60. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.gapMap_satisfiable_iff line 593
  61. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.output_count_gap line 597
  62. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.gapMap_clauseGap line 617
  63. theorem OAI.MaxCutGames.Foundations.PCP.TableGapReduction.finalClauseGap_le_one line 623