Vocabulary Workbench

The Vocabulary Workbench is where the corpus's vocabulary is governed: the claim registry you browse, the merge queue that guards what enters it, and the axioms that bridge the places where two sources do not share words.

It is the authoring counterpart to Corpus Health. Health tells you whether the rules are coherent; the Workbench is where you fix the vocabulary they are written against.

Getting There

Workspace sidebar → Corpus. That lands on Corpus Health; the tab strip at the top switches to Vocabulary Workbench. Four tabs sit under it — Registry, Rules, Merge queue and Axioms.

Explanation surfaces elsewhere in the product link straight to a specific entry — a finding that names a claim links to that claim's row, a finding that names an axiom links to that axiom — and the target arrives ringed so you land on it rather than hunting the list.

The Corpus entry is available to every user, and everything on it is scoped to your active group.

The Registry Tab

Every claim in the registry, with what it means and what depends on it.

Four controls narrow the list: a search box matching on id or gloss, a namespace picker built from the first dotted segment of the ids in the registry, a vetting filter (draft, reviewed, authoritative), and an Ordered only checkbox for finding the claims that carry an order — verdict claims, and the comparable enums that share the flag.

Each row shows:

• The id and current version — clas.portion_level v1. This is the id a rule names, under the @ sigil: @clas.portion_level.
• The gloss — the precise denotation. This is the anti-collision field: it exists so that when someone later proposes a claim that sounds the same, a reviewer can tell whether it is the same.

• The extraction status, in one of three forms — never a blank, because a blank is indistinguishable from an oversight, and never one sentence for two different states:

  Status	The row reads	What it means
  Extracted	"Question: Does the portion state the operating frequency band?"	The claim has a question, so extraction answers it for every document it reads.
  Solved-for	"Solved-for — no extraction question, and never handed to extraction: its value follows from the rules and axioms that determine it."	A deliberate declaration (§12-D5), and what an ordered verdict level like clas.portion_level is.
  Incomplete	"Incomplete — no extraction question, and no rule or axiom determines it, so it can take no value at all and every verdict that reads it is UNKNOWN. Give it a question, or write a rule or axiom that determines it."	A defect. Shown in amber, and reported by verification as undetermined_solved_for_claim (error) once a rule in scope reads the claim.

  The status is derived on every read, never stored: it is the claim's question plus the answer to does anything in the corpus determine this claim? — so writing the rule that determines a claim, or deleting the last one that did, moves it between states with nothing to migrate. A floor or ceiling determines only the claim it targets; every other claim it names it merely tests, which is why reading a claim is not determining it.

• Badges — the claim type, an ordered badge where it applies, the extraction status, the vetting state, and — only when they apply — Silence unsettled and Ahead of verification (below). Only the two states with a consequence are badged; badging the ordinary ones would bury them.

• Ahead of verification, when this claim has moved past what its rules pin — see below. The card carries the sentence as well as the badge, because nothing else on the page moves when a claim drifts.
• Linked rules — "Linked by 3 rule(s): …", or "No rule links this claim." Counted across every version of every rule, because that is what the registry refuses a deletion on: a rule version's claim pins are frozen at the version that wrote them, so a rule edited to stop naming a claim keeps the pin on its superseded version and goes on linking the claim. It is the server's count, and the same one the delete confirmation and the registry's own refusal use. An axiom naming the claim is not counted here — see Deleting a claim. An unreferenced claim in scope is also reported by verification as orphan_claim (info).
• Version history — expands the full version list, each with its gloss, vetting state, and author.

Three ways a claim enters the registry

A claim is a vocabulary commitment shared by every rule that names it, so most claims arrive from the work that needed them rather than being typed up in advance.

• Promoted from a rule in the Ruleset Studio (below) — the path most people use.
• Accepted in the merge queue, where proposals from an LLM, the solver, or a reviewer are reviewed.
• Written directly here: New claim on this tab, or Edit on a row, opens the claim editor — every registry field including the range and the level map. Editing appends a version rather than rewriting one.

Promoting a Local Claim into the Vocabulary

This is how a claim usually enters the registry, and it starts in the rule that needs it rather than here.

A claim declared without the sigil is private to its rule. Two rules that declare the same local name declare two unrelated claims that merely look alike — which is fine until a second rule genuinely needs to state the same fact, and then it is not.

Where: open a ruleset in the Ruleset Studio, select a rule, and open the claim in the claim editor. A claim that is a bare local shows Promote to vocabulary beside its name. A claim that is already a registry claim shows an explanation instead of the button — there is nothing to promote. The button is disabled when the rule's current DSAIL has no declaration for that claim, because there would be nothing to rewrite.

What the modal asks for:

Field	Notes
Namespace and Name	Together they make the id. A registry claim is named @namespace.name, so the id needs at least two dotted segments; anything shorter is blocked with that explanation.
Type	Inferred from the rule's own declare line, not from anything stored. Change it only if the declaration is what is wrong.
Gloss	Required. Another author picks this claim out of the registry by its gloss; without one the entry is unusable to everyone but you.
Canonical question	Required. Every rule that adopts this claim inherits this question, which is what makes the answer the same claim across rules.

The submit button reads Register as draft, and that is deliberate: a claim minted from one rule has been reviewed by nobody, so it starts at vetting draft rather than pretending to authority it has not earned.

Three outcomes, and the modal never picks silently:

Mint — the id is free. The claim is registered, and the rule is rewritten: the declaration and every reference become the @ form. Strings, units, comments, boolean subtypes such as Bool.Tri, and assertion or function names that happen to share the word are all left alone, and multi-instance bindings are preserved.

Link — the id is taken by a claim of the same type and domain. The existing gloss, type, version and vetting are shown, and the offer is Link to this claim. Nothing is registered and the existing definition is untouched; this rule simply starts naming it. This is the merge case, and it is the common one.

Refuse — the id is taken by a claim of a different type, or an enum over a different domain. Both definitions are shown and neither path is offered, because a rule declaring a type the registry disagrees with does not compile against the corpus. Pick a different id, or fix the declaration if the registry is the one that is right.

Two more behaviours worth knowing:

• Other rules using the same local name are named, and left alone. The modal lists them and says so. Each rule is validated and versioned on its own, so rewriting rules you are not looking at would be a change you did not review. Once the claim exists, promoting the same local in one of those rules takes the Link path — which is the merge, done deliberately, one rule at a time.
• A registry read that fails is shown as a warning, not treated as "no collision." "The registry could not be read, so an existing claim with this id cannot be ruled out." Minting against an unread registry is the one thing that could quietly create a duplicate.

The Merge Queue Tab

The queue holds proposed claims awaiting vocabulary review. Proposals arrive from three places, and each candidate records which:

Proposed by	Typical source
llm	An extraction pass over a policy document that found a concept the registry does not carry
solver	A conflict whose resolution is "these two rules were talking about subtly different things" — the missing distinguishing concept, queued from the finding itself
human	A reviewer who noticed a gap

The Add distinguishing claim action on a Corpus Health finding is the solver path: it queues a candidate here, prefilled with the claims the conflict's witness turned on, and defers the finding pending this review.

Two routes fill the queue from the workbench itself. Propose a claim for review, above the queue, takes a dotted claim id, a gloss and an optional extraction question, and queues a human proposal directly — nothing is registered, it only enters the queue for a decision. The question is worth writing there: a decision registers the claim from the proposal, so a proposal with no question becomes a claim with none, and the registry shows that claim as incomplete — able to take no value at all — until a rule or axiom determines it. And writing a rule or axiom whose source names an identifier the registry does not carry — @new.namespace.claim in the rule or axiom editor — mints it as a draft claim and queues it here, so vocabulary invented while authoring is reviewed rather than absorbed silently. The minted claim is a boolean carrying a provisional question, phrased from its own name and labelled as provisional, plus a gloss naming the rule or axiom that referred to it: a review task, not a finished claim, and never a stub that reads as deliberately solved-for.

Each candidate card shows the proposed name and gloss, and beside it the nearest existing claims the corpus found, best first. They are chosen by comparing claim ids, so a one-character typo finds the claim it was a typo of — and by the same matcher, with the same cutoff, that the save receipt uses when it reports a mint. That is what stops the card and the receipt naming different claims about the same proposal. Each cell carries that claim's own gloss, with the words that differ from the proposal's highlighted, and its type — a near match of the wrong type is a signal about the proposal rather than a candidate to merge into, and the merge control below cannot offer it. Fewer than three matches is normal and none is normal: this is a cutoff, not a ranking of the registry. The proposal's own name is never among them — a mint puts it in the registry before anyone opens the queue, and an axiom relating a claim to itself asserts nothing. That comparison is the whole job: "is this the same claim?" is a judgement about wording, and the fastest way to make it is to read the two glosses side by side.

Three actions. Each requires a rationale, on the same reasoning as a finding's disposition: nothing re-raises a rejected proposal, and a confirmation adds vocabulary every ruleset in the group can name. Every one of the three also states what it wrote when it completes — the claim registered, the axiom minted, that nothing entered the registry, or, when the proposal came from a source that already minted its claim, that the draft claim is still there.

Confirm

The proposal stands as its own concept, so it is registered as a draft claim. The confirmation panel shows the id it will be registered under — editable, because a solver-pinned slot proposes a concept without naming one — and the gloss it will carry, which is the proposal's. Type, wording and extraction question are not decided by "is this the same claim?", so they are left as proposed and the draft rung records that nobody has settled them; finish the claim in the Registry tab. Confirming is refused when the id is not a dotted claim id, or when the registry already holds it — that one is a merge, not a second claim under one name.

Reject

The proposal is not wanted. This records the decision, with the reason, behind a confirmation that says what rejecting costs — and what it costs depends on how the proposal arrived, because one of the two routes into this queue has already written the claim.

On the propose, extraction and solver routes, nothing was registered, so rejecting writes nothing but itself: the proposal leaves the queue and whatever asked for this vocabulary still has nothing to name the concept with. A rejection is not a deferral — nothing re-raises it — so record why, and the next proposal of the same claim can be judged against this decision.

On the mint-on-reference route — a rule or axiom was saved naming an unregistered @namespace.name, which minted the claim and queued this review — the claim is already in the registry. So rejecting decides the proposal, not the vocabulary: the proposal leaves the queue with your reason against it, the draft claim stays at draft vetting, and the source goes on naming it. Nothing re-raises the proposal, which also means nothing will bring that claim back here for review. The card says so, and names the source that minted it.

Reject and remove the draft claim is the way back out, where there is one. It deletes the claim first and records the rejection after, in that order and for a reason: the deletion is the half the registry can refuse, so a refusal leaves the proposal in the queue with Reject still available, rather than trading a recoverable state for a rejection nothing re-raises over a draft claim nothing will bring back. If the removal is refused, nothing is rejected.

The action is only offered when it can finish; otherwise it is shown disabled with the blocker named, because the source has to stop naming the claim first. The registry refuses to delete a claim while any version of a rule links it — a rule whose vocabulary has been deleted stops compiling — and a superseded rule version keeps its pinned claim links. So correcting the spelling and saving again does not unblock the deletion: the old version's link still stands, and that rule has to be deleted before the claim can be. An axiom naming the claim is a separate case: the registry would not refuse that deletion, which is why the workbench refuses it here instead rather than leaving an axiom naming vocabulary that is gone. Either way the card links to the rule, axiom or claim so the blocker can be dealt with in one step.

Merge

The proposal is the same concept as an existing claim. Choose the claim to merge into and the axiom shape — Alias (equivalence), Refinement, Subsumption, or Disjoint, the four the axiom catalog records — and the drafted DSAIL appears beneath so you can read what will be written. It is a complete statement, assert <name> { … };, under a name derived from the axiom id and made unique against every assertion the corpus already defines — exactly the text that gets minted, because a corpus source is a statement and an expression on its own does not load.

Mint axiom and merge writes both halves in one transaction: the proposal's claim is registered as a draft claim from the proposal's own payload — its gloss, its type, its extraction question — and the axiom bridging it to the target is minted. Both, or neither. Both names have to resolve for the bridge to assert anything, and a rule already written against the proposal's name needs the claim to exist before it can compile. The panel says which of the two cases you are in before you act, and the receipt names the claim and the axiom afterwards. When the registry already holds the proposal's name, there is nothing to register and the merge is only the bridge — the receipt says that instead.

Each of the four shapes drafts a different expression, so the one you pick changes what is asserted and not just how it reads. Refinement and Subsumption are the pair to be careful with: they are converses, not synonyms. A refinement says the proposal is the narrower case, so it entails the claim it merges into — Or(Not(proposal), target). A subsumption says the proposal is the broader concept, so the claim it merges into entails it — Or(Not(target), proposal). Over one pair of claims in one order, the two assert opposite implications. Read the drafted line before minting — it is the whole of what gets written.

An axiom bridges two registry claims, so a merge is refused when the proposal's own name is not a dotted claim id: nothing DSAIL can reference is nothing an axiom can name. The proposal's own id is never offered as a merge target, because an axiom relating a claim to itself asserts nothing.

Merge into offers only the claims the chosen shape can actually relate, with a line under it saying how many were left out and why. The list therefore changes when you change the shape, because compatibility is a property of the pair and the shape:

• An alias relates two claims of one type — two booleans, two numerics (integral and real are one numeric domain), or two enums over the same domain. For enums, what counts as the same domain follows how each was declared: an unordered enum ({...}) declares no ordering, so the same labels listed in another order are the same domain and an alias between them is offered; an ordered enum ([...]) declares its order, so two orderings over one label set are two domains, and so are an ordered and an unordered enum over the same labels. The line under the picker says which of the two it is when two identical-looking label lists are still two domains. That ordering is not bookkeeping: it is what lets a rule write >= against the claim at all — see Ordered enums — so an ordered declaration is a statement about the domain and not a spelling of it.
• A refinement, a subsumption and a disjointness relate two booleans. All three compile to propositional connectives over their two sides, so a numeric or an enum cannot take one — two numeric claims are a legitimate alias and never a legitimate refinement.

An enum with no allowed values can be related by nothing at all: the corpus cannot build a domain for it, so no axiom can name it. Give it its allowed values in the claim editor first. A proposal that declares no type is treated as boolean, because that is what the merge will register it as.

A selection made under one shape and left standing under another is not dropped from the control and not silently re-pointed at another claim — it stays visible, unselectable, and the merge is blocked with the type mismatch named. Writing an axiom the reviewer did not choose would be worse than refusing.

What each decision writes

Confirm registers one draft claim and nothing else — no rule reads it until one names it. Merge registers one draft claim and mints one axiom, together or not at all, and queues nothing further. Reject writes nothing at all on the propose, extraction and solver routes. On the mint-on-reference route the claim was registered when the source was saved, so a plain rejection leaves it in the registry and Reject and remove the draft claim is what takes it back out — one draft claim deleted, then the rejection recorded. In every case the decision itself, its reviewer and its rationale are recorded against the candidate, and the workbench states the result at the top of the page rather than leaving an emptied queue as the only evidence.

The Axioms Tab

An axiom is the constraint that says two vocabularies mean the same thing. This tab is where alignment is authored, and it is the one place in the corpus where a single save changes results everywhere.

Axioms are the highest-risk object in the corpus

A wrong or over-broad axiom silently changes conflict detection, validation and marking wherever it applies — and it does so quietly, because the rules it affects were never edited. That is why this editor type-checks as you type, previews the blast radius before you save, and docks a preflight panel beside the source.

It is also why verification halts on an inconsistent axiom set instead of reporting the downstream noise a broken bridge produces.

The editor carries:

• Axiom id — a dotted catalog key, conventionally ax.<what_it_aligns>.
• Summary — the human sentence every explanation surface renders instead of the id. Required.
• Shape — equivalence, subsumption, disjoint, or refines. The shape is governance metadata and a statement about the logic; do not label an implication an equivalence.
• The DSAIL source, in the editor.

• A live type check. Every @namespace.name in the source must resolve to a registered claim. A bare identifier is not flagged — it is a name local to this axiom, which is what the sigil is for. The server re-checks on save; this is the fast copy that keeps the editor honest.

  The check reports "Not in the registry: …" as soon as a name misses, because naming an identifier the registry does not carry can only be a caution. The pass — "Every identifier resolves to a registered claim" — appears only once something has actually parsed the source: until then the panel says "Not checked yet", and if preflight reports the source does not load it says so instead. A green verdict on a draft nothing has looked at is not a weaker pass, it is a claim about a check that never ran.

• An impact preview — how many rules and claims the save pulls into the claim closure, counted from the source in the editor. The rule count is the number that matters: it is how far the axiom reaches. If it is larger than you expected, that is the moment to find out. Like the type check, it is a measurement over a source that loads: an empty editor reaches nothing, an unchecked one has counted nothing, and a source that does not load has no closure — each says which rather than showing zeroes that read like a measurement.

• Preflight — runs the verification checks over the draft and shows, in the docked panel, only what this draft introduces. Pre-existing findings in the same scope are collapsed to a single line linking to the full report rather than mixed in, because an author editing one axiom needs to see the findings their edit caused or the panel becomes noise they learn to dismiss. It re-checks when you click Preflight, when you click the panel's own Check button, and when you leave the editor.
• Save axiom.

The panel's header also carries the vetting ladder — draft → reviewed → authoritative — with the draft's current rung marked, and a gate badge reading Gate not run, Gate clear or Publish blocked. In the axiom editor the badge reads Gate not run: the gate has a verdict only after a publish attempt has been refused, and blockers then appear beneath it. Findings themselves are grouped by severity, errors first, each rendered as prose with the DSAIL and the raw core behind a disclosure.

Below the editor, every existing axiom is listed with its id and version, its summary, its DSAIL source, its shape and its vetting badge.

Authoring an axiom

Take a crosswalk between two vocabularies: one guide talks about "frequencies above 10 GHz"; the canonical vocabulary carries the frequency as a number. They are one fact in two vocabularies.

1. Make sure the source-local claim exists and carries no question. Its value is going to come from the axiom, and asking the document a second, near-identical question would invite the two answers to disagree.

2. Open Corpus → Vocabulary Workbench → Axioms and fill in:

   Field	Value
   Axiom id	ax.alpha_freq_meaning
   Shape	equivalence
   Summary	SCG Alpha's "above 10 GHz" means the operating frequency exceeds 10 GHz.
   DSAIL	assert ax_alpha_freq_meaning { @scg_alpha.freq_above_10ghz == (@sys.operating_frequency > 10.0) };

3. Watch the type check go green, and read the impact preview.

4. Preflight, read the docked panel, then Save axiom. The save re-runs load-time validation at the point the axiom would be stored, and on this tab every fault refuses it: a syntax fault, a type error, an undeclared bare name, and an @namespace.name the registry does not hold. An axiom bridges vocabulary that already exists, so it does not mint the way a rule does — register the claim on the Registry tab first, or fix the spelling. The docked panel names the unresolved claim before you save, so the typo case costs nothing to fix.

Each catalogued axiom carries Delete, behind a confirmation that counts what it reaches. Removing an axiom is the highest-blast-radius edit in the corpus, and the blast runs the opposite way from the one people expect: the axiom is what makes two vocabularies one, so removing it un-bridges them and every entailment that ran through it stops holding — rules that never mention the axiom change meaning without changing a character. Stored verification reports are left as they are and go stale.

The Shape field offers the four the catalog records — equivalence, subsumption, disjoint and refines — and each names a different constraint. Two pairs are worth distinguishing carefully: conflating an equivalence with an implication is how a crosswalk quietly over-constrains a corpus, and conflating the two implications is how it quietly inverts one.

Alias (equivalence) — the two claims denote the same thing, in both directions: a == b. The local claim carries no question of its own; the question is answered once at the canonical claim and the equivalent local claim inherits the value when the corpus solves. An axiom is design-time reasoning: it does not change what a ruleset run asks. Two rules share one question only when they name the very same claim — see One claim, one answer.

Refinement — a is strictly narrower than b: Or(Not(a), b), which is material implication, not equivalence. a keeps its own question.

Subsumption — the converse implication, Or(Not(b), a): a is the broader claim, and b entails it. "a subsumes b" and "b refines a" say the same thing, which is exactly why the two shapes are not interchangeable: over one pair of claims written in one order, refines and subsumption assert opposite implications.

Disjoint — the two claims can never both hold: Not(And(a, b)).

In this editor the shape is governance metadata — it is what a reviewer reads and what Corpus Health prints beside a finding, while the DSAIL you write is what the solver sees. So the two have to agree: do not label an implication an equivalence, and do not label a refinement a subsumption. The source, not the label, is what changes every result. (In the merge queue the shape generates the source, so there the label and the logic cannot disagree — but picking the wrong one still mints the wrong axiom.)

An axiom may also connect a claim to an expression, as the example above does. Cross-source unification leans on that shape constantly, because sources state thresholds in prose while vocabularies carry measurements as numbers.

Rules should reference the claim faithful to their own source

A rule transcribed from a privacy regulation should reference the gdpr.* claim, not the canonical one, and let an axiom do the crosswalk. That keeps every rule a faithful transcription of the document it came from, and concentrates all the interpretive risk in one governed place — the axiom catalog — where it can be reviewed.

Authoring a Claim

Most claims arrive by promotion from a rule. What follows is what to get right whichever way a claim is created, in order of how often it goes wrong.

1. The gloss states the denotation, not the topic. "The message steers the prospect on the basis of who they are" is a gloss. "Steering" is a label, and two people will read it two ways.
2. The question is asked exactly once, here. Rules reference the claim and never restate the question, so every rule that names it inherits the same wording. Two rules asking the same thing in slightly different words is how two answers end up disagreeing.
3. A claim with no question is solved-for only if something determines it. With a rule or axiom behind it, leaving the question empty is a deliberate declaration: never handed to extraction, its value coming from the rules. An ordered verdict claim is the canonical case, as is a source-local claim whose meaning an axiom supplies. With nothing behind it the same empty field is a half-written claim — the registry calls it incomplete, and it can take no value at all.
4. The claim id is what rules name it by, under the @ sigil. The name is the id, and an id is unique within a group, so two claims can never compile to one identifier and there is no second spelling to keep in step. The gloss is what the screens show; it carries no weight in any rule.
5. What silence means, for a boolean claim. What silence means settles whether an unanswered document makes the claim False (the document is the whole subject — a claim about the text) or Unknown (the document is only evidence — a claim about the world). Left undeclared, the judge reads the intent from the question's wording on every call, which is stable only while the wording lands squarely on one side. A question that asks something of the text and something about the world is badged Silence unsettled here, and until it is settled the same document can answer False on one run and Unknown on the next. See what a claim asks.
6. Type and domain. boolean, numeric or enum, plus the domain the claim needs: a minimum and maximum for a numeric, the allowed values for an enum, units where a number has any, and whole-numbers-only where it applies. Ordered applies to two of the three and means something different in each: on a numeric it is what makes the claim markable, and on an enum it declares that the allowed values are listed in order — which is what lets a rule compare it. See the two uses of Ordered.
7. Require provenance on any claim whose value must be traceable to a document reference and span.

The one shape worth spelling out: an ordered verdict claim

Everything about marking depends on this one. It is a numeric claim, restricted to whole numbers, with a declared range, a label for each level, and no question:

clas.portion_level v1 · numeric · ordered · Solved-for · authoritative

The classification level at which this portion must be marked.

Solved-for — no extraction question, and never handed to extraction: its value follows from the rules and axioms that determine it.

Levels: 0 = U, 1 = C, 2 = S, 3 = TS

Supplying level labels is what makes the claim ordered and integral when the slice is built. Give it a range as well, so the levels are bounded and a level outside the scale cannot be solved for. Without labels an ordered claim can still be minimised, but it has no level names — and a mark with no name is not a mark, which is why the Analysis mark chip appears only for a claim that has both.

Add a level gloss for each level as well. It is what the ⓘ serves wherever that level appears, and it is the difference between a scale a reviewer can read and one they have to be told about out of band.

In the claim editor the labels and their glosses are one table: set the type to numeric, tick Ordered and Whole numbers only, give the range, then Fill from range to generate a row per level and write the label and gloss side by side. A level with a gloss but no label is refused — nothing could render it.

The editor keeps the labels and the glosses in one table on purpose. They are two halves of the same statement, and edited apart they drift: a scale acquires a fifth level whose name renders and whose explanation is still the old four. Note the line under the id — it tells you the sigil the claim will answer to, so you know what to type in a rule before you have saved it. Leaving Canonical question empty is what makes an ordered verdict claim solved-for, which is what it must be — and the hint under that field says which state the claim is actually in, because an empty question with no floor or ceiling behind it leaves the claim incomplete rather than solved-for.

The other use of Ordered: a comparable enum

Ordered is offered on an enum as well, and there it does something else entirely. An enum's domain is its allowed values, and ticking Ordered says the list is in order — which is what lets a rule compare the claim instead of only testing it for equality:

risk.tier v1 · enum · ordered · Extracted · draft

The risk tier the portion establishes.

Allowed values: info, warn, error

Set the type to enum, type the allowed values in the order you mean them, and tick Ordered. A rule may then write @risk.tier >= "warn", which the corpus reads as "warn or error" — the labels the declared order puts at or above warn.

Three things follow, and each one is a place authors get it wrong:

• The order is the declaration. info, warn, error and warn, info, error are two different domains over the same three labels, not one domain typed two ways. Re-ordering the list therefore appends a version, and a rule written against the earlier one keeps the version it was pinned to — the registry flags the pin as needing review rather than silently comparing against a new order.
• There is no level table. The Levels table belongs to a numeric scale, where display maps the number 2 to the word S; an enum's values are already their own labels, and the registry refuses a level map on an enum for exactly that reason. So ticking Ordered on an enum asks nothing further of you, and not ticking it costs the rules their comparisons.
• It is not a verdict claim. An ordered enum is a comparable domain, not a scale a rule can push along: floors, ceilings, minimize and maximize all need an ordered numeric claim with a range, and the rule editor's Target claim picker offers those only.

What the rules may then write, and what stays refused, is in Ordered enums.

Versions, and why pins go stale

Registry entries are immutable. Changing a field appends the next version; changing only the vetting state transitions the current version in place. Every reference from a rule or an axiom pins the version it was written against, and nothing resolves "latest" at solve time.

That pinning is what makes staleness detectable rather than silent. A rule linking a claim at @1 while the registry has moved to @2 was written against a different question, so verification reports stale_pin and every answer surfaces it instead of quietly upgrading the rule to a question its author never read. Fixing it is a deliberate act: re-save the rule against the new version, having read what changed.

Verification pins; evaluation does not. That asymmetry is the part worth holding onto, because both halves are deliberate and neither is a defect:

• A corpus rule's claim links are frozen at the rule version that wrote them. That is what makes a verification report a proof about something: it describes exactly the versions it compiled.
• A ruleset rule naming @ns.foo carries no version, so its runs inherit the claim's current question and its current declared reading. That is what lets one edit to a shared claim reach every ruleset that names it, with no stale copies left behind.

So rewording a governed claim changes what runs ask while every verification report goes on correctly reading current — the reports describe the pinned version, and it has not moved. Nothing is stale and nothing is wrong; what would be wrong is neither surface saying so. Two do:

Where	What it says
The claim's card here	Ahead of verification — "a run will ask this version while every verification report describes the older one its rules pin" — with the pinned version and which of the two live-read fields moved.
The report	stale_pin, a warning when a live-read field moved and an info when the newer version changed only documentation.

Both are graded the same way and by one implementation, so the card and the report never disagree. A version newer in nothing but its gloss is not badged at all: a run asks exactly what was checked, so there is nothing to act on, and a badge on it would teach you to ignore the badge that matters.

The remedy for a real drift is a deliberate act, and there is one control for it. Open each rule the drift names in the Rules tab: when any of its pins are behind, the editor says so above the DSAIL source, naming every claim with the version it reads and the version the registry holds, and offers Re-pin claims to current. That re-resolves the rule's stored source against the registry as it stands now and appends a version recording that you accepted the newer wording — nothing else about the rule changes, and it keeps its ruleset membership. Re-verify afterwards, and the badge and the report's stale_pin both go.

Nothing does this on its own, and the button is the only thing that does it: a rule's claim links are rewritten when its source is re-validated, which happens when the source is edited — so before this control existed, a rule nobody had reason to edit kept its old pins for good and went on contributing a finding to every report and a warning to every mark it took part in.

Deleting a claim

The claim editor carries Delete, behind a confirmation. Because registry entries are immutable and versioned there is no coherent way to remove only the current one: every version goes at once, along with the extracted values recorded against them, and stored verification reports are left untouched and go stale — they describe a slice this claim was part of.

A claim any rule still links is refused, and the dialog says so before you press anything: it names the rules, each one a link to the rule editor, and the delete button is disabled with the count on it rather than offered as an action that can only fail. Deleting the vocabulary a rule reads would break the rule rather than retire the claim: the rule would no longer compile.

A rule links a claim through any of its versions. Editing a rule to stop naming the claim clears the link only when it is the current version that carries it — a superseded version keeps its pins, so a rule that once named the claim has to be deleted, not merely re-saved with the name corrected. That is why the dialog can name a rule whose source, as you read it now, does not mention the claim at all.

The count in the dialog, the count on the registry card and the count in the server's refusal are one number from one place, so no two of them can disagree. An axiom naming the claim is deliberately outside it: the registry does not refuse that deletion, so counting axioms would promise a block that never comes. (The merge queue's Reject and remove refuses on an axiom anyway, and says that it is the workbench refusing rather than the registry — see The Merge Queue.)

Authoring a Rule

Corpus rules are authored on the Rules tab. New rule opens the editor; Edit on any row opens it on that rule and saves as the next version. The DSAIL source sits on the left and the preflight panel is docked beside it, so what a rule introduces is visible before it is saved rather than after.

Role and Target claim are the two fields worth slowing down on, and the editor keeps them consistent: choosing Floor or Ceiling requires a target and offers only ordered numeric claims, because bounding a claim that has no order is meaningless and an ordered enum has no scale to be pushed along — a verdict level is a number on a range; choosing Constraint clears the target. Rulesets can be set only when the rule is created — membership is fixed at authoring time, so a later version of a rule can never quietly change which slice it belongs to.

What a corpus rule carries, and why:

• summary is required, and it is not decoration: it is the sentence every explanation surface renders in place of the id. A finding that reads "contradicts policy.steering_floor@1" is useless; one that reads "contradicts House policy: telling a prospect an area does or does not suit people like them is a Violation" routes itself.
• role is constraint (the default — bounds nothing), floor (raises the target ordered claim when its condition holds), or ceiling (caps it). A floor or ceiling must name its target claim. That annotation is what makes the safe mark computable, and a rule that reads the ordered claim without declaring a role leaves the verdict undetermined — which the conflict scan reports as unknown rather than clean, naming the rules whose missing annotation caused it.
• completion_policy is neutral (the default), pessimistic or optimistic, and governs how unknowns are resolved for this rule.
• authority_source is the citation the rule was transcribed from. Corpus Health prints it beside the rule in every finding, and prints "no authority cited" when it is absent.
• rulesets is the corpus ruleset membership. A bare name means version 1. This is the grouping every Analysis question and every scope profile selects on.
• scope tags restrict where the rule applies. An untagged rule is in scope everywhere. Tag deliberately: a tagged rule disappears from every query that does not supply the tag.
• vetting starts at draft unless you say otherwise. Moving to authoritative runs the publish gate.

The editor also carries Delete on an existing rule, behind a confirmation. Every version goes at once, with its ruleset memberships and pinned claim links. When the rule is the only member of a ruleset, the confirmation says so: a ruleset exists because rules belong to it, so deleting the last one removes the ruleset, and any scope profile still naming it resolves an empty slice. Stored reports are left as they are and go stale.

What load-time validation checks

Every create and update runs the same validation, through the one DSAIL front-end the rest of the platform uses:

1. The DSAIL parses.
2. Every @namespace.name resolves to a registry claim at the pinned version — or, on a surface where minting is available, is minted as an unreviewed draft and queued for review (below). Every bare identifier is declared local; a bare identifier cannot mint, because a name without the sigil is rule-local by definition.
3. The formula type-checks against the claim types.
4. A pin below the registry's current version is recorded as a fault needing review (stale_pin), never silently upgraded.

A failure is rejected with the faults listed, so a broken rule never reaches the registry. Minted claims are written only when validation otherwise succeeds, so a rejected draft leaves no vocabulary behind.

Step 2 is one half of a pair, and the two halves close the gap differently. Entering the registry, an unresolvable @name is minted rather than refused: the claim appears as a draft with a provisional gloss and question naming the rule it came from, and a merge candidate is queued so a reviewer either confirms it or merges it into the claim that already meant that. Leaving the registry, the same broken state is refused outright — DELETE /claims/{id} answers 409 while any rule version still links the claim, naming the rules to fix first. Between the two, a stored rule can never be left naming a claim the registry does not have — which is why Corpus Health has no finding for one.

Minting is deliberately not available everywhere. It is a rule-authoring affordance, and two surfaces switch it off:

• The bridging axiom of a merge decision. Its source is validated with minting disabled, so a mistyped claim there is an unknown_identifier error instead of quietly inventing more vocabulary in the middle of a vocabulary review.
• The Axioms tab. An axiom is a bridge between vocabulary that already exists, so a hand-authored axiom naming a claim the registry does not hold is refused, not minted — and the docked panel says so rather than promising a mint the editor will not perform. Inventing a claim from a bridge is how a crosswalk silently asserts something about a concept nobody has defined.

So the two editors differ on purpose: the Rules tab mints and tells you what it minted, the Axioms tab refuses and tells you what to fix first.

The one asymmetry to expect between layers

A floor on an ordered verdict translates to an ordinary ruleset assertion mechanically: assert that the violating condition does not hold. A ceiling has no analogue at all — capping a verdict presupposes a verdict, and the production evaluation path has none.

That is the reason the corpus exists: a false-positive guard is a statement about the interaction of rules, and only a layer that reasons over rules together can hold one.

Supplementary: registering claims, axioms and rules over the API

Everything above describes the screens. For bulk import, for a migration, or for a pipeline that keeps the corpus in step with a source repository, the same objects are POST-able:

Object	Endpoint
Claim	POST /api/v1/corpus/claims, next version with PATCH /api/v1/corpus/claims/{claim_id}
Axiom	POST /api/v1/corpus/axioms
Corpus rule	POST /api/v1/corpus/rules
Merge candidate decision	POST /api/v1/corpus/merge-candidates/{id}/decide

Field-by-field detail, including the exact JSON for an ordered verdict claim, is in the Corpus API reference.

Vetting, and What It Gates

Claims, axioms and rules each carry a vetting state: draft → reviewed → authoritative.

Moving a rule or an axiom toward authoritative runs the publish gate, which requires a current, clean verification report and a recorded disposition on every warning implicating the object. See The publish gate for the three conditions and how to clear or override them.

None of this checks the rules against the source policy

Verification checks the rules against each other. Nothing in the Workbench or in Corpus Health can tell you that a rule faithfully transcribes the regulation it came from, that a threshold is the right threshold, or that a guide's intent survived the translation into DSAIL. A clean report and an authoritative badge together mean "internally coherent and reviewed by a human" — not "correct".

That is what the authority citation and the human review step are for, and it is why they are required rather than optional.

Related Concepts

• The Corpus — claims, the @ sigil, axioms, ordered verdicts, scopes, slices, and where claim values come from
• Corpus Health — the checks, the dispositions, the coverage tab, and the publish gate
• Analysis — asking the corpus questions about a project's rules and runs
• DSAIL Language — the language claims, axioms and rules are written in, and the editor's registry support
• Corpus API — the full REST surface, including every field above
• SCG Portion Marking Tutorial — building a vocabulary, an axiom and five rules from scratch