# Paper README Status Vocabulary

Paper-local theorem ledgers use a controlled status vocabulary. Keep nuance in
the `Remaining assumptions / notes` cell, not in the `Status` cell.

Terminology rule: in this repository, a paper/result that is verified by Lean is
called `formalized`. Do not use `Verified in Lean` as a separate status label;
Lean verification is the mechanism, not a distinct paper-status category.

Allowed public paper-row statuses:

- `formalized`: The listed Lean declaration(s) close the intended paper item.
  The remaining-assumptions cell must be `None` or start with `None;` followed
  only by notes about explicit paper assumptions already encoded as
  `Assumptions.lean` declarations, listed in `status.json`
  `review_surface.assumption_names`, and checked by `assumption_match_llm.json`.
  DAG style: use `dag_result` for theorem/proposition/corollary nodes,
  `dag_lemma` for lemma/support nodes, and `dag_model` for definition/model
  nodes.
- `formalized with caveat`: Lean closes a precise variant of the paper item,
  but the theorem needs something on top of the paper statement, such as an
  additional assumption, restriction, corrected statement, or indispensable
  source mismatch. Do not use this status merely because Lean also refutes a
  broader abstraction outside the paper model; mark the paper theorem
  `formalized` and record the overbroad target as a scope note. DAG style:
  `dag_caveat`.
- `partially formalized`: Substantial definitions, helper lemmas, finite
  analogues, or boundary-dependent variants are formalized, but the full source
  item is not closed. Use this public status for results that remain conditional
  on an explicit extra certificate, bridge theorem, external theorem, or
  hypothesis not yet discharged; name that boundary in the notes rather than
  using `conditional` as a separate public status label. DAG style:
  `dag_partial`, with `dag_conditional` reserved for visual boundary/certificate
  nodes when useful.
- `paper draft`: The source paper itself is still moving. Use this only in the
  private incubator for an active draft whose source inventory, proof targets,
  and Lean wrappers may need to be remapped when a new draft arrives. This is
  not a public completion status. DAG style: use `dag_scaffold` for inventoried
  source regions and `dag_unformalized` for not-yet-started paper results.
- `scaffold`: Names, interfaces, or theorem shells exist, but no substantive
  source proof has been closed. DAG style: `dag_scaffold`.
- `not started`: No meaningful Lean artifact exists yet for the paper item.
  DAG style: `dag_unformalized`.
- `not formalized`: The item is intentionally not represented one-for-one, is
  out of scope, or is superseded by another formalized route. DAG style:
  `dag_unformalized`.

For every status other than `formalized`, the final column should state the
exact caveat, closed sub-result, remaining certificate, or reason for deferral.

The dependency DAG legend should expose this same vocabulary. For a formalized
node, the color additionally records the paper-object type: green for
theorems/results, yellow for lemmas/support, and blue for definitions/models.
For non-fully-closed statuses, the style records the status directly.

The default repository audit enforces this status vocabulary, checks that DAGs
input the shared TikZ preamble, and checks that the template legend mentions all
allowed statuses.