`ComparatorChallenges/RecursivePotentials.lean`

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

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

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

160 declarations, 1 contain sorry, 0 declared as axioms

The final claim constructs the spaces and states all eleven original results. Analysis.RecursivePotentials.Challenge.main_iff_original verifies statement preservation.

def OAI.RecursivePotentials.leastPair line 18
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:18 (same declaration text).
structure OAI.RecursivePotentials.FiniteRootedTree line 20
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:20 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.children line 35
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:35 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.maxDepth line 38
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:38 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.fields line 40
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:40 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.Initial line 53
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:53 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.ancestors line 59
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:59 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.ancestorClosure line 64
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:64 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.restrict line 67
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:67 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.extend line 75
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:75 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.head line 79
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:79 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.projectHead line 81
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:81 (same declaration text).
structure OAI.RecursivePotentials.CofiniteSubspace line 85
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:85 (same declaration text).
def OAI.RecursivePotentials.averagedGain line 94
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:94 (same declaration text).
def OAI.RecursivePotentials.averagedInner line 96
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:96 (same declaration text).
def OAI.RecursivePotentials.averagedModulus line 99
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:99 (same declaration text).
def OAI.RecursivePotentials.sequenceTree line 105
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:105 (same declaration text).
abbrev OAI.RecursivePotentials.ComponentNode line 116
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:116 (same declaration text).
abbrev OAI.RecursivePotentials.JoinedNode line 118
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:118 (same declaration text).
def OAI.RecursivePotentials.joinedTree line 120
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:120 (same declaration text).
def OAI.RecursivePotentials.WeaklyNull line 147
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:147 (same declaration text).
structure OAI.RecursivePotentials.EquivalentNorm line 150
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:150 (same declaration text).
def OAI.RecursivePotentials.EquivalentNorm.inner line 163
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:163 (same declaration text).
def OAI.RecursivePotentials.EquivalentNorm.modulus line 166
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:166 (same declaration text).
def OAI.RecursivePotentials.EquivalentNorm.AUC line 169
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:169 (same declaration text).
def OAI.RecursivePotentials.IsReflexive line 175
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:179 (same declaration text).
abbrev OAI.RecursivePotentials.SquareSum.Space line 183
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:187 (same declaration text).
def OAI.RecursivePotentials.completionEquivOfDense line 189
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:197 (same declaration text).
def OAI.RecursivePotentials.componentTree line 212
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:222 (same declaration text).
def OAI.RecursivePotentials.logarithmicGamma line 224
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:236 (same statement text; different proof or body). Qualify references as OAI.RecursivePotentials.logarithmicGamma@path.
structure OAI.RecursivePotentials.ChildExponent line 235
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:249 (same declaration text).
def OAI.RecursivePotentials.ChildExponent.agg line 243
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:257 (same declaration text).
def OAI.RecursivePotentials.FiniteRootedTree.pfields line 253
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:267 (different declaration text). Qualify references as OAI.RecursivePotentials.FiniteRootedTree.pfields@path.
def OAI.RecursivePotentials.VariableExponent.heightExponent line 270
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:284 (same declaration text).
def OAI.RecursivePotentials.VariableExponent.cubicConstant line 272
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:286 (same declaration text).
def OAI.RecursivePotentials.VariableExponent.sixthConstant line 274
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:288 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.leastPair line 290
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:304 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree line 292
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:306 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Initial line 301
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:315 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.restrict line 307
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:321 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.extend line 309
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:323 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.head line 311
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:325 (same declaration text).
class OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Heads line 313
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:327 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.P line 319
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:333 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Q line 323
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:337 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.normSum line 327
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:341 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.projectHead line 329
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:343 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeVector line 335
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:349 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 341) line 341
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 343) line 343
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 345) line 345
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 347) line 347
class OAI.ComparatorModel.RecursivePotentials.TreeVector.Construction line 349
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:363 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 359) line 359
instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 362) line 362
def OAI.ComparatorModel.RecursivePotentials.TreeVector.coordinateLinear line 364
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:378 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeVector.coordinate line 369
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:383 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeVector.projectionLinear line 375
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:389 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeVector.projection line 390
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:404 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.TreeSpace line 401
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:415 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeSpace.coordinate line 410
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:424 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeSpace.P line 412
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:426 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeSpace.Q line 415
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:429 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeSpace.projection line 418
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:432 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.TreeSpace.tail line 421
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:435 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.averagedModulus line 430
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:444 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.sequenceTree line 434
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:448 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.ComponentNode line 436
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:450 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.JoinedNode line 438
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:452 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.joinedTree line 440
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:454 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.XSigma line 442
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:456 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.XJoined line 444
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:458 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector line 446
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:460 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 453) line 453
instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 456) line 456
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.toTree line 459
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:473 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 462) line 462
class OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.Construction line 464
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:478 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 472) line 472
instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 474) line 474
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.inclusion line 476
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:490 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.projectionLinear line 479
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:493 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.projection line 488
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:502 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace line 498
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:512 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.inclusion line 507
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:521 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.projection line 509
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:523 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.tail line 512
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:526 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.XZero line 517
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:531 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.coordinate line 525
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:539 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.coordinate@path.
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.P line 528
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:542 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.P@path.
def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.Q line 530
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:544 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.Q@path.
abbrev OAI.ComparatorModel.RecursivePotentials.WeaklyNull line 536
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:550 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm line 538
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:552 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm.modulus line 544
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:558 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm.AUC line 546
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:560 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.IsReflexive line 552
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:570 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.SquareSum.Space line 559
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:577 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.completionEquivOfDense line 565
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:587 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.componentTree line 567
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:591 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.logarithmicGamma line 569
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:595 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.logarithmicGamma@path.
def OAI.ComparatorModel.RecursivePotentials.XJoined_separated_familiesStatement line 575
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:603 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.XJoined_separated_familiesStatement@path.
abbrev OAI.ComparatorModel.RecursivePotentials.ChildExponent line 582
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:610 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.heightExponent line 586
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:614 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.cubicConstant line 588
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:616 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.sixthConstant line 590
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:618 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.VariableTree.P line 601
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:629 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.VariableTree.Q line 605
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:633 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.VariableTree.normSum line 609
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:637 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationVector line 613
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:641 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 620) line 620
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 622) line 622
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 624) line 624
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 626) line 626
class OAI.ComparatorModel.RecursivePotentials.AggregationVector.Construction line 628
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:656 (same declaration text).
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 636) line 636
instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 639) line 639
def OAI.ComparatorModel.RecursivePotentials.AggregationVector.coordinateLinear line 641
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:669 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationVector.coordinate line 646
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:674 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.AggregationSpace line 656
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:684 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.coordinate line 667
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:695 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.P line 670
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:698 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.Q line 673
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:701 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.AggregationVector.basisVector line 683
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:711 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.basisVector@path.
instance OAI.ComparatorModel.RecursivePotentials.ChildExponent.(instance at line 691) line 691
abbrev OAI.ComparatorModel.RecursivePotentials.AggregationVector.CoordinateLp line 703
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:733 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.CoordinateLp@path.
def OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLpLinear line 705
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:735 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLpLinear@path.
class OAI.ComparatorModel.RecursivePotentials.AggregationVector.LpConstruction line 708
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:738 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.LpConstruction@path.
def OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLp line 720
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:750 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLp@path.
def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.lpEquiv line 737
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:767 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationSpace.lpEquiv@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.exponent line 755
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:785 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Component line 760
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:790 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Xv line 762
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:792 (same declaration text).
abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Node line 764
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:794 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.componentEquiv line 766
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:796 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.componentCoordinate line 779
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:809 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.coordinate line 782
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:812 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.basis line 785
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:815 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.FiniteTotalSupport line 788
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:818 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.projection line 790
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:820 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.AdmissibleHeads line 792
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:822 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.cubic_stabilityStatement line 797
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:827 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.cubic_stabilityStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.sixth_stabilityStatement line 801
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:831 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.sixth_stabilityStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.weakTailConstant line 807
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:835 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.theta line 809
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:837 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.weak_tailStatement line 811
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:839 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.weak_tailStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.one_sided_modulus_zeroStatement line 822
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:850 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.Variable.no_equivalent_AUCStatement line 825
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:853 (same declaration text).
structure OAI.ComparatorModel.RecursivePotentials.RootSumCompletionStatement line 832
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:860 (same declaration text).
structure OAI.ComparatorModel.RecursivePotentials.ZeroRootCompletionStatement line 853
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:881 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.rec_completionStatement line 877
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:905 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.rec_mainStatement line 881
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:909 (same declaration text).
def OAI.ComparatorModel.RecursivePotentials.stop_all_radiiStatement line 890
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:918 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.stop_all_radiiStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.nu line 895
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:925 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.nu@path.
structure OAI.ComparatorModel.RecursivePotentials.Variable.SourceNormStatement line 899
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:929 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.SourceNormStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.spaceStatement line 907
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:937 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.spaceStatement@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.aggregateChildren line 918
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:948 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.aggregateChildren@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.lpPotentials line 922
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:952 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.lpPotentials@path.
def OAI.ComparatorModel.RecursivePotentials.Variable.lp_model_exactStatement line 927
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:957 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.lp_model_exactStatement@path.
def OAI.ComparatorModel.RecursivePotentials.MainClaim line 937
Also declared: OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean:973 (same declaration text).
theorem OAI.ComparatorModel.RecursivePotentials.main Challenge statement: Recursive-potential spaces and midpoint convexity sorry line 955
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 7 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
2. The repository's comparator configuration selects OAI.Analysis.RecursivePotentials.Challenge as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Analysis/RecursivePotentials/Challenge.lean:259 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.main@path.
```
theorem main : MainClaim := by
…
```
Mentions: OAI.ComparatorModel.RecursivePotentials.MainClaim