The turn

Everything in dregg is one sentence, given algebra:

A turn is the exercise of an attenuable, proof-carrying token over owned state, leaving a verifiable receipt.

Every word in that sentence is load-bearing, so let's take them one at a time.

"…an attenuable, proof-carrying token…"

Authority in dregg is a capability: a token naming a target cell, the rights it licenses, the caveats that narrow it, an expiry, and a revocation epoch. Holding one is not like holding a key that a lock silently accepts — it is holding a piece of constructive knowledge: something you can exhibit a witness for at the point of use. The system never consults a global registry of who-may-do-what; there isn't one. Authority is established by presenting a discharging witness and checking it.

This rests on a deliberate asymmetry: proof-checking is cheap and trusted; proof-search is undecidable and untrusted. The protocol is organized so that every trust decision is a check, never a search. Whoever wants to act carries the burden of producing the witness; whoever guards state only ever verifies.

Attenuable means a holder can always make a strictly weaker token — fewer rights, more caveats, shorter life — and hand that on instead. The narrowing is a theorem about the token algebra, not a convention.

The demand ⊣ supply gate

Each action inside a turn is a matched pair: the target cell demands a predicate (its AuthRequired), and the action supplies a witnessed Authorization. Admissibility is exactly "does the supplied witness realize the demanded predicate?" — the Predicate ⊣ Witness adjunction, evaluated as Verify P w. Alongside the authority demand, the action must satisfy every guard in scope: the cell's own program constraints, the caveats riding the presented token, and any preconditions the turn declares. (Guards are one shared algebra — rung 3.)

The action is also bound: a signature over the canonical message (federation, nonce, action, effects) pins the witness to this exact step, so an authorization cannot be replayed into a context it was not proved for.

"…over owned state…"

All state lives in cells, and every cell has an owner and a frame: it changes only under its own program, only by an authorized actor, and a turn touching one cell leaves every other cell untouched. The frame rule is proven once and pays out four ways — sovereignty (your cell is untouchable), joint turns (disjoint footprints compose), sharding (disjoint frames commute), and offline operation (your frame advances alone and merges soundly). Cells and the four substances they gather are rung 2.

A turn is atomic

A turn is a forest of actions executed as a transaction: every action admits and every effect lands, or the whole turn is rejected and the state is exactly what it was. There is no partial success to reason about. Multi-party turns are the same shape — several cells advance under one commitment, each contributing its own authorization.

"…leaving a verifiable receipt."

A committed turn produces Q — a receipt that commits the entire post-state under one commitment scheme. The receipt is not a log line; it is a judgment: anyone holding the receipt chain can verify that every transition was admissible without re-running anything. Receipts are rung 4; verifying whole histories from receipts alone is rung 5.

Grounding

The executor entry is execFullForestG in metatheory/Dregg2/Exec/FullForestAuth.lean — the credential-and-caveat-gated whole-forest step the node invokes (the dregg_exec_full_forest_auth FFI export). Its gate is two-valued and fail-closed:

• execFullForestG_unauthorized_fails — a forged credential, unauthorized capability, or undischarged caveat on any leg rejects the whole forest.
• execFullForestG_no_amplify — every delegation edge in the forest is non-amplifying.
• execFullForestG_conserves_per_asset — value conservation survives the gate.
• AssuranceCase.running_entry_sound — the three conjoined, stated over the thing that runs, not over an abstract model.

Next: 2 · Cells & the four substances →