# Methodology

## Evidence order

For each survey result:

1. Identify the survey row and cited original source.
2. Search Mathlib and other maintained Lean repositories.
3. Search maintained formalizations in other proof assistants.
4. Reproduce external builds where practical.
5. Attempt a new Lean proof only when the result is missing, useful, and tractable.

Records distinguish an exact statement from an equivalent, related,
dependency-only, or unclear formalization. A repository name or search hit is
not enough: verified records include the version, module/file, declaration, and
license.

## Workbench metrics vs statement-match grades

The atlas is a **workbench and launchpad**. Report progress on three tracks:

1. **Workbench capital** — importable Lean (including `RELATED`), facades,
   examples; published units rebuild and pass the axiom policy.
2. **Statement-match** — reproduced `EXACT` or `EQUIVALENT` only. Conservative
   citation grade, not the primary score; do not raise it by weakening grades.
3. **AI-system bridges** — human-reviewed interpretation; never implied by math
   alone.

`RELATED` is scoped capital with documented deltas—not “failed EXACT,” and not
by itself a claim that paper-parity work is finished (see residual notes under
`docs/provenance/`). Statement-match and `RELATED` are reported separately so
specializations are not read as full source matches.

### What separates the three

Both `EXACT` and `EQUIVALENT` assert **complete coverage** of the printed
statement. They differ in how it is rendered.

- **`EXACT`** — the Lean statement *is* the printed statement: the source's own
  objects, hypotheses and conclusion, transcribed rather than reformulated. A
  record earns it only when no residual is outstanding; BY-005 was moved here
  from `RELATED` on 2026-08-17 when the last two closed, which is the shape of
  the promotion in general.
- **`EQUIVALENT`** — the printed statement in full, through a different but
  provably equivalent representation: the source's objects unpacked, or the
  claim stated over the paper's own abstraction rather than its notation. Every
  `EQUIVALENT` record carrying declarations documents that re-rendering in
  `scope_delta`, and that documentation is what makes the equivalence
  checkable rather than asserted.
- **`RELATED`** — deliberately partial coverage, with the delta written down.

**None of the three says anything about generality.** A transcription can still
be more general than print, because a Lean statement inherits whatever the
typeclass it is stated over admits. That axis is graded per printed
statement in `docs/provenance/source-coverage-audit.md`, and it is independent:
`EXACT` + `Wider` is a coherent and common combination, and so is `RELATED` +
`Same` on the part that is covered.

**A `RELATED` record that a reader can reach carries its delta as data.** When
the record's module is on the public root import, or its row's bridge status has
graduated past `HUMAN_REVIEW`, or the row exposes a `BRIDGE` declaration, the
record must supply `scope_delta`: a one-line summary of what the atlas core does
not cover relative to its source, and a path to the document that establishes it.
The validator rejects a missing delta and an evidence path that does not resolve.

The trigger is **reach, not grade**. Internal helper material that nothing public
exposes — an upstream `Mathlib` or `Foundation` module that a wrapper happens to
name — stays lighter, because no reader meets it holding a claim. Nothing here
weakens grading: `relationship` still gates headline counting, and a delta is a
disclosure obligation on `RELATED`, never a licence to record one where
`EXACT`/`EQUIVALENT` was warranted.

Formalization licenses use SPDX identifiers. Repository URLs and any recorded
source locators must be syntactically valid HTTP(S) locations. A source locator
may remain absent when the cited bibliography does not provide a verified
online location; the validator does not invent one. Every `reproduced: true`
record names its build environment and command.

External records use an immutable upstream revision or content-addressed
archive. A formalization stored in this repository uses version `IN_TREE`:
its source is resolved in the same immutable checkout or release tag as the
registry record. This avoids an impossible self-reference in which a commit
would need to contain its own hash. Publication audits should establish the
reachability of the registry's release ref, which then anchors every `IN_TREE`
record in that tree.

## One ledger, two kinds of row

`registry.yaml` holds every result. A row carrying `informal_claim` is a **claim**
— something a source asserted — and must supply the claim fields and a bridge
status. A row without one is an **artifact**: a formalization standing on its own
account, using the `LAND-` prefix, forbidden from carrying claim fields, and
required to record at least one formalization, since otherwise it asserts
nothing.

The prefix says what a row is, not where it came from. `BY-###` is the closed
survey block, `CLM-*` is a claim catalogued from any other source and must name
that provenance in `original_source_refs`, `LAND-*` is an artifact. Only survey
rows carry `paper_reference`, `survey_proof_assessment`,
and `formal_library_search`: those record how one survey presented and searched
its own rows, and they are questions another source's claim cannot answer.
Requiring them everywhere meant a real AISI or MAIS claim could only be admitted
by inventing survey vocabulary for it — the ledger would render as source-neutral
while the schema stayed survey-shaped.

There were two files. A landscape entry and a registry `formalizations[]` record
shared five fields outright and duplicated two more concepts under different
names, so the split modelled one thing twice. Its justification was that
landscape must never increase the statement-match count, which stopped being a
concern when the counts stopped having denominators.

**Closure belongs to the source, not to the file.** The Brcic–Yampolskiy block
must stay contiguous `BY-001`…`BY-044` and complete, because that catalogue is
finished. Everything else is open: artifact rows, and claims from any other
catalogued source, neither of which inherits the six-corpus sweep — that sweep is
the `baseline-catalogue` profile of one source.

## Parsimony and source roles

A survey result is counted once regardless of how many provers, proofs, or
representations establish it. Formalization records are evidence records, not
additional theorem-coverage claims.

For the public Lean API, select one canonical maintained result when one is
available and expose only the atlas aliases and bridges needed by downstream
work. If no maintained package is available, use a pinned, licensed, audited
source and record that the atlas assumes its version-migration burden. An
alternative proof remains provenance unless it adds a documented capability
such as a stronger statement, a required representation, an explicit
composable reduction, useful constructive content, or necessary dependency
independence.

### Parsimony governs duplication; foundations get a different test

The rule above answers one question: is a second way of establishing the same
thing worth its maintenance? Applied to a *foundation* — a definitional layer
that catalogued rows cannot be stated without at all — it asks for consumers
that are themselves blocked on the layer being judged. That is a rule no
foundation can pass, and its cost is invisible: nothing is rejected, results
simply never get proposed, because the first contributor would have to pay for
the layer alone.

A concrete instance is on the board now. `NC-006` records that the pinned
Mathlib carries no Shannon entropy, hence no conditional entropy or mutual
information. `BY-004` (Law of Requisite Variety) and `BY-005`
(information-theoretic control limits) both need exactly that, and neither can
be first, because the entry cost is identical for each and neither result
justifies it alone.

So a foundation may land ahead of its consumers when all four of these hold, and
they are checkable rather than speculative:

1. **Two blocked rows, by id.** At least two existing `BY-`/`CLM-`/`LAND-` rows
   or `tasks.yaml` entries that cannot be *stated* without it. Recorded in the
   artifact row, so the claim is auditable rather than atmospheric.
2. **The gap is upstream and recorded.** A `novelty_checks` entry showing the
   pinned corpora lack it. Without that the blocker may be that nobody bothered,
   which is not a reason to build a layer.
3. **Definitions may precede consumers; theorems may not.** The definitional
   half of a foundation is usually cheap and is the half that removes the
   barrier, so it may land with no consumer. The theorem half is expensive and
   cannot be guessed — which theorems a consumer needs is exactly what is
   unknown until one arrives — so it requires a consumer landing in the same
   change or the next.
4. **An expiry.** The row names a release by which a consumer must land, after
   which the layer is deleted or demoted to provenance. This is what makes the
   bet reversible, and reversibility is what makes it takeable. Removal is an
   ordinary outcome here: the `doc-gen4` pipeline was built and removed on cost
   grounds.

A foundation is a `LAND-` artifact row. It never enters headline coverage and
never carries a statement-match grade against a source it does not state.

The trade this strikes: parsimony keeps its teeth where duplication and
speculative *theorem* work are concerned, and gives up only the veto over cheap
definitional layers whose blocked consumers can be named in advance. A layer
admitted this way that no one uses is deleted at a known date rather than
accumulating.

Research reports and literature surveys are discovery inputs. Claims from them
enter the verified registry only after checking a primary source, an immutable
revision, the declaration itself, the license, and, where practical, a local
build.

Relevant formalizations outside the survey inventory are recorded in
`registry.yaml` (machine-readable) and narrated in the
external-evidence documentation. The generated
[landscape index](../status/landscape-index.md) lists them. Landscape entries do **not**
enter survey-coverage counts. A landscape result may appear on the public Lean
root import (for example attribution impossibility) only when it is listed in
`root_import: true`. Turning an artifact row into a claim row still requires the
normal admission checks.

## Formal-library discovery evidence

Discovery searching runs under one of two **profiles**, and the difference is
what each one attaches to.

**`baseline-catalogue`** is a completeness artifact for one catalogued source:
a single synchronized sweep across every row of that source, kept in sync with
its row set. It is not a standing obligation. A new source, result, landscape
entry, or conjecture does not inherit a six-corpus sweep, and nothing is blocked
on one. Requiring it per row would make a second catalogued source impossible to
add, which is a good reason not to require it.

**`novelty-check`** attaches to a **claim**, not to a row. It is required
whenever the repository asserts that no formalization or no proof of something
exists — in a conjecture's `prior_art`, in a task calling a target greenfield, in
a note saying a result is unformalized. The claim records what was searched, at
which revision, on what date, and what the search did not cover. One corpus is a
legitimate novelty check if the claim is about that corpus; six are needed only
if the claim is that broad.

**Write the record, not the prose.** The obligation is not paperwork over a
conclusion already reached — producing the record is what tests the claim. A
prose absence claim is reached by whatever the author happened to look at; a
`novelty-check` forces naming a corpus and a revision and then grepping it, and
that step routinely disagrees with the prose.

The worked case is `NC-005`. The embedded self-knowledge sweep concluded in prose
that no usable *categorical* Lawvere formalization existed. Writing the record
required naming corpora, and grepping the pinned AFP release produced
`Category_Set`'s `Lawveres_fixed_point_theorem` immediately — licensed,
maintained, at the same release the atlas already pins for two other entries. The
prose claim had been reached by web search rather than by searching a corpus, and
it was wrong. What survived was a *narrower* true claim: over ETCS rather than an
arbitrary cartesian closed category, and in Isabelle rather than Lean. See
[the sweep](../provenance/embedded-self-knowledge-landscape.md#lawvere--already-in-the-dependency-tree).

So: no absence claim ships on prose. Not because a reviewer demands the artifact,
but because writing it is the only part of the process that can tell you the
claim is false.

A claim of absence is the one claim a reader cannot check for themselves, which
is why it carries its own evidence. The usual failure is to assert that
something is unformalized when the search would have found a published result;
a recorded `novelty_checks` entry makes that failure visible before the claim
ships rather than after.

Both profiles live in
[`formalization-search.json`](../provenance/formalization-search.json) and are
validated: the file declares its profile, states both obligations, and every
`novelty_checks` entry must name a corpus with a pinned revision on record.

The baseline sweep itself: every survey row receives a case-insensitive,
Unicode-normalized token and phrase search across pinned snapshots of
**six classical corpora**: Mathlib,
Isabelle AFP, the Rocq Library of Undecidability, HOL4, HOL Light, and the Agda
standard library. This is a **baseline classical corpus pass**, not a complete
search of all formalizations: third-party Lean packages (for example
FormalizedFormalLogic/Foundation, KolmogorovMathlib, SocialChoiceLean, DASH)
are outside those trees and must be recorded via `candidate_formalizations` or
`registry.yaml` when discovered manually. The query terms, corpus versions,
per-query file counts, and representative candidate paths are retained in
[`formalization-search.json`](../provenance/formalization-search.json).

A candidate path is not a verified formalization. It must be compared at the
statement level and, where practical, built in its native prover before being
added to a registry `formalizations` list. Conversely, zero phrase hits are only
scoped negative search evidence for the six corpora; they do not prove that no
formalization exists anywhere. The evidence is rebuilt with
`scripts/update_formalization_search.py`; the registry validator rejects drift
between its queries, candidate corpora, and the generated evidence.

## Progress and bridge status

Whether a row has Lean behind it is read from the row, not stored beside it: a
`lean_artifact` is present or it is not. There was a `progress_status` field
duplicating that fact, and a validator asserting the two agreed — a stored copy
of something already computable is a second thing to keep in sync for no gain.

`ai_interpretation_status` is separate and has a defined lifecycle vocabulary:
`HUMAN_REVIEW`, `STATEMENT_REVIEWED`, and `REVIEWED`. `HUMAN_REVIEW` (the
default) means no theorem connecting the mathematics to an AI-system claim has
passed semantic review. `STATEMENT_REVIEWED` means a maintainer has reviewed and
accepted the encoded mathematical statement of the bridge, but not its
AI-system interpretation. `REVIEWED` means both the mathematical statement and
the AI-system interpretation have passed maintainer review. It is not a general
progress state. Any status other than `HUMAN_REVIEW` requires a `interpretation_review`
record (`reviewer`, `date`, `statement_reviewed`, `interpretation_reviewed`,
`evidence`); a `HUMAN_REVIEW` row must carry none. The v0.1 release shipped all
rows at `HUMAN_REVIEW`, and that historical snapshot is asserted only by the
immutable release audit (`scripts/audit_release_v0_1.py` via
[`v0.1.md`](../releases/v0.1.md)), not by ordinary current-state validation, so a genuine
future graduation can be recorded without editing a timeless validator.

A declaration stated over an AI-system model may also carry an `application` line.
That line is a proposed reading for discovery and contributor discussion; it is
not evidence that the theorem applies to a deployed or real-world system. The
generated [`applications.md`](../status/applications.md) view makes these lines
findable and displays the separate bridge status. Only a `REVIEWED` bridge, with
its review record and evidence, supports a reviewed AI-system interpretation.

A result may also carry `candidate_formalizations`: structured, non-coverage
leads for a formalization that has been discovered but not yet accepted. Each
lead records `repository`, `revision`, `framework`, `license`, `declaration`,
`inspection_state` (`UNVERIFIED`/`SOURCE_INSPECTED`/`REPRODUCED`),
`relationship_review` (`PENDING`/`EXACT`/`EQUIVALENT`/`RELATED`/`DISTINCT`/
`UNCLEAR`), and `notes`. A candidate lead never substitutes for a
`formalizations` record and never changes headline coverage; promotion still
requires reproduction and statement-level classification. Its `declaration`
field is intentionally free-form lead prose: it may name several files or
theorems while the source is still being inspected. The one-identifier-per-list-
entry rule below applies only after promotion to a `formalizations` record or
to `lean_artifact.declarations[*].source_declarations`.

Each entry in `lean_artifact.declarations` classifies one atlas declaration as
`REFERENCE`, `WRAPPER`, `NEW_PROOF`, or `BRIDGE` and records its source
declaration(s) when it adapts or exposes an upstream result. An atlas-authored
`NEW_PROOF` may intentionally have an empty source-declaration list; wrappers,
references, and bridges must name what they expose or extend. Classification is
per declaration because one survey result may
expose both a thin wrapper and a nonredundant representation bridge.

For a formalization record, `module` names the module or file in the repository
identified by that record's `repository`; `modules` is the list form for a
multi-file development. When an external Lean development is
adapted into the atlas, `atlas_module` separately names the local atlas facade
that exposes the recorded declaration. This prevents an atlas path from being
published as if it existed in an upstream repository; the validator checks both
the external provenance spelling and the local atlas module. Use `declaration`
for one declaration name and `declarations` for several; each list entry is one
identifier, with no packing punctuation or whitespace. The same one-name-per-
entry rule applies to `lean_artifact.declarations[*].source_declarations`.

Current status tables and registry declaration-presence checks are generated by
`scripts/generate_registry_views.py`. The separate hand-written public-API
examples protect statement shapes that cannot be inferred from registry names.

## Theorem layers

1. Existing mathematical theorem.
2. Atlas-facing Lean interface.
3. AI-safety bridge theorem.
4. Claim about an AI system or safety architecture.

Layers 3 and 4 require semantic review. A proof at layer 1 does not silently
inherit an AI-safety interpretation.

### Which declarations need bridge review?

| Declaration type | Bridge review (`ai_interpretation_status`)? |
|---|---|
| `WRAPPER` / `REFERENCE` of classical math | **No** by default — classical content is not an AI-system claim. Row may still carry `HUMAN_REVIEW` until any BRIDGE on that row is reviewed. |
| `BRIDGE` with AI-facing vocabulary (agents, verifiers, safety specs, robots, …) | **Yes** before treating the row as `STATEMENT_REVIEWED` or `REVIEWED`. |
| `NEW_PROOF` of classical math only | Usually no AI bridge review unless an AI-system reading is asserted. |
| Landscape entries | Not survey `ai_interpretation_status`; document scope in landscape notes / literature map. |

**Row-level status:** `ai_interpretation_status` is per survey result. When a row mixes
wrappers and bridges, a `REVIEWED` status documents the **AI-facing bridge(s)**
named in `interpretation_review.evidence`, not a re-review of every upstream classical
proof. State that clearly in the evidence file and release notes (see v0.2).

## New proofs and bridges

Before `NEW_PROOF` or `BRIDGE` work, add a statement-intent note beside the Lean
file. The note states objects and domains, assumptions, quantifier order,
intended conclusion, and differences from the source or informal claim.

Released Lean modules must build without `sorry`, `admit`, axioms, direct
`sorryAx`, or proof-producing shortcuts that extend the trusted base such as
`native_decide` and `@[implemented_by]`. The current-state validator masks
comments and strings, self-tests these cases, and enforces this strict-trust
policy over every atlas Lean source. Novelty, priority, first-formalization,
real-system implications, and exact capture of informal claims are never
asserted without human review.

## What validators prove (and do not)

CI and the ordinary validator suite prove a **bounded** perimeter. Passing
validation means:

- registry schema, licenses, URL syntax, and reproduction *fields* are present;
- generated views (`formalization-status`, atlas index, landscape index, README
  scope, `Registry.lean`, STATE snapshot) match source data;
- every atlas Lean module is built (root import or explicit target manifest);
- banned tokens (`sorry`, `admit`, project-local `axiom`, `sorryAx`,
  `native_decide`, `implemented_by`) are absent from atlas sources after
  comment/string masking;
- named atlas declarations in the registry elaborate (`#check` via
  `Registry.lean`);
- every public theorem and lemma in the facade closure, **and** every public
  theorem, lemma and definition in the off-root build targets and their import
  closure -- which is where the conjecture layer lives -- is kernel axiom-clean
  up to the three standard classical axioms (`scripts/check_print_axioms.py` /
  `#print axioms`). The same script asserts that no `.lean` under
  `AISafetyAtlas/` sits outside that set, so the scope is a checked property
  rather than a description that can drift.

Validators do **not** prove:

1. that a relationship label (`EXACT` / `EQUIVALENT` / `RELATED`) is
   semantically correct relative to the survey informal claim — that is human
   statement review;
2. that a well-typed theorem matches the intended informal or paper statement
   beyond elaborating under the given name;
3. that `source_declarations` (including Isabelle or external Lean names)
   exist outside the atlas build;
4. that `reproduced: true` commands were executed in this CI run (Isabelle and
   external Lean reproduces are offline / Docker scripts);
5. that Lake dependencies (Mathlib, Foundation) are free of project-external
   axioms beyond what `#print axioms` reports for the atlas wrapper theorems.

"Validators pass" therefore never means "coverage labels and AI-safety
interpretations are approved." Those remain under `ai_interpretation_status` and human
review.

## Blocking policy

Stop work on one theorem after three materially different failed approaches, a
plausible counterexample, an unresolved statement choice, or 20% of an
autonomous work batch. Record the blocker and pivot to reusable work.