ComparatorChallenges/ChoicelessPolynomialTime.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

78 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.CPTSeparation.Scalar line 11

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:11 (same declaration text).

  2. inductive OAI.CPTSeparation.Symbol line 13

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:13 (same declaration text).

  3. structure OAI.CPTSeparation.Input line 17

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:17 (same declaration text).

  4. abbrev OAI.CPTSeparation.Input.Edge line 24

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:24 (same declaration text).

  5. abbrev OAI.CPTSeparation.Input.Config line 26

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:26 (same declaration text).

  6. instance OAI.CPTSeparation.Input.(instance at line 28) line 28
  7. instance OAI.CPTSeparation.Input.(instance at line 30) line 30
  8. def OAI.CPTSeparation.Input.coefficient line 32

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:32 (same declaration text).

  9. def OAI.CPTSeparation.Input.incident line 37

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:37 (same declaration text).

  10. def OAI.CPTSeparation.Input.normalized line 41

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:41 (same declaration text).

  11. def OAI.CPTSeparation.Input.consistent line 44

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:44 (same declaration text).

  12. def OAI.CPTSeparation.Input.query line 48

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:48 (same declaration text).

  13. structure OAI.CPTSeparation.Input.Iso line 51

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:51 (same declaration text).

  14. abbrev OAI.CPTSeparation.Hereditary.HF line 60

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:62 (same declaration text).

  15. def OAI.CPTSeparation.Hereditary.mk line 66

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:68 (same declaration text).

  16. def OAI.CPTSeparation.Hereditary.atom line 68

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:70 (same declaration text).

  17. def OAI.CPTSeparation.Hereditary.isSet line 70

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:75 (same declaration text).

  18. def OAI.CPTSeparation.Hereditary.rawElements line 73

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:78 (same declaration text).

  19. def OAI.CPTSeparation.Hereditary.elements line 77

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:112 (same declaration text).

  20. instance OAI.CPTSeparation.Hereditary.(instance at line 105) line 105
  21. def OAI.CPTSeparation.Hereditary.ofFinset line 107

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:144 (same declaration text).

  22. def OAI.CPTSeparation.Hereditary.rawRank' line 110

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:147 (same declaration text).

  23. def OAI.CPTSeparation.Hereditary.rawRank line 115

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:152 (same declaration text).

  24. def OAI.CPTSeparation.Hereditary.rank line 117

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:176 (same declaration text).

  25. def OAI.CPTSeparation.Hereditary.double line 146

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:218 (same declaration text).

  26. def OAI.CPTSeparation.Hereditary.ordinal line 148

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:220 (same declaration text).

  27. abbrev OAI.CPTSeparation.Operational.empty line 162

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:234 (same declaration text).

  28. abbrev OAI.CPTSeparation.Operational.truth line 164

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:236 (same declaration text).

  29. def OAI.CPTSeparation.Operational.boolean line 166

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:238 (same declaration text).

  30. def OAI.CPTSeparation.Operational.inputRelation line 168

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:240 (same declaration text).

  31. def OAI.CPTSeparation.Operational.allAtoms line 171

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:243 (same declaration text).

  32. def OAI.CPTSeparation.Operational.unionHF line 173

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:245 (same declaration text).

  33. def OAI.CPTSeparation.Operational.uniqueHF line 175

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:247 (same declaration text).

  34. def OAI.CPTSeparation.Operational.cardinalityHF line 178

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:250 (same declaration text).

  35. abbrev OAI.CPTSeparation.Operational.Location line 180

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:252 (same declaration text).

  36. structure OAI.CPTSeparation.Operational.State line 182

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:254 (same declaration text).

  37. def OAI.CPTSeparation.Operational.State.initial line 188

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:260 (same declaration text).

  38. def OAI.CPTSeparation.Operational.State.support line 190

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:262 (same declaration text).

  39. abbrev OAI.CPTSeparation.Operational.Update line 194

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:266 (same declaration text).

  40. def OAI.CPTSeparation.Operational.State.Consistent line 196

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:270 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.Consistent@path.

  41. def OAI.CPTSeparation.Operational.State.updatedValue line 199

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:273 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.updatedValue@path.

  42. def OAI.CPTSeparation.Operational.State.applyUpdates line 203

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:277 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.applyUpdates@path.

  43. inductive OAI.CPTSeparation.Operational.Control line 213

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:289 (same declaration text).

  44. def OAI.CPTSeparation.Hereditary.closure line 225

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:301 (different declaration text). Qualify references as OAI.CPTSeparation.Hereditary.closure@path.

  45. def OAI.CPTSeparation.Hereditary.familyClosure line 276

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:352 (different declaration text). Qualify references as OAI.CPTSeparation.Hereditary.familyClosure@path.

  46. def OAI.CPTSeparation.Operational.State.critical line 288

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:366 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.critical@path.

  47. def OAI.CPTSeparation.Operational.State.active line 291

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:369 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.active@path.

  48. inductive OAI.CPTSeparation.FullCPT.Term line 306

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:386 (same declaration text).

  49. def OAI.CPTSeparation.FullCPT.Term.eval line 331

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:411 (same declaration text).

  50. inductive OAI.CPTSeparation.FullCPT.Rule line 356

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:436 (same declaration text).

  51. def OAI.CPTSeparation.FullCPT.Rule.updates line 366

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:446 (same declaration text).

  52. structure OAI.CPTSeparation.FullCPT.Program line 378

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:458 (same declaration text).

  53. abbrev OAI.CPTSeparation.FullCPT.Program.functionArity line 388

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:468 (same declaration text).

  54. abbrev OAI.CPTSeparation.FullCPT.Program.Store line 390

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:470 (same declaration text).

  55. def OAI.CPTSeparation.FullCPT.Program.flag line 392

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:472 (same declaration text).

  56. def OAI.CPTSeparation.FullCPT.Program.step line 394

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:474 (same declaration text).

  57. def OAI.CPTSeparation.FullCPT.Program.run line 399

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:479 (same declaration text).

  58. def OAI.CPTSeparation.FullCPT.Program.active line 403

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:483 (same declaration text).

  59. def OAI.CPTSeparation.FullCPT.Term.roots line 422

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:502 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Term.roots@path.

  60. def OAI.CPTSeparation.FullCPT.Rule.roots line 440

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:526 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Rule.roots@path.

  61. def OAI.CPTSeparation.FullCPT.Program.stepRoots line 459

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:545 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.stepRoots@path.

  62. def OAI.CPTSeparation.FullCPT.Program.occurring line 462

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:548 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.occurring@path.

  63. def OAI.CPTSeparation.FullCPT.Program.evaluationAccepts line 467

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Model.lean:553 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.evaluationAccepts@path.

  64. def OAI.CPTSeparation.FullCPT.EvaluationDefinable line 473

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:559 (same declaration text).

  65. abbrev OAI.CPTSeparation.OrderedQuery.Data line 487

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:573 (same declaration text).

  66. def OAI.CPTSeparation.OrderedQuery.indexSymbol line 491

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:577 (same declaration text).

  67. def OAI.CPTSeparation.OrderedQuery.cellValue line 500

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:586 (same declaration text).

  68. def OAI.CPTSeparation.OrderedQuery.tableBits line 505

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:591 (same declaration text).

  69. abbrev OAI.CPTSeparation.OrderedQuery.OrderedInput line 507

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:593 (same declaration text).

  70. abbrev OAI.CPTSeparation.GaussMachine.Letter line 513

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:599 (same declaration text).

  71. def OAI.CPTSeparation.GaussMachine.boolCode line 515

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:601 (same declaration text).

  72. abbrev OAI.CPTSeparation.CounterLang.Letter line 521

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:607 (same declaration text).

  73. def OAI.CPTSeparation.TableMachine.bitLetter line 529

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:615 (same declaration text).

  74. def OAI.CPTSeparation.TableMachine.tableInput line 531

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:617 (same declaration text).

  75. def OAI.CPTSeparation.TableMachine.code line 534

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:620 (same declaration text).

  76. def OAI.CPTSeparation.Input.ordered line 539

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:627 (same declaration text).

  77. def OAI.CPTSeparation.OrdinaryPolynomialTime line 542

    Also declared: OAI/ModelTheory/Choiceless/Model.lean:630 (same declaration text).

  78. theorem OAI.CPTSeparation.main Challenge statement: Polynomial-time query outside choiceless polynomial time sorry line 549

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 2 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.ModelTheory.Choiceless.Separation as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/ModelTheory/Choiceless/Separation.lean:7 (same statement text; different proof or body). Qualify references as OAI.CPTSeparation.main@path.

    theorem main :
    (∀ (A B : Type) [Fintype A] [Fintype B] (S : Input A) (T : Input B),
      S.Iso T → (S.query ↔ T.query)) ∧
    OrdinaryPolynomialTime ∧
    ¬ FullCPT.EvaluationDefinable (fun {_} [_] I => I.query) := by
…

    Mentions: OAI.CPTSeparation.Input, OAI.CPTSeparation.OrdinaryPolynomialTime, OAI.CPTSeparation.FullCPT.EvaluationDefinable