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

16 declarations, 1 contain sorry, 0 declared as axioms

def OAI.DirectedFeedback.natBits Unary self-delimiting natural numbers line 8
Source documentation
Unary self-delimiting natural numbers. Outputs are explicit, not succinct.
L4DEL explanation
Unary self-delimiting natural numbers. Outputs are explicit, not succinct.
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/Computability/DirectedFeedback/Model.lean:8 (same declaration text).
```
def natBits (n : ℕ) : List Bool := List.replicate n true ++ [false]
```
def OAI.DirectedFeedback.pairBits The explicit framing used for an input and its NP certificate line 11
Source documentation
The explicit framing used for an input and its NP certificate.
L4DEL explanation
The explicit framing used for an input and its NP certificate.
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/Computability/DirectedFeedback/Model.lean:11 (same declaration text).
```
def pairBits (p : List Bool × List Bool) : List Bool :=
…
```
def OAI.DirectedFeedback.FiniteAlphabet Finitely many stacks and control states are already part of FinTM2 line 16
Source documentation
Finitely many stacks and control states are already part of FinTM2. This additionally excludes infinite stack alphabets.
L4DEL explanation
Finitely many stacks and control states are already part of FinTM2. This additionally excludes infinite stack alphabets.
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/Computability/DirectedFeedback/Model.lean:16 (same declaration text).
```
def FiniteAlphabet (M : Turing.FinTM2) : Prop := ∀ k, Finite (M.Γ k)
```
structure OAI.DirectedFeedback.NPVerifier Polynomially bounded certificates checked by an actual deterministic finite-alphabet machine, on the explicitly encoded input/certificate pair line 20
Source documentation
Polynomially bounded certificates checked by an actual deterministic finite-alphabet machine, on the explicitly encoded input/certificate pair.
L4DEL explanation
Polynomially bounded certificates checked by an actual deterministic finite-alphabet machine, on the explicitly encoded input/certificate pair.
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/Computability/DirectedFeedback/Model.lean:20 (same declaration text).
```
structure NPVerifier where
…
```
def OAI.DirectedFeedback.NPVerifier.Accepts line 26
Also declared: OAI/Computability/DirectedFeedback/Model.lean:26 (same declaration text).
def OAI.DirectedFeedback.InNP NP is defined independently of SAT or any hardness assertion line 31
Source documentation
NP is defined independently of SAT or any hardness assertion.
L4DEL explanation
NP is defined independently of SAT or any hardness assertion.
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/Computability/DirectedFeedback/Model.lean:31 (same declaration text).
```
def InNP (language : List Bool → Prop) : Prop :=
…
```
structure OAI.DirectedFeedback.Digraph Finite loopless digraph line 36
Source documentation
Finite loopless digraph. Opposite arcs are permitted. Every arc is listed explicitly. No symmetric closure or undirected-cycle convention is used.
L4DEL explanation
Finite loopless digraph. Opposite arcs are permitted. Every arc is listed explicitly. No symmetric closure or undirected-cycle convention is used.
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/Computability/DirectedFeedback/Model.lean:36 (same declaration text).
```
structure Digraph where
…
```
def OAI.DirectedFeedback.Digraph.IsCycle An actual simple directed cycle of positive length line 47
Source documentation
An actual simple directed cycle of positive length. A cyclic enumeration of r + 1 distinct vertices supplies every successive arc, including the closing arc. A 2-cycle is allowed; looplessness rules out length 1.
L4DEL explanation
An actual simple directed cycle of positive length. A cyclic enumeration of r + 1 distinct vertices supplies every successive arc, including the closing arc. A 2-cycle is allowed; looplessness rules out length 1.
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/Computability/DirectedFeedback/Model.lean:47 (same declaration text).
```
def IsCycle (G : Digraph) {r : ℕ} (c : Fin (r + 1) → Fin G.n) : Prop :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.Feedback A feedback set intersects EVERY actual directed cycle line 51
Source documentation
A feedback set intersects EVERY actual directed cycle.
L4DEL explanation
A feedback set intersects EVERY actual directed cycle.
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/Computability/DirectedFeedback/Model.lean:51 (same declaration text).
```
def Feedback (G : Digraph) (F : Finset (Fin G.n)) : Prop :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.dfvs Minimum number of vertices of a feedback set line 56
Source documentation
Minimum number of vertices of a feedback set. No weights or auxiliary cost oracle appear in this definition.
L4DEL explanation
Minimum number of vertices of a feedback set. No weights or auxiliary cost oracle appear in this definition.
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/Computability/DirectedFeedback/Model.lean:56 (same declaration text).
```
noncomputable def dfvs (G : Digraph) : ℕ := by
…
```
Mentions: OAI.DirectedFeedback.Digraph
def OAI.DirectedFeedback.Digraph.bits Full explicit vertex and arc serialization, including isolated vertices line 64
Source documentation
Full explicit vertex and arc serialization, including isolated vertices.
L4DEL explanation
Full explicit vertex and arc serialization, 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/Computability/DirectedFeedback/Model.lean:64 (same declaration text).
```
def bits (G : Digraph) : List Bool :=
…
```
Mentions: OAI.DirectedFeedback.Digraph
structure OAI.DirectedFeedback.GapInstance Output includes a strictly positive integer threshold line 71
Source documentation
Output includes a strictly positive integer threshold.
L4DEL explanation
Output includes a strictly positive integer threshold.
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/Computability/DirectedFeedback/Model.lean:71 (same declaration text).
```
structure GapInstance where
…
```
def OAI.DirectedFeedback.GapInstance.bits line 76
Also declared: OAI/Computability/DirectedFeedback/Model.lean:76 (same declaration text).
structure OAI.DirectedFeedback.GapReduction A strict YES/NO gap reduction implemented by a finite-alphabet machine with polynomial runtime in the raw input bit length line 81
Source documentation
A strict YES/NO gap reduction implemented by a finite-alphabet machine with polynomial runtime in the raw input bit length.
L4DEL explanation
A strict YES/NO gap reduction implemented by a finite-alphabet machine with polynomial runtime in the raw input bit length.
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/Computability/DirectedFeedback/Model.lean:81 (same declaration text).
```
structure GapReduction (A : ℝ) (language : List Bool → Prop) where
…
```
def OAI.DirectedFeedback.MainStatement Constant-factor directed feedback vertex set hardness for all NP languages line 92
Source documentation
Constant-factor directed feedback vertex set hardness for all NP languages.
L4DEL explanation
Constant-factor directed feedback vertex set hardness for all NP languages.
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/Computability/DirectedFeedback/Model.lean:92 (same declaration text).
```
def MainStatement : Prop :=
…
```
theorem OAI.DirectedFeedback.main Challenge statement: Constant-factor hardness of directed feedback vertex set sorry line 98
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 5 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
2. The repository's comparator configuration selects OAI.Computability.DirectedFeedback.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Computability/DirectedFeedback/Main.lean:1132 (different declaration text). Qualify references as OAI.DirectedFeedback.main@path.
```
theorem DirectedFeedback.main : DirectedFeedback.MainStatement := by
…
```
Mentions: OAI.DirectedFeedback.MainStatement