ComparatorChallenges/CoordinateTrace.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

64 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThorpNine.Harmonic.Thorp.Card line 11

    Also declared: ComparatorChallenges/ThorpRemaining.lean:89 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1180 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:11 (same declaration text).

  2. def OAI.ThorpNine.Harmonic.Thorp.switchFun line 13

    Also declared: ComparatorChallenges/ThorpRemaining.lean:91 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1182 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:13 (same declaration text).

  3. theorem OAI.ThorpNine.Harmonic.Thorp.switchFun_involutive line 16

    Also declared: ComparatorChallenges/ThorpRemaining.lean:94 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1185 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:16 (same declaration text).

  4. def OAI.ThorpNine.Harmonic.Thorp.pairSwitch line 25

    Also declared: ComparatorChallenges/ThorpRemaining.lean:103 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1194 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:25 (same declaration text).

  5. def OAI.ThorpNine.Harmonic.Thorp.Coins line 31

    Also declared: ComparatorChallenges/ThorpRemaining.lean:120 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:13 (same declaration text).

  6. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 35) line 35
  7. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 38) line 38
  8. def OAI.ThorpNine.Harmonic.Thorp.rotate line 41

    Also declared: ComparatorChallenges/ThorpRemaining.lean:130 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:23 (same declaration text).

  9. def OAI.ThorpNine.Harmonic.Thorp.step line 47

    Also declared: ComparatorChallenges/ThorpRemaining.lean:136 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:29 (same declaration text).

  10. def OAI.ThorpNine.Harmonic.Thorp.run line 51

    Also declared: ComparatorChallenges/ThorpRemaining.lean:140 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:33 (same declaration text).

  11. def OAI.ThorpNine.Harmonic.Thorp.law line 55

    Also declared: ComparatorChallenges/ThorpRemaining.lean:144 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:37 (same declaration text).

  12. lemma OAI.ThorpNine.Harmonic.Thorp.card_positions line 59

    Also declared: ComparatorChallenges/ThorpRemaining.lean:148 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Coins.lean:130 (same declaration text).

  13. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Cell line 67

    Also declared: ComparatorChallenges/ThorpRemaining.lean:155 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1264 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:95 (same declaration text).

  14. def OAI.ThorpNine.Harmonic.Thorp.Specht.row line 69

    Also declared: ComparatorChallenges/ThorpRemaining.lean:157 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1266 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:97 (same declaration text).

  15. def OAI.ThorpNine.Harmonic.Thorp.Specht.col line 71

    Also declared: ComparatorChallenges/ThorpRemaining.lean:159 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1268 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:99 (same declaration text).

  16. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.row_lt_colLen line 73

    Also declared: ComparatorChallenges/ThorpRemaining.lean:161 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1270 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:101 (same declaration text).

  17. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowIndex line 76

    Also declared: ComparatorChallenges/ThorpRemaining.lean:164 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1273 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:104 (same declaration text).

  18. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Tabloid line 79

    Also declared: ComparatorChallenges/ThorpRemaining.lean:167 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1276 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:107 (same declaration text).

  19. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 82) line 82
  20. def OAI.ThorpNine.Harmonic.Thorp.Specht.baseTabloid line 84

    Also declared: ComparatorChallenges/ThorpRemaining.lean:172 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1281 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:112 (same declaration text).

  21. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct line 86

    Also declared: ComparatorChallenges/ThorpRemaining.lean:174 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1283 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:114 (same declaration text).

  22. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_apply line 101

    Also declared: ComparatorChallenges/ThorpRemaining.lean:189 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1298 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:129 (same declaration text).

  23. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_one line 104

    Also declared: ComparatorChallenges/ThorpRemaining.lean:192 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1301 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:132 (same declaration text).

  24. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_mul line 108

    Also declared: ComparatorChallenges/ThorpRemaining.lean:196 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1305 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:136 (same declaration text).

  25. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep line 113

    Also declared: ComparatorChallenges/ThorpRemaining.lean:201 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1310 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:141 (same declaration text).

  26. def OAI.ThorpNine.Harmonic.Thorp.Specht.delta line 125

    Also declared: ComparatorChallenges/ThorpRemaining.lean:213 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1322 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:153 (same declaration text).

  27. def OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup line 128

    Also declared: ComparatorChallenges/ThorpRemaining.lean:216 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1325 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:156 (same declaration text).

  28. def OAI.ThorpNine.Harmonic.Thorp.Specht.permSign line 134

    Also declared: ComparatorChallenges/ThorpRemaining.lean:222 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1331 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:162 (same declaration text).

  29. def OAI.ThorpNine.Harmonic.Thorp.Specht.alternator line 143

    Also declared: ComparatorChallenges/ThorpRemaining.lean:228 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1338 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:169 (same declaration text).

  30. def OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid line 153

    Also declared: ComparatorChallenges/ThorpRemaining.lean:235 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1345 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:176 (same declaration text).

  31. def OAI.ThorpNine.Harmonic.Thorp.Specht.space line 156

    Also declared: ComparatorChallenges/ThorpRemaining.lean:238 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1348 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:179 (same declaration text).

  32. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.orbit_mem_space line 159

    Also declared: ComparatorChallenges/ThorpRemaining.lean:241 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1351 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:182 (same declaration text).

  33. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.action_mem_space line 162

    Also declared: ComparatorChallenges/ThorpRemaining.lean:244 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1354 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:185 (same declaration text).

  34. def OAI.ThorpNine.Harmonic.Thorp.Specht.subrepresentation line 174

    Also declared: ComparatorChallenges/ThorpRemaining.lean:256 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1366 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:197 (same declaration text).

  35. def OAI.ThorpNine.Harmonic.Thorp.Specht.representation line 177

    Also declared: ComparatorChallenges/ThorpRemaining.lean:259 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1369 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:200 (same declaration text).

  36. abbrev OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.H line 188

    Also declared: ComparatorChallenges/ThorpRemaining.lean:270 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1380 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:211 (same declaration text).

  37. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertEquiv line 195

    Also declared: ComparatorChallenges/ThorpRemaining.lean:277 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1387 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:218 (same declaration text).

  38. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertSpace line 199

    Also declared: ComparatorChallenges/ThorpRemaining.lean:281 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1391 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:222 (same declaration text).

  39. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.continuousRepresentation line 209

    Also declared: ComparatorChallenges/ThorpRemaining.lean:293 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1403 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:234 (same declaration text).

  40. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator line 222

    Also declared: ComparatorChallenges/ThorpRemaining.lean:304 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1414 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:245 (same declaration text).

  41. def OAI.ThorpNine.Harmonic.Thorp.Specht.spaceHilbertEquiv line 230

    Also declared: ComparatorChallenges/ThorpRemaining.lean:312 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1422 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:253 (same declaration text).

  42. def OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation line 233

    Distinct definitions of this name: ComparatorChallenges/ThorpRemaining.lean:315 (same statement text; different proof or body), ComparatorChallenges/ThorpRouting.lean:1425 (same statement text; different proof or body), OAI/Probability/ThorpRouting/Harmonic/Model.lean:256 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation@path.

  43. def OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary line 243

    Also declared: ComparatorChallenges/ThorpRemaining.lean:321 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1431 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Model.lean:262 (same declaration text).

  44. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_cell line 252

    Also declared: ComparatorChallenges/ThorpRemaining.lean:329 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:73 (same declaration text).

  45. def OAI.ThorpNine.Harmonic.Thorp.Specht.cellRowsEquiv line 255

    Also declared: ComparatorChallenges/ThorpRemaining.lean:332 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:729 (same declaration text).

  46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_eq_sum_rowLen line 262

    Also declared: ComparatorChallenges/ThorpRemaining.lean:339 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:736 (same declaration text).

  47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.sum_rowLens line 266

    Also declared: ComparatorChallenges/ThorpRemaining.lean:343 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:740 (same declaration text).

  48. def OAI.ThorpNine.Harmonic.Thorp.Specht.diagramPartition line 275

    Also declared: ComparatorChallenges/ThorpRemaining.lean:352 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:749 (same declaration text).

  49. def OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram line 280

    Also declared: ComparatorChallenges/ThorpRemaining.lean:357 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/ModifiedReverseCoins.lean:754 (same declaration text).

  50. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_rowLens line 283

    Also declared: ComparatorChallenges/ThorpRemaining.lean:360 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:11 (same declaration text).

  51. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_card line 289

    Also declared: ComparatorChallenges/ThorpRemaining.lean:366 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:17 (same declaration text).

  52. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_diagramPartition line 294

    Also declared: ComparatorChallenges/ThorpRemaining.lean:371 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:22 (same declaration text).

  53. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Shapes line 303

    Also declared: ComparatorChallenges/ThorpRemaining.lean:380 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:31 (same declaration text).

  54. def OAI.ThorpNine.Harmonic.Thorp.Specht.shapePartitionEquiv line 305

    Also declared: ComparatorChallenges/ThorpRemaining.lean:382 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:33 (same declaration text).

  55. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 319) line 319
  56. def OAI.ThorpNine.Harmonic.Thorp.Specht.labels line 321

    Also declared: ComparatorChallenges/ThorpRemaining.lean:398 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Shapes.lean:66 (same declaration text).

  57. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardLabels line 324

    Also declared: ComparatorChallenges/ThorpRemaining.lean:401 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Main.lean:487 (same declaration text).

  58. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation line 327

    Also declared: ComparatorChallenges/ThorpRemaining.lean:404 (same declaration text), OAI/Probability/ThorpRouting/Harmonic/Main.lean:490 (same declaration text).

  59. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.Q line 343

    Also declared: ComparatorChallenges/ThorpRemaining.lean:419 (same declaration text), OAI/Probability/ThorpRouting/TraceModel.lean:15 (same declaration text).

  60. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.absoluteTrace line 347

    Also declared: ComparatorChallenges/ThorpRemaining.lean:423 (same declaration text), OAI/Probability/ThorpRouting/TraceModel.lean:19 (same declaration text).

  61. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.regularTrace line 352

    Also declared: ComparatorChallenges/ThorpRemaining.lean:428 (same declaration text), OAI/Probability/ThorpRouting/TraceModel.lean:24 (same declaration text).

  62. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.sweepDistance line 356

    Also declared: ComparatorChallenges/ThorpRemaining.lean:432 (same declaration text), OAI/Probability/ThorpRouting/TraceModel.lean:28 (same declaration text).

  63. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.MainStatement line 360

    Also declared: OAI/Probability/ThorpRouting/TraceModel.lean:32 (same declaration text).

  64. theorem OAI.ThorpNine.Harmonic.Thorp.LowPlanes.regular_trace_smoothing Challenge statement: Regular trace smoothing and full-permutation mixing sorry line 366

    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 13 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Probability.ThorpRouting.RegularTrace as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/ThorpRouting/RegularTrace.lean:69 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.LowPlanes.regular_trace_smoothing@path.

    theorem regular_trace_smoothing : MainStatement := by
…

    Mentions: OAI.ThorpNine.Harmonic.Thorp.LowPlanes.MainStatement