The registry cardano-keri · the AID registry as an MPFS instance: one leaf per identity — active, dormant, convicted — checkpoints that come and go, requests that never contend, folds anyone may land · Alice, Bob, Hal, Sam, Cora and Mallory

slot 0
0 / 0
What the words mean: the bond, the tip, the two min-ADAs, the phases, and the rooms a leaf moves through

What can happen next the story's continuations, and every move the machine would accept from here · everyone here is anyone with an interest; every move is a public transaction, and the tag says what it must carry: only public KERI data, a duplicity proof, or the keys · a move from a visited step opens a branch

what the machine refuses now
The scene KERI, the registry and its checkpoints, the inbox, the readers and payees · every step plays on it; click an actor to act as them

The theorems · T7 parity with the Lean, then R1–R14 of RegistryGoals.lean (R1d, the absence proof, is a second lamp under R1) · a lamp lights when this step shows it and names the theorem it instantiated; every one is checked on every step · click to read

Evidence by hand the Env: what the plugin and the policy would verify over the bytes, decided by you
Tick what the world holds: an inception that verifies, a witnessed rotation from a key state, a duplicity proof against a key state, the owner's quorum. A row is enabled exactly when the machine can read it.
The registry in numbers the UTxO, the leaves, the checkpoints, the inbox and its phases
Checkpoints
The inbox
Phase 1: a fold may process. Phase 2: only the owner may retract. Phase 3 (or a future timestamp): anyone may reject a posted request. A go-request is dated at the end of time: never phase 2; the cage would reject it but the plugin refuses — only processed.
Value over the play bonds locked in checkpoints held by the inbox paid out (refunds, tips, premiums) · the current branch
Who holds what by component; every payment named by the flow
What this is and is not

A transcription of lean/CardanoKeri/Registry.lean: one registry UTxO holding a leaf per AID (active token, dormant k, convicted), the requests of an inbox that never contend, the permissionless fold at a named generation with the plugin's body, the checkpoints that come and go outside the registry, the reap of a bondless checkpoint into a go-request dated at the end of time. The theorems of RegistryGoals.lean run as properties on every step; every step is looked up in the Lean's own corpus (T7). Each story is a tree: the trunk and the branches where an attempt is refused or the world differs; ‹ and › walk it; click any node of the tree to jump there.

Not here: cryptography (evidence is a row you decide), the rotations that keep a checkpoint live and its bonds beyond one abstract D, the ledger's fee (the samaritan theorems carry it as a parameter), the receipt token that couples a reap to its go-request. A Lean Nat is unbounded; this page represents it exactly up to 2^53 − 1 and refuses anything else by name. Run the self-test.