What the words mean: the three pots, W, and the states a checkpoint 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, or a signature by the key holders · a move from a visited step opens a branch
what the machine refuses now
The scene KERI, the Cardano UTxO, the readers and payees · every step plays on it; click an actor to act as them
The theorems · T1–T16 of CheckpointGoals.lean: one checker row per theorem, folded into fourteen lamps (T11 and T13 were never stated) · a lamp lights when this step shows one of its theorems; every row is checked on every step · click to read
Evidence by hand the Env: what the validator would verify over the bytes, decided by you
The checkpoint in numbers the datum, the three sums, the treasury's verdict and its conjuncts
Value over the play conviction bond D freeze bond B pool · arrows are flows · the current branch
Who holds what lovelace, by component; every payment named by the flow
What this is and is not
A transcription of lean/CardanoKeri/Checkpoint.lean: the states, the actions (exactly the redeemers), the evidence as a table of decisions, value as three components that never mix, the consumer's state-side check. The theorems of CheckpointGoals.lean run as properties on every step. Each story is a tree: the trunk and the branches the story implies; ‹ and › walk it as an editor walks its history; click any node of the tree to jump there.
Not here: cryptography (keys are an epoch counter; evidence is a row you decide), validity (D-027, reserved), the consumer's own threshold check, UTxO mechanics, delegation, record trees, hunter bounties. A Lean Nat is unbounded; this page represents it exactly up to 2^53 − 1 and refuses anything else by name.