# Contributor Tasks Bounded, ready-to-take units. Each states goal, acceptance evidence, and what it does **not** change. Use this with or without an AI coding agent. Difficulty: **S** one sitting · **M** Lean/schema · **L** design / multi-module. **Not survey-only.** Tasks below include survey pointers, but the workbench also needs domain consumers, non-claims, examples, landscape leads, and new claims on existing primitives. If nothing here fits, open an issue describing the gap. ## Open now **Agent-friendly default:** pick an S task or a small Lean use-site; let the agent draft; you (or CI) run `lake build`, `scripts/agent_gate.sh`, and `python3 scripts/check_print_axioms.py` when theorems change. Wrong Lean is a red build, not a social failure. A green build is **kernel validity of the encoding** — not paper match, model adequacy, non-vacuous assumptions, or system interpretation (see [CONTRIBUTING](../../CONTRIBUTING.md)). **Have a question rather than an answer?** Propose a conjecture — an open question stated precisely enough to be false is a deliverable here, and you do not need Lean to contribute one. See [conjectures](conjectures.md). **Looking for a target rather than a task?** Read the `work_queue` in [`docs/status/consumers.json`](../status/consumers.json) — every atlas declaration that nothing outside `Examples/` builds on. (`python3 scripts/report_consumers.py --queue` recomputes the same list in a couple of seconds; the committed file is what CI checks against.) A theorem with no downstream consumer has untested ergonomics — that is the gap CT-4 closed for `Verification.rice` and CT-16 opened for the bounded portfolio target. Giving one a real consumer, or arguing it should be retired, is contribution either way. The count is a queue, not a score. New here, and unsure whether a task is even the right shape for what you have? The README's [Get started](../../README.md#get-started) table routes that. If a task is what you want: CT-11, CT-12 and CT-14 need no Lean, CT-13 is the toolchain exercise. CT-1…CT-5 are completed history. ### CT-11 — Add a candidate lead to an uncovered row (S) — **Pointer rung** - **Goal:** pick one `MAPPED`-only survey row in [`registry.yaml`](../../registry.yaml) whose `candidate_formalizations` is `[]`, and add **one** lead pointing at an *existing* formalization. The entry needs all eight schema fields: a `repository` URL, its immutable `revision`, the `framework`, the `declaration` name, a `license`, an `inspection_state` (`UNVERIFIED` if you have only read the source), a `relationship_review` (`PENDING` is fine), and `notes` — a bare paper URL is not a candidate lead. A pen-and-paper result with no existing formalization goes to **CT-14** instead. No Lean, no proof, no coverage claim. - **Acceptance:** a schema-valid `candidate_formalizations` entry; `scripts/setup.sh --pointer` (i.e. `scripts/agent_gate.sh`) green. A lead is candidate evidence, not coverage. - **Does not change:** the row's `status` or any coverage count — a candidate is not a formalization until reproduced and classified. ### CT-12 — Verify one citation against its source (S) — **Verification rung** - **Goal:** take one `original_source_refs` entry in [`registry.yaml`](../../registry.yaml) — e.g. `survey-ref-018` (doi `10.1162/neco.1996.8.7.1391`) — confirm the DOI/arXiv id resolves to the cited paper and that the transcribed title, authors, and pages match. Correct the entry if anything is off. - **Acceptance:** every outcome leaves a durable record. Found a mismatch? Open a PR with the precise transcription fix (`scripts/agent_gate.sh` green). Checks out clean? Report it on the row's tracking issue (or a new verification issue) with the resolved link and what you confirmed — no empty PR. Source verification is a first-class contribution. - **Does not change:** any Lean, any relationship classification. ### CT-13 — Add one Lean use-site over a shipped theorem (S) — **Onboarding exercise** **This is a toolchain exercise, not coverage work — one per contributor.** The public API is already fully exercised: [`AISafetyAtlas/Examples/PublicAPI.lean`](../../AISafetyAtlas/Examples/PublicAPI.lean) carries an applied use-site for every declaration on the README "Lean API" list, and [`NFLConcrete.lean`](../../AISafetyAtlas/Examples/NFLConcrete.lean) covers the learning-layer schedules. A new `example` adds no coverage, closes no gap, and changes no status file. What it does is prove you can drive the toolchain — fork, branch, `lake build`, `agent_gate.sh`, PR — before you take on work where a mistake is expensive. That is the whole point, and it is worth one PR. - **Goal:** copy [`AISafetyAtlas/Examples/FirstContribution.lean`](../../AISafetyAtlas/Examples/FirstContribution.lean) as your model and add one new `example` that exercises an existing shipped theorem (e.g. `no_free_lunch_supervised`, or anything on the README "Lean API" list over `import AISafetyAtlas`). No new math — a use-site, not a reproof. **Append it at the bottom of that file**, under the marker after the "YOUR TURN" block — not between the examples already there. Appending keeps contributors' diffs from colliding. - **Acceptance:** `lake build AISafetyAtlas.Examples.FirstContribution` (or `.PublicAPI`) green and `scripts/agent_gate.sh` clean. A non-public `example` needs no local axiom audit — CI runs `check_print_axioms.py` for you, over the facade closure *and* the off-root build targets; reserve that check for new *public* theorems, definitions and bridges. Runs under the fast `scripts/setup.sh --quick` path if you stay on the learning layer. - **Terminal rung — do not repeat it.** Once your CT-13 has merged, a second one will be closed. Varying a type parameter (`Fin 2` → `Fin 3`) or a constant in an already-exercised theorem is not a distinct use-site. - **Next:** CT-11 / CT-12 / CT-14; a **nontrivial** facade consumer (pattern: [`WorkbenchConsumers.lean`](../../AISafetyAtlas/Examples/WorkbenchConsumers.lean) — cross-surface composition, instantiated model, boundary at a use site, or downstream theorem; not a trivial restatement); or domain work (Preference / Wireheading / Compositional primary surfaces). Survey `Formalize BY-0xx` / CT-6 / CT-9 / CT-15 remain optional, not required. With an agent: prefer Lean rungs — green build + axiom check is the **kernel** bar; alignment and usefulness stay review questions. - **Does not change:** any theorem statement or the public facade. ### CT-14 — Report a proof we don't have (S) — **Pointer rung** - **Goal:** you know a result — or a proof of one — not in the catalogue. Report where it lives, via the [Known formalization issue form](https://github.com/mbrcic/ai-safety-formalization-atlas/issues/new?template=known-formalization.yml). Value grades by readiness: **pen and paper** (a formalization target) → **another prover** (an Isabelle/Coq/HOL reproduction candidate) → **already in Lean** (a possible thin vendor/alias). This is the reuse thesis as a rung: point us at a building block instead of reinventing it. - **Acceptance:** a filled discovery issue, or a schema-valid `candidate_formalizations` entry with source coordinates and license; `scripts/agent_gate.sh` green if you touch the registry. No coverage claimed until reproduced and classified. - **Does not change:** any coverage count — a lead is candidate evidence only. ### CT-15 — Formalize the survey's own three theorems (BY-042 / BY-043 / BY-044) (L) — **New proof rung** The three results the survey [*Impossibility Results in AI: A Survey*](https://doi.org/10.1145/3603371) introduces **itself** — listed in the results table but, unlike the imported results, developed and argued by the authors in a dedicated section with proof sketches. BY-042 remains `PROOF_SKETCH` and unformalized; BY-043 already carries a `RELATED` formalization; BY-044 now carries an `EQUIVALENT` process-compositional formalization and an executable cyclic non-vacuity model. A sketch is a scaffold, not a full proof, so mechanizing one audits the sketch. One target among many, taken on the same grounds as any other: whether it makes something else easier to state or prove. - **Targets (pick one):** - **BY-044 — Limited self-awareness (completed 2026-08-12):** `AISafetyAtlas.SelfAwareness` separates the local strict-awareness-extension obstruction from the maximal-composite proof, permits ordinary awareness cycles, and explicitly unpacks the awareness definition's implicit non-cancellation/resource semantics. First-author statement-level review confirms that this is intended source content rather than a new physical premise. Fixed-horizon and semilattice representational choices are recorded in `docs/provenance/limited-self-awareness.md`; the row is `EQUIVALENT`. - **BY-043 — Misaligned embodiment:** mistakenly cloned self-interested agents cannot perfectly control one another. The sketch turns on operational cloning, functional identity, self-interest, and competition over a scarce resource — not obviously self-reference. Pin those definitions first. - **BY-042 — Unfairness of explainability:** a verifier and a decision-maker hold structurally unequal strategic positions when explanations omit the full execution trace. Two distinct claims — verifier indistinguishability without a full trace, and growing adversarial advantage as the decision-maker better models surrounding actors — needing game-theoretic / information-asymmetry machinery; scope the hardest, take last. - **Step 0 (do first, low effort):** in [`registry.yaml`](../../registry.yaml) add `"brcic-yampolskiy-2023-own-results"` to the chosen row's `original_source_refs` — the `work` record for the survey's authored section, **not** `brcic-yampolskiy-2023`, which is the Table 1 directory and states no theorem to grade against. `original_source_refs` must hold `source_catalog` keys, never raw DOIs, or `agent_gate.sh` rejects the change. Then write a provenance note under [`../provenance/`](../provenance/) that pins the **exact** paper statement, section/theorem number, the sketch, and every definition it assumes (e.g. what "perfectly self-aware" or "operational boundaries" mean formally). Pin the model before writing Lean. - **Acceptance:** a kernel-checked Lean theorem under the facade (new namespace as needed — `AISafetyAtlas.SelfAwareness`, `.Embodiment`; `.Explainability` already exists) with an honest `EXACT`/`EQUIVALENT`/`RELATED` classification against the paper statement; the provenance note stating exactly which assumptions are and are not mechanized and **any gap the sketch leaves**; `agent_gate.sh` + `lake build` green; kernel axioms clean. - **Does not change:** the other two rows until each lands; no retro-claim of coverage in README/registry until a proof (not a statement) is in. ### CT-16 — Instantiate the bounded portfolio target on your own architecture (M) — **Onboarding exercise** `AISafetyAtlas.Oversight.JointObservation` defines what a *correct* portfolio of observations would be — `PortfolioCovers`, `InclusionMinimalCovering`, a declared `PortfolioCost`, `CostOptimalCovering` — and checks one three-principal instance in [`Examples.Oversight.JointObservation.Portfolio`](../../AISafetyAtlas/Examples/Oversight/JointObservation/Portfolio.lean). Nothing outside that example has ever instantiated it. That is the gap: a target specification nobody has consumed is a specification whose ergonomics are untested. - **Goal:** bring your own bounded architecture — principals, a finite execution enumeration, a hazard family of at least two hazards, a declared candidate family, and a declared cost — and prove a portfolio for it covers, is inclusion-minimal, and is or is not cost-optimal. The interesting instances are the ones where the two orderings *disagree*, since `inclusionMinimal_of_costOptimal` gives only one direction and the non-implication is exhibited rather than proved. - **Where to start:** read [joint observation model](joint-observation-model.md), then the example above; it is fully explicit and every step is `decide`-able on a small enumeration. - **Acceptance:** a new `Examples/` module that imports only the facade `AISafetyAtlas.Oversight.JointObservation`, restates no kernel definition, and adds its build target to `scripts/lean_build_targets.txt`; `agent_gate.sh` + `lake build` green; kernel axioms clean. - **Does not change:** any coverage count. This is landscape infrastructure (`LAND-JOINTOBS-001`), not a survey row, and an instance claims nothing about strategic production — everything stays under the truthful mechanism `M0`. - **Report back:** what the type of `joint` made awkward. Coalition access is enforced by type rather than by a side condition, and that is exactly the design choice a second consumer is positioned to falsify. ### CT-18 — State the margin conditions (M1)–(M6) and place the three colliding models in the class (M) — **done (2026-08-19)** - **Goal:** state MAIS-A2 Definition 3.1's margin conditions (M1)–(M6) in Lean over `AISafetyAtlas.Causal.Model`, and prove the three models of [`BehavioralCollision.lean`](../../AISafetyAtlas/Examples/Causal/BehavioralCollision.lean) satisfy them at `λ = 1/10`. Until this lands, that module checks a *collision of transforms*; MAIS-O23 quantifies over the margin class `M(s, λ)`, so the collision does not answer it. - **The six, and what each costs.** Five are arithmetic on concrete rationals and should fall to `decide` or `norm_num` once stated; one needs new structure. - **(M1)** every table entry in `[λ, 1-λ]`. Entries are `1/2`, `4/5`, `1/5`. Easy. - **(M2)** `|g(z)| ≥ λ` for every `z`. Here `|g| = 1/2`. Easy. - **(M3)** `g` takes both signs on every observation-compatible slice. With `O = ∅` this is just *`g` takes both signs*. Easy. - **(M4)** every edge has strength `≥ λ`: some pair of parent configurations differing only in the tail gives a table difference `≥ λ`. `X → Y` gives `|4/5 - 1/5| = 3/5`; `Y → X` gives `|4/5 - 1/2| = 3/10`; the edgeless model has no edges, so it is vacuous — state it so that the vacuous case is visibly the definition and not an omission. - **(M5)** `Anc(U) = C` and `O ⊊ C`. **This is the one with a cost.** It needs ancestry — the reflexive-transitive closure of the parent relation — which `Model` does not currently expose. The `rank` field gives a well-founded order to recurse on, so the closure is definable without `Finset` fixpoint machinery, but it is a definition plus its lemmas, not a `decide`. - **(M6)** `u` sensitive to each utility parent. Requires the skeleton's `u` as an object; currently only the gap `g` is present, which is what (M6) is stated in terms of, so this is `|g(z) - g(z')| ≥ λ` over pairs differing in one coordinate. Easy. - **Acceptance:** a `MarginClass` predicate (or six named predicates) over an arbitrary `Fintype` of variables, three membership theorems at `λ = 1/10`, and the registry row `LAND-CAUSAL-COLLISION-001` updated to say what the module then establishes. `lake build`, `scripts/agent_gate.sh`, `python3 scripts/check_print_axioms.py` green. - **Scope warning.** Membership in the margin class makes the construction an answer to MAIS-O23 *as the atlas states it*. Whether it answers the problem as MAIS states it is a review question for MAIS, not a build question — the atlas records that a stated construction checks, and asserts no resolution. Note also that the general class `M(s, λ)` admits the edgeless graph while the agenda's two-variable class `MM₂(λ)` does not: `MM₂(λ)` is defined as the models carrying `G→` or `G←`. The collision is stated against the general class; do not silently narrow it to `MM₂`. - **Does not change:** the collision theorems, which are correct as they stand, or `Model`'s existing fields. - **Owner note:** general causal machinery here is reusable — MAIS-A2 carries fourteen problems in this setting, twelve of them causal. - **Closed 2026-08-19.** All six hold for all three models at `λ = 1/10`: `edgeless_mem`, `arrowXY_mem`, `arrowYX_mem`. (M5) cost far less than priced here — the least parent-closed superset is definable as an intersection of all of them, so `Model.ancestors` needed no iteration and no fixpoint-stability lemma, and `Model.ancestors_eq_univ_iff` gives the decidable elimination form. The estimate above was wrong about the only item it called costly; kept as written so the misprice is visible. ### CT-19 — Carry the utility in Skeleton, so regret becomes statable (M) — **done (2026-08-19)** Completed 2026-08-19. `Skeleton` carries bounded utility on categorical assignments and derives `gap` only in the Bool-decision specialization. `AISafetyAtlas.Causal.Decision` states probability mixtures, generic finite policies factored through visible variables, unmediated value, identified sets, model error, and a rational `IsRadius` predicate. `Examples.Causal.Decision` supplies a non-vacuity witness. The layer is the RE24 Assumption-1 projection, not a full CID, and does not state O27/O28/O34(b). ### CT-20 — Prove the finite-fibre maximum for causal policy regret (M) — **done (2026-08-19)** Completed 2026-08-19, then generalized in the categorical-kernel handoff. `fibreRep` picks one representative per visible fibre; `fibreScore`, `bestDecision`, and `bestPolicy` construct the optimum for any finite decision alphabet. `regret_decomp` and `regret_eq_zero_iff` prove zero regret exactly when positive policy support lies on the fibrewise argmax, with ties unconstrained. The Bool corollary `value_le_sign` recovers the sign policy. `Examples.Causal.card_fibreRep_empty` is the empty-visible cardinality tripwire. ### CT-17 — Pin Breuer 1995 at source and grade the self-measurement row (S) — **done (verified 2026-08-11)** Completed 2026-08-11. The primary PDF is pinned in [`self-measurement-kernel.md`](../provenance/self-measurement-kernel.md): §3.2 defines the inference map and exact measurement, §3.3 defines proper inclusion and the restriction map, §3.5 defines meshing, and Propositions 1–2 give the abstract no-go results. The generic fibre skeleton remains LAND-SELFMEAS-001; the source-faithful abstract inference-map core is LAND-SELFMEAS-002 with relationship RELATED and an explicit scope delta. Physical apparatus construction, dynamics, quantum structure, EPR, and philosophical consequences remain intentionally omitted. The Lean and registry gates are green. No DOI was confirmed; the direct PDF and PhilPapers catalogue locators are recorded in the provenance note. ### CT-6 — First possibility proof: continuous free lunches (BY-022) (L) — **New proof rung** - **Goal:** give BY-022 (*Free lunches in continuous spaces and coevolution*, Auger–Teytaud 2010 / Wolpert–Macready coevolutionary) its first Lean statement — a setting where the finite NFL symmetry provably fails, dual to `AISafetyAtlas.Learning.no_free_lunch`. - **Acceptance:** a kernel-checked Lean theorem under the facade (or a landscape entry if the natural home is adjacent), a `formalizations`/landscape record with honest `EXACT`/`EQUIVALENT`/`RELATED` classification against `survey-ref-047`/`survey-ref-048`, provenance note, `agent_gate.sh` + `lake build` green, kernel axioms clean. - **Does not change:** the impossibility rows; do not retro-claim BY-022 as formalized in README/registry until this lands. ### CT-7 — Reproduce DeepMind doubly-efficient debate into the landscape (M) — **done (reproduced 2026-07-20)** The formalization exists and is Lean 4: `google-deepmind/debate` (Apache-2.0), a machine-checked correctness proof of the stochastic oracle protocol from Brown-Cohen–Irving–Piliouras 2023 (*Scalable AI Safety via Doubly-Efficient Debate*, arXiv 2311.14125). This is a **possibility / scalable-oversight guarantee**, not an impossibility — a live landscape anchor dual to the impossibility rows. - **Coordinates:** repo `github.com/google-deepmind/debate`, revision `de3a6e500ae1a65dfeea2f91ef519ebad9704be0` (single `main`, no release tag, last commit 2024-10-08). Main theorems in `Debate/Correct.lean`: `completeness`, `soundness`, `correctness` (paper Theorem 6.2). License Apache-2.0. - **Version gap (closed 2026-08-20):** upstream pins `leanprover/lean4:v4.8.0` and Mathlib `v4.8.0`; the atlas was then on `v4.31.0`. The original scope was therefore Path A only — build at the upstream toolchain from a separate checkout, like Chaitin/Isabelle. A later port closed the gap; see Path B below. - **Acceptance:** clean build at the pinned revision under its own toolchain; strict-trust scan of the reproduced tree; a `registry.yaml` record (`LAND-DEBATE-001` — revision, `Debate/Correct.lean`, the three theorem names, Apache-2.0, relationship `RELATED`, reproduction status; an artifact row, so never headline coverage); `scripts/reproduce_debate.sh`; regenerated views; provenance note. Never a headline coverage count. - **Honest scope:** carry upstream's own caveats — correctness only; space complexity not formalized; time counts oracle queries only; Lipschitz oracle machine defined slightly differently (a stronger variant). No AI-system reading without a separate reviewed bridge. - **Does not change:** survey `registry.yaml` coverage; the build closure. - **Done (2026-07-20):** clean build at the pinned revision under upstream `leanprover/lean4:v4.8.0` (`Debate.Correct`, 1721/1721 targets); strict-trust scan clean across 19 upstream Lean sources; `completeness`/`soundness`/ `correctness` present in `Debate/Correct.lean`. Landscape record `LAND-DEBATE-001` (artifact row, no atlas import surface); `scripts/reproduce_debate.sh`; evidence [`debate-reproduction.md`](../provenance/debate-reproduction.md). First reproduced possibility / scalable-oversight anchor. Never headline coverage. - **Path B done (2026-08-20):** the Lean v4.31.0 port moves the development to the atlas's own Mathlib commit without weakening a theorem. Vendored as 18 modules under `AISafetyAtlas/Upstream/Debate/`, wrapped by `AISafetyAtlas.Oversight.Debate`, witnessed by `AISafetyAtlas/Examples/Oversight/Debate.lean`, migrated in place to Lean v4.33.0 on 2026-08-31, and checked by `scripts/reproduce_debate.sh --in-tree` (trust scan, build, kernel `#print axioms` on all six facade declarations). The facade is deliberately **off** the root import, so `root_import` stays `false` and the audit reaches it through `OFF_ROOT_FACADES`. Path A is kept as a check on the upstream artifact; its lane never covered query complexity. Still never headline coverage. Detail: [`debate-reproduction.md`](../provenance/debate-reproduction.md). ### CT-8 — BY-025 Uncontainability: bridge or documented no-map (M) — **Bridge rung** - **Goal:** decide whether BY-025 (still `MAPPED`) earns a dedicated bridge over Rice/halting with an explicit containment model, or stays mapped-only. - **Acceptance:** either a bridge declaration with stated modeled system, assumptions, quantifier order, conclusion, and the practical claim it does **not** establish (`ai_interpretation_status: HUMAN_REVIEW`), or a provenance note recording why no clean statement map exists. Do not claim BY-025 is formalized. - **Does not change:** the Alfonseca/AgentBehavior packaging; no fake bridge graduation. ### CT-9 — Formalize a debate follow-up with no existing proof (L) — **New proof rung** Greenfield as far as anyone here has looked: a manual search on 2026-07-20 found no interactive-theorem-prover formalization of these debate refinements. That search recorded no corpus or revision, so it is **not** a novelty check under [methodology](methodology.md#formal-library-discovery-evidence) and the claim is scoped to it. Before asserting more than "none was found," record a `novelty_checks` entry. Formalizing one is original work, dual to CT-7's *reproduction* of the already-formalized doubly-efficient debate. Each target has a complete pen-and-paper proof; the task is to mechanize it. Pointer to the informal proof is given per target. - **Targets (pick one):** - *Avoiding Obfuscation with Prover-Estimator Debate* (arXiv 2506.13609) — relaxes the equal-compute-provers assumption of doubly-efficient debate. **Pen-and-paper proof:** the paper has exactly three theorems — **6.1** (completeness: honest debater wins under (ε,ρ)-stability) and **6.2** (soundness: honest output is truth in every Stackelberg equilibrium), the two "main theorems" in Section 6; and **8.3** (Section 8), the training-convergence companion (debaters reach Stackelberg equilibria via standard gradient methods). Supporting proofs in Appendices A–D. Formalize any one; smallest scoped core is Theorem 6.1 completeness alone. - *How to Avoid Debate: Scalable AI Safety via Doubly-Efficient Interactive Proofs* (arXiv 2607.03561) — doubly-efficient **single-prover** interactive proofs/arguments for oracle-aided (relativizing) computation. **Pen-and-paper proof:** two main-results settings — (1) robust computation (output stable if a small fraction of oracle answers are wrong) and (2) low-degree-polynomial oracle; pick one setting's protocol + soundness proof. (Paper is days old as of 2026-07-20; take exact theorem numbers from the arXiv PDF, HTML not yet rendered.) - **Acceptance:** a kernel-checked Lean statement + proof of the paper's central guarantee (or an explicitly scoped core of it) under the facade or landscape; honest relationship classification against the paper theorem; provenance note stating exactly which theorem and which assumptions are and are not mechanized; `agent_gate.sh` + `lake build` green; kernel axioms clean. - **Reuse first:** the `google-deepmind/debate` Lean development (CT-7) is the natural scaffold, and since 2026-08-20 it is **in-tree**, at Lean 4.33 since the toolchain migration of 2026-08-31 — `import AISafetyAtlas.Upstream.Debate` gives you its `Prob`/`Comp` monads, `Oracle`, and the protocol definitions directly. Build on those before rebuilding primitives. - **Honest scope:** a possibility/oversight guarantee, `RELATED` at most; no AI-system reading without a separate reviewed bridge. Do not claim the paper is "formalized" until a proof (not a statement) lands. - **Does not change:** survey `registry.yaml` coverage. ## CT-10 — Reproduce the closed-under-permutation NFL iff (BY-020, optional) (L) — **done** - **Done (2026-08-16), on both axes:** `AISafetyAtlas.Learning.Sharp` proves `nfl_adaptive_iff_permInvariant`. Graded **`RELATED`**, not `EQUIVALENT`. The atlas statement widens the printed one on the **weight** axis (any real weight, no nonnegativity or normalization, where the source has a probability distribution) and **meets** it on the algorithm axis: `nfl_adaptive_of_permInvariant` proves sufficiency over `AdaptiveRule` with the no-revisit hypothesis `∀ c, Injective (ruleVisit r c)`, which is the source's non-repeating black-box class, quantified over every sample length and every cost-sequence measure. `permInvariant_of_nfl` is **stronger** than the source — it assumes schedule-independence only at the single length `|X|`, only over non-adaptive schedules, and only at indicator measures. `nfl_of_permInvariant` is the fixed-schedule special case, kept because it is the form the rest of the atlas consumes. Schumacher–Vose–Whitley's set form is `permInvariant_of_closedUnderPermutation`, and their basis-class identity is `basisClass_histogram_eq_permOrbit`. The uniform cores are the constant-weight case (`no_free_lunch_embedding_of_sharp`) and are unchanged. Non-vacuity is exhibited in **both** directions in `AISafetyAtlas.Examples.Learning.Sharp`: a weight off the condition for which NFL demonstrably fails, and a proper permutation-closed prior for which it holds. - **Registry home: `BY-021`, not `BY-020`.** Both sources quantify over non-repeating black-box *search* algorithms — Igel–Toussaint's Figure 1 is captioned "the optimization scenario considered in NFL-theorems" — so these records belong on the optimization row. They sat on `BY-020` (Wolpert 1996 supervised learning) until 2026-08-16 and were refiled then. - **Nothing open.** Two things that can look like gains are not: the source's Theorem 5 quantifies over `m` as well, so every sample length is printed, and the sufficiency half for the source's adaptive non-repeating algorithms is closed by `nfl_adaptive_of_permInvariant`. What remains out of scope is time-varying objectives. The papers' stochastic algorithms are now COVERED: Igel-Toussaint's cited randomized class is Droste-Jansen-Wegener's, and `mixtureTrace`/`nfl_mixture_of_permInvariant` is their definition and their proof step; Schumacher-Vose-Whitley's §2 is deterministic and never carried a gap. Wolpert-Macready 1997's stochastic algorithms are a different paper and remain open on `BY-020`. Provenance: [`../provenance/lean-wolpert-nfl.md`](../provenance/lean-wolpert-nfl.md). The original scoping follows. - **Goal:** reproduce the sharp *both-directions* NFL characterization on the **prior axis**: over a distribution `P` on target functions `X → Y`, expected performance is algorithm-independent **iff** `P` is closed under permutation of the domain. This is the general boundary that subsumes every uniform-prior core already in `AISafetyAtlas.Learning` (`no_free_lunch`, `no_free_lunch_supervised`, `no_free_lunch_adaptive`) — those are the trivially-c.u.p. special case. - **Source (in the literature — citable proof to diff against):** Schumacher, Vose, Whitley, *The No Free Lunch and Problem Description Length* (GECCO 2001, first c.u.p. iff); Igel & Toussaint, *A No-Free-Lunch Theorem for Non-Uniform Distributions of Target Functions* (J. Math. Modelling & Algorithms 2004, doi `10.1023/B:JMMA.0000049381.24625.f7`, both directions). Because it is a published result, this graduates to **`EXACT`/`EQUIVALENT`** — not the folklore `NEW_PROOF` status of the loss-axis iff `homogeneous_iff_learner_indep`. - **Acceptance:** kernel-checked Lean theorem under the facade; finite weighted sums over `Fintype` suffice (no Mathlib probability needed); honest `EXACT`/`EQUIVALENT`/`RELATED` classification against `survey-ref-018`; provenance note in [`../provenance/lean-wolpert-nfl.md`](../provenance/lean-wolpert-nfl.md) recording which paper and which assumptions; `agent_gate.sh` + `lake build` green; kernel axioms clean. - **Why it may wait (read before taking):** no current downstream consumer needs it — the uniform cores already carry the headline. Its distinctive value is bridge-readiness: c.u.p. is the exact condition under which NFL is *vacuous* (real learning priors are structured, not permutation-symmetric), so it is the one NFL variant with a plausible AI-safety bridge story. Pull it only if a bridge needs "which priors kill learning"; otherwise it is completeness polish. - **Does not change:** the existing `NEW_PROOF` loss-axis iff stays as-is; no retro-claim of c.u.p. coverage in README/registry until a proof lands. See reference note `nfl-cup-iff-lineage` and [`ct2-nfl-triage.md`](../provenance/ct2-nfl-triage.md). ## CT-1 — Reproduce the Chaitin BY-015 candidate (M) — **done** - **Goal:** reproduce `AlexeyMilovanov/kolmogorov-complexity-lean` at revision `005ac4c81eefe09642ef561057199d489cd79485`, compare `FormalSystem.chaitinIncompleteness` against survey source `survey-ref-039`, and classify the relationship. - **Done (2026-07-19):** clean build at the pinned revision; trust scan clean; Lean/Mathlib 4.31 compatible; statement comparison in [`external-formalizations.md`](../provenance/external-formalizations.md); relationship **`EQUIVALENT`**; `formalizations` record + `scripts/reproduce_chaitin.sh`; thin aliases `AISafetyAtlas.Logic.chaitin_incompleteness` / `chaitin_bound` (vendored import closure for the Lean module boundary). Follow-on (done): BY-013 Unprovability now covered by classical Gödel first incompleteness from `FormalizedFormalLogic/Foundation` (Lake dependency, `EQUIVALENT`, `godel_first_incompleteness`), with Gödel second incompleteness (`godel_second_incompleteness`) as a `RELATED` companion on the same row. The earlier Kritchman–Raz skeleton is retired. ## CT-2 — Triage AFP `No_Free_Lunch_ML` for BY-020 / BY-021 (L) — **done (reproduced)** - **Goal:** inspect the AFP `No_Free_Lunch_ML` declarations and hypotheses, reproduce a pinned AFP artifact, and classify each of BY-020 and BY-021 as same theorem, partial overlap, or distinct. - **Acceptance evidence:** a pinned AFP revision and Isabelle version; a reproduction log; a per-row relationship classification with reasoning. - **Does not change:** coverage until each row is reproduced and classified; a repository link alone is candidate evidence, not coverage. - **Done (2026-07-19):** AFP `No_Free_Lunch_ML` reproduced (pinned `2026-02-06`, SHA-256 `93ce8953…173588`, `isabelle build` exit 0 via `scripts/reproduce_isabelle.sh nfl`) and triaged as the Shalev-Shwartz–Ben-David PAC no-free-lunch (Understanding ML §5.1) — **DISTINCT** from BY-020 (Wolpert supervised NFL) and BY-021 (Wolpert–Macready optimization NFL). Candidate tags removed from both rows; reproduced SSBD entry recorded as landscape row `LAND-NFL-001`. Evidence: [`ct2-nfl-triage.md`](../provenance/ct2-nfl-triage.md). ## CT-3 — Domain and statement review of the robot bridge (M) — **done (reviewed)** - **Goal:** review `AISafetyAtlas.Verification.Robot.action_safety_unverifiable` against van Leeuwen & Wiedermann Theorem 1: the modeled total-trace system, the explicit switching-construction certificate, and the `RELATED` classification. - **Review package:** [`ct3-robot-review-package.md`](../interpretation-reviews/ct3-robot-review-package.md). - **Done (2026-07-19):** maintainer **reviewed** statement and scoped interpretation; accepts transparent **`RELATED`** packaging (Lean assumes `SwitchingConstruction`; not paper EXACT). Registry: formalization **`RELATED`**, bridge **`REVIEWED`**. - **Does not change:** machine-checked statement; headline coverage still excludes BY-033 as RELATED-only. ## CT-4 — Give `Verification.rice` a downstream consumer or retire it (M) — **done** - **Goal:** decide whether the `AISafetyAtlas.Verification.rice` interface earns its public slot. - **Done (2026-07-19):** `AISafetyAtlas.Verification.AgentBehavior` models encoded agents (Mathlib codes), `SafetySpec` / `BehavioralSafetyVerifier`, and proves `no_behavioral_safety_verifier` by reducing through `Verification.rice`. Root import, PublicAPI smoke example, and BY-012 registry declaration updated. - **Bridge review (2026-07-19):** maintainer accepted statement and scoped interpretation; BY-012 is `REVIEWED` ([`review-by-012-agentbehavior.md`](../interpretation-reviews/review-by-012-agentbehavior.md)). ## CT-5 — Surface the generated atlas index in project navigation (S) — **done** - **Goal:** link the generated full-registry human view from README/docs entry points. - **Done:** README repository-contents list links it (now the per-source report [`brcic-yampolskiy-2023.md`](../status/sources/brcic-yampolskiy-2023.md)); landscape index is linked alongside it. ## Public issue queue Do **not** open GitHub issues without maintainer authorization. When authorized, open issues for remaining outward work (e.g. CT-2) using the acceptance evidence above as the issue body. Suggested title: 1. `CT-2: Triage AFP No_Free_Lunch_ML for BY-020 / BY-021` ## Completed - Bridge-status lifecycle vocabulary (`HUMAN_REVIEW` / `STATEMENT_REVIEWED` / `REVIEWED`) with `interpretation_review` evidence, enforced by `scripts/validate_registry.py`; the v0.1 all-`HUMAN_REVIEW` snapshot now lives only in the release audit. - Structured `candidate_formalizations` schema; BY-015 Chaitin promoted to coverage; BY-001 / BY-020 / BY-021 candidates populated. - Generated full-registry human view at [`sources/brcic-yampolskiy-2023.md`](../status/sources/brcic-yampolskiy-2023.md). - `registry.yaml` + generated landscape index for non–Table-1 formalizations . - Status breakdown of WRAPPER vs BRIDGE; generated STATE snapshot. - Kernel `#print axioms` CI check; Upstream LICENSE copies. - Validator perimeter documented in methodology. - CT-4 AgentBehavior consumer; CT-3 review package.