OAI/Computability/MaxCut/PCP/PreprocessingRegularSoundness.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the executable regularization tables

The fixed input base table is required only to have its proved spectral certificate. Every positive cloud uses the actual recursively generated table at its computed size. Its spectral certificate gives the precise cut bound used by majority rounding. Empty clouds are handled by their zero cardinality. Thus neither expansion nor the desired count comparison is an input premise.

  1. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 20
  2. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 24
  3. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 31

    Source documentation

    Erasing a proof-equal table size preserves its exact spectral certificate.

    theorem resizeTable_certificate {n m q : Nat} (h : n = m)
    (table : ExpanderTables.Table n q) (lambda : ℝ)
    (certificate : SpectralCertificate (ExpanderTables.graph table) lambda) :
    SpectralCertificate (ExpanderTables.graph (resizeTable h table)) lambda := by
…

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

  4. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 38
  5. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 49
  6. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 59

    Source documentation

    The exact finite cut inequality needed to pay for each changed cloud label.

    theorem cloud_expansion (H : BaseTable)
    (certificate : SpectralCertificate (ExpanderTables.graph H) (1 / 100 : ℝ))
    (t : GraphTables.Table) (v : Fin t.vertices)
    (S : Finset (PreprocessingCloudIndex.PaddedCloud t (padding t) v))
    (hsmall : S.card ≤
      Fintype.card (PreprocessingCloudIndex.PaddedCloud t (padding t) v) / 2) :
    2 * S.card ≤ (CloudRounding.directedCut
      (fun ed => ((cloudGraphs t (padding t) (familyCloudTable H t) v).rot ed).1) S).card := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud, OAI.MaxCutGames.Foundations.PCP.CloudRounding.directedCut

  7. def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 82

    Source documentation

    Decode the actual numbered output labels by majority in each padded cloud.

    noncomputable def roundLabels (t : GraphTables.Table)
    (labels : Fin (vertexCount t (padding t)) → GraphTables.Label) :
    Fin t.vertices → GraphTables.Label :=
…

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

  8. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 90

    Source documentation

    Direct soundness for the generated tables, with no matching-base premise.

    theorem soundness (H : BaseTable)
    (certificate : SpectralCertificate (ExpanderTables.graph H) (1 / 100 : ℝ))
    (t : GraphTables.Table)
    (labels : Fin (vertexCount t (padding t)) → GraphTables.Label) :
    (GraphTables.semantics t).rejectionCount (roundLabels t labels) ≤
      (PortTables.baseGraph (regularize H t)).rejectionCount labels := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph

  9. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 101
  10. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 111

    Source documentation

    Completeness preserves the number of rejected original dart occurrences.

    theorem lift_rejectionCount (H : BaseTable) (t : GraphTables.Table)
    (labels : Fin t.vertices → GraphTables.Label) :
    (PortTables.baseGraph (regularize H t)).rejectionCount
        (liftedLabel t (padding t) labels) = (GraphTables.semantics t).rejectionCount labels :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GraphTables.Label, OAI.MaxCutGames.Foundations.PCP.PortTables.baseGraph, OAI.MaxCutGames.Foundations.PCP.GraphTables.semantics

  11. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 117
  12. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 139
  13. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 148
  14. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext_inline_PreprocessingTableSpectral line 170
  15. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 179

    Source documentation

    Materialization retains exactly the explicitly reindexed rotation.

    theorem materialize_portGraph {n d : Nat} {D : Type*}
    (G : ConstraintGraph (Fin n) (Fin n × D) PortTables.Label)
    (ports : D ≃ Fin d) :
    PortTables.portGraph (PreprocessingOverlayTables.materialize G ports) =
      GraphTransport.reindex (Overlay.originalPortGraph G) (Equiv.refl _) ports := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.PortTables.Label, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.materialize, OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex, OAI.MaxCutGames.Foundations.PCP.Overlay.originalPortGraph

  16. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 191

    Source documentation

    The stored overlaid graph is the actual semantic overlay in numbered port coordinates. This is equality of reversible port graphs.

    theorem overlay_portGraph {n d e : Nat} (G : PortTables.Table n d)
    (H : ExpanderTables.Table n e) :
    PortTables.portGraph (PreprocessingOverlayTables.overlay G H) =
      GraphTransport.reindex
        (Overlay.portGraph (PortTables.portGraph G) (ExpanderTables.graph H))
        (Equiv.refl _) (PreprocessingOverlayTables.overlayPorts d e) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay, OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex, OAI.MaxCutGames.Foundations.PCP.Overlay.portGraph, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts

  17. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 201
  18. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 212

    Source documentation

    The stored lazy graph is exactly the Boolean-flag lazy graph, with the declared false-first port encoding.

    theorem lazy_portGraph {n d : Nat} (G : PortTables.Table n d) :
    PortTables.portGraph (PreprocessingOverlayTables.lazy G) =
      GraphTransport.reindex (lazyGraph (PortTables.portGraph G))
        (Equiv.refl _) (PreprocessingOverlayTables.lazyPorts d) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.MaxCutGames.Foundations.PCP.GraphTransport.reindex, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts

  19. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 220
  20. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 231

    Source documentation

    An actual half-spectral expander overlay gives a 7/8 certificate for the stored table. The original table needs no spectral certificate. The degree hypothesis supplies nonempty old and expander port types.

    theorem overlay_certificate_seven_eighths {n d e : Nat}
    (G : PortTables.Table n d) (H : ExpanderTables.Table n e)
    (hn : 0 < n) (hdegree : d = e + 1) (he : 8 ≤ e)
    (hH : SpectralCertificate (ExpanderTables.graph H) (1 / 2 : ℝ)) :
    SpectralCertificate (PortTables.portGraph (PreprocessingOverlayTables.overlay G H))
      (7 / 8 : ℝ) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.graph, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph, OAI.MaxCutGames.Foundations.PCP.PreprocessingOverlayTables.overlay

  21. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 249

    Source documentation

    An actual 7/8 certificate gives a 31/32 certificate for the materialized lazy table. Only the original port set must be nonempty.

    theorem lazy_certificate_31_32 {n d : Nat} (G : PortTables.Table n d)
    (hd : 0 < d) (hG : SpectralCertificate (PortTables.portGraph G) (7 / 8 : ℝ)) :
    SpectralCertificate (PortTables.portGraph (PreprocessingOverlayTables.lazy G))
      (31 / 32 : ℝ) := by
…

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

  22. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 273
  23. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 286
  24. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 299
  25. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 307
  26. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 317

    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.MaxCutGames.Foundations.PCP.ExpanderTables.graph, OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PortTables.portGraph

  27. def OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 325
  28. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 330
  29. def OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.roundLabels line 338
  30. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.soundness line 342
  31. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.completeness line 350
  32. theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 363
  33. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringLabels.PortWords line 406
  34. instance OAI.MaxCutGames.Foundations.PCP.PoweringLabels.finitePortWords line 408
  35. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.Ball line 412
  36. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.wordToBall line 415
  37. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 418
  38. instance OAI.MaxCutGames.Foundations.PCP.PoweringLabels.finiteBall line 425
  39. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.card_portWords line 429
  40. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.card_ball_le line 433
  41. structure OAI.MaxCutGames.Foundations.PCP.PoweringLabels.AddressSelector line 440
  42. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.classicalSelector line 444
  43. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.scanWitness line 450

    Source documentation

    Executable first-match search, with a proof that a match is present.

    def scanWitness {A : Type*} (p : A → Prop) [DecidablePred p] :
    (xs : List A) → (∃ a ∈ xs, p a) → {a // p a}
  | [], h => False.elim (by simp at h)
  | a :: xs, h =>
    if ha : p a then ⟨a, ha⟩ else
      scanWitness p xs (by
        obtain ⟨b, hb, hp⟩ := h
…
  44. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.listSelector line 463

    Source documentation

    A concrete complete address list supplies a computational selector. Its length depends on the degree and radius, not on the ambient vertex count.

    def listSelector [DecidableEq V] (G : PortGraph V D) (t : Nat) (v : V)
    (addresses : List (PortWords D t)) (complete : ∀ w, w ∈ addresses) :
    AddressSelector G t v where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringLabels.PortWords, OAI.MaxCutGames.Foundations.PCP.PoweringLabels.AddressSelector

  45. abbrev OAI.MaxCutGames.Foundations.PCP.PoweringLabels.PaddedLabel line 474
  46. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.encode line 476
  47. def OAI.MaxCutGames.Foundations.PCP.PoweringLabels.decode line 479
  48. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.decode_encode line 482
  49. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.decode_surjective line 489
  50. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.encode_injective line 493
  51. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 500
  52. theorem OAI.MaxCutGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 506
  53. def OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allWords line 529

    Source documentation

    All words of a specified length, ordered first by their head port.

    def allWords (d : Nat) : (n : Nat) → List (Fin n → Fin d)
  | 0 => [Fin.elim0]
  | n + 1 => (List.finRange d).flatMap fun a =>
      (allWords d n).map fun p => Fin.cases a p
  54. theorem OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.mem_allWords line 534
  55. def OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allAddresses line 551

    Source documentation

    The complete address list, including the unique empty word.

    def allAddresses (d t : Nat) : List (PortWords (Fin d) t) :=
…
  56. theorem OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.mem_allAddresses line 555
  57. theorem OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.length_allWords line 563
  58. theorem OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.length_allAddresses line 574

    Source documentation

    The selector's search-list bound depends only on degree and radius.

    theorem length_allAddresses (d t : Nat) :
    (allAddresses d t).length = ∑ n : Fin (t + 1), d ^ n.val := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allAddresses

  59. def OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.finitePortSelector line 581

    Source documentation

    A fully executable selector from the explicit bounded address list.

    def finitePortSelector {d : Nat} [DecidableEq V] (G : PortGraph V (Fin d))
    (t : Nat) (v : V) : AddressSelector G t v :=
…
  60. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressCount line 603

    Source documentation

    The number of words with length at most t, including the empty word.

    def addressCount (d t : Nat) : Nat := ∑ i : Fin (t + 1), d ^ i.val
  61. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 607

    Source documentation

    Reverse the digit positions before using the little-endian arithmetic encoding from mathlib. Both directions are the same executable operation.

    def reverseWordEquiv (d n : Nat) : (Fin n → Fin d) ≃ (Fin n → Fin d) where
…
  62. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.wordEquiv line 614

    Source documentation

    An executable bijection from fixed-length port words to their ranks.

    def wordEquiv (d n : Nat) : (Fin n → Fin d) ≃ Fin (d ^ n) :=
…
  63. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 617
  64. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressEquiv line 621

    Source documentation

    Arithmetic prefix sums give a rank for every bounded-length address.

    def addressEquiv (d t : Nat) : PortWords (Fin d) t ≃ Fin (addressCount d t) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressCount

  65. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 625
  66. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 635

    Source documentation

    A padded label is a base-q integer whose digits are indexed by the explicit bounded-address equivalence.

    def paddedLabelEquiv (d t q : Nat) :
    PaddedLabel (Fin d) t (Fin q) ≃ Fin (q ^ addressCount d t) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.addressCount

  67. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 640
  68. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv line 646

    Source documentation

    False and true are the adjacent orientation digits zero and one.

    def orientationEquiv : Bool ≃ Fin 2 := finTwoEquiv.symm
  69. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 648
  70. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 649
  71. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 652

    Source documentation

    A vertex's block consists of one adjacent orientation pair per word.

    def dartBlockEquiv (d n : Nat) :
    ((Fin (n + 1) → Fin d) × Bool) ≃ Fin (2 * d ^ (n + 1)) :=
…
  72. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 657
  73. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 664

    Source documentation

    The tuple permutation putting the vertex before its word and orientation.

    def dartVertexEquiv (vertices d n : Nat) :
    (Bool × (Fin vertices × (Fin (n + 1) → Fin d))) ≃
      (Fin vertices × ((Fin (n + 1) → Fin d) × Bool)) where
…
  74. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartEquiv line 673

    Source documentation

    Executable vertex-major dart numbering, with adjacent orientations.

    def dartEquiv (vertices d n : Nat) :
    (Bool × (Fin vertices × (Fin (n + 1) → Fin d))) ≃
      Fin (2 * vertices * d ^ (n + 1)) :=
…
  75. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 682
  76. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 692

    Source documentation

    The true orientation immediately follows the false orientation.

    theorem dartEquiv_true_eq_false_add_one (vertices d n : Nat) (v : Fin vertices)
    (p : Fin (n + 1) → Fin d) :
    (dartEquiv vertices d n (true, (v, p))).val =
      (dartEquiv vertices d n (false, (v, p))).val + 1 := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.dartEquiv

  77. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeWord line 699
  78. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeWord line 700
  79. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 702
  80. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 705
  81. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeAddress line 708
  82. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeAddress line 711
  83. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 714
  84. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 717
  85. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeLabel line 720
  86. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeLabel line 723
  87. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 727
  88. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 730
  89. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 733
  90. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeDart line 737
  91. def OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeDart line 741
  92. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 745
  93. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 750
  94. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.card_words line 755
  95. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.card_addresses line 758
  96. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.card_labels line 762
  97. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.card_darts line 766
  98. theorem OAI.MaxCutGames.Foundations.PCP.PoweringEnumeration.length_allAddresses line 771