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

48 declarations, 1 contain sorry, 0 declared as axioms

All abbreviations in this namespace expand to formulas of the pure language of equality and membership. Functions are sets of Kuratowski pairs inside the structure. In particular, no quantification over external Lean functions is used in PP, Choice, or ordinal-indexed Choice.

inductive OAI.PartitionConsistency.Formula Pure first-order membership syntax with equality line 11
Source documentation
Pure first-order membership syntax with equality. n variables are in scope. A quantifier binds the last variable in its body. There are no atoms/urelements, function symbols, constants, semantic predicates, or mathematical assumptions in this syntax.
L4DEL explanation
Pure first-order membership syntax with equality. n variables are in scope. A quantifier binds the last variable in its body. There are no atoms/urelements, function symbols, constants, semantic predicates, or mathematical assumptions in this syntax.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:30 (same declaration text).
```
inductive Formula : ℕ → Type where
…
```
abbrev OAI.PartitionConsistency.Formula.neg line 23
Also declared: OAI/SetTheory/PartitionConsistency/Logic/Proofs.lean:42 (same declaration text).
abbrev OAI.PartitionConsistency.Formula.iff line 24
Also declared: OAI/SetTheory/PartitionConsistency/Logic/Proofs.lean:43 (same declaration text).
def OAI.PartitionConsistency.Formula.liftRen Under a binder, a renaming leaves the newly bound variable bound line 27
Source documentation
Under a binder, a renaming leaves the newly bound variable bound.
L4DEL explanation
Under a binder, a renaming leaves the newly bound variable bound.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:46 (same declaration text).
```
def liftRen {n m} (r : Fin n → Fin m) : Fin (n + 1) → Fin (m + 1) :=
…
```
def OAI.PartitionConsistency.Formula.rename Capture-avoiding renaming; in this relational language all terms are variables line 31
Source documentation
Capture-avoiding renaming; in this relational language all terms are variables.
L4DEL explanation
Capture-avoiding renaming; in this relational language all terms are variables.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:50 (same declaration text).
```
def rename {n m} (r : Fin n → Fin m) : Formula n → Formula m
  | .bot => .bot
  | .mem x y => .mem (r x) (r y)
  | .equal x y => .equal (r x) (r y)
  | .imp p q => .imp (rename r p) (rename r q)
  | .conj p q => .conj (rename r p) (rename r q)
  | .disj p q => .disj (rename r p) (rename r q)
  | .all p => .all (rename (liftRen r) p)
  | .ex p => .ex (rename (liftRen r) p)
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.liftRen
abbrev OAI.PartitionConsistency.Formula.raise line 41
Also declared: OAI/SetTheory/PartitionConsistency/Logic/Proofs.lean:60 (same declaration text).
def OAI.PartitionConsistency.Formula.instantiate Substitution of a variable term for the variable just quantified line 44
Source documentation
Substitution of a variable term for the variable just quantified.
L4DEL explanation
Substitution of a variable term for the variable just quantified.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:63 (same declaration text).
```
def instantiate {n} (p : Formula (n + 1)) (x : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.Formula.close Universal closure of all the free variables line 48
Source documentation
Universal closure of all the free variables.
L4DEL explanation
Universal closure of all the free variables.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:67 (same declaration text).
```
def close : {n : ℕ} → Formula n → Formula 0
  | 0, p => p
  | _ + 1, p => close (.all p)

end Formula
```
Mentions: OAI.PartitionConsistency.Formula
abbrev OAI.PartitionConsistency.Sentence line 54
Also declared: OAI/SetTheory/PartitionConsistency/Logic/Proofs.lean:122 (same declaration text).
abbrev OAI.PartitionConsistency.Theory line 55
Also declared: OAI/SetTheory/PartitionConsistency/Logic/Proofs.lean:123 (same declaration text).
inductive OAI.PartitionConsistency.Derives Classical first-order natural deduction with equality line 61
Source documentation
Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The allI and exE rules use a fresh last variable, and shift all assumptions to avoid capture. We allow finitely many free variables in proofs of closed sentences.
L4DEL explanation
Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The allI and exE rules use a fresh last variable, and shift all assumptions to avoid capture. We allow finitely many free variables in proofs of closed sentences.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:129 (same declaration text).
```
inductive Derives : {n : ℕ} → Set (Formula n) → Formula n → Prop where
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.Theory.at Sentences are usable as open hypotheses with any finite supply of variables line 102
Source documentation
Sentences are usable as open hypotheses with any finite supply of variables.
L4DEL explanation
Sentences are usable as open hypotheses with any finite supply of variables.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:170 (same declaration text).
```
def Theory.at (T : Theory) (n : ℕ) : Set (Formula n) :=
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.Consistent Ordinary syntactic consistency: there is no finite natural-deduction proof of falsity from the theory, with any finite supply of free variables line 107
Source documentation
Ordinary syntactic consistency: there is no finite natural-deduction proof of falsity from the theory, with any finite supply of free variables.
L4DEL explanation
Ordinary syntactic consistency: there is no finite natural-deduction proof of falsity from the theory, with any finite supply of free variables.
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/SetTheory/PartitionConsistency/Logic/Proofs.lean:175 (same declaration text).
```
def Consistent (T : Theory) : Prop := ∀ n, ¬ Derives (T.at n) .bot
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Derives
def OAI.PartitionConsistency.SetLanguage.subset a ⊆ b line 118
Source documentation
a ⊆ b.
L4DEL explanation
a ⊆ b.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:16 (same declaration text).
```
def subset {n} (a b : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.empty a = ∅ line 122
Source documentation
a = ∅.
L4DEL explanation
a = ∅.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:20 (same declaration text).
```
def empty {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.nonempty a ≠ ∅, stated as existence of a member line 126
Source documentation
a ≠ ∅, stated as existence of a member.
L4DEL explanation
a ≠ ∅, stated as existence of a member.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:24 (same declaration text).
```
def nonempty {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.unorderedPair p = {x,y} line 130
Source documentation
p = {x,y}.
L4DEL explanation
p = {x,y}.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:28 (same declaration text).
```
def unorderedPair {n} (p x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.successor b = a ∪ {a} line 135
Source documentation
b = a ∪ {a}.
L4DEL explanation
b = a ∪ {a}.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:33 (same declaration text).
```
def successor {n} (b a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.orderedPair Kuratowski ordered pair: p = {{x},{x,y}} line 140
Source documentation
Kuratowski ordered pair: p = {{x},{x,y}}.
L4DEL explanation
Kuratowski ordered pair: p = {{x},{x,y}}.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:38 (same declaration text).
```
def orderedPair {n} (p x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.edge The internal graph relation ⟨x,y⟩ ∈ f line 146
Source documentation
The internal graph relation ⟨x,y⟩ ∈ f.
L4DEL explanation
The internal graph relation ⟨x,y⟩ ∈ f.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:44 (same declaration text).
```
def edge {n} (f x y : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.functionOn f is a set graph of a function whose domain is exactly d line 153
Source documentation
f is a set graph of a function whose domain is exactly d. The first conjunct excludes non-pairs and graph entries outside the domain; the second conjunct asserts totality and single-valuedness.
L4DEL explanation
f is a set graph of a function whose domain is exactly d. The first conjunct excludes non-pairs and graph entries outside the domain; the second conjunct asserts totality and single-valuedness.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:51 (same declaration text).
```
def functionOn {n} (f d : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.mapsTo Internal set function f : d → r line 161
Source documentation
Internal set function f : d → r.
L4DEL explanation
Internal set function f : d → r.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:59 (same declaration text).
```
def mapsTo {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.surjection Internal set surjection f : d ↠ r line 167
Source documentation
Internal set surjection f : d ↠ r.
L4DEL explanation
Internal set surjection f : d ↠ r.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:65 (same declaration text).
```
def surjection {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.injection Internal set injection f : d ↪ r line 173
Source documentation
Internal set injection f : d ↪ r.
L4DEL explanation
Internal set injection f : d ↪ r.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:71 (same declaration text).
```
def injection {n} (f d r : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.transitiveSet Transitivity of a set (not transitivity of the external structure) line 181
Source documentation
Transitivity of a set (not transitivity of the external structure).
L4DEL explanation
Transitivity of a set (not transitivity of the external structure).
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:79 (same declaration text).
```
def transitiveSet {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.membershipLinear Membership is an internal strict linear order on a line 186
Source documentation
Membership is an internal strict linear order on a.
L4DEL explanation
Membership is an internal strict linear order on a.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:84 (same declaration text).
```
def membershipLinear {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.membershipWellFounded Every nonempty internal subset of a has a membership-minimal element line 196
Source documentation
Every nonempty internal subset of a has a membership-minimal element. This does NOT assert external well-foundedness of the relation.
L4DEL explanation
Every nonempty internal subset of a has a membership-minimal element. This does NOT assert external well-foundedness of the relation.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:94 (same declaration text).
```
def membershipWellFounded {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.ordinal A von Neumann ordinal: a transitive set internally wellordered by membership line 202
Source documentation
A von Neumann ordinal: a transitive set internally wellordered by membership.
L4DEL explanation
A von Neumann ordinal: a transitive set internally wellordered by membership.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:100 (same declaration text).
```
def ordinal {n} (a : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.choiceOn A choice function on the set A of nonempty sets line 206
Source documentation
A choice function on the set A of nonempty sets.
L4DEL explanation
A choice function on the set A of nonempty sets.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:104 (same declaration text).
```
def choiceOn {n} (c A : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.nonemptyFamily A graph F coding a family of nonempty sets indexed by ordinal η line 212
Source documentation
A graph F coding a family of nonempty sets indexed by ordinal η.
L4DEL explanation
A graph F coding a family of nonempty sets indexed by ordinal η.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:110 (same declaration text).
```
def nonemptyFamily {n} (F η : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.choiceForFamily c(ξ) ∈ F(ξ) for every ξ ∈ η, with c an internal function line 218
Source documentation
c(ξ) ∈ F(ξ) for every ξ ∈ η, with c an internal function.
L4DEL explanation
c(ξ) ∈ F(ξ) for every ξ ∈ η, with c an internal function.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:116 (same declaration text).
```
def choiceForFamily {n} (c η F : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.PP The Partition Principle line 226
Source documentation
The Partition Principle. The reverse injection is not required to be a section of the original surjection. Both X and Y range over all sets.
L4DEL explanation
The Partition Principle. The reverse injection is not required to be a section of the original surjection. Both X and Y range over all sets.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:124 (same declaration text).
```
def PP : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.AC Ordinary Choice for every set of nonempty sets line 230
Source documentation
Ordinary Choice for every set of nonempty sets.
L4DEL explanation
Ordinary Choice for every set of nonempty sets.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:128 (same declaration text).
```
def AC : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.ACwo Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model line 235
Source documentation
Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model.
L4DEL explanation
Choice for every ordinal-indexed family of nonempty sets, including ordinals which may fail to be well founded from outside a model.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:133 (same declaration text).
```
def ACwo : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.extensionality line 241
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:139 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.emptySet line 244
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:142 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.pairing line 246
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:144 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.union line 248
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:146 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.powerSet line 251
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:149 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.infinity line 253
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:151 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.foundation line 257
Also declared: OAI/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:155 (same declaration text).
def OAI.PartitionConsistency.SetLanguage.separation The instance of Separation for an entirely arbitrary formula p(params,x) line 264
Source documentation
The instance of Separation for an entirely arbitrary formula p(params,x). All parameters are universally closed. Neither the quantifier complexity of p nor the number of parameters is bounded.
L4DEL explanation
The instance of Separation for an entirely arbitrary formula p(params,x). All parameters are universally closed. Neither the quantifier complexity of p nor the number of parameters is bounded.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:162 (same declaration text).
```
def separation {n} (p : Formula (n + 1)) : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.relation Substitution into a binary formula with n additional parameters line 273
Source documentation
Substitution into a binary formula with n additional parameters.
L4DEL explanation
Substitution into a binary formula with n additional parameters.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:171 (same declaration text).
```
def relation {n m} (p : Formula (n + 2)) (params : Fin n → Fin m) (x y : Fin m) :
    Formula m :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.replacement The instance of Replacement for an entirely arbitrary formula p(params,x,y): if it is single-valued and total on A, its image is a set line 280
Source documentation
The instance of Replacement for an entirely arbitrary formula p(params,x,y): if it is single-valued and total on A, its image is a set. As with Separation, the parameters are all universally closed.
L4DEL explanation
The instance of Replacement for an entirely arbitrary formula p(params,x,y): if it is single-valued and total on A, its image is a set. As with Separation, the parameters are all universally closed.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:178 (same declaration text).
```
def replacement {n} (p : Formula (n + 2)) : Sentence :=
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Sentence
inductive OAI.PartitionConsistency.SetLanguage.IsZFAxiom Exactly the axioms and all schema instances of pure first-order ZF line 297
Source documentation
Exactly the axioms and all schema instances of pure first-order ZF.
L4DEL explanation
Exactly the axioms and all schema instances of pure first-order ZF.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:195 (same declaration text).
```
inductive IsZFAxiom : Sentence → Prop where
…
```
Mentions: OAI.PartitionConsistency.Sentence
def OAI.PartitionConsistency.SetLanguage.ZF Zermelo–Fraenkel set theory, without Choice line 309
Source documentation
Zermelo–Fraenkel set theory, without Choice.
L4DEL explanation
Zermelo–Fraenkel set theory, without Choice.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:207 (same declaration text).
```
def ZF : Theory := {p | IsZFAxiom p}
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.SetLanguage.IsZFAxiom
def OAI.PartitionConsistency.SetLanguage.targetTheory ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice line 312
Source documentation
ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice.
L4DEL explanation
ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice.
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/SetTheory/PartitionConsistency/Logic/SetLanguage.lean:210 (same declaration text).
```
def targetTheory : Theory := ZF ∪ {PP, ACwo, AC.neg}
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SetLanguage.PP, OAI.PartitionConsistency.SetLanguage.ACwo
theorem OAI.PartitionConsistency.main_consistency Challenge statement: Relative consistency of the Partition Principle with ordinal Choice and failure of Choice sorry line 318
Source documentation
Relative consistency of ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice.
L4DEL explanation
Relative consistency of ZF with the Partition Principle, ordinal-indexed Choice and failure of Choice.
1. This explanation is a condensed rendering of this declaration's own doc comment at the pinned source commit.
2. The linked formalization note covers 2 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
3. The repository's comparator configuration selects OAI.SetTheory.PartitionConsistency.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/SetTheory/PartitionConsistency/Main.lean:181 (same statement text; different proof or body). Qualify references as OAI.PartitionConsistency.main_consistency@path.
```
theorem main_consistency :
    Consistent SetLanguage.ZF → Consistent SetLanguage.targetTheory := by
…
```
Mentions: OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.SetLanguage.ZF, OAI.PartitionConsistency.SetLanguage.targetTheory