FABRIC.md: sweep terminology to Stadium

Review item REVIEW-C4.

The header claimed §1-15 retained "arena" to stay quotable, but the rule was
not applied consistently -- §15 had been swept, §13 had not. A document with two
names for its central object costs every reader something on every section.

Swept all body text. "arena" now survives in four places only, each deliberate:
the src/starkernel/vm/arena.c file path; the two naming notes, which discuss the
word itself; §12's preserved question list, which the section explicitly retains
as the source several later sections quote; and the block quotes of §12 in §21
and §23.

One deviation from the review's stated rule, which said quoted text keeps the
original word. §17.3 quotes §4 and §17.6 quotes §13 -- both self-quotes within
this document, whose sources were just swept. Left unswept they would cite text
that no longer exists, so a reader following the reference finds different
words. Those two were updated to track their sources. §12's quotes were not,
because §12 itself is deliberately preserved.

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

FABRIC.md

@@ -10,10 +10,11 @@ they happened. **Where the two disagree, the later section wins** — earlier te
 standing, with a pointer, because §19.4 and §19.5 quote it directly and because retracing
 the reasoning matters more than a tidy read.
 
-**On the name.** The thing described here is the **Stadium**. §1–15 call it "the arena",
-which was the working name until it collided with `src/starkernel/vm/arena.c` — the
-PMM-backed VM page allocator, an unrelated structure. Read "arena" as "Stadium" throughout
-the early sections; the word was not swept, to keep the original text quotable.
+**On the name.** The thing described here is the **Stadium**. "The arena" was the working
+name until it collided with `src/starkernel/vm/arena.c` — the PMM-backed VM page allocator,
+an unrelated structure. The document has been swept; "arena" now survives only inside block
+quotes that reproduce an earlier section verbatim, and in §12's preserved question list,
+which several sections quote.
 
 **§25 is the punch list.** It is the authoritative statement of what is done and what is
 not. Read its instructions before doing any work against this document.
@@ -44,7 +45,7 @@ message has.
 
 ---
 
-## 2. The arena
+## 2. The Stadium
 
 A single region of memory, outside any VM, holding everything currently **live**.
 
@@ -76,7 +77,7 @@ A single region of memory, outside any VM, holding everything currently **live**
 
 The critical scoping decision, and the one that keeps this from sprawling:
 
-> **The arena holds what is live. Not everything that exists.**
+> **The Stadium holds what is live. Not everything that exists.**
 
 **DECIDED.**
 
@@ -152,7 +153,7 @@ one car makes that corner of the hall hot. Density generates heat; nobody comput
 Consequences:
 
 - **Ranking is read, not decided.** There is no scheduler because there is no policy.
-  The arena is simply already in heat order when you look at it.
+  The Stadium is simply already in heat order when you look at it.
 - **K constrains the total,** so ordering is forced by conservation rather than by tuned
   parameters. There is nothing to tune wrongly. This is the defensible distinction from
   a scheduler and it belongs in the write-up.
@@ -181,16 +182,16 @@ departure mechanisms, not two: TTL, heat decay, and pin.
 
 ---
 
-## 5. What is *not* in the arena
+## 5. What is *not* in the Stadium
 
 This section exists because forcing everything in is how this design turns into a mess.
 
-- **Storage is beneath the arena.** The show floor is not the warehouse. Artemis is where
+- **Storage is beneath the Stadium.** The show floor is not the warehouse. Artemis is where
   entries live when they are not in play. Blocks migrate onto the floor when hot and back
   out when cold — which is heat-driven block migration, already built. Artemis does not
-  become an arena occupant; it becomes what the arena pages against.
-- **Devices are beside the arena.** The framebuffer is the building's lighting, not an
-  occupant. Console's dirty *events* are arena entries; the pixels are not.
+  become a Stadium occupant; it becomes what the Stadium pages against.
+- **Devices are beside the Stadium.** The framebuffer is the building's lighting, not an
+  occupant. Console's dirty *events* are Stadium entries; the pixels are not.
 
 **DECIDED**, and completed by §17.5, which supplies the third edge this section counted but
 did not list, and sharpens the second:
@@ -211,7 +212,7 @@ the Stadium, not the basement of the Stadium, a third thing.
 
 The engine cannot be a VM service, because VMs live inside the thing it manages.
 
-1. LithosAnanke establishes the arena and starts the engine.
+1. LithosAnanke establishes the Stadium and starts the engine.
 2. Hera becomes the first entry in it.
 3. Hera births everything else, sizing each VM as it goes.
 
@@ -227,7 +228,7 @@ step 2 makes Hera the first patron in it (§20).
 
 ## 7. Hera
 
-Hera's job becomes arena distribution. This is not a new responsibility — allocating a
+Hera's job becomes Stadium distribution. This is not a new responsibility — allocating a
 VM's share *is* birthing it, and lifecycle is already what Hera is for.
 
 ~~**OPEN:**~~ **RESOLVED in §22 — elastic.** Whether a VM's share is a hard bound or an
@@ -293,7 +294,7 @@ are closed:
 | ~~Screen cell~~ | — | — | — | **not a patron** (§17.5) |
 
 Screen cells were the suspect case and the suspicion was correct. A cell never expires — it
-is a fixed grid position always present, so cells-as-entries would leave most of the arena
+is a fixed grid position always present, so cells-as-entries would leave most of the Stadium
 inert and permanently pinned. §17.5 confirms the reading anticipated here: **the patron is
 the dirty event, not the cell.** The grid stays outside, and the event turns out to be a
 message with a different destination rather than a sixth kind.
@@ -410,18 +411,18 @@ What the design gives Isabelle/HOL, more or less for free:
   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
+- **No pointers.** Fixed-size cells with index links means the Stadium 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
   research project.
 - **Finite state.** Bounded capacity means the state space is finite. Induction over the
-  arena is straightforward, and model checking becomes available alongside theorem proving.
+  Stadium is straightforward, and model checking becomes available alongside theorem proving.
 - **One conservation theorem.** *Every engine operation preserves K.* Proved once against
   the engine, it holds for every entry kind — because the engine cannot distinguish them.
   Previously this was four proofs plus their interactions.
-- **A clean model boundary.** Storage below and devices beside the arena means disk I/O and
+- **A clean model boundary.** Storage below and devices beside the Stadium means disk I/O and
   framebuffer writes sit outside the model, at the C primitive boundary already drawn.
-- **A trivial initial state.** Boot order — kernel, then arena, then engine, then Hera —
+- **A trivial initial state.** Boot order — kernel, then Stadium, then engine, then Hera —
   gives a base case that is trivially conserving, with everything else following by
   induction on operations.
 
@@ -487,9 +488,9 @@ fourth — "departure is unconditional" — knew only one mechanism.)*
 ## 16. Substrate findings — 2026-08-03
 
 Naming: the arena is now called the **Stadium**, because `src/starkernel/vm/arena.c`
-already owns "arena" for the PMM-backed VM page allocator — an unrelated concept. §1–15
-still use the old word; see the note in the header. Their *substance* has since been
-reconciled against §16–24, with each superseded claim marked in place.
+already owns "arena" for the PMM-backed VM page allocator — an unrelated concept. The
+document has since been swept to the new name, and §1–15's *substance* reconciled against
+§16–24 with each superseded claim marked in place.
 
 Four findings from reading the tree. The first three change what step one costs. The
 fourth changes what the engine is allowed to be.
@@ -724,7 +725,7 @@ slot came up in the rotation.
 That is a direct contradiction of §4:
 
 > *Ranking is read, not decided. There is no scheduler because there is no policy. The
-> arena is simply already in heat order when you look at it.*
+> Stadium is simply already in heat order when you look at it.*
 
 Round-robin eviction is exactly a policy — an arbitrary one, uninformed by the physics the
 rest of the system runs on.
@@ -906,7 +907,7 @@ two are no longer alternatives.
 
 §13 is unambiguous:
 
-> *No pointers. Fixed-size cells with index links means the arena models as a total
+> *No pointers. Fixed-size cells with index links means the Stadium 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
 > research project.***
@@ -1348,7 +1349,7 @@ built, or to collapse it into a single region and discard the level that works.
 Marked as proposal, not finding: `VMPhysics` currently holds only `execution_heat_q48`,
 `last_active_ns` and `is_live` (`capsule_vm_physics.c:59-63`). There is no share field.
 
-§7 says Hera's job is arena distribution, and that *allocating a VM's share is birthing
+§7 says Hera's job is Stadium distribution, and that *allocating a VM's share is birthing
 it*. If that share is the VM's mass, §19's density definition applies unchanged at the
 outer level, and §7 stops being abstract.
 
@@ -1467,7 +1468,7 @@ With locking removed from the argument, six discriminators remain:
 | Fault containment | a VM cannot corrupt another's Stadium | one bad patron reaches everything |
 | Capacity transfer (§7) | meaningful — VMs have shares to trade | no per-VM share exists to transfer |
 | K semantics | conserved per level; existing fleet K survives unchanged | fleet K needs re-deriving |
-| Verification (§13) | prove the engine once, instantiate at both levels — demonstrates genericity | one arena, marginally simpler |
+| Verification (§13) | prove the engine once, instantiate at both levels — demonstrates genericity | one region, marginally simpler |
 | **If SMP ever happens** | **messages are the only boundary-crossers → no shared memory, still no locks** | **needs real locks, and the no-op stubs become a live correctness hole** |
 
 The last row is the strongest, and it is what Q6 was reaching for. Nested does not avoid
@@ -1517,7 +1518,7 @@ level it was born on.
 a hard bound, or elastic under pressure with transfer arbitrated by Hera?
 
 **Resolved: elastic.** And the layout that makes it cheap is a single global cell pool with
-per-VM quotas, not separate physical arenas.
+per-VM quotas, not separate physical regions.
 
 **DECIDED.**
 
@@ -1565,9 +1566,9 @@ settle that.
 
 | Layout | Elastic cost | Isolation | §13 verification |
 |---|---|---|---|
-| Separate physical arenas | expensive — transferring capacity means moving memory, and arenas fragment against each other | physical | two index spaces |
+| Separate physical regions | expensive — transferring capacity means moving memory, and regions fragment against each other | physical | two index spaces |
 | **One cell pool, per-VM quota** | **trivial — arithmetic on two integers** | logical (disjoint index sets) | **one index space, one total function** |
-| Separate arenas, hard bounds | n/a | physical | two index spaces |
+| Separate regions, hard bounds | n/a | physical | two index spaces |
 
 **Chosen: one global array of cells, one global index space.** Nesting becomes a
 *partition* of that index set rather than separate allocations. A VM's quota is a **count,
@@ -1602,15 +1603,15 @@ is still arithmetic plus a list splice, and still arbitrated at a known point (
 Two reasons this is the right trade:
 
 - **§13 gets simpler rather than harder.** One array, one datatype, one total function over
-  one finite index set. A partition of a finite set is trivial in HOL. Separate arenas
-  would mean two of everything and a cross-arena invariant to maintain.
+  one finite index set. A partition of a finite set is trivial in HOL. Separate regions
+  would mean two of everything and a cross-region invariant to maintain.
 - **§21's reasoning survives intact.** Its argument for nesting was K conserved per level
   with messages as the only boundary-crossers — both preserved. SMP-safety also survives:
   what matters is that VMs never touch each other's cells, and disjoint index sets give
   that provided quota changes are arbitrated by Hera, which §7 already requires.
 
 What is given up is *physical* fault containment — a corrupt index could reach another VM's
-patrons where separate arenas would fault instead. That was one of §21.3's six
+patrons where separate regions would fault instead. That was one of §21.3's six
 discriminators and not the decisive one. It is a real cost, recorded here rather than
 glossed.