OAI/Computability/MaxCut/PCP/ExpanderFamily.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

A concrete finite family from the Cayley base

The initial graph has one vertex and the fixed number of loop ports. Each subsequent graph is the actual square-and-zigzag construction. Consequently the vertex sizes are exact powers of one fixed integer, including size one. The finite base is selected from the proved existence theorem.

  1. abbrev OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Port line 19
  2. abbrev OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.CloudPort line 20
  3. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth line 21
  4. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.card_port line 23
  5. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 27
  6. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 33
  7. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 36
  8. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 40
  9. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 43
  10. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 46
  11. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Vertex line 49
  12. instance OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.vertexFintype line 53
  13. instance OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 61
  14. instance OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 64
  15. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.graph line 73

    Source documentation

    The family is a recursive rotation algorithm when its fixed base is given.

    def graph (H : PortGraph CloudPort BasePort) : (n : Nat) → PortGraph (Vertex n) Port
  | 0 => { rot := Equiv.refl _, rot_involutive := fun _ => rfl }
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.CloudPort, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Vertex, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.Port

  16. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.graph_certificate line 77
  17. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.family line 100
  18. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.family_certificate line 102
  19. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.card_vertex line 105
  20. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.level line 114

    Source documentation

    The least geometric level covering a requested size. Nat.clog is the ordinary finite ceiling logarithm algorithm.

    def level (k : Nat) : Nat := Nat.clog growth k

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth

  21. def OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.size line 116
  22. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.le_size line 118
  23. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.size_le_mul line 120
  24. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.padded_family_size line 134
  25. def OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedSize line 159

    Source documentation

    Leave empty clouds empty; pad every positive size to a geometric level.

    def paddedSize (k : Nat) : Nat := if k = 0 then 0 else ExpanderFamily.size k

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.size

  26. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedSize_zero line 161
  27. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedSize_of_pos line 163
  28. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.le_paddedSize line 167
  29. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedSize_le_mul line 174
  30. def OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedCloudEquiv line 183

    Source documentation

    The actual padded tail fiber contains old darts and exactly the dummy darts indexed by that tail, with transport along the sigma index equality.

    def paddedCloudEquiv (G : ConstraintGraph V E A) (dummy : V → Type*) (v : V) :
    Cloud (paddedGraph G dummy) v ≃ Cloud G v ⊕ dummy v where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy

  31. def OAI.MaxCutGames.Foundations.PCP.CloudPadding.dartCloudEquiv line 207

    Source documentation

    Every original dart occurs in exactly one cloud.

    def dartCloudEquiv (G : ConstraintGraph V E A) : E ≃ Σ v : V, Cloud G v where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  32. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.sum_card_cloud line 218
  33. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_padded_cloud line 222
  34. abbrev OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy line 229

    Source documentation

    The precise number of always-accepting loop darts to add at each vertex.

    abbrev dummy (G : ConstraintGraph V E A) (v : V) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph

  35. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_cloud line 232
  36. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_dummy_of_empty line 240
  37. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_cloud_of_empty line 244
  38. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_cloud_eq_family line 249
  39. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_paddedDart_eq_sum line 258

    Source documentation

    Exact count over all padded tail fibers, including empty original fibers.

    theorem card_paddedDart_eq_sum (G : ConstraintGraph V E A) :
    Fintype.card (PaddedDart G (dummy G)) =
      ∑ v, paddedSize (Fintype.card (Cloud G v)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy, OAI.MaxCutGames.Foundations.PCP.CloudPadding.paddedSize

  40. theorem OAI.MaxCutGames.Foundations.PCP.CloudPadding.card_paddedDart_le line 272

    Source documentation

    Padding increases the total number of darts by at most the fixed family growth factor, independent of the number of empty vertices.

    theorem card_paddedDart_le (G : ConstraintGraph V E A) :
    Fintype.card (PaddedDart G (dummy G)) ≤ ExpanderFamily.growth * Fintype.card E := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.CloudPadding.dummy, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth

  41. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv line 304

    Source documentation

    An explicit complete list supplies both directions of a finite encoding. The forward direction searches the list; its inverse performs list indexing.

    def listEquiv {α : Type*} [BEq α] [LawfulBEq α] (xs : List α)
    (nodup : xs.Nodup) (complete : ∀ a, a ∈ xs) : α ≃ Fin xs.length where
…
  42. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_val line 313
  43. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.listEquiv_symm_apply line 317
  44. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts line 322

    Source documentation

    Retain the input dart order and test only the stored tail index.

    def cloudDarts (t : Table) (v : Fin t.vertices) : List (Fin t.darts) :=
…
  45. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.mem_cloudDarts line 325
  46. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_nodup line 329
  47. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_sublist line 335

    Source documentation

    Filtering preserves the original ordering, including repeated row values at different dart indices.

    theorem cloudDarts_sublist (t : Table) (v : Fin t.vertices) :
    (cloudDarts t v).Sublist (List.finRange t.darts) := List.filter_sublist

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts

  48. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize line 338
  49. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_le_darts line 340
  50. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect line 345

    Source documentation

    Read the original dart stored at a valid local cloud index.

    def cloudSelect (t : Table) (v : Fin t.vertices) (i : Fin (cloudSize t v)) :
    Cloud (semantics t) v :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  51. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank line 351

    Source documentation

    Find the local index of an original dart belonging to this cloud.

    def cloudRank (t : Table) (v : Fin t.vertices) (e : Cloud (semantics t) v) :
    Fin (cloudSize t v) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  52. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_val line 356
  53. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_val line 360
  54. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_cloudRank line 364
  55. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank_cloudSelect line 369
  56. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudEquiv line 376

    Source documentation

    This equivalence contains executable rank and select functions, including when both its domain and codomain are empty.

    def cloudEquiv (t : Table) (v : Fin t.vertices) :
    Cloud (semantics t) v ≃ Fin (cloudSize t v) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  57. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_card_cloud line 383
  58. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudDarts_eq_nil_iff line 387
  59. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize_eq_zero_iff line 391
  60. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.sum_cloudSize line 395
  61. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.oldCloudIndex line 405

    Source documentation

    An original global dart carries its own owner and executable local rank.

    def oldCloudIndex (t : Table) (e : Fin t.darts) :
    Fin (cloudSize t t.rows[e].tail) := cloudRank t t.rows[e].tail ⟨e, rfl⟩

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudRank

  62. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSelect_oldCloudIndex line 408
  63. abbrev OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud line 414

    Source documentation

    Padding counts are supplied as executable natural-valued data, without choosing enumerations of the semantic clouds by their cardinalities.

    abbrev PaddedCloud (t : Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) :=
…
  64. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedOld line 418
  65. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedNew line 422
  66. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudEquiv line 427

    Source documentation

    Local padded order: old cloud indices first, then increasing dummy index.

    def paddedCloudEquiv (t : Table) (padding : Fin t.vertices → Nat)
    (v : Fin t.vertices) : PaddedCloud t padding v ≃ Fin (cloudSize t v + padding v) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.cloudSize

  67. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank line 433
  68. def OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect line 437
  69. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_rank line 441
  70. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_select line 446
  71. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old line 451
  72. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new line 456
  73. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_old_val line 461
  74. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudRank_new_val line 466
  75. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_castAdd line 471
  76. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.paddedCloudSelect_natAdd line 483
  77. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.card_paddedCloud line 489
  78. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.rowIndex line 500
  79. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.rowIndex_val line 502
  80. structure OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table line 506

    Source documentation

    Stored reverse-dart indices, with a proof of the finite involution law.

    structure Table (v d : Nat) where
…
  81. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.reverseIndex line 510
  82. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.lookup line 513
  83. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.lookup_involutive line 516
  84. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph line 523
  85. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph_rot line 527
  86. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.ofGraph line 530
  87. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 538
  88. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph_ext_inline_ExpanderTables line 543
  89. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 551
  90. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.row_count line 554
  91. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexIndex line 558

    Source documentation

    Explicit mixed-radix vertex coordinates for one square/zigzag step.

    def vertexIndex (v q : Nat) : Fin v × (Fin q × Fin q) ≃ Fin (v * (q * q)) :=
…
  92. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.stepGraph line 562

    Source documentation

    The actual square/zigzag graph, expressed in the table's integer coordinates.

    def stepGraph {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d) :
    PortGraph (Fin (v * ((d * d) * (d * d)))) (Fin (d * d)) :=
…

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

  93. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.step line 571

    Source documentation

    Materialize every row of the next table in the declared order.

    def step {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d) :
    Table (v * ((d * d) * (d * d))) (d * d) := ofGraph (stepGraph G H)

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.ofGraph, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.stepGraph

  94. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.stepLookup line 576

    Source documentation

    A row uses exactly the displayed four lookups in already stored tables.

    def stepLookup {v d : Nat} (G : Table v (d * d))
    (H : Table ((d * d) * (d * d)) d)
    (x : Fin (v * ((d * d) * (d * d))) × Fin (d * d)) :
    Fin (v * ((d * d) * (d * d))) × Fin (d * d) :=
…

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

  95. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.lookup_step line 590
  96. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.step_certificate line 603
  97. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.initial line 614
  98. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.initial_certificate line 617
  99. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexCount line 627
  100. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 631
  101. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 636
  102. def OAI.MaxCutGames.Foundations.PCP.ExpanderTables.family line 643

    Source documentation

    A bottom-up vector of rotation rows. The recursive result is passed once to step, whose row formula reads only that already materialized table.

    def family {d : Nat} (H : Table ((d * d) * (d * d)) d) :
    (n : Nat) → Table (vertexCount (d * d) n) (d * d)
  | 0 => initial d
  | n + 1 => step (family H n) H

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexCount, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.initial, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.step

  103. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.family_certificate line 648
  104. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.family_row_count line 659
  105. theorem OAI.MaxCutGames.Foundations.PCP.ExpanderTables.exists_base_table line 664

    Source documentation

    The only selected data is one fixed finite table, independent of the input.

    theorem exists_base_table : ∃ H : Table
    ((Expanders.baseDegree * Expanders.baseDegree) *
      (Expanders.baseDegree * Expanders.baseDegree)) Expanders.baseDegree,
    SpectralCertificate (graph H) (1 / 100 : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph

  106. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop line 687
  107. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop_level_le line 694

    Source documentation

    At most fuel continuing iterations can increment the exponent.

    theorem levelLoop_level_le (g k fuel e s : Nat) :
    (levelLoop g k fuel e s).1 ≤ e + fuel := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop

  108. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop_power line 706

    Source documentation

    The carried size remains the exact power of the carried exponent.

    theorem levelLoop_power (g k fuel e : Nat) :
    (levelLoop g k fuel e (g ^ e)).2 =
      g ^ (levelLoop g k fuel e (g ^ e)).1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop

  109. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop_covers line 717
  110. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop_le_of_covering_power line 734

    Source documentation

    The search never passes an exponent whose power already covers the request. This remains true even without a sufficient fuel budget.

    theorem levelLoop_le_of_covering_power (g k fuel e j : Nat)
    (he : e ≤ j) (hj : k ≤ g ^ j) :
    (levelLoop g k fuel e (g ^ e)).1 ≤ j := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.levelLoop

  111. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.searchResult line 751
  112. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel line 755

    Source documentation

    An executable exponent, computed with at most k multiplications.

    def boundedLevel (k : Nat) : Nat := (searchResult k).1

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.searchResult

  113. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize line 758

    Source documentation

    The algorithm returns the power it has already computed.

    def paddedSize (k : Nat) : Nat := (searchResult k).2

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.searchResult

  114. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_zero line 760
  115. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize_zero line 762
  116. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_input line 764
  117. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize_power line 768
  118. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.le_paddedSize line 773
  119. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_eq_level line 778

    Source documentation

    The bounded multiplication loop computes the existing ceiling logarithm.

    theorem boundedLevel_eq_level (k : Nat) :
    boundedLevel k = ExpanderFamily.level k := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.level

  120. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize_eq_size line 788
  121. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel_le_of_le_power line 793

    Source documentation

    The returned exponent is the least exponent whose power covers k.

    theorem boundedLevel_le_of_le_power {k j : Nat}
    (h : k ≤ ExpanderFamily.growth ^ j) : boundedLevel k ≤ j := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel

  122. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize_positive line 798
  123. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize_bounds line 804

    Source documentation

    Positive cloud sizes and positive whole-graph vertex counts increase by at most the single fixed growth factor.

    theorem paddedSize_bounds {k : Nat} (hk : 0 < k) :
    k ≤ paddedSize k ∧ paddedSize k ≤ ExpanderFamily.growth * k := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize, OAI.MaxCutGames.Foundations.PCP.ExpanderFamily.growth

  124. def OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize line 810

    Source documentation

    Empty clouds remain empty; nonempty clouds use the geometric family.

    def cloudPaddedSize (k : Nat) : Nat := if k = 0 then 0 else paddedSize k

    Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize

  125. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_zero line 812
  126. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_of_pos line 814
  127. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.cloudPaddedSize_bounds line 818
  128. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.table_vertexCount_eq_paddedSize line 827

    Source documentation

    The executable table family has exactly the size returned by the loop.

    theorem table_vertexCount_eq_paddedSize (k : Nat) :
    ExpanderTables.vertexCount (Expanders.baseDegree * Expanders.baseDegree)
        (boundedLevel k) = paddedSize k := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.vertexCount, OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.paddedSize

  129. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.family_row_count_at_size line 838