OAI/Computability/DeterministicSum/Decision.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Exact polynomial-filter decision, false-triple charges and distinct-position role searches.

  1. structure OAI.DeterministicThreeSum.DeterministicDecision.Grouping line 12
  2. lemma OAI.DeterministicThreeSum.DeterministicDecision.Grouping.subset line 20
  3. lemma OAI.DeterministicThreeSum.DeterministicDecision.Grouping.size_le line 24
  4. def OAI.DeterministicThreeSum.DeterministicDecision.ExactPair line 27
  5. def OAI.DeterministicThreeSum.DeterministicDecision.ModularHit line 30
  6. def OAI.DeterministicThreeSum.DeterministicDecision.ExactCell line 33
  7. def OAI.DeterministicThreeSum.DeterministicDecision.RoleSolution line 37
  8. def OAI.DeterministicThreeSum.DeterministicDecision.hitCount line 40
  9. def OAI.DeterministicThreeSum.DeterministicDecision.groupSum line 45
  10. def OAI.DeterministicThreeSum.DeterministicDecision.allCells line 49
  11. def OAI.DeterministicThreeSum.DeterministicDecision.selectedCells line 52
  12. def OAI.DeterministicThreeSum.DeterministicDecision.CleanAgreement line 57
  13. lemma OAI.DeterministicThreeSum.DeterministicDecision.hitCount_le line 64
  14. lemma OAI.DeterministicThreeSum.DeterministicDecision.clean_sum line 69
  15. lemma OAI.DeterministicThreeSum.DeterministicDecision.cast_count_ne_zero line 79
  16. lemma OAI.DeterministicThreeSum.DeterministicDecision.hitCount_pos_iff line 91
  17. lemma OAI.DeterministicThreeSum.DeterministicDecision.clean_selected_iff line 96
  18. lemma OAI.DeterministicThreeSum.DeterministicDecision.exact_modular line 107
  19. lemma OAI.DeterministicThreeSum.DeterministicDecision.exact_cell_selected line 112
  20. theorem OAI.DeterministicThreeSum.DeterministicDecision.role_decision_iff line 123
  21. def OAI.DeterministicThreeSum.DeterministicDecision.falseTriples line 136
  22. def OAI.DeterministicThreeSum.DeterministicDecision.unsuccessfulClean line 142
  23. lemma OAI.DeterministicThreeSum.DeterministicDecision.unsuccessful_has_false line 148
  24. theorem OAI.DeterministicThreeSum.DeterministicDecision.unsuccessful_clean_card_le line 162
  25. lemma OAI.DeterministicThreeSum.DeterministicDecision.threeSUM_of_distinct line 182
  26. lemma OAI.DeterministicThreeSum.DeterministicDecision.role_solution_threeSUM line 197
  27. def OAI.DeterministicThreeSum.DeterministicDecision.residue line 212
  28. lemma OAI.DeterministicThreeSum.DeterministicDecision.residue_cast line 214
  29. lemma OAI.DeterministicThreeSum.DeterministicDecision.residue_lt line 219
  30. def OAI.DeterministicThreeSum.DeterministicDecision.shiftedTable line 223
  31. lemma OAI.DeterministicThreeSum.DeterministicDecision.shiftedTable_agreement line 229
  32. def OAI.DeterministicThreeSum.DeterministicDecision.baseDigits line 257
  33. lemma OAI.DeterministicThreeSum.DeterministicDecision.baseDigits_value line 261
  34. def OAI.DeterministicThreeSum.DeterministicDecision.residueDigits line 275
  35. lemma OAI.DeterministicThreeSum.DeterministicDecision.residueDigits_value line 278
  36. def OAI.DeterministicThreeSum.DeterministicDecision.splitOffset line 283
  37. def OAI.DeterministicThreeSum.DeterministicDecision.splitLocal line 286
  38. lemma OAI.DeterministicThreeSum.DeterministicDecision.splitOffset_multiple line 289
  39. lemma OAI.DeterministicThreeSum.DeterministicDecision.splitOffset_bound line 292
  40. lemma OAI.DeterministicThreeSum.DeterministicDecision.split_value line 302
  41. def OAI.DeterministicThreeSum.DeterministicDecision.polynomialEntries line 309
  42. def OAI.DeterministicThreeSum.DeterministicDecision.dirtyCells line 317
  43. theorem OAI.DeterministicThreeSum.DeterministicDecision.polynomial_clean_agreement line 326
  44. theorem OAI.DeterministicThreeSum.DeterministicDecision.polynomial_decision_iff line 350
  45. theorem OAI.DeterministicThreeSum.DeterministicDecision.residue_polynomial_decision_iff line 367
  46. def OAI.DeterministicThreeSum.DeterministicDecision.checkedPrefix line 388
  47. lemma OAI.DeterministicThreeSum.DeterministicDecision.checkedPrefix_sublist line 392
  48. lemma OAI.DeterministicThreeSum.DeterministicDecision.checkedPrefix_success_unique line 402
  49. lemma OAI.DeterministicThreeSum.DeterministicDecision.checkedPrefix_success_iff line 416
  50. theorem OAI.DeterministicThreeSum.DeterministicDecision.checked_cell_count line 432
  51. theorem OAI.DeterministicThreeSum.DeterministicDecision.pair_check_count line 468
  52. def OAI.DeterministicThreeSum.DeterministicDecision.Roles.bitLength line 492
  53. def OAI.DeterministicThreeSum.DeterministicDecision.Roles.positionBits line 494
  54. lemma OAI.DeterministicThreeSum.DeterministicDecision.Roles.positionBits_injective line 497
  55. abbrev OAI.DeterministicThreeSum.DeterministicDecision.Roles.Color line 512
  56. def OAI.DeterministicThreeSum.DeterministicDecision.Roles.sampledColor line 514
  57. lemma OAI.DeterministicThreeSum.DeterministicDecision.Roles.separating_coordinates line 517
  58. abbrev OAI.DeterministicThreeSum.DeterministicDecision.Roles.Search line 541
  59. def OAI.DeterministicThreeSum.DeterministicDecision.Roles.role line 543
  60. lemma OAI.DeterministicThreeSum.DeterministicDecision.Roles.role_disjoint line 546
  61. lemma OAI.DeterministicThreeSum.DeterministicDecision.Roles.search_card line 552
  62. lemma OAI.DeterministicThreeSum.DeterministicDecision.Roles.positions_covered line 558
  63. theorem OAI.DeterministicThreeSum.DeterministicDecision.Roles.threeSUM_iff_search line 572