diff --git a/docs/margin-collapse-experiment.md b/docs/margin-collapse-experiment.md
index 87820236..9324da43 100644
--- a/docs/margin-collapse-experiment.md
+++ b/docs/margin-collapse-experiment.md
@@ -1,80 +1,59 @@
 # Margin-collapse experiment
 
 Runs `docs/logic-layer.md` -> "Experiment that settles it": CSS 2.1 8.3.1 margin
-collapsing encoded as Datalog rules, checked against a live three-engine vote and scored
-against seeded rule mutants, to decide whether a logic-programming layer earns its place
-as an oracle for intermediate layout facts. The rules agree with the browsers everywhere
-they have a verdict, and where they disagree with a seeded bug they usually know it one
-level earlier than the geometry diff does — so the answer is adopt, matching the top-level
-verdict in `docs/logic-layer.md`.
+collapsing written as Datalog rules, checked against a live three-engine vote and scored
+against deliberately broken copies of the rules (**mutants**), to decide whether a
+logic-programming layer earns its place as an oracle for intermediate layout facts.
+
+**Result: adopt.** The rules agree with the browsers on every measurement (1195/1195), and
+on a seeded bug they usually know one level earlier than the geometry diff does — in one
+case the geometry vote never notices at all.
+
+```mermaid
+flowchart LR
+  doc["case document"] --> facts["facts.rs<br/>tree shape + style"]
+  facts --> rules["rules.rs<br/>Datalog (ascent)"]
+  rules --> coll["collapsed<br/>(which margins adjoin)"]
+  rules --> off["rel_top / rel_bottom<br/>(offsets)"]
+  off --> vote{"matches the<br/>3-engine vote?"}
+  coll --> fact{"mutant's collapsed<br/>differs?"}
+  vote --> geom["geom-caught"]
+  fact --> fc["fact-caught"]
+```
 
 ## What was built
 
-`crates/logic`, a workspace member that depends on `dom`, `layout` and `harness` and
-compiles independently of any browser:
-
-- `src/facts.rs` — reads a parsed `dom::Document` and the `layout::boxtree::BoxTree`
-  built over it and produces `Facts`, the rules' input relations: tree shape
-  (`parent_of`, `first_child`, `last_child`, `next_sibling`, `no_children`) computed in
-  plain Rust, plus computed-style relations (margins, padding, border widths, height —
-  explicit, auto, or unresolved — `border-box` sizing, and whether a box establishes a
-  new block formatting context). The box tree's root is marked as if it were an
-  `overflow: hidden` box, since it has nothing above it for a margin to escape into.
-- `src/rules.rs` — the rule set itself, an `ascent` Datalog program (`MarginCollapseRules`):
-  8.3.1's four adjoining cases (parent/first-child top margin, parent/last-child bottom
-  margin, sibling top/bottom, and a self-collapsing box's own top and bottom margins),
-  each gated by a `feature_*` relation that a mutant can starve of its one row; the
-  collapsed value of an adjoining group (largest positive margin plus most negative,
-  computed with `ascent`'s `max`/`min`/`sum` aggregators, selectable by a `mutant_mode`
-  relation for the margin-sign mutants); how much of a group's margin actually separates
-  a parent from a child once escaping is accounted for; a running max/min carried through
-  a chain of self-collapsing siblings, checked against live engines, for where each one's
-  own reported position is measured from; and CSS 2.1 10.6.3's auto-height and
-  `border-box`-height rules. `run()` executes the program once per (document, mutant)
-  pair and returns an `Output` exposing `rel_top`/`rel_bottom` (parent-relative block
-  offsets in 1/64px) and `collapsed` (the intermediate fact mutant scoring localizes to).
-- `src/mutants.rs` — `MutantConfig` (which `feature_*` relations are on, and which arm of
-  `combine_margins` is selected) and `Mutant::ALL`, 15 single-rule mutants: each turns off
-  exactly one condition or picks one wrong combine-margins arm, never two at once, so a
-  caught mutant localizes to one spec condition. Nine drop or weaken an adjoining/
-  self-collapsing condition (`BfcBlocksTopOff`, `BfcBlocksBottomOff`, `ParentTopAdjoinOff`,
-  `ParentBottomAdjoinOff`, `SiblingAdjoinOff`, `SelfCollapsingOff`,
-  `SelfCollapsingIgnoresChildren`, `ZeroHeightNotSelfCollapsing`, `BoxSizingIgnored`); six
-  pick a wrong collapsed-value arm (`IgnoreNegativeSign`, `DropNegativeMargins`,
-  `DropPositiveMargins`, `SumInsteadOfMaxPositive`, `SumInsteadOfMinNegative`, `SignFlip`).
-- `src/px64.rs` — a 1/64 CSS pixel fixed-point integer type, so the rules add and compare
-  integers rather than floats; no such type exists elsewhere in the workspace.
-- `src/vote_check.rs` — `evaluate()`, comparing the rules' `rel_top`/`rel_bottom` offsets
-  against a live three-engine vote's trustworthy `OffsetY` measurements, within
-  `harness`'s tolerance; used by both binaries below.
-- `src/smt.rs` (behind the `smt` feature) — Z3-backed backward sampling of 4 of the 9
-  margin-collapsing recipes in `crates/harness/src/cases.rs` (`recipe_collapse_siblings`,
-  `recipe_collapse_negative`, `recipe_collapse_self_collapsing_empty`,
-  `recipe_collapse_bfc_root`) — the ones whose defining relation is a handful of
-  independent sign/range constraints rather than structural nesting.
-- `src/bin/crosscheck.rs` and `src/bin/mutation_score.rs` — the two binaries that produce
-  this doc's numbers (steps 2 and 3 below).
-- `tests/against_cases.rs` — runs the rules over `harness::cases::enumerated()` offline
-  (no browser), independent of the live-vote binaries.
-
-The `smt` feature builds `z3` through its `gh-release` sub-feature, fetching a prebuilt
-binary at build time instead of compiling from source: the `bundled` feature needs
-`cmake`, which is not installed on the machine this experiment ran on and cannot be added
-without root.
+`crates/logic`, which depends on `dom`, `layout` and `harness` and runs without a browser:
+
+- `src/facts.rs` — turns a parsed document and its box tree into `Facts`: tree shape
+  (`parent_of`, `first_child`, `last_child`, `next_sibling`, `no_children`) plus margins,
+  padding, borders, height (explicit, auto or unresolved), `border-box` sizing, and
+  whether a box starts a new block formatting context. The box tree's root is treated as
+  `overflow: hidden`, since there is nothing above it for a margin to escape into.
+- `src/rules.rs` — `MarginCollapseRules`, an `ascent` program: 8.3.1's four adjoining
+  cases, each gated by a `feature_*` relation a mutant can switch off; the collapsed value
+  of a group (largest positive plus most negative, via `max`/`min`/`sum` aggregators); how
+  much margin separates parent and child after escaping; a running max/min through chains
+  of self-collapsing siblings (`chain_pos`/`chain_neg`); and 10.6.3's auto and
+  `border-box` height. `run()` returns `rel_top`/`rel_bottom` (parent-relative offsets in
+  1/64 px) and `collapsed`.
+- `src/mutants.rs` — 15 single-rule mutants, each switching off exactly one condition or
+  picking one wrong arithmetic arm, so a caught mutant points at one spec condition.
+- `src/vote_check.rs` — compares the rules' offsets with the vote's trustworthy `OffsetY`
+  measurements within `harness`'s tolerance.
+- `crates/harness/src/smt.rs` (feature `smt`) — Z3 sampling backward from 4 of the 9
+  margin recipes, the ones defined by independent sign/range constraints.
+- `src/bin/crosscheck.rs`, `src/bin/mutation_score.rs` produce the numbers below;
+  `tests/against_cases.rs` runs the rules offline.
+- The 1/64 px integer type these use now lives in `crates/dom/src/px64.rs`, shared with
+  `layout`.
+
+`z3` is built through its `gh-release` feature (a prebuilt binary), because the `bundled`
+feature needs `cmake`, which this host lacks without root.
 
 ## Agreement with the browsers
 
-`docs/logic-layer.md`'s step 2 says to run the rules over "the existing 235 documents".
-That set — cited elsewhere as the Phase 0 baseline (`docs/infrastructure.md`,
-`docs/platform-economics.md`, `docs/firefox-app-units.md`) — no longer regenerates to the
-same count, since `crates/harness/src/cases.rs`'s recipe list has changed since those
-numbers were recorded. This experiment instead ran the corpus as it stands today: 227
-cases, 27 enumerated (one per recipe, boundary-adjacent pool values) plus 200
-seeded-random (seed `0xC0FFEE`), against a live three-engine (Chromium, Firefox, WebKit)
-vote.
-
-Every category agreed completely, with no case the rules had no verdict for and none
-excluded as an untrustworthy (split-vote) measurement:
+227 cases (27 enumerated plus 200 seeded-random, seed `0xC0FFEE`) against a live vote:
 
 | Category | Agreed/Checked |
 |---|---|
@@ -104,16 +83,13 @@ excluded as an untrustworthy (split-vote) measurement:
 | FixedBox | 107/107 |
 
 Overall: **1195/1195** trustworthy `OffsetY` measurements agreed, 0 with no verdict, 0
-excluded as untrustworthy, 0 dump/rule shape mismatches, 0 cases the vote itself could not
-run for.
+untrustworthy, 0 shape mismatches.
 
 ## Mutant detection
 
-For each of the 15 mutants, two independent checks per case: **fact-caught** — does the
-mutant's `collapsed` relation (which margins adjoin, and to what value) differ from the
-correct rules', for any edge, needing no browser — and **geom-caught** — does the
-mutant's final offset disagree with the same live three-engine vote, for any box. The
-oracle is queried once per case and its dump reused across every mutant.
+Per case, two checks: **fact-caught** — the mutant's `collapsed` relation differs from the
+correct rules' (no browser needed); **geom-caught** — the mutant's final offsets disagree
+with the vote for some box.
 
 ### Enumerated (n=27)
 
@@ -175,105 +151,46 @@ oracle is queried once per case and its dump reused across every mutant.
 | sum-instead-of-min-negative | 0/20 | 0/20 |
 | sign-flip | 20/20 | 20/20 |
 
-Across both the enumerated and seeded-random sets, fact-caught is at or above geom-caught
-for every mutant that either check catches at all, and strictly above it for most:
-`parent-bottom-adjoin-off` is the sharpest case — the geometry vote catches it in 0 of 227
-enumerated-plus-random cases, while the intermediate `collapsed` fact catches it in 1/27
-and 11/200. `bfc-blocks-bottom-off`, `sibling-adjoin-off`, `self-collapsing-off` and
-`self-collapsing-ignores-children` show the same pattern at smaller margins. SMT-sampled
-inputs push two mutants (`drop-positive-margins`, `sign-flip`) to 20/20 on both checks —
-markedly higher than either fixed set's rate for the same mutants (roughly a third) —
-because every sampled sibling-collapse and negative-collapse case has a nonzero adjoining
-margin for those mutants to get wrong, where the fixed pools sometimes land on values the
-mutant happens to still get right.
+Fact-caught is at or above geom-caught for every mutant either check catches, and
+strictly above for most. **`parent-bottom-adjoin-off`** is the sharpest: the geometry vote
+misses it in all 227 cases, the `collapsed` fact catches it in 1/27 and 11/200. SMT
+inputs push `drop-positive-margins` and `sign-flip` to 20/20, against roughly a third on
+the fixed sets, because every sampled case has a nonzero adjoining margin to get wrong.
 
 ## Closing the corpus gaps
 
-An earlier run of this experiment found three mutants scoring 0/0 on every input kind,
-fact and geometry alike — corpus gaps, not rule equivalences, per the case analysis
-below. Three recipes now close them: `recipe_collapse_self_collapsing_zero_height`,
-`recipe_collapse_negative_sum` and `recipe_box_sizing_border_box_with_sibling`.
-
-**`zero-height-not-self-collapsing`** made only `height: auto` boxes eligible for
-self-collapsing, not an explicit `height: 0`, though CSS 2.1 8.3.1 treats them alike. The
-corpus's only self-collapsing recipe (`recipe_collapse_self_collapsing_empty`) gave the
-empty box no `height` declaration at all, leaving it `auto` — no recipe ever gave a
-self-collapsing-eligible box an explicit `height: 0`.
-`recipe_collapse_self_collapsing_zero_height` repeats that recipe's shape with an
-explicit `height: 0` on the empty box instead, and now catches the mutant: 1/27
-enumerated, 4/200 seeded-random, on both checks.
-
-**`box-sizing-ignored`** makes the rules never recognise `border-box` sizing, so
-`border_box_height`'s `border-box` arm is never selected. `collapsed` — the relation
-fact-caught compares — only carries margin-adjoining information; `border-box` sizing
-feeds `border_box_height` alone, which `collapsed` never depends on, so this mutant stays
-`0/0` on the fact check by construction, for any corpus — not a gap. On the geometry
-check it was a corpus gap: the only recipe exercising `border-box` sizing
-(`recipe_box_sizing_border_box`) put the affected box as an only child with nothing after
-it in flow, so its own resolved height never fed into another box's offset — the one
-thing the geometry check can observe. `recipe_box_sizing_border_box_with_sibling` adds an
-in-flow sibling after the same `border-box`-sized box, and now catches the mutant on the
-geometry check: 1/27 enumerated, 2/200 seeded-random (fact-caught stays 0/27, 0/200, as
-expected).
+An earlier run left three mutants at 0 on every check. Three recipes closed them:
 
-**`sum-instead-of-min-negative`** replaces the most-negative margin in a group with the
-sum of every negative margin in it — indistinguishable from the correct rule whenever a
-group has at most one negative margin, since a single value's sum and min are the same
-number. The only recipe drawing from a negative-margin pool (`recipe_collapse_negative`)
-paired exactly one negative margin against one positive one — no recipe ever put two or
-more negative margins in the same adjoining group. This was a corpus gap, confirmed by
-contrast with the sibling mutant `sum-instead-of-max-positive`, which *was* already
-caught (7/22, 42/200 in the earlier corpus):
-`recipe_collapse_self_collapsing_empty`'s adjoining group has several positive margins in
-it (an empty box's own margins plus both neighbours'), giving `sum` and `max` room to
-diverge on the positive side even though no recipe did the equivalent for negatives.
-`recipe_collapse_negative_sum` puts a parent's own margin-top and its first child's
-margin-top — both drawn from the negative pool — in one adjoining group (case 1), and now
-catches the mutant: 1/27 enumerated, 5/200 seeded-random, on both checks.
+- **`zero-height-not-self-collapsing`** (treats `height: 0` differently from `auto`): no
+  recipe gave a self-collapsing box an explicit `height: 0`.
+  `recipe_collapse_self_collapsing_zero_height` does; now 1/27 and 4/200 on both checks.
+- **`box-sizing-ignored`**: `collapsed` never depends on `border-box` sizing, so the fact
+  check cannot catch it by construction. The geometry check could, but the only
+  `border-box` box had nothing after it. `recipe_box_sizing_border_box_with_sibling` adds
+  a sibling; now 1/27 and 2/200 on geometry.
+- **`sum-instead-of-min-negative`** (sums negative margins instead of taking the most
+  negative): identical whenever a group has one negative margin, and no recipe had two.
+  `recipe_collapse_negative_sum` puts a parent's and its first child's negative top
+  margins in one group; now 1/27 and 5/200 on both checks.
 
 ## Verdict
 
-`docs/logic-layer.md`'s decision rule, applied literally: "If the rules catch or localize
-mutants the geometry corpus misses, adopt them for the Phase 1 layout step." They do:
-across the enumerated and seeded-random sets, 8 of the 15 mutants have a fact-caught count
-strictly above their geom-caught count, and `parent-bottom-adjoin-off` is caught at the
-fact level (1/27, 11/200) while the geometry vote misses it entirely (0/27, 0/200) — the
-literal case of a mutant the rules localize and the geometry corpus misses outright. The
-first branch of the decision rule is satisfied, so the experiment's answer is **adopt**,
-consistent with `docs/logic-layer.md` -> "Verdict"'s narrow adoption as an oracle for
-intermediate facts. SMT-sampled inputs also caught two mutants (`drop-positive-margins`,
-`sign-flip`) at a materially higher rate than either fixed input set (20/20 versus roughly
-a third) — evidence for the decision rule's second branch too — but the first branch
-already settles the question.
+`docs/logic-layer.md`'s rule: "If the rules catch or localize mutants the geometry corpus
+misses, adopt them for the Phase 1 layout step." They do: 8 of 15 mutants are fact-caught
+strictly more often than geom-caught, and `parent-bottom-adjoin-off` is caught only by the
+facts. **Adopt**, narrowly, as an oracle for intermediate facts (`docs/logic-layer.md` ->
+"Verdict"). The rules now gate margin-collapse admission in the generation loop
+(`crates/generation/src/margin_runner.rs`).
 
 ## Caveats
 
-- The 235-document baseline cited in `docs/infrastructure.md`, `docs/platform-economics.md`
-  and `docs/firefox-app-units.md` predates changes to `crates/harness/src/cases.rs`'s
-  recipe list and no longer regenerates; every number above is from the corpus as it
-  stands today (227 cases), not a reproduction of that count. The 222-case corpus this
-  experiment first ran against is itself now superseded twice over: by the three recipes
-  "Closing the corpus gaps" adds (225 cases), and by two more recipes closing corpus gaps
-  unrelated to margin collapsing (`recipe_border_width_without_style`,
-  `recipe_display_none_with_child` — `roadmap.md` -> "Phase 1 — Engine bootstrap").
-- SMT-sampled inputs cover 4 of the 9 margin-collapsing recipes — the ones whose defining
-  relation is a small number of independent sign/range constraints. The five left out
-  (`recipe_collapse_parent_first_child`, `recipe_collapse_parent_last_child`,
-  `recipe_collapse_through_chain`, `recipe_collapse_self_collapsing_zero_height`,
-  `recipe_collapse_negative_sum`) are built by structural nesting rather than value
-  choice, which running backwards through Z3 does not suit
-  (`docs/logic-layer.md` -> "Claimed benefit 2").
-- The self-collapsing chain rules (`chain_pos`/`chain_neg` in `src/rules.rs`) are scoped
-  to boxes reached via `next_sibling`; a self-collapsing box that is instead a first child
-  with a later sibling is not covered by the current corpus and is out of this crate's
-  scope.
-- A percentage or `calc()` height leaves a box with no `border_box_height` fact, so
-  neither its own offset nor anything stacked below it in the same parent gets a rules
-  verdict — an honest no-verdict, not a wrong one, and such cases are excluded from the
-  agreement counts above rather than counted as failures.
-- `z3` is built through the `gh-release` feature (a prebuilt binary fetched at build
-  time); the `bundled` feature, which compiles from source, needs `cmake`, not installed
-  on the machine this ran on and not addable without root.
-- Mutation scoring runs the rules once per (document, mutant) pair, so `mutation_score`'s
-  cost scales with corpus size times mutant count; this was not a bottleneck at 227 cases
-  but would need reconsidering at a materially larger corpus.
+- The 235-document Phase 0 baseline no longer regenerates; every number here is from the
+  227-case corpus (which grew from 222 through the three recipes above and two unrelated
+  ones, `recipe_border_width_without_style` and `recipe_display_none_with_child`).
+- SMT sampling covers 4 of 9 margin recipes; the other five are built by nesting, which
+  backward solving does not suit (`docs/logic-layer.md` -> "Claimed benefit 2").
+- The self-collapsing chain rules follow `next_sibling` only; a self-collapsing first
+  child with a later sibling is not covered.
+- A percentage or `calc()` height gives no `border_box_height` fact, so that box and those
+  after it get no verdict — excluded, not counted as failures.
+- Mutation scoring costs corpus size × mutant count; fine at 227 cases.