OAI/Combinatorics/ParityLifts/Detection.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.sum_eq_of_color_histograms line 13
  2. lemma OAI.ParityWL.atomic_eq_adj line 27
  3. lemma OAI.ParityWL.joint_eq_old line 33
  4. lemma OAI.ParityWL.separate_eq_old line 37
  5. def OAI.ParityWL.tripleCount line 41
  6. lemma OAI.ParityWL.tripleCount_sum line 44
  7. lemma OAI.ParityWL.coordinate_outside line 48
  8. lemma OAI.ParityWL.coordinate_other line 62
  9. lemma OAI.ParityWL.tripleCount_eq_separate_one line 69
  10. lemma OAI.ParityWL.tripleCount_eq_joint_one line 84
  11. def OAI.ParityWL.MainClique line 100
  12. def OAI.ParityWL.templateExtensions line 103
  13. def OAI.ParityWL.templateHomsEquiv line 107
  14. lemma OAI.ParityWL.homCount_card_equiv line 139
  15. lemma OAI.ParityWL.homCount_template line 144
  16. lemma OAI.ParityWL.templateExtensions_eq_separate_one line 151
  17. lemma OAI.ParityWL.homCount_template_eq_separate_one line 166
  18. def OAI.ParityWL.extendTuple line 173
  19. def OAI.ParityWL.faceIndex line 176
  20. lemma OAI.ParityWL.extend_face line 179
  21. lemma OAI.ParityWL.face_avoiding line 189
  22. lemma OAI.ParityWL.extend_adj_eq line 198
  23. lemma OAI.ParityWL.extend_triple_eq line 209
  24. lemma OAI.ParityWL.extensions_eq_joint_vector line 220
  25. def OAI.ParityWL.jointTemplateValue line 236
  26. lemma OAI.ParityWL.jointTemplateValue_eq line 239
  27. def OAI.ParityWL.extendTupleEquiv line 245
  28. lemma OAI.ParityWL.homCount_template_joint line 253
  29. lemma OAI.ParityWL.homCount_template_eq_joint_two line 263
  30. lemma OAI.ParityWL.tripleCount_inl line 270
  31. lemma OAI.ParityWL.tripleCount_inr line 275
  32. lemma OAI.ParityWL.templateExtensions_inl line 280
  33. lemma OAI.ParityWL.templateExtensions_inr line 288
  34. lemma OAI.ParityWL.homCount_template_eq_pure_separate_one line 296
  35. lemma OAI.ParityWL.extendTuple_map line 306
  36. lemma OAI.ParityWL.jointTemplateValue_inl line 311
  37. lemma OAI.ParityWL.jointTemplateValue_inr line 324
  38. lemma OAI.ParityWL.homCount_template_eq_pure_joint_two line 337
  39. theorem OAI.ParityWL.successful_detected line 350

    Source documentation

    The "compatible choice" direction, including the claimed short round and both implementations. This uses the actual uncolored graphs.

    theorem successful_detected (k : ℕ) (hk : 4 ≤ k) (c : Convention)
    (C : ChoiceSystem (bagParameter c k)) (hs : C.Successful) :
    ¬ sameHistogram (zeroLift C) (starLift C) c k (detectionRound c) ∧
    ¬ samePureHistogram (zeroLift C) (starLift C) c k (detectionRound c) := by
…

    Mentions: OAI.ParityWL.Convention, OAI.ParityWL.ChoiceSystem, OAI.ParityWL.bagParameter, OAI.ParityWL.sameHistogram, OAI.ParityWL.zeroLift, OAI.ParityWL.starLift, OAI.ParityWL.detectionRound, OAI.ParityWL.samePureHistogram

  40. theorem OAI.ParityWL.equivalent_no_choice line 368
  41. theorem OAI.ParityWL.pure_equivalent_no_choice line 374