Singular · the permanent M1 registry
These profiles execute the active M1 model: registration and permanent termination. Historical redeemer encodings remain available as refusal controls.
A leaf is Unknown or Known one of three states. Only insertActive and updateTerminal move it, each with an approval and an active-token delta. Five historical edge encodings are refused.
A journey
Where the key stands
| witness | outstanding | shape |
|---|
Free play — two supported edges and five refused encodings
What the cage refuses
Refusal is the complement of the edge table. Every (primitive, value, before-leaf) triple that is not a row of it is refused, with its own reason.
| edge | on leaf | reason |
|---|
The corpus this page replays
| statement | coverage | applicable | vacuous | held | exercised |
|---|
Naming: permanent retirement
Naming uses the same registry model. Register an unknown name, retire its active token, then observe refusal of the historical terminal-witness encoding. Retirement leaves the terminal key occupied.
| step | edge | verdict | leaf | active | absent | terminal |
|---|
The rest of a name's life
A name is seeded, maintained, recovered and retired. Each row below is a verdict the Lean computed and this page inspects — evidence, not a replay: an acceptance, or a refusal with the reason that caused it.
| what | row | outcome |
|---|