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

99 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.Thorp.Position line 13

    Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:14 (same declaration text), OAI/Probability/ThorpShuffle/Model.lean:13 (same declaration text).

  2. abbrev OAI.Thorp.State line 14

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:14 (same declaration text).

  3. def OAI.Thorp.Coins line 16

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:16 (same declaration text).

  4. instance OAI.Thorp.coinsFintype line 20

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:20 (same declaration text).

  5. instance OAI.Thorp.coinsInhabited line 23

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:23 (same declaration text).

  6. def OAI.Thorp.pairSwitch line 26

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:26 (same declaration text).

  7. def OAI.Thorp.rotate line 36

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:36 (same declaration text).

  8. def OAI.Thorp.step line 39

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:39 (same declaration text).

  9. abbrev OAI.Thorp.History line 46

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:46 (same declaration text).

  10. def OAI.Thorp.run line 48

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:48 (same declaration text).

  11. def OAI.Thorp.fairMass line 51

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:51 (same declaration text).

  12. def OAI.Thorp.law line 55

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:55 (same declaration text).

  13. def OAI.Thorp.uniform line 57

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:57 (same declaration text).

  14. def OAI.Thorp.tv line 59

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:59 (same declaration text).

  15. def OAI.Thorp.distance line 62

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:62 (same declaration text).

  16. def OAI.Thorp.lawFrom line 64

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:64 (same declaration text).

  17. abbrev OAI.Thorp.LabelList line 67

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Objects.lean:12 (same declaration text).

  18. def OAI.Thorp.coordinateRun line 69

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Objects.lean:14 (same declaration text).

  19. def OAI.Thorp.images line 72

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Objects.lean:17 (same declaration text).

  20. def OAI.Thorp.listTV line 76

    Also declared: OAI/Probability/ThorpShuffle/FixedLists/Objects.lean:21 (same declaration text).

  21. def OAI.Thorp.mixingTime line 79

    Also declared: OAI/Probability/ThorpShuffle/Model.lean:67 (same declaration text).

  22. abbrev OAI.ThorpNine.Harmonic.Thorp.Card line 89

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

  23. def OAI.ThorpNine.Harmonic.Thorp.switchFun line 91

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

  24. theorem OAI.ThorpNine.Harmonic.Thorp.switchFun_involutive line 94

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

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

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

  26. def OAI.ThorpNine.Harmonic.Thorp.Coins line 120

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

  27. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 124) line 124
  28. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 127) line 127
  29. def OAI.ThorpNine.Harmonic.Thorp.rotate line 130

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

  30. def OAI.ThorpNine.Harmonic.Thorp.step line 136

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

  31. def OAI.ThorpNine.Harmonic.Thorp.run line 140

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

  32. def OAI.ThorpNine.Harmonic.Thorp.law line 144

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

  33. lemma OAI.ThorpNine.Harmonic.Thorp.card_positions line 148

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

  34. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Cell line 155

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

  35. def OAI.ThorpNine.Harmonic.Thorp.Specht.row line 157

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

  36. def OAI.ThorpNine.Harmonic.Thorp.Specht.col line 159

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

  37. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.row_lt_colLen line 161

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

  38. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowIndex line 164

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

  39. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Tabloid line 167

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

  40. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 170) line 170
  41. def OAI.ThorpNine.Harmonic.Thorp.Specht.baseTabloid line 172

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

  42. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct line 174

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

  43. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_apply line 189

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

  44. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_one line 192

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

  45. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_mul line 196

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

  46. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep line 201

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

  47. def OAI.ThorpNine.Harmonic.Thorp.Specht.delta line 213

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

  48. def OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup line 216

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

  49. def OAI.ThorpNine.Harmonic.Thorp.Specht.permSign line 222

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

  50. def OAI.ThorpNine.Harmonic.Thorp.Specht.alternator line 228

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

  51. def OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid line 235

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

  52. def OAI.ThorpNine.Harmonic.Thorp.Specht.space line 238

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

  53. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.orbit_mem_space line 241

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

  54. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.action_mem_space line 244

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

  55. def OAI.ThorpNine.Harmonic.Thorp.Specht.subrepresentation line 256

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

  56. def OAI.ThorpNine.Harmonic.Thorp.Specht.representation line 259

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

  57. abbrev OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.H line 270

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

  58. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertEquiv line 277

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

  59. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertSpace line 281

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

  60. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.continuousRepresentation line 293

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

  61. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator line 304

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

  62. def OAI.ThorpNine.Harmonic.Thorp.Specht.spaceHilbertEquiv line 312

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

  63. def OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation line 315

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

  64. def OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary line 321

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

  65. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_cell line 329

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

  66. def OAI.ThorpNine.Harmonic.Thorp.Specht.cellRowsEquiv line 332

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

  67. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_eq_sum_rowLen line 339

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

  68. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.sum_rowLens line 343

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

  69. def OAI.ThorpNine.Harmonic.Thorp.Specht.diagramPartition line 352

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

  70. def OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram line 357

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

  71. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_rowLens line 360

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

  72. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_card line 366

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

  73. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.partitionDiagram_diagramPartition line 371

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

  74. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Shapes line 380

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

  75. def OAI.ThorpNine.Harmonic.Thorp.Specht.shapePartitionEquiv line 382

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

  76. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 396) line 396
  77. def OAI.ThorpNine.Harmonic.Thorp.Specht.labels line 398

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

  78. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardLabels line 401

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

  79. def OAI.ThorpNine.Harmonic.Thorp.Specht.cardRepresentation line 404

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

  80. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.Q line 419

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

  81. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.absoluteTrace line 423

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

  82. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.regularTrace line 428

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

  83. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.sweepDistance line 432

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

  84. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.weightedMoment line 445

    Distinct definitions of this name: OAI/Probability/ThorpResults/UniformMoments.lean:13 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.LowPlanes.weightedMoment@path.

  85. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.signedEntropy line 452

    Also declared: OAI/Probability/ThorpResults/SignedBudget.lean:11 (same declaration text).

  86. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.budgetCoefficient line 456

    Also declared: OAI/Probability/ThorpResults/SignedBudget.lean:15 (same declaration text).

  87. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.remainderBudget line 459

    Also declared: OAI/Probability/ThorpResults/SignedBudget.lean:18 (same declaration text).

  88. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.logWeightedMoment line 464

    Distinct definitions of this name: OAI/Probability/ThorpResults/SignedBudget.lean:23 (same statement text; different proof or body). Qualify references as OAI.ThorpNine.Harmonic.Thorp.LowPlanes.logWeightedMoment@path.

  89. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2Squared line 469

    Also declared: OAI/Probability/ThorpResults/FullDensity.lean:14 (same declaration text).

  90. def OAI.ThorpNine.Harmonic.Thorp.LowPlanes.densityL2SquaredFrom line 473

    Also declared: OAI/Probability/ThorpResults/FullDensity.lean:18 (same declaration text).

  91. def OAI.ThorpResults.FrameMain line 488

    Also declared: OAI/Probability/ThorpResults/Statements.lean:17 (same declaration text).

  92. def OAI.ThorpResults.InformationMain line 492

    Also declared: OAI/Probability/ThorpResults/Statements.lean:21 (same declaration text).

  93. def OAI.ThorpResults.SpectrumMain line 507

    Also declared: OAI/Probability/ThorpResults/Statements.lean:36 (same declaration text).

  94. def OAI.ThorpResults.SignedMain line 512

    Also declared: OAI/Probability/ThorpResults/Statements.lean:41 (same declaration text).

  95. def OAI.ThorpResults.DegreeSavingMain line 520

    Also declared: OAI/Probability/ThorpResults/Statements.lean:49 (same declaration text).

  96. def OAI.ThorpResults.FullDensityMain line 528

    Also declared: OAI/Probability/ThorpResults/Statements.lean:57 (same declaration text).

  97. def OAI.ThorpResults.ForwardMixingMain line 532

    Also declared: OAI/Probability/ThorpResults/Statements.lean:61 (same declaration text).

  98. def OAI.ThorpResults.OptimalOrderMain line 536

    Also declared: OAI/Probability/ThorpResults/Statements.lean:65 (same declaration text).

  99. theorem OAI.ThorpResults.remaining_main Challenge statement: Frame, spectral, and density estimates for Thorp mixing sorry line 543

    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.ThorpResults.FullDevelopment as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/ThorpResults/Main.lean:8 (same statement text; different proof or body). Qualify references as OAI.ThorpResults.remaining_main@path.

    theorem remaining_main :
    FrameMain ∧ InformationMain ∧ SpectrumMain ∧ SignedMain ∧
      DegreeSavingMain ∧ FullDensityMain ∧ ForwardMixingMain ∧ OptimalOrderMain := by
…

    Mentions: OAI.ThorpResults.FrameMain, OAI.ThorpResults.InformationMain, OAI.ThorpResults.SpectrumMain, OAI.ThorpResults.SignedMain, OAI.ThorpResults.DegreeSavingMain, OAI.ThorpResults.FullDensityMain, OAI.ThorpResults.ForwardMixingMain, OAI.ThorpResults.OptimalOrderMain