SCG Portion Marking Tutorial

Two security classification guides govern the same program. SCG Alpha covers an RF system; SCG Bravo covers deployment and operations. They were written by different offices, they use different words for the same things, and in one place they flatly disagree. Your job is to mark the portions of an incoming document.

This tutorial builds that corpus from nothing, in the product. You will write a ruleset, promote its claims into the shared vocabulary, connect one guide's phrasing to a canonical measurement with an axiom, transcribe a floor from each guide, watch the platform find the disagreement between them, add a cross-guide mosaic rule, mark a document, and ask what it would take to downgrade it.

It is small enough to reason about by hand and it exercises every mechanism the corpus has.

Before you start

A Jaxon platform instance with the corpus surface enabled — the Corpus item appears in the workspace sidebar when it is — and an active group you can write to.

Familiarity with DSAIL at the level of the SOX Compliance Tutorial is assumed. The concepts behind this walkthrough are The Corpus, Corpus Health, and Analysis; you can read them first or after.

Every step of this tutorial is done on screen. Claims and corpus rules are authored in the Vocabulary Workbench (Registry and Rules tabs), axioms on its Axioms tab, and the scope profile in Corpus Health. Nothing here needs the API, a script, or a terminal.

---

Step 1: Write the ruleset that reads the document

The corpus reasons over claim values, and values come from a run. So start where the values will come from.

1. Projects → Create Project. Call it SCG Portion Marking.

2. Inside the project, Rulesets → Create Ruleset. This opens a five-step wizard, and only the first three matter here:

   • Details — name the ruleset SCG portion items. This step also carries a Governed by list, which is where a ruleset names the corpus rulesets whose axioms and precedence apply to it. Leave it empty for now; Step 7 comes back to it once those corpus rulesets exist.
   • Type — choose Empty Ruleset. From Policy Documents is the other option, and it distils rules out of a document you upload; here you are writing the rules by hand. Choosing Empty greys out Select Documents and Create Rules & DSAIL, so the step count shrinks from five to three.
   • Models — the defaults are fine for this tutorial. Press Create.

3. The new ruleset opens in the Ruleset Studio. Add a rule with New Rule: the dialog asks only for a Rule Name and a Natural Language Description, and the DSAIL comes afterwards, in the studio itself.

   Name it Portion items — band and location, describe it as "Flags a portion that mentions a frequency band and a deployment location together", and press Create Rule. Then put this in the studio's DSAIL Code box and save:

   declare freq_band_mentioned as boolean;
   declare deploy_location_mentioned as boolean;
   
   assert band_and_location_not_together [pessimistic] {
     Not(And(freq_band_mentioned, deploy_location_mentioned))
   };
   

   The [pessimistic] annotation moves the studio's posture selector — the optimistic / neutral / pessimistic control above the DSAIL box — to pessimistic on its own. You do not set it separately, and the two can never disagree: the annotation in the source is what the rule means.

4. Add a second rule the same way, Portion items — waveform and frequency, described as "Reads whether the portion reveals waveform X, and the operating frequency it states":

   declare item_waveform_x as boolean;
   declare operating_frequency as numeric;
   
   assert waveform_x_absent [pessimistic] {
     Not(item_waveform_x)
   };
   
   assert frequency_at_or_below_10ghz [pessimistic] {
     operating_frequency <= 10.0 "GHz"
   };
   

Every name in both rules is a bare identifier, so every one of them is local to its rule. That is exactly the situation the corpus exists to improve on: four facts about a portion, each of which both guides will want to talk about, currently owned by nobody.

Step 2: Promote the claims into the shared vocabulary

Open the first rule's claim editor. Each local claim shows Promote to vocabulary beside its name.

Promote all four, one at a time. The modal defaults the name from the local; set the namespace and fill in the gloss, the canonical question, and — for the booleans — what a silent portion means:

Local name	Namespace	Gloss	Canonical question	Silence
freq_band_mentioned	sys	The portion states the operating band.	Does the portion state the operating frequency band?	About the text
deploy_location_mentioned	ops	The portion names a deployment site.	Does the portion name a deployment site?	About the text
item_waveform_x	scg_alpha	The portion reveals that this item uses waveform X.	Does the portion reveal that this item uses waveform X?	About the text
waveform_x_exists	sys	The portion reveals that waveform X exists, without attributing it to this item.	Does the portion reveal that waveform X exists?	About the text
operating_frequency	sys	The operating frequency the portion states, in GHz.	What is the operating frequency?	— (numeric)

Declare the reading on every marking boolean

A presence claim is a claim about the text: the portion is the whole subject, so a portion that does not state the band answers False, not Unknown. Leaving that to the wording works when the wording is as plain as these four are — but it is decided again on every extraction call, and a question that later grows a clause about the world starts being decided both ways. Declaring it settles it once, and it is the same field the mark depends on. See Declaring a reading.

Numerics take no reading: a number the portion does not give is Unknown either way, and there is nothing to settle.

Phrase marking claims as presence questions

Every question above asks whether the portion states, names, or reveals something. That phrasing is what lets answers compose upward: asked over a larger span — a document of many passages — a presence question is true exactly when any part makes it true, which is how the mark assembles a mosaic across passages in step 7. A universally-phrased claim ("is every record in the portion encrypted?") does not compose that way; keep that shape out of marking rules, or restate it as presence of the violation ("does the portion contain an unencrypted record?").

If the claim already exists, promotion adopts it instead of forking

On a shared instance this is the common case, not the exception: somebody has usually registered @sys.operating_frequency already. Promotion checks before it writes, and when the id is taken it refuses to mint a second one and shows you the claim that holds the name — its gloss, type, vetting, version and canonical question:

@scg_alpha.item_waveform_x already exists. The portion reveals that this item uses waveform X. boolean · v2 · authoritative · asks: Does the portion reveal that this item uses waveform X? Same type and domain as this rule's local, so this rule can adopt it. Nothing new is registered and the existing definition is not modified — this rule simply starts naming it.

Register as draft is disabled while that panel is up, and Link to this claim is the action you want: the rule is rewritten to the @ form exactly as a fresh promotion would rewrite it, and the registry is left alone. This is the whole point of a registry — two rules that mean the same thing end up naming one claim rather than two that drift apart. If the type or the enum domain disagrees, adoption is not offered at all: linking would leave the rule declaring @ns.name at one type while the registry defines it at another, which does not compile against the corpus. The modal shows you both definitions and asks you to choose a different id.

Each promotion registers the claim at vetting draft and rewrites that rule — its declaration and every reference — to the @ form. After the fourth, the second rule reads:

declare @scg_alpha.item_waveform_x as boolean;
declare @sys.operating_frequency as numeric;

assert waveform_x_absent [pessimistic] {
  Not(@scg_alpha.item_waveform_x)
};

assert frequency_at_or_below_10ghz [pessimistic] {
  @sys.operating_frequency <= 10.0 "GHz"
};

Watch the editor change

Registry claims are coloured differently from rule-local names — in the DSAIL editor and in the Claims panel beneath it — so the shared vocabulary is visible at a glance wherever a claim is named. Start typing @ in a declare and the editor offers the claims you just registered, matched on the gloss as well as the id, completing the whole declaration including the registry's own type.

The half-typed line is flagged as a syntax error while the list is still open, which is expected: the declaration is genuinely incomplete until you pick a claim. Choosing one completes it and the error clears.

Open Corpus → Vocabulary Workbench → Registry and all four are there, each with its gloss, its question, and its linked rules.

Give the frequency claim its domain

Promotion mints a claim from what a rule's declare says, and a declare carries no range: @sys.operating_frequency arrives as an unbounded number. A frequency is not unbounded, and the bound is what later lets the platform answer "what frequency would keep this U?" with a range rather than a half-line.

On the Registry tab, Edit sys.operating_frequency and set:

Field	Value
Range minimum	0
Units	GHz

Leave the maximum empty — a frequency has a floor that matters here and no ceiling this guide cares about, and either bound alone is a background constraint on every query.

Save new version. Registry entries are immutable, so this appends v2 — which is why it is done now, before any rule or axiom pins the claim. Everything from step 3 on is written against v2 and nothing goes stale.

Two claims that are authored, not promoted

The corpus needs two more claims, and neither arrives by promotion: promotion mints a claim from a rule's local, which always has a question and a plain type. Both of these end up solved-for — never asked of a document, their values coming from the rules and the axiom written in the next two steps. Author them directly on the Registry tab with New claim.

clas.portion_level — the ordered verdict. A numeric claim restricted to whole numbers, ranged 0 to 3, with a label and a gloss for each level, and no question: its value comes from the rules.

Set the type to numeric, leave Canonical question empty, tick Ordered and Whole numbers only, enter the range, then Fill from range and write the four levels:

Level	Label	Gloss
0	U	Nothing in the portion requires protection.
1	C	Disclosure would cause damage to national security.
2	S	Disclosure would cause serious damage to national security.
3	TS	Disclosure would cause exceptionally grave damage to national security.

Set Vetting to authoritative and Create claim.

scg_alpha.freq_above_10ghz — Alpha's own phrasing, also with no question. Alpha's prose says "frequencies above 10 GHz". That is Alpha's wording of a fact the canonical vocabulary already carries as a number, and asking the document a second, redundant question would invite the two answers to disagree. Step 3 gives it a meaning in terms of the canonical measurement instead.

A second New claim: id scg_alpha.freq_above_10ghz, type boolean, gloss "SCG Alpha's phrasing: the frequency is above 10 GHz.", Canonical question empty, vetting authoritative.

Both now appear in the Registry tab, the first badged ordered, and both badged Incomplete in amber — "no extraction question, and no rule or axiom determines it, so it can take no value at all". That is correct, and worth pausing on: right now nothing gives either claim a value. The axiom in step 3 gives scg_alpha.freq_above_10ghz its meaning and the floors in step 4 target clas.portion_level, and each badge turns Solved-for the moment it does. A claim still reading Incomplete at the end of the tutorial is a claim something is missing behind.

The Registry tab lists every claim in the group, so a shared instance shows other corpora's claims alongside yours — the search box and the namespace filter are how you narrow it to one.

Step 3: Connect the vocabularies with an axiom

This is the alignment work, and it is the whole point of the corpus. It is also entirely on screen.

Open Corpus → Vocabulary Workbench → Axioms and author:

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) };
Scope	program:rf

The editor type-checks the DSAIL against the registry as you write it, and shows an impact preview — how many rules and claims this axiom pulls into the closure — before you save. That preview matters: an axiom is the one object in the corpus that changes results everywhere without touching a single rule.

Click Preflight, read the docked panel, then Save axiom.

Note the shape of this alignment. It is not claim-to-claim; it is claim-to-expression, equating a boolean with a comparison on a numeric. Cross-guide unification leans on that shape constantly, because guides state thresholds in prose and vocabularies carry measurements as values.

Step 4: Transcribe the guides' rules

Corpus rules are authored in the Vocabulary Workbench → Rules tab. New rule opens the editor: the DSAIL source on the left, the role and its target claim beneath it, the rulesets to attach to, and a docked preflight panel on the right.

Four rules: two floors from Alpha, a ceiling from Bravo, and — in step 6 — a cross-guide mosaic. Each floor and ceiling names its Role and the ordered claim it bounds, so the platform knows which direction it pushes. Choosing Floor or Ceiling makes Target claim required, and it offers only ordered claims — which is why clas.portion_level had to exist first.

Rule 1 — SCG Alpha §3.2. New rule, and fill in:

Field	Value
Rule id	alpha.waveform_floor
Summary	Revealing that this item uses waveform X is SECRET.
DSAIL source	assert alpha_waveform_floor [pessimistic] { Or(Not(@scg_alpha.item_waveform_x), @clas.portion_level >= 2) };
Role	Floor — raises the verdict
Target claim	clas.portion_level
Completion policy	pessimistic
Authority source	SCG Alpha §3.2
Scope tags	program:rf
Rulesets	scg.alpha
Vetting	authoritative

Preflight runs when you leave the source box. Read the panel, then Create rule.

Rule 2 — SCG Alpha §2.1. Same shape, a different transcription:

Field	Value
Rule id	alpha.band_high_freq_floor
Summary	Stating the band of a system operating above 10 GHz is CONFIDENTIAL.
DSAIL source	assert alpha_band_high_freq_floor [pessimistic] { Or(Not(And(@sys.freq_band_mentioned, @scg_alpha.freq_above_10ghz)), @clas.portion_level >= 1) };
Role	Floor — raises the verdict
Target claim	clas.portion_level
Completion policy	pessimistic
Authority source	SCG Alpha §2.1
Scope tags	program:rf
Rulesets	scg.alpha
Vetting	authoritative

Rule 3 — SCG Bravo §1.4. Two fields change from the rules above: the role becomes Ceiling, and the completion policy goes back to neutral. Set it explicitly. It is the editor's default, but the field does not reset itself between rules, and a ceiling saved pessimistic resolves its unknowns the wrong way:

Field	Value

Two waveform claims, and the axiom between them

@scg_alpha.item_waveform_x asks whether this item uses waveform X; @sys.waveform_x_exists asks whether waveform X exists at all. They were one claim whose id said the first and whose gloss said the second, and a portion reading "waveform X is used only by the adversary system, not this item" answered True and marked SECRET.

Alpha's floor keys on item use, because that is what its guide classifies. Bravo's ceiling keys on existence, which is what its summary has always said. The axiom ax.waveform_item_implies_existence connects them as a subsumption — revealing that this item uses waveform X also reveals that waveform X exists, and not the reverse. That asymmetry is what makes the adversary-attribution portion mark U while a portion revealing this item's own use still collides Alpha against Bravo, which is the contradiction step 5 turns up.

| Rule id | bravo.waveform_alone_u | | Summary | The existence of waveform X, standing alone, is UNCLASSIFIED. | | DSAIL source | assert bravo_waveform_alone_u { Or(Not(And(@sys.waveform_x_exists, Not(@sys.freq_band_mentioned), Not(@ops.deploy_location_mentioned))), @clas.portion_level == 0) }; | | Role | Ceiling — caps the verdict | | Target claim | clas.portion_level | | Completion policy | neutral | | Authority source | SCG Bravo §1.4 | | Scope tags | program:rf | | Rulesets | scg.bravo | | Vetting | authoritative |

Two things about those three rules are worth pausing on.

Alpha's second floor is a faithful transcription. It says "above 10 GHz", exactly as the guide does, and it is connected to the actual frequency only through the axiom from step 3. That is the pattern to internalize: rules stay faithful to their source, and axioms do the crosswalk.

Bravo's ceiling is the step people get wrong

The tempting encoding of "standing alone, is UNCLASSIFIED" is nothing — just don't write a floor. It reads as equivalent and it is not.

Floors alone can never disagree. level >= 1 and level >= 2 are satisfiable together, so a corpus of nothing but floors is always clean, no matter how badly two guides contradict each other. It is only when Bravo's determination is encoded as a ceiling — an upper bound on the mark — that its disagreement with Alpha becomes a thing the platform can find.

("Standing alone" is stood in for here by three claims. In a real corpus it compiles over the portion's full item-claim set.)

Step 5: Declare what you are checking, and verify

Verification runs against declared scope combinations, so say which combination you mean.

Open Corpus → Corpus Health and click New profile:

Field	Value
Name	Program RF
Scope tags	program:rf
Rulesets	scg.alpha, scg.bravo, scg.cross
Publish gate	on

scg.cross has no rules in it yet — the mosaic in step 6 is the first. Naming it now is deliberate: the profile describes the slice you intend to govern, not the slice that happens to exist today. Type it into the box under the ruleset list and click Add. A ruleset a profile names is offered in the rule editor's Rulesets list from then on, so step 6 ticks it rather than retyping it — which is what keeps one slice from being spelled two nearly-identical ways.

Create profile. The header now shows a Program RF chip reading Unverified. Click Re-verify. The scan runs as a background job; the page refreshes with the report when it finishes.

The conflict

You get an error: rules_contradict, classified Across rulesets, implicating alpha.waveform_floor@1 and bravo.waveform_alone_u@1.

Revealing waveform X is SECRET. and The existence of waveform X, standing alone, is UNCLASSIFIED. cannot both be honoured.

any subject where not The portion names a deployment site and The portion reveals that waveform X exists and not The portion states the operating band

The witness is rendered as a scenario, not an assignment dump, and it is exactly the case both guides are talking about. Alpha floors that portion at S. Bravo caps it at U. There is no mark that satisfies both — and now you know, from the rules alone, before a single document has been uploaded.

This is what makes conflict detection worth running. Nothing about either rule looks wrong in isolation. Both are faithful transcriptions. The contradiction lives in the pair.

What else the run tells you

A warning comes with it: verdict_unreachable.

No rule in scope can produce clas.portion_level = TS — either a rule is missing or the level is unused.

A four-level scale where the top level is unreachable is worth knowing about before it is published.

Declare a coverage obligation

The checks so far find things that are wrong. Finding things that are missing needs you to say what "missing" means. This one is back on screen.

Coverage tab → Declare obligation:

Field	Value
Summary	A portion stating the frequency band must never remain UNCLASSIFIED.
Predicate (DSAIL)	@sys.freq_band_mentioned
Target claim	clas.portion_level
Requirement	Must not equal default
Default value	0
Scope	program:rf

Re-verify, and the Coverage tab reports a gap:

A portion stating the frequency band must never remain UNCLASSIFIED. — but an input exists where it does not hold.

any subject where The portion states the operating band

And it is right: a portion that mentions the band, with the frequency at 8 GHz and no deployment site named, marks U. Whether that is a hole in the guides or a mis-stated obligation is a human decision — but the platform found it without a document.

Deciding what to do about the conflict

Four actions are offered on the contradiction, and which one applies is a policy question, not a technical one. All four require a rationale.

• Accept precedence — one guide governs. If Bravo's standing-alone determination is the later authority, record it as governing and Alpha's floor is guarded so it does not apply in that case. This changes what the rules mean in every subsequent query, and changes the slice hash accordingly.
• Add distinguishing claim — if the resolution is "the two guides mean different waveform variants," then the corpus is missing a concept. This queues a candidate in the merge queue, prefilled from the witness, and defers the finding pending that review.
• Accept redundancy — for the other cross-source case, where two sources say the same thing on purpose. Not this finding: these two guides genuinely disagree.
• Not a conflict — dismiss with a reason.

See Dispositions for what each one does to subsequent queries.

For this tutorial, leave it open. The rest of the walkthrough uses portions where waveform X is absent, so the contradiction does not bear on them — which is itself worth noticing: a corpus can have a live contradiction and still mark most documents perfectly well.

Step 6: Add the mosaic

Cross-guide compilation guidance: the band and a deployment location, together, are SECRET — even though each alone is UNCLASSIFIED.

Back to Vocabulary Workbench → Rules → New rule, one more time:

Field	Value
Rule id	mosaic.band_location
Summary	The frequency band and a deployment location together are SECRET.
DSAIL source	assert mosaic_band_location [pessimistic] { Or(Not(And(@sys.freq_band_mentioned, @ops.deploy_location_mentioned)), @clas.portion_level >= 2) };
Role	Floor — raises the verdict
Target claim	clas.portion_level
Completion policy	pessimistic
Authority source	Cross-SCG compilation guidance
Scope tags	program:rf
Rulesets	scg.cross
Vetting	authoritative

Two things about this rule are worth pausing on.

It could not be written without the registry. Its two members come from different guides' vocabularies. Without shared claims and the axioms that connect to them, they are unrelated symbols and the cross-guide mosaic is inexpressible.

It is authored, not derived. "U plus U equals S" is not a logical consequence of anything — no amount of analysis will discover it. It is new classification guidance, and it lives as a rule because that is what it is.

Go back to Corpus Health and Re-verify. The Program RF chip goes stale the moment the rule lands, which is the point of the staleness status: a green badge against an edited corpus is worse than no badge at all.

Step 7: Mark a document

Now produce the values.

1. Documents → Create Document, and paste a portion that states the operating band and names a deployment site, without revealing waveform X and without stating a frequency.
2. Datasets → Create Dataset, and add that document.
3. Runs → New Run → Batch, select SCG portion items and the dataset, then Start Run.
4. When it completes, open Analysis.

Select the run and pin the document. A mark chip appears above the question catalog:

The classification level at which this portion must be marked. S as these rulesets mark it, from the 2 values the selected runs extracted

S, because the frequency band and the deployment location appear together and the mosaic fires. Hover the ⓘ for what that level means.

No chip at all?

The mark needs values. If the run answered none of the claims these rules read — everything came back Unknown, or its questions were rule-local names rather than the registry claims — Analysis says so instead of showing a level, because with every claim free the safe mark would land at the top of the scale for any document, including one the rules say nothing about. Check that the ruleset's claims are the @-sigil registry claims from Step 3.

The chip is the level; to see why, ask "Which of this document's answers is the level S load-bearing on?" from the catalog. It comes back naming the band mention and the deployment site — the two claims in the mosaic's condition — and marks the waveform answer as not load-bearing.

The unknown frequency

@sys.operating_frequency was never stated, so it is free, and the default policy is the safe mark — unknowns resolved to the worst case, so they can raise the level but never lower it. Here the frequency could exceed 10 GHz and trigger Alpha's band floor, but that floor only reaches C and the mosaic already forces S. So the unknown happens not to matter — which is exactly what the load-bearing answer tells you by leaving it out.

The cross-passage case

This is the interesting one, and it is why the mark is computed over the document rather than a paragraph. One passage mentions only the band. Another mentions only the deployment site. Neither alone triggers anything.

The run asks each question of the whole document, so both claims come back yes for the document however far apart they were stated. The mosaic fires, and the document marks S, even though no single passage would.

That is the mosaic problem in its real form: no part is a problem, and the whole is.

Note where the raised mark lands: on the document. Each passage on its own still discloses nothing classified, and marked as a standalone unit each would still mark U — correctly. Compilation raises the whole that juxtaposes the items, never the parts that compose it, so a part's mark stays a local fact: an extract carried out of the document keeps a label it can trust. (An item rule is different — revealing waveform X is SECRET marks every unit that contains the item, wherever it appears.)

Marking during the run

Analysis marked the document after the fact. The same mark can come back on the run itself. Both settings live in the Ruleset Studio, in the same panel as the input slots:

1. Set Mark target to @clas.portion_level. The picker offers only ordered claims with a range, since an unordered claim has no level to solve for.
2. Tick scg.alpha, scg.bravo and scg.cross in the Governed by list — the same list Step 1 told you to leave empty, now that those corpus rulesets exist. This is where a ruleset names the corpus rulesets it marks against; there is no separately-named field for it. The ids are unversioned: each names every version of that corpus ruleset, and every run records the slice it actually resolved.

Saving either one mints a new ruleset version, exactly as changing the input slots does — a version's governing slice is part of what that version means. Afterwards every run of SCG portion items returns the level as ordinary assert results alongside its per-rule verdicts:

assert marked_u  { @clas.portion_level == 0 };
assert marked_c  { @clas.portion_level == 1 };
assert marked_s  { @clas.portion_level == 2 };
assert marked_ts { @clas.portion_level == 3 };

Exactly one is TRUE — here marked_s, for the same reason the chip read S. The assert names come from the labels you gave the levels in step 2, so a scale labelled U / C / S / TS reads as above; label them Unclassified … Top Secret instead and the asserts are marked_unclassified … marked_top_secret.

Publishing it now goes through the gate

A Mark target turns the level into a determination the ruleset hands out, so publishing this ruleset is from now on gated on the corpus. The Program RF profile you declared in step 5 names all three corpus rulesets and has its publish gate on, so it is the profile that answers — and while the contradiction from step 5 sits there as an open error, Publish on SCG portion items is refused with a 409 naming it. Clearing it is the normal path: re-verify, then either fix the rules or record a disposition on the finding. See Marking rulesets pass a second version of it.

Two things this buys that Analysis cannot. An integration reads the mark the way it reads every other DSAIL result, with no override precedence to know. And the contradiction from step 5 becomes a per-document outcome: a portion that does reveal waveform X marks contradicted, naming alpha.waveform_floor@1 and bravo.waveform_alone_u@1 and the scenario behind them, while every other portion in the same batch marks normally. See the mark for the full contract, including the low/high bounds that make an unknown-driven mark visible.

Step 8: Ask what a lower mark would cost

Somebody has proposed marking this document C, and you have to decide whether that holds up. Ask "What would have to change for the level to be C in this document?" from the catalog.

The author's version of this is the same query. An author asks it to find the sentence to cut; a reviewer asks it to see what a proposed downgrade is actually claiming; a releasability officer asks it to cost a redaction before release. The answer is the same list of removals in all three cases — what changes is who reads it and what they do next.

Because this lowers an ordered verdict, the platform is asked for the smallest set of changes that reaches the goal — the fewest removals, not the first combination that happens to work.

Who may ask this, and what is recorded

A tool that names the sentence to delete in order to reach a lower classification is the first thing an accreditation reviewer asks about. Three answers, and none of them is a control somebody has to switch on.

The search can only propose removals. The claims it may change are the ones this document actually states — booleans a run answered yes — and the only direction it may move them is yes → no. It proposes deleting what is there; it never proposes asserting what the document does not say. That constraint belongs to this surface: POST /corpus/whatif takes the changeable set as a parameter and only requires each claim in it to be one the subject already answered, so an integration that builds its own request imposes the direction itself.

Every answer is recorded, acted on or not. Each query writes one immutable attestation row: the question as asked — the document pinned, the level asked for, and the claims the search was allowed to change — the answer returned including the redaction it proposed, the pinned rule, axiom and claim versions, the slice hash, the username that asked, and the timestamp. An audit entry lands with it, so the query appears in Activity → Logs naming the actor. Nothing is written back: asking what a downgrade would cost changes no claim value, marks nothing, and does not touch the document.

What is not recorded is a decision. A disposition cannot be saved without a rationale; this question takes no reason and requests no approval. The answer carries Advisory — not a determination, and acting on it is recorded wherever the redaction itself is recorded, not here. Nor is there a browsable list of past questions: an answer is retrieved by the result id shown in its attestation panel, so put that id in the review record if you may need to produce the query later.

Access is the platform's ordinary asset scoping — any member of the active group who can open this project can ask it. There is no separate reviewer role on this question.

Reachable.

The smallest change to this document

• The portion names a deployment site: yes → no

One change, and no alternative. Removing the band mention instead would also break the mosaic — but it would take Alpha's band floor with it, and the portion would fall to U rather than land on C. The question asked for C exactly, and only one redaction gets there.

Reachable is not the mark, and asking for U shows why

Ask the same question for U on the same portion and the answer offers two redactions — removing the site or removing the band:

The portion names a deployment site: yes → no or, instead: The portion states the operating band: yes → no

That is not a contradiction of the C answer, and neither answer is wrong. The three questions in this step and the next reason in three different frames over the same slice:

Question	Frame	On this portion, after removing the site
What would have to change for the level to be X?	Reachability — is there some way of resolving the claims nobody answered that gets to X?	both C and U are reachable
The mark chip, and step 7	Safe mark — the worst case over those same free claims	C
What if this claim were no instead of yes?	Strict entailment — every model has to agree	nothing is entailed: the level ranges U–C

The frequency is never stated in this portion, so it is free, and that is what lets all three differ. Removing the site leaves a portion that could be U (frequency at or below 10 GHz) or C (above it, so Alpha's band floor fires through the axiom) — so both are reachable, the safe mark is the worse of them, and nothing is entailed. Remove the band instead and the floor goes with it, so the mark is U, which is what the paragraph above says.

Each answer names its own frame on screen, because two of them read a minute apart look irreconcilable otherwise. When you want the level this document would actually be marked at, the mark is the question to ask — not reachability.

The instructive failure

Now try it on a portion where waveform X is revealed. The waveform is what the portion is about, so it is not something you can redact — it is not in the mutable set.

Not reachable for this document as it stands. Given the values the selected runs extracted, no change this question is allowed to make reaches that outcome.

Blocked by Revealing waveform X is SECRET.

Downgrading there requires rewriting, not redacting.

That is a first-class outcome, not an error, and it is frequently the more valuable one. A list of removals tells you what to do; an explained impossibility tells you that no amount of redaction will help and the portion needs to be rewritten.

Step 9: What values are allowed?

One more question, and review is where it earns its keep: how far can this be revised before it needs a higher marking? is a releasability question, and it is the more common ask — an author uses the same answer to decide what to write. A portion states the band, names no deployment site, and never states a frequency. What frequency would keep it U?

Ask "What values of the operating frequency would keep the level at U, for this document?":

The operating frequency the portion states, in GHz Allowed: 0–10 GHz

That region comes from Alpha's band floor reached through the alias axiom — band mentioned and above 10 GHz forces at least C — combined with the range you gave the frequency claim in step 2, whose minimum of 0 is what closes the region at the bottom. Skip that step and the answer is the same fact with an open end, because nothing in the corpus would say a frequency cannot be negative. The axiom you wrote in step 3 is what makes that connection; delete it and the region opens up, because Alpha's boolean would have nothing to do with the number.

The same question exists in the other catalog, phrased for the other scope: "What values of the operating frequency are consistent with the level being U, for any subject?" What tells them apart is what each one binds. The document question names a document and binds the values the selected runs extracted from it, so the region it returns is the room this portion has left — the band mention is already yes here, and that is what closes the region at 10 GHz. The any-subject question binds nothing: every claim stays free, the band mention included, so it answers about the rules and this portion's answers have no bearing on it. One is a fact about a case; the other is a fact about the rules.

Note that this is not a verdict, so completion policies do not apply. The answer is the constraint region.

Step 10: The full pipeline — portion marks and a document banner

Steps 7 to 9 marked the document. One run over the whole text, one level, and the mosaic fired across passages because a presence question asked of the whole document is true when any part of it makes it true. If a document mark is all you need, stop there — it is the cheapest correct answer.

Marking practice usually needs more: a mark per portion, stamped on each paragraph-level unit, plus an overall banner that can exceed every portion's mark, plus the compilation basis behind it. That is what this step builds. Four platform runs and one fold, and the only new platform mechanism is supplied answers.

The division of labour is fixed, and it is the thing to understand before writing any of it:

your workflow                                        the platform
─────────────────────────────────────────────────────────────────────────
 1  chunk document → portions P1..PN
 2                                                    run ruleset on each Pi
                                                      → portion mark Mi + claim answers Ai
 3  fold A1..AN per claim
 4                                                    run same ruleset on folded answers
                                                      → document mark M_doc + provenance
 5  banner := highest of (M1..MN, M_doc)
    stamp portions, banner, compilation note

One set of rules, evaluated per subject. A portion and a whole document are both subjects. Nothing in the corpus you built says the word "document": the mosaic fires on whichever subject holds both items — a single portion that states both, or the document whose folded values combine them. What changes between the two passes is only where the claim values come from.

Marks do not compose upward; claim values do. You cannot derive the document mark from the portion marks. All portions U with the document S is the mosaic's defining case. You derive it by folding the claim values and evaluating the rules again at that new point.

Chunk, and keep the spans

Split the document into portions with exact character spans, at the granularity marking practice requires — normally the paragraph, plus titles, captions and bullets. Keep the span table; it is what you stamp against at the end. The platform takes no position on portion boundaries, which is a feature: your chunker is deterministic and the marks anchor to spans you control.

Run the ruleset on each portion

One run per portion against SCG portion items:

POST /api/v1/runs/interactive
{ "ruleset_id": "<id>",
  "input_documents": { "input": { "document": "<portion text>" } } }

Each completed run gives you two things, and the second matters as much as the first: the portion's mark (its marked_* asserts, from step 7) and the portion's per-claim answers from the claims table. Keep both — the answers feed the fold.

Cost. N portions means N extraction passes. Interactive runs are judged one document at a time, so budget N× the LLM cost of a whole-document run. If that matters, load the portions as a dataset and use a batch run instead: the batch path packs one claim's question across many documents in a single request, which on a strong judge model brings a chunked document back to roughly the cost of marking it whole. On a weak judge model that packing is limited to numeric claims — nuanced booleans are asked one document at a time — and marking claims are overwhelmingly boolean, so the saving largely disappears. Decide this before committing to fine-grained portions. On this corpus, measured: three of the four marking claims are boolean and one is numeric, and the batch path saved nothing measurable over five interactive portion runs. Treat the batch saving as real only when your marking claims are mostly numeric.

Failure isolation. A portion run that errors fails that portion only. Record its mark as unavailable, exclude its answers from the fold, and carry on — one bad page must not fail a 400-portion document.

The platform can emit the span table for you

The instruction above is to build the span table yourself, and the argument for that stands — marking practice has opinions about portion boundaries that a generic sentence chunker will not share, and a deterministic chunker you control is what makes an audit reproducible. But it is worth making that choice knowing the alternative exists.

A run with streaming attribution returns an attribution payload whose chunks carry start/end character offsets, and whose flips record every value change with the flip_sentence that caused it and that sentence's own sentence_start/sentence_end. Those offsets are exact against the source text. unresolved_keys lists the claims no chunk answered, with their questions.

Streaming runs compute the mark as well, so one run can in principle give you both halves — the level and the span it anchors to. Three caveats, and the first is load-bearing:

• A streaming mark can read higher than the batch mark on the same text. Streaming leaves a claim no chunk answered in unresolved_keys, where the batch path applies the presence contract and answers False on silence. A claim left free resolves the unsafe way under the safe mark, so the level rises. The mark says so — unknown_driven is set and unanswered_claims names the claim — but do not treat the two paths as interchangeable for a determination until they agree. Take the mark from a batch run and the spans from the streaming one.
• Supplying answers is refused together with streaming, which derives per-claim state from the document as it is chunked.
• The chunk boundaries are the chunker's, not your marking guide's.

Fold the answers, per claim

This is your workflow's arithmetic, and it is deliberately simple.

Booleans — 3-valued existential. The document-level reading of a presence claim ("does the portion state the band?") is "does some portion state it":

Across portions	Document value
any True	True
no True, any Unknown	Unknown
all False	False

Numerics, enums, strings — agree or abstain. All answering portions agree → that value. They disagree → supply Unknown and log the conflict with the portions and values (P2: 12 GHz, P9: 8 GHz) for human review. Do not invent an aggregate — there is no defensible scalar "union" of two different frequencies, and Unknown hands the decision to the rules' completion policies, which is where classification policy already lives.

Reproduce this step without a model

The worked example above is built from extracted values, so you cannot check your own run against it unless extraction is working. The document pass can be driven from supplied values alone — no model call, no input_documents — which makes the whole of this step self-testable:

{
  "ruleset_id": "<your ruleset>",
  "supplied_answers": {
    "@sys.freq_band_mentioned":       {"value": "True",  "source": "run:portion-1"},
    "@ops.deploy_location_mentioned": {"value": "True",  "source": "run:portion-2"},
    "@scg_alpha.item_waveform_x":     {"value": "False", "source": "fold"},
    "@sys.operating_frequency":       {"value": "12.4",  "source": "run:portion-1"}
  }
}

POST /api/v1/runs/interactive with that body and no input_documents returns the mark solved from the four values, with skipped_supplied equal to the number of keys and no model calls at all. Supply exactly the claims the ruleset's rules declare — the mark target and any claim the corpus derives are refused, because their values come from the axioms and the floors.

Provenance rides the fold. For every value that survives, record which portion run it came from. This costs you nothing — your workflow performed the fold — and it becomes the compilation basis in the document result.

The fold is cheap, deterministic, and yours. Resist the urge to push it into a rule: it is document-structure logic, and document structure is the workflow's domain.

Run the same ruleset on the folded values

The same ruleset, with the folded values supplied instead of extracted:

POST /api/v1/runs/interactive
{ "ruleset_id": "<id>",
  "supplied_answers": {
    "@sys.freq_band_mentioned":       { "value": "True",  "source": "run:<P2-run-id>" },
    "@ops.deploy_location_mentioned": { "value": "True",  "source": "run:<P7-run-id>" },
    "@scg_alpha.item_waveform_x":     "False",
    "@sys.operating_frequency":       "Unknown"
  } }

• Keys carry the sigil, exactly as the rules declare them: @sys.freq_band_mentioned, not sys.freq_band_mentioned. The key is the claim key of the ruleset version being run.
• No document is needed. Every claim of this ruleset that could be extracted is supplied, so input_documents may be omitted entirely and the run makes no model calls at all — it is solver-only and effectively free. The map holds four claims because those are the four the ruleset's rules declare; @clas.portion_level and @scg_alpha.freq_above_10ghz belong to the corpus rules rather than to this ruleset, so they are not keys of this map at all — supplying one is a 400. Their values come from the axiom and the floors, as they always have.
• Unknown means "leave it free", and the rules' completion policies govern it exactly as they do for a claim no document answered — which is why the unstated frequency behaves here as it did in step 7.
• The run stores what you sent, verbatim, values and sources both, so the document pass is its own audit artifact. In the claims table each supplied claim's evidence reads supplied: run:<id> where an extracted answer would show the model's excerpt.

Read the document mark from the same marked_* asserts, and the compilation basis from the sources you sent. The per-rule verdicts come back too, computed over the folded vector — a point no single portion occupies, which is precisely what a mosaic is.

Supplying answers also works alongside a document: give input_documents and a partial map, and the supplied claims bind while the rest extract. That is how you re-mark after a human corrects one answer, without re-extracting the other forty.

Assemble the banner

• Banner = highest of (all portion marks, the document mark), per marking practice.
• When the document mark came from a mosaic, stamp the compilation note from the provenance: classified by compilation — band (P2) with deployment location (P7).
• If the document mark comes back lower than the highest portion mark, do not reconcile it arithmetically. The banner still takes the maximum, and you surface the discrepancy for a human. The usual cause is the fold answering a claim that a portion left Unknown: that portion's mark was the safe mark over an unknown, and a sibling portion's concrete answer replaced the worst case with the truth. This is not a ceiling capping the document — a ceiling that collided with a floor at a level the answers force would report the mark contradicted, not lower it.

The whole thing on one document

Corpus as you built it. A document with three relevant portions; the judge extracts:

	band mentioned	location mentioned	waveform X	frequency	portion mark
P2	True	False	False	12 GHz	C — Alpha's band floor via the axiom (band ∧ >10 GHz → ≥ 1)
P7	False	True	False	Unknown	U — no floor fires
P9	False	False	False	Unknown	U

Fold: band True (from P2), location True (from P7), waveform False, frequency 12 GHz (only P2 answered). The document run over those values:

floors active:  alpha band floor      → level ≥ 1
                mosaic band+location  → level ≥ 2
ceiling:        inactive (waveform not revealed)
solved:         level = 2   →  marked_s TRUE

Banner: highest of (C, U, U, S) = S.

(S)  ── banner, classified by compilation: band (P2) + deployment location (P7)
(C)  P2 …states the band, 12 GHz…
(U)  P7 …names the site…
(U)  P9 …

Both properties are visible at once: the document mark exceeded every portion's, and P2's mark stayed a local fact — carried out of the document alone, its (C) is still right.

Rules of the road

Five things to get right, each of which is a real mistake somebody has made.

Never derive the document mark from the portion marks. A maximum over portion marks misses every cross-portion mosaic — all portions U, document S. Marks don't compose; claim values do. Fold values, re-run rules.

A mosaic raises the document, never the contributing portions. Distinguish the rule types. An item rule ("revealing waveform X is S") marks every portion containing the item, at the portion pass, with no mosaic involved and non-contiguity irrelevant. An association rule ("band + location is S") classifies the co-presence, which no portion contains: the document carries the level, the portions keep their standalone marks, and the provenance names the witnesses. Marking the contributing portions would itself leak the association — an S stamp on a standalone-U sentence announces that it participates in a classified combination — would make P2's mark depend on P7's content, and has no principled answer to which portions when five state the band and three name sites. If an authority decides contributing portions should be upgraded anyway, that is a human disposition on the finding, recorded and attributed, never an automatic re-mark.

Presence-polarity claims only, in marking rules. The fold reads booleans existentially. A claim like "all records in the portion are encrypted" folds wrongly under OR. If you need one, keep it out of the marking rules or restructure it as presence of the violation — "does the portion contain an unencrypted record?" — which folds correctly. This is the same discipline step 2 asked for when phrasing the questions.

Entity-quantified rules contribute nothing at the document pass. Rules quantifying over entity scopes work normally inside each portion run — the portion's text is there to extract from. At the document pass there is no text and no instances, so those assertions report UNKNOWN with a warning, honestly, rather than a vacuously satisfied quantifier. If the mark depends on entity rules, mark on portions and treat the document pass as scalar-mosaic only.

Don't model portions as entities. It is tempting to declare Portion as an entity and feed the whole document to one run. Portions are positional units of the artifact, not semantic entities: they have no identity to merge or split on, their boundaries must be your chunker's exact spans rather than an extractor's opinion, a per-portion mark is not a quantified verdict, and one whole-document extraction is a single point of failure for 400 portions. The layering is: portions are subjects (runs); entities are instances within a subject.

Two accepted trade-offs, stated plainly

A neutral floor is still treated adversarially by the mark. A rule's [pessimistic] / neutral completion tag governs that rule's own verdict and the corpus checks. The mark is one joint solve under one policy — the safe mark — so a floor authored neutral still has its unknowns resolved to the worst case where the mark is concerned. The effect is always to over-classify, never to under-classify, which is why it is acceptable; it is worth knowing before you reach for neutral expecting the mark to soften.

A ruleset version's corpus rulesets are unversioned, so its slice can move. The ruleset names scg.alpha, scg.bravo, scg.cross — ids, not id-and-version — so two runs of one immutable ruleset version can resolve different slices as the corpus evolves. That is correct for a governance layer: a guide's revision is meant to reach the rulesets that cite it. What a given run actually used stays pinned, and that is the half that makes this a design rather than a defect. Every mark records the slice hash it was solved over — a digest over the version-pinned rule, axiom and claim references, the scope tags, and the precedence decisions in force — and on the Analysis side every corpus answer is stored as an attestation envelope carrying that same hash beside the version list, the claim values behind it, and a digest over the envelope itself — sha256-digest, which detects an altered record rather than proving who wrote it, because there is no result-signing key yet. So a past mark is reproducible after the fact even though the ref that produced it named no version, and a mark computed against a corpus that has since moved is detectable rather than silently stale: the recorded hash no longer matches the slice the same refs resolve today. What the unversioned ref costs you is stability, not traceability — a corpus change can move a published ruleset's marks, and detecting that is what the recorded slice hash and re-verification are for.

Be precise about the [publish gate](../concepts/corpus-health.md#marking-rulesets-pass-a-second-version-of-it) here, because it is narrower than it sounds. It refuses to **publish** a marking ruleset whose corpus does not verify clean, and it is checked at that moment only. It does not gate runs: a run resolves the ruleset's **head** version, so a ruleset that failed the gate still solves marks from head, and an ordinary settings save mints an equivalent version without consulting the gate at all. Treat it as a release-time check on the author's intent, not as an enforcement boundary around marking — the thing that tells you a mark went stale is the slice hash, not the gate.

---

What you built

Every step was done on screen.

Step	Where	Mechanism	Concept
1–2	Ruleset Studio	A ruleset whose claims were promoted into a shared registry	Claims and the sigil
2	Workbench → Registry	An ordered, solved-for verdict claim with its level map	Ordered verdicts
3	Workbench → Axioms	A claim-to-expression alias unifying two guides' phrasings	Axioms
4	Workbench → Rules	Floors and a ceiling, transcribed faithfully from each source	Floors and ceilings
5	Corpus Health	A real inter-guide contradiction, found from the rules alone, plus a declared coverage obligation	Corpus Health
6	Workbench → Rules	An authored cross-guide mosaic	Mosaics
7	Analysis	A document mark, and a mosaic assembled across passages	The mark
7	Runs	The same mark returned by the run itself, as marked_* asserts	The mark on a run
7	Ruleset Studio	A Mark target, and a publish refused until the slice verifies clean	The publish gate
8	Analysis	A minimal correction set, and an explained impossibility	What would have to change
9	Analysis	A feasible region — how far a value can move before the mark does	Which values would keep the outcome
10	Your workflow + Runs	Portion marks, a per-claim fold, a solver-only document run, and a banner with its compilation basis	Supplying claim answers

The durable asset here is not the four rules. Transcribing those took minutes. It is the six claims and the one axiom — the decision that Alpha's "above 10 GHz" and the canonical frequency are the same fact. That decision is what made the mosaic expressible, the conflict visible, and the feasible hint correct, and it is the thing that will still be paying off when the guides are revised.

Next Steps

• Corpus Health — the rest of the check suite, dispositions, and the publish gate
• Analysis — the other questions, including proposing a rule and asking what it would break
• Vocabulary Workbench — the registry, the merge queue, and promotion in full
• Corpus API — the same objects over REST, for integrations and bulk import
• Rules About Many Things — rules over the several things a document describes