Cells & the four substances

The kernel governs four substances. Each has its own discipline of use — a law about how it may move through time — and the whole kernel is the enforcement of those four laws plus the birth and retirement of the bundles that carry them.

• Value is linear: it moves, it never copies and never vanishes. Per asset, the sum of all balance changes in a turn is exactly zero (Σδ = 0). Linear logic's "no free copy or discard" is, here, a security law: no inflation, no loss.
• Authority is produced under non-forgeability. It genuinely grows — introduction hands a third party a new edge, a sealer/unsealer pair amplifies two facts into access neither names alone, a factory mints fresh authority — but every generative act is itself authorized by connectivity already held, and is receipt-disclosed. Miller's law: only connectivity begets connectivity. Attenuation narrows one edge freely; it is not the law of the whole system, because a system where authority only ever shrinks forbids exactly the patterns that make capabilities useful.
• Evidence is monotone: once known, never unknown. The nullifier and commitment ledgers only grow; a spent note stays spent.
• State is guarded-mutable: it changes only under its cell's program, only by its owner, inside the frame.

The cell

A cell is the four substances gathered behind one identity: an operator, a lifecycle, a nonce, a per-asset balance column, a sorted-Merkle capability list, a program (a predicate over its own transitions), and a slot record. Nothing in the system is ownerless: every object is a cell or lives in one. An asset is an issuer cell's promise — AssetId is the issuer's CellId, and mint/burn are the issuer moving value from and to its own well under its own program.

Registers are the L1; the heap is where apps live

A cell's programmable state is two tiers. The registers are a small, fixed set of named fields — the cell's L1: lifecycle, nonce, the capability root, and a handful of program slots. They are cheap, always present, and committed directly. Above them sits the heap: a single register, heap_root, commits an openable sorted-Poseidon2 Merkle map over (collection, key) → value. An app that needs more than a few slots — an order book, a per-member tally, a content index — keeps its data in the heap, and the cell still carries only one root.

The expressiveness uplift is that a heap key is a first-class subject of the guard algebra. A program can demand heap_get(collection, key) = v or heap_contains(collection, key) as a precondition, exactly as it demands a register relation — so a cell's rules can range over unbounded state without growing the kernel. A heap write is the write verb: it runs under the same caveat-gated frame discipline as any slot write (authority, membership, lifecycle, per-slot caveats), recomputes the root, and touches nothing else. The register and the heap are one object — the cell, the executor, and the circuit all read Heap.root of the same sorted leaf list — so installing the heap added no verb. The kernel did not grow; the addressable state did. (Where the heap binds today: kernel-proven against the deployed circuit::heap_root scheme; the per-turn in-circuit heap_root register rides the rotation relayout — rung 7.)

The eight verbs

The kernel signature is eight verbs. This is not parsimony for its own sake: each verb is the structural rule of one substance's discipline, and minimality is a theorem — drop any verb and the behavior it provides has no other provider (VerbRegistry.each_verb_irreplaceable).

Every kernel verb passes two gates: admission (the epistemic half — does the supplied witness realize the demanded predicate?) and a footprint law (the ontic half — the update respects what its substances are: the linear, produced, monotone, and guarded laws above, unified as one frame-preserving-update shape in the resource algebra of Dregg2/Resource.lean).

The wire surface, classified

The wire vocabulary that turns actually carry is larger than eight — and every one of its 27 live effect tags is classified onto the kernel by a total, compiler-checked cover (VerbRegistry.classify, effect_tag_count): it either is a kernel verb, or it is turn structure (exercising a capability is a use, not a verb; a refusal is an outcome; the nonce is prologue; pipelining is composition), or it is a factory pattern — a cell program built from the surviving verbs (escrows, obligations, queues, bridges, stored capabilities). Adding a wire variant without classifying it is a compile error; that is what "the catalog cannot drift" means. Factories are rung 6.

Grounding

• metatheory/Dregg2/Substrate/VerbRegistry.lean — the reified signature: minimality, each_verb_irreplaceable, classify_total, effect_tag_count, cover_hits_both, factory_builtFrom_are_survivors.
• metatheory/Dregg2/Resource.lean — the substance algebra: the ℕ-sum camera for value, the Auth camera for authority and evidence (ConfinesAuthority), excl_no_dup.
• metatheory/Dregg2/Exec/RecordKernel.lean — the kernel state the verbs act on, and the per-asset conservation keystones (recTransferBal_sum_conserve_moved, recTransferBal_untouched).
• metatheory/Dregg2/Substrate/{Heap,HeapKernel}.lean — the heap as the write verb: the openable sorted map (root_deterministic, root_injective under the named Poseidon2-CR floor) and its kernel face (heapStepGuarded, heapStep_conserves = balance-neutral, heapStep_root_written = the register binds the heap, heapStep_*_frame).
• metatheory/CONSTRUCTIVE-KNOWLEDGE.md §3 — why authority is production, not descent.

Live instance

← 1 · The turn · 3 · Guards →