# Theorem Binding Registry
P201 turns theorem packages into lookupable runtime metadata. The registry does
not prove the Rust runtime. It records which Lean theorem file is relevant,
which runtime evidence is required, how assumptions map to runtime data, what
checker transcript was captured, and which claims remain out of scope.
## Registry Entries
The default registry contains:
- `tokitai_padic_valuation_skip_sound_mod_pk`
- `tokitai_finite_sheaf_gluing_sound`
- `tokitai_finite_sheaf_incompatible_overlap_blocks_gluing`
Each entry records:
- theorem id and Lean file
- checker command and transcript file
- structured checker status
- assumption mapping
- runtime evidence requirements
- conclusion scope
- non-claims
## Runtime Evidence
The p-adic theorem requires `PadicPlanningResource`, a `valuation_cutoff` proof
object, and a valuation-skip plan step.
The finite-sheaf theorem requires a `cover_glue_check` plan step, the
`cover_local_to_global_glue` rewrite proof, compatibility evidence, and
restriction witnesses. The obstruction theorem requires the same plan/proof
boundary plus obstruction evidence.
## Checker Transcripts
The registry parses the transcript files under `docs/theorems/` and validates
that the transcript theorem file, theorem id, checker command, and status match
the descriptor. Local Lean checks are represented as `checked_locally`; default
offline validation still accepts structural checking when Lean is unavailable.
## Non-Claims
- The registry is metadata and validation plumbing, not a proof assistant.
- It does not formalize the Rust runtime.
- It does not broaden the p-adic or finite-site sheaf theorem scope.
- It does not make theorem checking mandatory for default offline builds.