docs(spec-0031): fold back what implementation proved the spec got wrong

[stellarfeline]

Three PRs implemented against spec-0031 and each found the spec inaccurate in a way the next reader would have had to re-derive. Corrections sit at the criteria they belong to, not in a changelog nobody reads.

AC2 — two corrections

A branch declaration is not a gate consumer. The criterion listed it. BranchDecl.flags is a pinning declaration — "these flags are SET on this branch" — read by the chronicle and the branch proofs. It is not a condition; purse == 500 has no meaning in it. Worth stating because the two read alike in JSON and only one gates anything. Measured: six consumer classes over 28 declaring sites.

The gate could not be a flattened shared struct, and the reason is a rule. serde rejects flatten in combination with deny_unknown_fields, which all 76 stage structs carry and which is what turns an author's typo into DW0100 instead of silence. The tidy struct would have cost deleting deny_unknown_fields from 25 sites — weakening an existing check to obtain a nicer type, which the debug doctrine forbids. So the fields sit on all 28 sites and a from-the-type test makes "every consumer carries the whole gate" a property rather than a habit. The criterion demands the property; the struct was only ever one way to get it.

AC8 — three corrections

• It never said through which channel the message is stated. The obvious reading — vanilla's death screen via the damage type's message_id — is blocked by spec-0029 §3: vanilla builds that component with no fallback, so a player who declines the resource pack sees a raw death.attack.… key, and DW0185 cannot catch it because the literal in the emission is the key, not the authored string.
• It omitted the completability half entirely — it lived only in the prose. Geometry that kills interacts with reachability; a criterion silent on that leaves the more important half unproven. Now folded in: volume cells are impassable, not merely solid.
• "Kills whatever enters it" is not literally implementable. Engine machinery lives in the world; a volume across a cutscene dolly would erase the camera. Five machinery types are exempt by name — content bodies deliberately are not, which is what makes a posted NPC inside a volume a diagnosable authoring error instead of a silent deletion on tick one.

on_death — why it is shaped as it is, and what is still unproven

Campaign-wide, one bundle, not a field on a checkpoint: where you come back is a checkpoint's property, that you died is true everywhere. Per-checkpoint would be N copies of one fact with N chances to forget one.

The desugar-vs-root rule, which is the reusable part: desugar when the sugar's whole meaning is the general construct; add a root when the bundle hangs off an object with runtime machinery of its own. An ambush is a trigger, so it desugars. A shortcut's unlock is not — its detection is a once-only sentinel poll that in the same function clears the gate region, retires the affordance and kills the wrong-side bodies. Desugaring would have put two independent detectors on one event, the exact defect the death edge exists to avoid.

And the honest part. on_death's compile-time shape is proven; its runtime behaviour is not. A generated PackTest cannot prove the corpse-side positive — it drives a fake player, and a fake player is alive — and none was added because no campaign declares on_death yet, so it would bind to zero campaigns and be a green that means nothing. The spec now carries the resulting obligation explicitly: the first campaign to declare on_death must carry a bot-tier proof of the corpse-side fire. Not optional, not the author's discretion.

What CI proves

Doc-only. check-doc-dupes green; check-reference-versions green. No behaviour changes.