# Case Generation, Proof & Canon

Every other open-world detective game ships a fixed shelf of hand-authored
cases. V8 (Ariadne) ships a _factory_ — and the one promise that makes a factory
of mysteries playable rather than terrifying is this: **you will never be handed
a case you cannot solve, and never lose one to a clue the game never showed
you.** Fairness in V8 is not a QA hope or a designer's gut feel. It is a
property the system _proves_ with a real constraint solver before the case is
allowed to exist. That is the feature this page is about — the mint, the proof,
and the canon that together keep a generated labyrinth fair, solvable, and
consistent with the city the player already knows. It is the difference between
"the generator usually produces good cases" and "nothing unsolvable, unfair, or
canon-breaking can reach a player," which is exactly what V8's definition of
done demands (`V8_features.md` § "Definition of done").

The mechanism is one sentence: **the LLM proposes; a constraint solver
disposes.** A case has a _symbolic skeleton_ — who did it, with what, and the
clues that distinguish them — that must be provably correct, and an _experienced
surface_ — prose, art, voice, interrogation — that agents realize from that
skeleton. Three subsystems own the skeleton, and they are where the real,
deterministic, CPU-only code concentrates. **Clew** is the generative engine: it
picks the answer _first_ and weaves a self-consistent world backward from it.
**Minos** is the verifier: it proves the player-visible clues admit _exactly
one_ answer and that it is the intended one. **Palimpsest** is the canon graph:
the persistent city every case is grounded in and writes back to, so the world
remembers what the player did. This page is the feature-side view; the deep
internals — the SAT layer, the alibi-sign bug, the exact data contracts — live
in the architecture companion. Hub: [../V8_features.md](../V8_features.md).

## What ships, honestly

The solvability proof is the strongest real thing V8 has, and it is genuinely
real — not a boolean stub renamed "verifier." `libs/v8/case-csp` is a complete
finite-domain constraint solver: backtracking search with node consistency,
minimum-remaining-values ordering, and forward checking (`csp-solver.ts:212`).
Its spec proves the canonical **Zebra (Einstein) puzzle** — exactly one
solution, "the Norwegian drinks water, the Japanese owns the zebra"
(`csp-solver.spec.ts:168`) — so the engine is anchored against a known-correct
result it cannot fake. `libs/v8/case-bundle`'s forge calls that proof **before a
single word of prose or byte of art is generated**, throwing on a non-unique
skeleton (`case-bundle.ts:237`). `libs/v8/case-gates` registers the seven
release gates on the shared `@oshun/content-release-gates` platform every Oshun
product uses, not a bespoke per-product checker (`index.ts:99`). And a _second_,
independent solver — a real DPLL SAT engine in `libs/yemaya/case-verifier`
(`sat/dpll.ts`) — decides the same uniqueness question, so the verdict is
cross-checked, not asserted.

What is a **seam, not a fabrication**: the media a finished case needs
(Stability/Flux portraits, Hunyuan3D/Meshy 3-D props, Suno music, ElevenLabs VO)
arrives through injected `CaseMediaGenerator` boundaries. An absent provider
yields a `not-configured` asset slot — never a fabricated asset
(`case-bundle.ts:262`). The prose writer is _required_: no writer wired means a
loud `CaseBundleNotConfiguredError` (`case-bundle.ts:242`), not invented flavor.
The `clingo` ASP backend is an optional accelerator that falls back to the
in-process DPLL and honestly reports which engine decided. Palimpsest's graph,
hybrid retrieval, per-claim consistency check, and outcome write-back are all
real and tested (`@yemaya/canon-graph`); its embedding signal is feature-hashing
— a documented approximation, not a neural model — and durable Postgres/Neo4j
persistence is the _named deployment target_, not something these libs pretend
to be.

## Clew — a case generated answer-first

### Solve-first, not author-first

A human mystery writer invents a crime and _hopes_ the clues add up. Clew
inverts that. It picks the culprit before anything else and gives them the three
things a culprit must have — means, opportunity, and no verified alibi — while
handing every innocent exactly one fair, discoverable exoneration: a verified
alibi, demonstrable absence, or no access to the weapon. Innocents usually
_keep_ a motive, so they still read as plausible suspects; they are the fair red
herrings, each cleared by a single fact the player can actually find. The
construction runs off a seeded RNG, so the same `(seed, canon)` reproduces the
same case bit-for-bit, and a timeline conflict the true culprit could not have
been present for _throws_ rather than shipping a broken case. (Those two passes
— Truth-Weaver and Clue-Smith — are detailed in the architecture companion; the
feature point here is that the answer is fixed first and the world is built to
fit it, which is what makes a uniqueness proof _possible_ in the first place.)

### The case as a constraint network

Clew's decisive output is not prose — it is a **constraint network**, the exact
object Minos solves. In the `libs/v8` vertical this is a `MysterySkeleton`
(`mystery-skeleton.ts:69`): a set of solution **dimensions**, each with a finite
domain (`culprit: [colonel, duchess, butler, doctor]`, plus `weapon`,
`location`, `motive`); the intended **ground truth**, one value per dimension;
and a list of **clues**, each either `presented` to the player or `withheld`,
each carrying a logical constraint over the dimensions. The constraint
vocabulary is small and honest: `is` / `is-not` pin or eliminate a value,
`one-of` narrows a dimension, `if-then` is a conditional deduction, `same` ties
two dimensions together, and `allowed` is the general escape hatch — an explicit
set of permitted tuples rather than a hidden predicate the data can't see
(`mystery-skeleton.ts:33`). A worked example from the spec interlocks five of
these into one answer: _weapon=poison (the coroner) ⇒ location=conservatory
(poison was stored there) ⇒ culprit=doctor (only the doctor had conservatory
access) ⇒ motive=blackmail_ (`mystery-skeleton.spec.ts:20`).

The load-bearing detail is the `presented` / `withheld` tag on every clue,
because **only the clues the player can reach count toward solvability.** A true
but withheld "confession" is excluded from the proof entirely
(`mystery-skeleton.spec.ts:76`). That single distinction is the whole game: a
case is fair only if it can be solved from what the player is actually shown —
not from facts the system happens to know.

## The solvability proof — why a V8 case is provably fair

This is the strongest real feature in V8, so it earns the most space.

### Three verdicts, one question

Minos's headline obligation is **uniqueness**: with only the player-reachable
clues, is the culprit the _only_ satisfying answer? Exactly three verdicts
matter. Zero satisfying solutions means the case is **unsolvable**
(over-constrained — the visible clues contradict each other). Two or more means
it is **ambiguous** (under-determined — the player could rightly accuse more
than one suspect). Exactly one means **unique** — the answer is _entailed_ by
the visible clues, and that is the only verdict that ships. A boolean "does this
look fair?" check cannot tell these three apart. Counting models can, which is
precisely why V8 spends real solver code here instead of a heuristic.

### A real solver, anchored against the Zebra puzzle

`solveCsp` (`csp-solver.ts:212`) is a textbook-complete backtracking search. It
seeds **node consistency** from the unary constraints (pruning impossible values
up front), then searches with **minimum-remaining-values** ordering — always
branching on the most-constrained variable, breaking early on a singleton
(`selectVar`, `:260`) — and **forward checking**, which after each assignment
prunes from each unassigned neighbour any value a shared constraint would now
definitely violate, recording every removal so it can be undone on backtrack
(`forwardCheck`, `:278`). The soundness hinge is `constraintViolated` (`:120`):
it returns true only when a constraint can _no longer_ be satisfied, leaving
undetermined constraints alone, so the search is both sound and complete. A
degenerate constraint that touches no assigned variable — a 0-ary relation the
incremental checks would never see — is still enforced by a full constraint
sweep at each leaf (`:314`), pinned by a dedicated soundness-guard test
(`csp-solver.spec.ts:68`).

The proof that this is a genuine engine and not a renamed boolean is the **Zebra
puzzle**: the solver returns the canonical answer — Norwegian in the first
house, the Norwegian drinks water, the Japanese owns the zebra — and _exactly
one_ solution (`csp-solver.spec.ts:168`). A solver that produces that specific
answer across fourteen interlocking constraints is doing real search. The same
domain-agnostic engine that solves the Zebra puzzle solves a murder.
`proveUniqueSolution` (`:356`) drives the uniqueness test efficiently: it asks
the search for up to _two_ solutions — none ⇒ `unsatisfiable`, one ⇒ `unique`
(with the witness assignment), two ⇒ `under-determined` — stopping the moment a
second model appears, because one counterexample is all uniqueness needs.

### Solvable _and_ correct: the two-part fairness check

`proveCaseUniqueness` (`mystery-skeleton.ts:239`) is where the fairness
guarantee is actually enforced, and it checks _two_ things, not one. First it
compiles **only the presented clues** into a CSP (`compileMysteryToCsp`, `:136`)
— the model the player can solve from — and demands a unique solution. Second,
it demands that the unique solution **equals the intended ground truth.** A case
is rejected if it is under-determined, if it is unsatisfiable, _or_ if the
visible clues prove a perfectly unique culprit who simply is not the one Clew
intended — a real generation bug the prover surfaces with a one-line, honest
`reason` (`:251`) rather than asserting away.

The spec pins every one of these failure modes. A case whose visible clues prove
the doctor while the author's ground truth says "butler" is caught:
`uniqueSolutionProven` is false, and `groundTruthSatisfiesAllClues`
(`mystery-skeleton.ts:180`) confirms the shipped clues contradict the shipped
answer (`mystery-skeleton.spec.ts:154`). And the most important one for
fairness: moving the two deducing clues from `presented` to `withheld` flips a
uniquely-solvable case to **under-determined for the player**, even though the
_full_ clue set still solves uniquely — proving the case isn't broken, it's just
unfair as presented (`mystery-skeleton.spec.ts:178`). This is the whole reason
the compiler defaults to presented-only: solvability is judged from what the
player can actually reach.

### Two solvers, one verdict

The CSP is not alone. The architecture names a second, independent route: a
propositional **DPLL SAT solver** (`libs/yemaya/case-verifier/sat/dpll.ts`) —
the real 1962 algorithm with unit propagation and pure-literal elimination
(`solveFrom`, `:98`) — that treats the case as a Boolean CNF over
`(suspect, attribute)` atoms and tests each suspect by assumption: suspect `s`
is a viable culprit iff `CNF ∧ culpritIs(s)` is satisfiable (`isSat`, `:129`;
`proveUniqueness`, `uniqueness.ts:47`). Count the survivors — 0 unsolvable, 1
unique, ≥2 ambiguous — and return every offender for the repair loop. Two
engines reducing the same question to model-counting is itself a cross-check,
and it earned its keep: this DPLL layer caught a real alibi-rule _sign_ error
during development that a boolean "looks fair" stub would have sailed straight
past (the mechanism is dissected in the companion). The `verifyCase`
orchestrator (`minos.ts:25`) runs this G1 uniqueness proof alongside
deductive-completeness and the existing Knox/Van-Dine fair-play checker; the
`clingo` ASP sidecar can offload the proof to a container and falls back to the
in-process DPLL when no binary is present, reporting `backend: 'dpll'` honestly
rather than fabricating a verdict.

### Prove first, generate never-if-unsolvable

The discipline becomes _executable_ in the forge. `forgeCaseBundle`
(`case-bundle.ts:236`) calls `proveCaseUniqueness` as its very first act and
throws `CaseNotSolvableError` on a non-unique skeleton **before any prose or
media is generated** (`:237`). The spec proves a watchful prose writer is never
even invoked for an unsolvable case (`case-bundle.spec.ts:169`), which means
fairness discipline and cost discipline are the _same_ act: you never pay to
generate art for a case that can't be solved. Only a proven case proceeds to
realization, and each produced asset is then C2PA-stamped — its bytes hashed and
a canonical manifest Ed25519-signed (`stampAsset`, `:184`) — so that
`verifyCaseAssetManifest` (`:215`) flips to false if any signed field is later
tampered (`case-bundle.spec.ts:147`).

### The seven gates

Solvability gates _generation_; a wider suite gates _release_.
`buildV8CaseGates` (`case-gates/src/index.ts:99`) registers seven gates — **G1**
fair-play, **G2** solvability, **G3** clue-grounding, **G4** suspect voice,
**G5** misdirection, **G6** prose, **G7** safety — on the shared
`@oshun/content-release-gates` service, composed from the platform's gate
builders rather than forked. The crucial wiring is that **G2 consumes the very
`uniqueSolutionProven` flag the CSP produced** (`index.ts:124`), so the symbolic
proof is literally what the release gate stands on. The suite is real: its spec
asserts each distinct fault blocks its own gate — solving on a withheld clue
trips G1, a non-unique case trips G2, a solution citing an invented clue trips
G3, and a maze of too many red herrings trips G5 (`case-gates.spec.ts:30`). A
case clears only when all seven required gates pass (`evaluateV8Case`, `:183`).

## Canon consistency — cases that fit the world and remember

### Grounded in a persistent city

A generated case is not a disconnected vignette. Palimpsest
(`@yemaya/canon-graph`) is the persistent world every case is grounded in — a
typed property graph of characters, locations, factions, timeline events,
prior-case outcomes, and open threads. Generation never sees the whole graph; a
bounded `CanonContext` is retrieved per case (`retrieval.ts`), ranked by a
genuine hybrid of lexical tf-idf and a feature-hashing embedding cosine, with
the required cast and locations force-included so a hard continuity constraint
is never pruned by the top-K cut. Prior-case outcomes are first-class
retrievable nodes carrying their current dynamic state, so a new case reuses the
city's _actual_ history rather than re-inventing it.

### The continuity gate, and a world that remembers

Two real mechanisms turn canon-consistency from a wish into a feature. First,
the **consistency check** (`consistency.ts`) is real per-claim contradiction
logic judged against the exact canon snapshot a draft was grounded on:
re-parenting a known location, negating a recorded character fact, or flipping a
recorded case outcome is a HARD violation, while a plausible _new_ fact is SOFT
and surfaced for review rather than silently rejected. Second, **write-back**
(`writeback.ts`) makes a played case durable world history — convicted suspects
become `convicted`, and the signature continuity move is the wrongly-accused
suspect, whose state becomes `freed-vengeful` and who opens a vengeance thread
the director can weave into a future case. Accuse the wrong man in case #7 and
he can resurface — freed and vengeful — in case #19. Every commit materializes a
content-hashed snapshot (`snapshot.ts`): a SHA-256 over a canonicalized
serialization that flips on _any_ node, edge, or state change, which together
with the seed and model versions forms the `(seed, model-versions, canon-hash)`
key that makes a generated case deterministically replayable. (Palimpsest's
retrieval ranking, the full consistency taxonomy, and the snapshot
canonicalization are detailed in the companion; the feature point is that the
world has a memory the player can feel.)

## The mint, end to end

The fairness guarantee is a pipeline, not a single check — generate, _prove_,
gate, ship, and write back, with the proof standing between generation and any
spend on realization.

```mermaid
flowchart TD
  REQ["Player request / daily drop<br/>(era, tone, difficulty, seed)"] --> PAL[("Palimpsest canon graph<br/>retrieve bounded CanonContext")]
  PAL --> CLEW["Clew: pick the culprit FIRST,<br/>weave the world backward → MysterySkeleton"]
  CLEW --> PROVE{"Minos: proveCaseUniqueness<br/>PRESENTED clues only"}
  PROVE -->|"CSP solveCsp + DPLL cross-check"| VERDICT{"unique AND<br/>matches ground truth?"}
  VERDICT -- "no: unsolvable / ambiguous / wrong" --> REJECT["CaseNotSolvableError<br/>regenerate — NO art generated"]
  REJECT --> CLEW
  VERDICT -- yes --> FORGE["forgeCaseBundle:<br/>prose + media, C2PA-stamped"]
  FORGE --> GATES["G1–G7 release gates<br/>(G2 = uniqueSolutionProven)"]
  GATES -->|blocked| REJECT
  GATES -->|cleared| SHIP["Fair, solvable, voiced case → player"]
  SHIP -.->|commitOutcome write-back| PAL
```

The arrows that make it a _proof_ rather than a hope are the two pointing back
to `REJECT`: an unsolvable skeleton never reaches the forge, and a gate failure
never reaches the player. Everything downstream — the writers' room, the asset
fabric, the living suspects — only ever sees a skeleton Minos has already
certified.

## Related

- [./overview-and-player-promise.md](./overview-and-player-promise.md) — the V8
  product, the endless case board, and the player promise this page makes good
  on.
- [./realization-and-living-suspects.md](./realization-and-living-suspects.md) —
  how the _verified_ skeleton becomes prose, art, voice, and live interrogation:
  the experienced surface built on top of the proven core.
- [../architecture/clew-minos-palimpsest-symbolic-core.md](../architecture/clew-minos-palimpsest-symbolic-core.md)
  — the deep architecture companion: Truth-Weaver / Clue-Smith internals, the
  DPLL/ASP layer, the alibi-rule sign bug, the seven-gate orchestrator, and the
  exact data contracts.
- Hub: [../V8_features.md](../V8_features.md)