FABRIC.md §3: declare the closed two-valued cell union

Review item REVIEW-A3.

§23.1 dissolved the payload threshold by making large patrons heavy -- a
1024-byte block is 17 cells, one header and sixteen of payload. Those sixteen
carry no identity, heat, TTL or code field, so they are a second cell shape,
which §3's opening line ("One structure. No variants") forbade without saying
so. An implementer reading §3 literally would have built the wrong structure.

Declared: a cell is either a patron header or a continuation cell owned by
exactly one patron. The union is closed, two-valued, and fixed at build time.

This introduces no new principle -- it is the same discipline §18.3 applies to
behaviours, and a two-valued union is the smallest instance of a closed
enumeration. It is not a type field: the distinction is structural, tells the
engine only whether a cell begins or continues a patron, and is exhausted by
that. Continuation cells are never ranked, reaped or dispatched; they are floor
space accounted for in their owner's mass.

§13's "one datatype" bullet amended -- the datatype is a two-constructor sum
rather than a bare record, costing one case split.

§23.4 #3 (identity elision) expanded: it is downstream of the
header/continuation encoding, since a scheme reusing the identity field as
discriminator would couple the two decisions.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

FABRIC.md

@@ -100,6 +100,30 @@ One structure. No variants, no type field, no subclassing.
 Fixed-size cells. Links are indices, so the Stadium stays an array — no fragmentation,
 and tractable for Isabelle later.
 
+#### A cell is one of exactly two things
+
+The wire table above describes a **patron header**. §23.1 establishes that a large patron is
+not held by reference but simply occupies more cells — a 1024-byte block is 17 cells, one
+header and sixteen of payload. Those sixteen carry no identity, no heat, no TTL and no code
+field.
+
+That is a second cell shape, and this section's opening line — *"One structure. No variants"*
+— forbade it without saying so. Declared properly:
+
+> **A cell is either a patron header or a continuation cell owned by exactly one patron.
+> The union is closed, two-valued, and fixed at build time.**
+
+This introduces no new principle. It is the same discipline §18.3 applies to behaviours: a
+closed enumeration fixed at build time is as tractable in HOL as a single record, and a
+two-valued union is the smallest possible instance of one. §13's "one datatype" remains true
+in substance — the datatype is now a two-constructor sum rather than a single record, which
+costs a case split and nothing else.
+
+What it is **not** is a type field. The engine does not ask a header what kind of patron it
+is; the two-valued distinction is structural, tells the engine only whether a cell begins a
+patron or continues one, and is exhausted by that. A continuation cell is never ranked,
+never reaped and never dispatched — it is floor space, accounted for in its owner's mass.
+
 > **Amended by §19.2 and §23.1.** `mass` is an eighth wire, added when density was
 > defined — density is heat ÷ mass, so mass has to live in the entry. And the original
 > payload rule ("inline if small, by reference if large") was dissolved rather than
@@ -382,8 +406,10 @@ and is where a verification effort usually dies. Unification deletes it outright
 
 What the design gives Isabelle/HOL, more or less for free:
 
-- **One datatype.** The arena entry is a single record. Everything else is payload. You
+- **One datatype.** The Stadium entry is a single record. Everything else is payload. You
   reason about `entry` once rather than about blocks, messages, VMs and events separately.
+  *(Amended by §3: a cell is a two-constructor sum — patron header or continuation cell —
+  not a bare record. That costs one case split and nothing else; the point stands.)*
 - **No pointers.** Fixed-size cells with index links means the arena models as a total
   function over a finite index set — no heap model, no separation logic, no aliasing, no
   null. This is the single biggest difference between a tractable proof effort and a
@@ -1708,11 +1734,17 @@ Firmness of each figure:
 2. **Cell size validation.** Build the header for real, count the bytes, and check that a
    typical message still fits in one cell with the behaviour tag and flags included.
 3. **Is `identity` needed at all for every patron kind?** For a word it is a name; for a
-   block a content hash; for a message possibly nothing — its identity could be its index.
+   block a handle (§24.4); for a message possibly nothing — its identity could be its index.
    If identity can be elided for some kinds, 8 bytes of a 32-byte header is a large saving.
    This must not become a per-kind branch (§18.3), so it is only worth doing if it can be
    expressed uniformly.
 
+   **Larger than it first appeared.** §3 now declares cells a closed two-valued union —
+   header or continuation. Whatever distinguishes the two occupies header space and
+   interacts directly with any identity elision: a scheme that reuses the identity field as
+   the discriminator, for instance, would couple the two decisions. Settle the
+   header/continuation encoding first; identity elision is downstream of it.
+
 ---
 
 ## 24. Mutation, identity, and mass stability