Analysis

Analysis is where you ask the corpus questions. It lives inside a project, beside its runs, and it answers about one subject at a time, across the corpus rulesets you put in scope.

It is not a second evaluator. Every value it reasons over was extracted by a run that already finished, and every answer it gives is advisory. That is the trade it makes: a run tells you whether a ruleset held; Analysis tells you what follows, what would have to change, and what the rules can do at all — and it does that across rulesets, which no single run can.

A question is not a determination

Every answer carries an Advisory — not a determination badge. Analysis is a review aid, a remediation preview, and an impact estimate. It is never a compliance verdict, and it must not be presented as one. If you need a determination, create a Run.

Getting There

Open a project and click Analysis in the project sidebar.

The page has three parts, top to bottom: a scope bar where you choose what the question is about, the question catalog where you pick one and fill in its parameters, and the answer below it.

Runs and Analysis: The Difference That Defines It

	Run	Analysis
Scope	One ruleset, at one pinned version	The corpus rulesets you put in scope
Subject	One document, a dataset of documents, or pasted text	Exactly one subject — one document, or no document at all
What it does	Asks the ruleset's questions of the document with an LLM, then solves	Reads answers a run already produced, then solves
What it produces	Per-rule determinations: TRUE, FALSE, UNKNOWN, AMBIGUOUS	Diffs, requirements, load-bearing claims, witnesses, feasible regions
Standing	A determination	Advisory, always
Uses an LLM	Yes	No — it never re-reads a document

The Two Modes

Under What are you asking about? the scope bar offers two, and the choice is explicit and visible because it decides which questions exist at all.

About one document. Questions about a case. Pin a document and the answer is about that document, computed from the values the selected runs extracted for it. Every question in this catalog says "this document".

About these rulesets. Questions about the rules, quantified over every possible subject. Nothing is pinned and no values are bound, so every answer is an input class, a witness, or a proof. Every question in this catalog says "any subject", or asks whether something can "ever" happen.

The mode and the pin are one invariant: choosing About these rulesets releases the pin, and pinning a document selects About one document.

What each mode needs before it will show you questions

Mode B, "About these rulesets", needs no run at all. These questions bind no claim values, pin no document, and read no results, so there is nothing a run could contribute. The scope bar shows a Corpus rulesets list instead — every corpus ruleset the registry knows, multi-select, each with its version — and you tick the ones to reason across.

This works on a project with zero runs, which is the common case when the rules are new and nothing has been evaluated yet. If runs happen to be selected, the rulesets they put in play arrive pre-ticked as a convenience — and every one of them can be unticked, so they are a starting point rather than a constraint. Once you change the selection by hand, later run selections leave it alone.

Mode A, "About one document", needs evidence, so it needs a run. Three things have to be true before its catalog appears:

1. The project has at least one completed run. Runs still in progress, and runs that failed, are not offered.
2. You have selected at least one of them, and pinned a document.
3. The claims those runs answered are claims the corpus registry knows. A ruleset whose claims were invented in the Ruleset Studio and never registered produces runs Analysis cannot read, and the page says exactly that — "These runs answered no claims the corpus registry knows, so there is no ruleset to reason across."

Until those hold, the page explains which one is missing rather than showing an empty catalog. Selecting nothing at all in Mode A reads: "Select at least one completed run above… Questions about the rulesets themselves do not — switch to 'About these rulesets' to ask those."

The Scope Bar

Completed runs

Each run shows its ruleset name, its id@version ref, when it started and the first characters of its run id, and how many documents it read. The time and the id are what tell two runs apart: everything else on the row describes what was run, so three runs of one ruleset over one document would otherwise be indistinguishable. A run whose ruleset has since been edited carries a Ruleset has moved on badge: its answers were produced by an earlier version of the ruleset, which is a fact about the evidence rather than an error.

A corpus question needs three things — which rulesets, which subject, and what is already known about that subject. In Mode A a run supplies all three at once, which is why Analysis lives beside a project's runs rather than on a document.

Corpus rulesets in play

In Mode A, below the run list, Corpus rulesets in play lists the corpus ruleset refs the answer will be computed over, as chips.

Where that list comes from — a declaration or an inference

The list is labelled, and the two labels are different kinds of fact that are never merged into one sentence.

Declared. A ruleset version can name the corpus rulesets its rules answer to. When the version a run pinned declares them, that declaration is the scope, and the line under the chips says so and names the version. The ids are unversioned — each names every version of that corpus ruleset — and each run's attestation records the slice it actually resolved, so a moving corpus stays reproducible after the fact.

Derived. A run names a platform ruleset, and corpus rulesets are a different namespace: the platform ruleset a run evaluated and the corpus rulesets that transcribe the same policy can have entirely different names, and often do. For a version that declares nothing, the scope is therefore derived from evidence rather than assumed: the claims the selected runs actually answered are matched to registry claims, and every corpus ruleset holding a rule that reads or targets one of them is in play. It is an inference, not a declaration, and the line under the chips says that too. Select runs of both kinds and both lines appear, each naming its runs.

Either way the chips exist so you can check it. Under a derivation, a ruleset you expected but do not see means the runs answered none of its claims; one you did not expect means it shares a claim with something the runs did answer. The commonest reason one is missing: the platform rule asked its questions as rule-local names rather than registry claims. A run that answers deploy_location_mentioned has answered a local, not @ops.deploy_location_mentioned, so no corpus rule reading the registry claim is matched. Promote the local in the Vocabulary Workbench and re-run, declare the refs on the ruleset version, or switch to Mode B and pick the ruleset directly.

Every request Analysis sends names these refs explicitly, so an answer is never computed over a wider slice than the screen shows.

Scope tags

Below the ruleset controls, Scope tags decides which of those rulesets' rules are loaded. Leave it empty and the question is asked under every context — every rule in the selected rulesets takes part, whatever it is tagged for. That is the default because it is the only default that cannot silently answer a question about nothing.

Tick a declared tag, apply a declared profile's scope, or type a tag of your own, and the slice narrows: only rules tagged for what you named — or tagged for nothing at all — take part. Every answer states the scope it was computed under, and if narrowing left out a rule from a ruleset you named, the answer says so instead of presenting the result as a proof about rules it never saw.

Which document can be pinned

Only documents present in every selected run. A claim value means something only for a document the run actually read, so the intersection is the honest offer — a document missing from one run has no values from it, and an answer built that way would quietly be about a different slice of evidence than the screen claims. Select two runs with no document in common and the pin control explains that rather than offering a partial subject.

Which claims get bound

In Mode A, Analysis binds the pinned document's claim values from the selected runs' results. For each claim a run answered, the value is coerced to the registry claim's type and bound. Runs are read in selection order and the first stated value for a claim wins. A value that cannot be coerced to the claim's type is not bound at all, which reads as UNKNOWN rather than as a type error from the solver.

A claim no selected run asked stays free, and free claims are not a gap — they are the mechanism behind the safe mark and behind every what-if. They appear in the claim pickers displayed as not stated, which makes them the most interesting things to inject.

The same answers are also recorded into the corpus as claim values on the document, the first time a completed run's results are read. Only registry claims are recorded — a rule-local answer is a claim about one rule, not a governed corpus claim — each against the claim version the rule referenced, with origin: extracted and provenance naming the document and the run. An answer of UNKNOWN records nothing: a free claim and a claim bound to nothing are the same fact. Entity-scoped (multi-instance) claims are answered once per instance and a claim value is one value per document, so they are deliberately not recorded.

The Mark

With a document pinned, an ordered verdict claim in the slice, and at least one value bound that the slice's rules actually read, a chip appears above the catalog:

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

The chip always carries the level's label in words, so a mark is never encoded by colour alone, and an ⓘ beside it gives that level's meaning followed by what the scale as a whole measures — both served from the registry claim, so the explanation is the vocabulary owner's, not a hardcoded string. A slice with no ordered verdict claim shows no chip at all rather than an empty placeholder.

A chip that reads S unanswered is not a measurement. One bound value is enough to render the chip, and under the safe mark every claim the runs left unanswered still resolves the unsafe way — so a level can be driven entirely by what nobody answered even though something was bound. The word unanswered beside the letter says exactly that, and the caption beside the chip says which claims would settle it. Read it as the worst the rules admit for this document, and answer the named claims to turn it into a finding.

The mark is the level the rules force under the pessimistic completion policy — the safe mark, where an unanswered claim can raise the level but never lower it. A ceiling reaching the slice is the one thing that can push the chip the other way, and it does not do it by capping — read that before concluding a low chip is a bug.

A document with nothing bound gets no mark, and a sentence instead. That is the same policy read the other way: with every claim free, the safe mark resolves each one the unsafe way, so the floors fire and any document — including one the rules say nothing about — comes out at the top of the scale. That number is arithmetic about the rules, not a finding about the document, so it is not shown as one. Select a run whose ruleset asks the registry claims these rules read, and the mark appears.

The chip is the level, and only the level. To find out why it landed there, ask a question; the catalog below is how.

The same mark, asked twice

A ruleset that names an ordered claim as its Mark target solves this same mark during the run, over the same rules and axioms and under the same safe-mark policy, and returns it as assert results on the run. The two answers are the same determination reached at two moments: the run's mark is about the document it just read, and this chip is about whatever runs you selected. Two differences are worth knowing. The run's mark carries low and high beside the level and states above the level rows when an unanswered claim drove it; and where a slice cannot honestly be marked — an unannotated rule over the target, no rule bearing on it at all — the run reports the mark undetermined with a reason rather than showing a level, which is the same judgement this surface makes when it withholds the chip from a document with nothing bound.

When a ceiling lowers the chip

The chip can read lower than the floors bearing on the document would demand, and lower than it read yesterday over the same evidence, because a ceiling reaching the slice takes levels away rather than adding them. Nothing is broken. It is the safe mark choosing among the readings that are left.

The safe mark is the highest level reachable under some resolution of the still-free claims that satisfies every rule in the slice — ceilings included. A resolution in which a floor and a ceiling collide is not a resolution: it drops out, and the level that floor would have demanded goes with it. So when the only way to fire a floor is also the way to fire a ceiling that contradicts it, that floor can never set the level, and the chip falls to whatever survives.

In the two-guide corpus the worked examples use, on a portion that states neither the operating band nor a deployment site, with does this reveal waveform X? unanswered, Bravo's standing-alone ceiling takes the chip from S to U — and puts clas.portion_level in the entailed list at U, where without that ceiling the level was not entailed at all. Both answers are correct about their own slice, and the second is the sharper statement: across every reading of this portion that both guides can honour, waveform X is absent. That is a fact about the rules, not about the document.

So read a surprisingly low chip as a prompt to answer the open claim, never as a cap to reason around. Answering it resolves the apparent paradox in whichever direction is true: yes, it reveals waveform X is the collision the ceiling exists to catch, and comes back from Do these rulesets disagree about this document? naming Alpha's floor and Bravo's ceiling together; no, it does not is U on its own merits. The same mark solved during a run says so in its result: a mark decided by a claim the run left unanswered is reported unknown-driven whether or not the ceiling collapsed low and high onto a single level, and assumed_claims names the claims the rules settled rather than evidence did. Both now reach the screen: the chip carries the word unanswered when the level was unknown-driven, and its caption names the claims the corpus rather than the evidence settled. The run's own mark says the same thing above its level rows, with the range the rules admit.

The Question Catalog

Pick a question, fill in the parameters it declares — only those; a question that needs none shows none — read the preview sentence under the form, and click Ask. When the slice has an ordered verdict claim it arrives pre-selected as the Outcome, because it is the outcome nearly every question is about.

Claims are named in these sentences by their gloss, never their id, so the question reads as English. Where a level has to be chosen, the dropdown lists the level names and states the chosen level's meaning underneath — an option inside a dropdown cannot carry a hover, so the gloss is set out in the open instead.

About one document — five questions:

Question	The sentence you get
What if an answer were different?	What if {claim} were {value} instead of {current}, for this document?
What would have to change?	What would have to change for {claim} to be {value} in this document?
Which answers is the outcome load-bearing on?	Which of this document's answers is {outcome} load-bearing on?
Do the rulesets disagree?	Do these rulesets disagree about this document?
Which values would keep the outcome?	What values of {claim} would keep {outcome}, for this document?

About these rulesets — five questions:

Question	The sentence you get
Can the rulesets contradict each other?	Can these rulesets ever contradict each other, for any subject?
What would a proposed rule break?	If we adopted this proposed rule, what would break for any subject?
Is an outcome reachable at all?	Is {outcome} ever reachable by any subject, and what is the smallest input that reaches it?
Is a rule already redundant?	Does any rule in these rulesets already make {rule} redundant, for any subject?
Which values are consistent with the outcome?	What values of {claim} are consistent with {outcome}, for any subject?

Why the modes ask different questions

This is the distinction worth internalising, and the product enforces it by construction: the two catalogs share no question. A question of the wrong scope is not greyed out — it is not there.

"What if this answer were different?" is meaningless without a document. It is defined as a diff against a baseline, and the baseline is this document's answers. With nothing bound there is no baseline to diff against, and every claim is already free, so "changing" one changes nothing.

"Can these rules ever contradict each other?" is strictly stronger than "do they contradict here?". The first quantifies over every possible input and is answered by solving, so a negative answer is a proof that no document can ever trigger the collision, and a positive one is a proof that some document could. The second is one point in that space. "No document has hit this yet" is not evidence of anything; "no input can hit it" is.

---

Worked Examples

The examples below run against the corpus built step by step in the SCG Portion Marking Tutorial — two security classification guides, one alignment axiom, two floors, a ceiling and a cross-guide mosaic, all bearing on one ordered claim clas.portion_level with the scale U (0), C (1), S (2), TS (3). Build it there and every answer below is one you can reproduce.

About one document

The document states the operating band and names a deployment site. It does not reveal waveform X, and it never states a frequency. A run has answered those questions, and the mark chip reads S.

Do these rulesets disagree about this document?

No parameters.

No — every rule in these rulesets can be honoured together for this document.

clas.portion_level: S

The list underneath is what the rules force — entailed, not merely consistent — and it covers the slice's solved-for claims, the ones with no extraction question whose values are supposed to fall out of the rules. The verdict is in it because the floors compile into a definition of the level — the highest level any floor whose condition holds demands, or the bottom of the scale when none does — so the level comes out determined rather than merely bounded. Ceilings are checked against that definition rather than folded into it — a ceiling is never a term in the arithmetic that sets the level. That is not the same as a ceiling never changing the level you read, and the difference is worth knowing before you meet it: see When a ceiling lowers the chip. In this slice the ceiling is slack, and the verdict is S because the mosaic rule forces it.

When the answer is yes, it names the rules that cannot both be honoured and renders the scenario that triggers them.

Which answers is the outcome load-bearing on?

Outcome clas.portion_level at S (2). The platform flips each answered claim in turn and reports which ones change whether the outcome holds:

The outcome turns on 2 of 3 answers.

• The portion names a deployment site — yes — load-bearing — flips the outcome at no
• The portion states the operating band — yes — load-bearing — flips the outcome at no
• The portion reveals that waveform X exists — no — not load-bearing

Two answers out of three are worth a human's time to verify rather than all three, and the two named are exactly the mosaic rule's conjuncts. Load-bearing means the outcome depends on this answer, in either direction — an answer can be load-bearing while being answered no, if flipping it to yes would fire a floor.

What if an answer were different?

Claim The portion names a deployment site, value no. The preview reads "What if The portion names a deployment site were no instead of yes, for this document?"

The classification level at which this portion must be marked. S → C

no longer entailed — The classification level at which this portion must be marked

The mark chip shows the transition with the old level struck through and a dashed border, the dash meaning hypothetical.

This answer repays a second look, because the obvious guess is wrong. Without the deployment site the mosaic's conjunction breaks — but the band is still mentioned, and the frequency is still unknown. Under the safe mark the frequency could be above 10 GHz, which fires Alpha's band floor, so the level lands at C, not U. An unknown that did not matter at S matters at C, and the answer says so by moving the mark only one step.

The answer is a diff, not a re-listing: claims whose entailed value changed, claims now entailed that were not before, and claims no longer entailed. An absolute list of everything entailed would bury the one thing that moved.

"No longer entailed" is not "no longer marked." Entailment is the strictest frame the platform reasons in: a claim is entailed only when every reading of the document agrees on its value. A change that widens the range of possible levels therefore drops the level out of the entailed list while the subject still marks perfectly well — the mark takes the worst case rather than requiring agreement. Where the claim is the ruleset's mark target, the row says so, because on its own it reads as though the level had been lost.

The injected value is marked hypothetical, the whole answer is advisory, the document is never touched, and nothing is persisted except the record of what was asked.

What would have to change?

Claim clas.portion_level, value C (1). Because this lowers an ordered verdict on a pinned document, the question becomes a redaction question: the platform is asked for the smallest set of changes that reaches the goal, with the search restricted to claims the document actually states, booleans only, in the "make it false" direction. It proposes removing what is there; it never proposes fabricating what is not.

Reachable.

The smallest change to this document

• The portion names a deployment site: yes → no

One change, and no alternative is offered — which is the informative part. Removing the band mention instead would break the mosaic too, but it would also remove the only thing Alpha's band floor keys on, so the portion would fall to U rather than land on C. The question asked for C exactly, and only one redaction gets there.

Where an equally small alternative does exist, it is shown as "or, instead: …", with its own yes → no transition — an alternative is a change and reads like one.

Reachable is not the mark

Reachability is existential: it asks whether some way of resolving the claims the runs left unanswered gets to the outcome. The mark is a different question over the same slice — the worst case over those same free claims — and "What if an answer were different?" is a third, strict entailment, which needs every reading to agree. All three are correct and all three can differ on one document, so each answer names its frame on screen.

The portion above shows how. Its frequency is never stated, so after removing the deployment site it could be U (frequency at or below 10 GHz) or C (above it, firing Alpha's band floor through the alias). So C and U are both reachable, the safe mark is C, and nothing is entailed — the level ranges U–C. Ask for the mark when you want the level a document would actually be marked at; reachability answers a weaker question on purpose.

The instructive failure

Now ask the same question about a portion that does reveal waveform X. The waveform is what the portion is about, so it is not something you can redact.

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.

Whether any subject could reach it is a different question — ask "Is an outcome reachable at all?" under "About these rulesets".

Blocked by Revealing waveform X is SECRET.

Each blocker carries the reason it is one, where the solver has it to give — "no rule in scope raises this beyond the floors that fired" rather than only the name of the thing that blocked. A blocker named without a reason is worst on exactly the questions where it matters most: ask for a level the rules cannot produce and the bare name is the claim you asked about, which tells you nothing.

Which is the other half of this answer. When the outcome is out of reach for every subject, the pinned question says so instead of pointing at the any-subject question:

Not reachable for this document as it stands. …

No input reaches that outcome under these rulesets, so this is not about this document: no rule in scope can produce it. Either a rule is missing or the outcome is unused.

That is the answer worth having, because it settles the follow-up rather than posing it: no redaction of this portion reaches the outcome and none ever would. It is the same fact verification reports as verdict_unreachable, checked here against the rules alone — with no extracted values and no redactions — so it is only ever said when it is true of the rules.

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 has to be rewritten.

Unreachable here is not unreachable ever

Abduction on a pinned document runs with that document's answers already bound, so it can only propose values for claims the runs left free. Ask for a value that contradicts an answer a run gave and the outcome is unreachable by construction, whatever the rules allow.

That is why the wording is scoped: with a document pinned the answer says "for this document as it stands". It points at the any-subject question unless it can already settle it — when the outcome is unreachable for every subject, the pinned answer says that outright rather than deferring, because it is checked against the rules alone. What the pinned question never does is infer the stronger fact from its own failure. To explore a change to an answer a run gave, use "What if an answer were different?", which is what injection is for.

Which values would keep the outcome?

Take a portion that states the band, names no deployment site, and never states a frequency. Claim sys.operating_frequency, outcome clas.portion_level = U (0). The answer is a region, not an example:

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

That region comes from Alpha's band floor reached through the alignment axiom — band mentioned and above 10 GHz forces at least C — combined with the registry's own lower bound of 0 on the frequency claim. Delete the axiom and the region opens up, because Alpha's boolean would have nothing to do with the number.

In Mode A, ask this about a claim the selected runs left free. Asked about an answered claim it is a tautology: a bound claim's feasible region is its own value.

A region arrives in one of two shapes, and both are rendered. A real-valued claim comes back as a hull of intervals, as above; where that hull may contain gaps it is badged approximate, which is the honest label, because a hull presented as an exact range is a quietly wrong answer. A claim with a finite domain — a boolean, an enum, or a short integer scale such as an ordered verdict — comes back enumerated, and each allowed value is spoken in the claim's own vocabulary. An enumeration that hit the solver's cap is labelled "and possibly others" rather than presented as the complete list.

This question is not a verdict, so completion policies do not apply. The answer is the constraint region.

About these rulesets

Switch to About these rulesets. The pin is released, nothing is bound, and the catalog changes. No run is needed for anything below.

Can these rulesets ever contradict each other?

No parameters.

Yes — 1 collision exists.

conditional · inter_ruleset

• Revealing waveform X is SECRET. alpha.waveform_floor@1 · scg.alpha
• The existence of waveform X, standing alone, is UNCLASSIFIED. bravo.waveform_alone_u@1 · scg.bravo

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

That last paragraph is the witness, and it is the point of the whole answer. It is not a dump of every claim in the slice; it is the class of inputs that triggers the collision, reduced to the literals the finding actually depends on and rendered from the claims' own glosses.

Read it and the disagreement is obvious. Alpha floors a portion revealing waveform X at S. Bravo caps that same portion, standing alone, at U. There is no level that satisfies both. Neither rule looks wrong in isolation, and both are faithful transcriptions — the contradiction lives in the pair.

Two conflict kinds are reported. unsatisfiable means the rules cannot be complied with at all, whatever the input. conditional — this one — means there is an input class under which the level the rules determine violates one of them. The inter_ruleset classification is what routes it: resolving this needs both guides' owners in the room, and Corpus Health is where the decision gets recorded.

Why that finding needs no document

Nothing was pinned. No document was read. The answer was produced by solving over the rules, so it covers every input that could ever arrive — including inputs nobody has written yet. That is a stronger statement than any run can make, and it is available the day the rules are written.

A corpus can carry a live contradiction and still mark every document in front of it perfectly well, which is exactly why finding it takes a data-free check.

Is an outcome reachable at all?

Outcome clas.portion_level = TS (3):

Not reachable. No input satisfies that outcome under these rulesets.

Blocked by The classification level at which this portion must be marked — no rule in scope raises this beyond the floors that fired

On a four-level scale, a level no input can reach is either a missing rule or an unused level, and both are worth knowing before the scale is published. Corpus Health checks the same property as verdict_unreachable across every declared scope profile.

Ask it about C (1) instead and the answer is the opposite shape:

Reachable.

The smallest input that reaches it

• The portion names a deployment site must be no
• The portion reveals that waveform X exists must be no
• The portion states the operating band must be yes
• The operating frequency the portion states, in GHz must be 11

Reaching the middle of a scale means clearing everything above it as well as triggering something, and the minimal entailing assignment shows that plainly. The frequency the solver picked is one concrete member of the class — any value above 10 GHz does the same job — not a threshold in its own right.

Is a rule already redundant?

Pick a rule from the selected rulesets. The answer arrives in three buckets:

What it contradicts — Nothing — it can be honoured alongside every rule in these rulesets.

What it makes redundant — Nothing.

What it makes unreachable — Nothing — every verdict level a rule here can produce is still reachable.

When a rule is subsumed, the severity depends on where the two rules live. Across rulesets it is reported as info — the same requirement genuinely appearing in two policies is expected, and deleting either would lose an authority citation. Within one ruleset the identical finding is a warning, because there it is usually an authoring mistake.

This check re-runs the rule against its own neighbourhood, which is why it also tells you what the rule contradicts and what it makes unreachable. It is the read-only sibling of the next question.

What would a proposed rule break?

Paste a DSAIL assertion, give it a one-sentence summary, and say how it bears on the verdict — Constraint (bounds nothing), Floor (raises the verdict), or Ceiling (caps it). A floor or ceiling must name the ordered claim it bounds. The draft is checked against the selected rulesets and is never saved; it exists for the duration of the request.

The answer uses the same three buckets. A draft that does not compile against the registry gets the honest version instead — "That rule does not compile against this registry, so nothing can be concluded from it" — with the faults listed, because a rule that will not parse cannot be reasoned about.

Re-verify first

The check subtracts findings that were already present, using the last stored verification report for the current slice. When there is no such report — because the corpus changed since the last run — there is nothing to subtract against, and a pre-existing finding can read as something your draft introduced. Run Re-verify on Corpus Health first, then come back. The count of findings that were already present and are not attributed to the draft is shown at the foot of the answer.

Which values are consistent with the outcome?

Asked about a boolean with no document bound, the answer is the enumeration: The portion states the operating band with outcome U (0) comes back Allowed: yes, no — a portion can mention the band and still be U, provided the frequency is at or below 10 GHz. Ask the same question about the frequency instead and you get the interval that makes that true.

The Mode A and Mode B versions of this question differ in exactly one way: Mode A has the document's answers bound, so its region is tighter. Both are correct; they are answers to different questions.

---

Reading an Answer

Every answer, whatever the question, carries the same frame.

Part	What it is
The question	The question as it was actually asked, every parameter resolved, so you never reconstruct it from the form controls
Advisory — not a determination	Always present, on every answer, whether or not anything hypothetical was injected
Verified	Which engine answered, and whether it was solver-confirmed
Over …	The corpus ruleset refs the answer was computed over — pinned to a version where the ref names one, and unversioned where a ruleset version declared it that way
Scope: …	The context tags the slice was resolved under, or "every context (no scope tags)"
The body	The parts described per question above
Warnings	Compilation and resolution warnings, each as a sentence — for example a rule pinning a claim version below the registry's current one. Internal codes are never printed
The solver budget ran out…	Shown when the answer is partial rather than complete. Every operation reports it the same way — status unknown with timed_out: true and a warning naming the stage — and none of them answers no on a proof it did not finish: a conflict scan that ran out of budget says so rather than reporting a shorter list of conflicts as the whole of them
What exactly did I ask?	The disclosure described below

A narrowed slice is never served as a proof

Several answers here are universally quantified: "No — no input can make these rulesets contradict each other", "Not reachable. No input satisfies that outcome", "No value of that claim is consistent with the outcome". Each is a proof, and each is only ever a proof about the slice the solver actually saw.

So when the slice was smaller than the rulesets named on screen — scope tags excluded a rule, a chosen ruleset contributed none, a bound claim was not in the slice — the answer does not make the unqualified statement. It says the result holds across the rules that were in this slice, and carries a panel naming what was left out and why. The caveat sits with the headline rather than in the warning list below it, because by the time a reader reaches the warnings they have already read the answer.

Verified, and what the badge would say otherwise

The badge reads Verified when the SMT solver produced and confirmed the answer. The design allows for an approximating engine to answer interactive questions faster, in which case the badge reads Fast preview and the answer is not presentable as anything at all. Today every answer on this surface is solver-computed, so the badge reads Verified on all of them.

What exactly did I ask?

The disclosure at the foot of every answer repeats:

• the resolved question sentence;
• Runs read — each selected run's ruleset ref, with (behind current) on any whose ruleset has moved on;
• Rulesets — the corpus refs, pinned;
• Subject — the document and how many extracted values were bound, or any subject — no values bound;
• Slice — the slice hash;
• Full attestation — the stored record: every pinned version, each claim's origin, the engine, the signature and its algorithm, the request hash, and the timestamp.

This is the reproducibility affordance. The slice hash is the identity of a corpus configuration, so two answers computed under the same hash are comparable, and an answer whose hash no longer matches the current corpus was computed against a corpus that no longer exists.

What Analysis does not show you

Two things, so you do not go looking for them.

The mark has no always-on explanation panel. The chip is the level. The rules holding it there are reachable through the questions — the load-bearing answers, the blocking rules on an unreachable downgrade, the core on a disagreement — but there is no permanent "why this level" panel beside the chip.

There is no document pane. Analysis reasons over claim values, not text. Claim values carry provenance back to the document they were read from, and that provenance travels into the attestation record, but there is no highlighted-span view on this surface. Read the text on the project's Documents page, and the extracted answers in the run's own Evaluation tab.

Limits

Stated plainly, because each is a design decision rather than a gap to work around:

• One subject at a time. Analysis never answers across a document set; the tab pins exactly one document.
• It never evaluates. No claim is extracted, no document is re-read, no LLM is called. If a value is missing, the fix is another run — not another question.
• It changes nothing you are reasoning about. Hypothetical values and proposed rules are not persisted, the document is untouched, the corpus is unchanged. It is not silent, though: every answer writes one immutable attestation row — the question as asked, the answer returned, the pinned versions, the slice hash, who asked and when — and an audit entry that surfaces in Activity → Logs. Asking is recorded; nothing you asked about is altered.
• Advisory, always. For a verdict, use a Run.
• A question large enough to run as a background job reports that instead of an answer, and the result appears in Activity. Nothing this tab sends today crosses that threshold: it always names its rulesets and pins at most one subject, which are exactly the two conditions that keep a request synchronous.

Supplementary: the same questions over the API

For integrations, not for using the product

Everything above is the UI. The same reasoning is available over the REST API for callers that need it — a nightly re-check, a gate in a pipeline, an agent that must validate before it asserts. The endpoints are the ones the tab itself calls.

Question in the catalog	Endpoint and mode
What if an answer were different?	POST /api/v1/corpus/whatif, mode whatif_forward
What would have to change?	POST /api/v1/corpus/whatif, mode whatif_backward
Which answers is the outcome load-bearing on?	POST /api/v1/corpus/whatif, mode levers
Do the rulesets disagree?	POST /api/v1/corpus/validate
Which values would keep / are consistent with the outcome?	POST /api/v1/corpus/solve, mode feasible
Can the rulesets contradict each other?	POST /api/v1/corpus/conflicts
What would a proposed rule break? / Is a rule redundant?	POST /api/v1/corpus/preflight
The mark itself	POST /api/v1/corpus/solve, mode mark
The lowest / highest level the rules admit	POST /api/v1/corpus/solve, mode lowest / highest

The mark has its own mode, and minimize is retired. An objective is a fact about the constraint region — lowest is the lowest value the rules admit, highest the highest, and neither takes a completion policy. mark is the verdict about a subject, and unknown_policy is how the claims nobody answered get resolved before there is one. The four modes are here; every answer says which end of the range it returned in optimum.resolved_at.

A question about no particular subject — the Mode B form — is expressed by sending one unconstrained context, which leaves every claim free. Full field-by-field detail is in the Corpus API reference.

Related Concepts

• The Corpus — claims, axioms, ordered verdicts, floors and ceilings, mosaics, scopes, and slices
• Corpus Health — the standing data-free verification of the rules against each other, and where a conflict is dispositioned
• Vocabulary Workbench — the registry, the merge queue, and authoring the axioms this reasoning depends on
• Runs — production evaluation, which produces the values Analysis reads and which Analysis never touches
• SCG Portion Marking Tutorial — build the corpus these examples run against
• Corpus API — the endpoints behind every question on this page