`ComparatorChallenges/FKCRT.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

35 declarations, 1 contain sorry, 0 declared as axioms

Finite Fortuin–Kasteleyn maps and the Brownian continuum random tree.

All combinatorial maps below have a distinguished dart 0 and are quotiented by orientation-preserving dart relabellings fixing that dart. A rotation system with Euler characteristic 2 encodes precisely a connected oriented-sphere map. No simplicity restriction is imposed. Vertices and edges are rotation and edge-reversal orbits, respectively. Every edge subset is included in the law. The index n here represents source size n+1, so the limit is through ALL positive edge sizes, not a subsequence.

MetricMeasureData packages the actual distance, measurable space and measure, without using arbitrary representatives of measure-preserving isometry classes as a global typeclass. Valid objects are compact metric probability spaces. The GHP extended distance is the infimum over common isometric embeddings, represented by pseudometrics on the disjoint union; zero cross distances simply identify points in the common ambient space. Tests are bounded functions continuous for that distance on valid objects. Thus GHP convergence is written in its bounded-continuous-test (weak distributional convergence) definition.

A standard normalized Brownian excursion is represented in its standard three-dimensional Bessel-bridge realization: the norm of three independent standard Brownian bridges of duration 1. No rescaling of the excursion is used.

abbrev OAI.FKCRT.Dart line 36
Also declared: OAI/Probability/FKMaps/Model.lean:36 (same declaration text).
abbrev OAI.FKCRT.Orbit line 38
Also declared: OAI/Probability/FKMaps/Model.lean:38 (same declaration text).
def OAI.FKCRT.orbit line 41
Also declared: OAI/Probability/FKMaps/Model.lean:41 (same declaration text).
instance OAI.FKCRT.(instance at line 44) line 44
def OAI.FKCRT.spanningGraph Documented declaration: spanningGraph line 49
Source documentation
The spanning graph with precisely the edges in A, with loops omitted only from adjacency: they still exist as edge orbits, have FK weight, and contribute two darts to the degree measure. Omitting loops does not change distance or k.
L4DEL explanation
The spanning graph with precisely the edges in A, with loops omitted only from adjacency: they still exist as edge orbits, have FK weight, and contribute two darts to the degree measure. Omitting loops does not change distance or k.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:49 (same declaration text).
```
def spanningGraph {n : ℕ} (a s : Equiv.Perm (Dart n)) (A : Set (Orbit a)) :
    SimpleGraph (Orbit s) :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
def OAI.FKCRT.MapConditions Labelled connected orientable genus-zero rotation systems line 55
Source documentation
Labelled connected orientable genus-zero rotation systems.
L4DEL explanation
Labelled connected orientable genus-zero rotation systems.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:55 (same declaration text).
```
def MapConditions {n : ℕ} (P : Equiv.Perm (Dart n) × Equiv.Perm (Dart n)) : Prop :=
…
```
Mentions: OAI.FKCRT.Dart
abbrev OAI.FKCRT.LabelledMap line 60
Also declared: OAI/Probability/FKMaps/Model.lean:60 (same declaration text).
def OAI.FKCRT.MapIso Root-preserving isomorphism of oriented maps (both dart permutations intertwine) line 64
Source documentation
Root-preserving isomorphism of oriented maps (both dart permutations intertwine).
L4DEL explanation
Root-preserving isomorphism of oriented maps (both dart permutations intertwine).
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:64 (same declaration text).
```
def MapIso {n : ℕ} (M N : LabelledMap n) : Prop :=
…
```
Mentions: OAI.FKCRT.LabelledMap
abbrev OAI.FKCRT.RootedMap line 69
Also declared: OAI/Probability/FKMaps/Model.lean:69 (same declaration text).
instance OAI.FKCRT.(instance at line 71) line 71
def OAI.FKCRT.reversal line 73
Also declared: OAI/Probability/FKMaps/Model.lean:73 (same declaration text).
def OAI.FKCRT.rotation line 75
Also declared: OAI/Probability/FKMaps/Model.lean:75 (same declaration text).
abbrev OAI.FKCRT.Vertex line 77
Also declared: OAI/Probability/FKMaps/Model.lean:77 (same declaration text).
abbrev OAI.FKCRT.Edge line 78
Also declared: OAI/Probability/FKMaps/Model.lean:78 (same declaration text).
def OAI.FKCRT.graph line 80
Also declared: OAI/Probability/FKMaps/Model.lean:80 (same declaration text).
def OAI.FKCRT.clusterCount The source k_M(A), including isolated vertices line 84
Source documentation
The source k_M(A), including isolated vertices.
L4DEL explanation
The source k_M(A), including isolated vertices.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:84 (same declaration text).
```
def clusterCount {n : ℕ} (M : RootedMap n) (A : Finset (Edge M)) : ℕ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge
def OAI.FKCRT.fkWeight Exact decorated finite-map weight from eq:finite-law line 88
Source documentation
Exact decorated finite-map weight from eq:finite-law.
L4DEL explanation
Exact decorated finite-map weight from eq:finite-law.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:88 (same declaration text).
```
def fkWeight {n : ℕ} (q : ℝ) (M : RootedMap n) (A : Finset (Edge M)) : ℝ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge
def OAI.FKCRT.partition line 92
Also declared: OAI/Probability/FKMaps/Model.lean:92 (same declaration text).
structure OAI.FKCRT.MetricMeasureData Unbundled presentation of a measured metric space; validity is specified below line 96
Source documentation
Unbundled presentation of a measured metric space; validity is specified below.
L4DEL explanation
Unbundled presentation of a measured metric space; validity is specified below.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:96 (same declaration text).
```
structure MetricMeasureData where
…
```
def OAI.FKCRT.MetricMeasureData.Valid Exactly compact metric probability spaces, with their Borel sigma algebras line 103
Source documentation
Exactly compact metric probability spaces, with their Borel sigma algebras.
L4DEL explanation
Exactly compact metric probability spaces, with their Borel sigma algebras.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:103 (same declaration text).
```
def MetricMeasureData.Valid (X : MetricMeasureData) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.degreeMass Normalized degree measure is uniform dart mass pushed to vertices line 111
Source documentation
Normalized degree measure is uniform dart mass pushed to vertices.
L4DEL explanation
Normalized degree measure is uniform dart mass pushed to vertices.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:111 (same declaration text).
```
def degreeMass {n : ℕ} (M : RootedMap n) :
    @Measure (Vertex M) ⊤ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Vertex
def OAI.FKCRT.mapSpace Root and decoration are not included in the metric probability space line 118
Source documentation
Root and decoration are not included in the metric probability space.
L4DEL explanation
Root and decoration are not included in the metric probability space.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:118 (same declaration text).
```
def mapSpace {n : ℕ} (scale : ℝ) (M : RootedMap n) : MetricMeasureData where
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.Amalgamates An ambient pseudometric on the disjoint union giving isometric embeddings line 125
Source documentation
An ambient pseudometric on the disjoint union giving isometric embeddings.
L4DEL explanation
An ambient pseudometric on the disjoint union giving isometric embeddings.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:125 (same declaration text).
```
def Amalgamates (X Y : MetricMeasureData)
    (m : PseudoMetricSpace (X.Carrier ⊕ Y.Carrier)) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.ambientCost line 131
Also declared: OAI/Probability/FKMaps/Model.lean:131 (same declaration text).
def OAI.FKCRT.ghpEDist The common-isometric-embedding definition of the source GHP distance line 144
Source documentation
The common-isometric-embedding definition of the source GHP distance.
L4DEL explanation
The common-isometric-embedding definition of the source GHP distance.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:144 (same declaration text).
```
def ghpEDist (X Y : MetricMeasureData) : ℝ≥0∞ :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.IsGHPTest Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations line 150
Source documentation
Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations.
L4DEL explanation
Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:150 (same declaration text).
```
def IsGHPTest (F : MetricMeasureData → ℝ) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.excursionDist Source excursion pseudometric, with the closed interval minimum line 156
Source documentation
Source excursion pseudometric, with the closed interval minimum.
L4DEL explanation
Source excursion pseudometric, with the closed interval minimum.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:156 (same declaration text).
```
def excursionDist (e : unitInterval → ℝ) (s t : unitInterval) : ℝ :=
…
```
abbrev OAI.FKCRT.ExcursionTree line 159
Also declared: OAI/Probability/FKMaps/Model.lean:159 (same declaration text).
def OAI.FKCRT.treeProjection line 162
Also declared: OAI/Probability/FKMaps/Model.lean:162 (same declaration text).
def OAI.FKCRT.treeSpace The quotient by d_e=0, its induced metric, and pushforward of uniform time line 168
Source documentation
The quotient by d_e=0, its induced metric, and pushforward of uniform time. The equivalence closure is redundant for continuous e; the induced distance is independent of representatives, as required by the pseudometric proof.
L4DEL explanation
The quotient by d_e=0, its induced metric, and pushforward of uniform time. The equivalence closure is redundant for continuous e; the induced distance is independent of representatives, as required by the pseudometric proof.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:168 (same declaration text).
```
def treeSpace (e : unitInterval → ℝ) : MetricMeasureData :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.standardExcursion Standard normalized excursion, realized as the 3D Bessel bridge line 178
Source documentation
Standard normalized excursion, realized as the 3D Bessel bridge.
L4DEL explanation
Standard normalized excursion, realized as the 3D Bessel bridge.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:178 (same declaration text).
```
def standardExcursion {Ω : Type} (B : Fin 3 → ℝ≥0 → Ω → ℝ) (ω : Ω)
    (t : unitInterval) : ℝ :=
…
```
def OAI.FKCRT.finiteExpectation Exact expectation under the finite law, with n+1 edges line 184
Source documentation
Exact expectation under the finite law, with n+1 edges.
L4DEL explanation
Exact expectation under the finite law, with n+1 edges.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:184 (same declaration text).
```
def finiteExpectation (q scale : ℝ) (n : ℕ) (F : MetricMeasureData → ℝ) : ℝ :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.brownianExpectation line 188
Also declared: OAI/Probability/FKMaps/Model.lean:188 (same declaration text).
def OAI.FKCRT.MainStatement thm:main line 194
Source documentation
thm:main. The quantifiers over Brownian realizations express that the limit is the standard excursion-tree law, not a coupling-specific object.
L4DEL explanation
thm:main. The quantifiers over Brownian realizations express that the limit is the standard excursion-tree law, not a coupling-specific object.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Probability/FKMaps/Model.lean:194 (same declaration text).
```
def MainStatement : Prop :=
…
```
theorem OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt Challenge statement: The geometric phase diagram, diffusion, and spectra of random planar maps sorry line 208
Source documentation
Finite FK maps converge in GHP distribution to the standard Brownian CRT.
L4DEL explanation
For every fixed $q>4$, the formalization proves the Brownian continuum-random-tree limit for critical finite Fortuin–Kasteleyn planar maps. After rescaling graph distances in an $n$-edge map by a constant depending on $q$ times $n^{-1/2}$ and using normalized degree measure, the metric-measure space converges in distribution to the Brownian continuum random tree in the Gromov–Hausdorff–Prokhorov topology. The convergence holds through all positive integer sizes.
1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
2. The repository's comparator configuration selects OAI.Probability.FKMaps.Convergence as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Probability/FKMaps/Convergence.lean:68 (same statement text; different proof or body). Qualify references as OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt@path.
```
theorem finite_fk_maps_converge_to_brownian_crt : MainStatement := by
…
```
Mentions: OAI.FKCRT.MainStatement