RFD 0090 — In-body determinedness tests: a check-plane operator over the undetermined verdict

• State: committed (owner decision, 2026-07-24) — adopted over the declaration-level disposition attribute #[undetermined(block | pass | report)], the rival surface this record considered and rejected (its design, and the full comparison against it, are recorded here — D4, the comparison table, and the before/after table; its implementation was drafted in pull request #1840, closed unmerged with the branch preserved). That attribute is the superseded alternative for the disposition surface; the two designs share one foundation — the honesty gate of RFD 0086 slice 1 (pull request #1826), which makes undetermined a first-class verdict — and that foundation ships regardless of this decision. Implementation of this RFD is open, not merged: pull request #1848, stacked on the honesty-gate base.
• Opened: 2026-07-24
• Decides: that the per-check disposition of an undetermined membership verdict is expressed in the check body, by a determinedness test — a body atom undetermined(A) (and its dual determined(A)) that reads the converged model and holds iff the membership atom A’s verdict is not definite there — a well-founded standoff, or, for an open-world concept, an unrefuted absence of evidence (D1) — rather than by a declaration-level attribute. The operator is check-plane-only: checks are post-fixpoint consumers, so reading Can-ness in a check body is sound (D2); the same operator in a derive/query body is truth-value reflection feeding the fixpoint (circular, unsound under the well-founded semantics) and is refused (D2, OE1431). A check body that uses a determinedness operator yet leaves some membership atom’s Can-ness routed to no clause — the check’s firing verdict can still be Can on that path — raises an exhaustiveness warning (OW0744, D3, armed per-body: the analysis runs only on checks that use the operator, and then holds every membership atom of that check to explicit disposition) and falls through to RFD 0086 slice 1’s severity-derived default. An operator-free check body is not armed and never warns: it takes the same severity-derived default as a check under RFD 0086 slice 1 alone, silently.
• Affects: the check-declaration grammar and body vocabulary (a new body-atom form); the parser, lowering, and check-discharge planes (oxc-syntax, oxc-check, oxc-runtime); the check-rule registry (RFD 0081) — a new static well-formedness row (the plane-boundary refusal) and integration with the existing honesty-gate inventory row; the well-founded-semantics mechanization (spec/lean/Argon/Reasoning/Checks.lean). No Core-IR extent representation change — the operator reads the existing three-valued model, exactly as RFD 0086’s gate does.
• Builds on: RFD 0086 (the honesty gate — the shared base; read it first), RFD 0025 (check discharge; K3 “fire on is only”), RFD 0017 / RFD 0070 (defined-concept membership), RFD 0081 (the check-rule registry), RFD 0028 (the defeat plane’s undefined-by-decision cycles).

In plain language

Argon’s membership questions are three-valued. “Is x a member of computed concept C?” can come back yes, no, or undetermined — the evidence is absent, or the classifying rules sit in a negation/defeat standoff the well-founded semantics resolves to undefined (Can), not to true or false. RFD 0086 establishes that a check whose verdict hinges on an undetermined membership must not guess: undetermined is a first-class verdict, and each check decides what to do with it. That much is shared base and not in question here.

The question this record settles is how the modeler expresses that decision. One answer is a declaration-level attribute — #[undetermined(block | pass | report)] written above the check, one policy for the whole check. This record considered that surface, rejected it (D4), and answers differently: with an operator in the check body. You write undetermined(A) (or its dual determined(A)) as an ordinary body atom, and the check body itself branches on it. Because a check runs after the fixpoint has converged, asking “is this membership undetermined?” in a check body is the same sound read the RFD 0086 gate already performs internally — the operator just names it in the surface.

Why put it in the body rather than on the declaration? Because a body can express things an attribute cannot. A statutory tie-breaker ladder — “if residency is undetermined, fall back to the domicile test; if both are undetermined, block” — is a cascade of conditions the single-policy attribute cannot state. A data-quality check can route undetermined memberships to a report head while definite violations block, in one check. The attribute forces one disposition per check; the body operator lets one check carry several, each guarded by which membership is undetermined.

The cost is real and this RFD does not hide it (see Maintainability). The attribute is nearly free in the compiler — one recognized word, one lookup. The body operator is a new expression form threaded through parse, lowering, and discharge, plus a new coverage analysis that warns when a check leaves some undetermined path unhandled. The two designs also read differently to a human: the attribute is trivially grep-able for governance (“show me every deliberately-lenient check”); the body operator recovers that only by making the compiler report each check’s inferred disposition. The body operator buys expressiveness at a maintainability price. This RFD lays both out; the trade was settled for the body operator (see State).

The shared base (not in question)

Both designs stand on RFD 0086 slice 1 (pull request #1826):

1. The three verdicts, never collapsed (RFD 0086 D1). For each candidate violation tuple, discharge distinguishes definite violation (body holds under wfTrue — fire on is), definite non-violation, and inconclusive (the firing verdict hinges on a membership atom that is Can). Inconclusive is exactly wfPossible ∖ wfTrue lifted to the check head — mechanized as bodyHoldsPossible ∖ bodyHoldsK3 in spec/lean/Argon/Reasoning/Checks.lean on the slice-1 branch.
2. The default disposition, severity-derived (RFD 0086 D3 defaults column). An unhandled inconclusive tuple blocks on Severity::Error (OE1430), reports at undefined grade on Warning/Info or #[observe], and is not emitted for an => emit check. This RFD reuses that default exactly — it is what an unhandled path in a body falls through to (D3).
3. Admission-point discharge, point-free honesty, registry integration (RFD 0086 D2/D4/D6/D7). Unchanged and orthogonal; this RFD is a consumer of the same converged model at the same admission point.

The only thing this RFD replaces is the surface for per-check disposition — the declaration-level attribute. Everything else is shared.

Design

Terms are RFD 0086’s. A membership-gated check is a check whose violation body consumes membership in an iff/shape-defined concept. A standoff is a membership verdict the well-founded semantics leaves undefined (Can) at a point. A below ranges over membership atoms of the check body — x : C, not x : C, or the predicate spelling C(x) over a computed concept.

D1 — The determinedness test as check-body syntax

A determinedness test is a body atom over a membership atom A of the check. It reads the converged three-valued model and its truth is fixed by A’s verdict at the discharge point:

Two sources of indefiniteness, and the operator reads both. A verdict is left indefinite by a well-founded standoff or by absence of evidence under an open world, and the two are independent:

This is exactly the classification the four-valued assert [not] derivable verdict computes over the same model (§6.9 / RFD 0045; RFD 0010 for the refutation carrier). Two surfaces reading one model must not disagree about which subjects it decides, so the four inputs — the extent, the well-founded undefined companion, the refutation extent, and the concept’s world — are read once per surface against the same rule rather than one surface re-deriving a narrower one. A denotation over wfPossible ∖ wfTrue alone would be the standoff row only, and would report open-world absence as decided — the opposite of the world-assumption semantics.

Under an open world the undetermined region is therefore every subject that is neither an established member nor refuted, with no narrower domain: that is the manual’s reading of absence, and the assertion surface applies it to any tuple. Two consequences are worth stating rather than discovering:

• The region an implementation materializes is bounded by the individuals that exist in the model read. That bound is not a semantic narrowing — every binding a body can produce comes from an extent or a declared individual, so no subject outside it is addressable — but it does mean an undetermined(C(x)) whose subject is bound by nothing else in the body ranges over the whole population.
• Argument shape: the atom takes a membership atom over ONE subject (D5). For a wider tuple the open-world region would be a product of that population, which is neither a set worth materializing nor a shape a membership atom has, so the compiler refuses it rather than silently answering the standoff-only question.

determined(A) ≡ not undetermined(A); both spellings ship so a body reads naturally either way (determined(residency) in a positive guard, undetermined(...) in a fallback). The atom is a predicate over a membership atom, not over an arbitrary term — its argument is syntactically a membership atom of the same check body (D5 constrains the argument set).

Spelling — candidates recorded, one chosen. Three surfaces were considered against the existing body vocabulary (the predicate spelling C(x), the type-test x : C, the reflection intrinsics iof/extent/implements — all function-call-shaped atoms over the model):

1. undetermined(A) / determined(A) — an intrinsic-predicate atom, sibling to iof/extent/implements (function-call atoms that read the model in a body). Chosen. It reuses the exact vocabulary word the rejected declaration-level attribute spends (undetermined), so a reader who knows one knows the other, and the two designs’ surfaces are directly comparable — which is the point, since one supersedes the other. It is grep-able (\bundetermined\() and composes as an ordinary conjunct.
2. A is undetermined / A is determined — a postfix modal spelling on the reserved is keyword (reserved today, no active grammar rule). Reads as prose but introduces a second is-form and a state-word lexicon (undetermined, determined) in operator position; rejected to avoid a bespoke postfix grammar for one operator.
3. A? postfix / possible(A) — rejected: ? collides with optionality (T?, Truth4Of<T>), and possible names wfPossible (true-or-undefined), not the Can-only residue this operator needs.

The chosen form is used throughout below, fenced argon,ignore.

D2 — The load-bearing boundary: check-plane-only (soundness)

This operator is legal only in a check body. In a derive/query body it is refused (OE1431). That free-slot check has since been carried out: the code space immediately around the honesty gate proved collision-prone exactly as anticipated, and the allocated codes are the ones recorded in “New-syntax inventory” below.

The soundness argument is the whole RFD, so it is stated precisely.

A check is a denial rule over the well-founded model (RFD 0025): it is a consumer that runs after the WFS fixpoint has converged and contributes no facts back into it (Cat3 — observers, not derivers). At that point the three-valued model is a fixed object: every atom’s verdict is settled as wfTrue, wfFalse (∉ wfPossible), or Can (wfPossible ∖ wfTrue). Reading Can-ness here is reading a converged value — exactly the read RFD 0086’s honesty gate performs internally to compute bodyHoldsPossible ∖ bodyHoldsK3. The operator surfaces that read; it adds no new access to the model, only a name for one the gate already uses.

In a derive body the same read is truth-value reflection feeding the fixpoint. A derive rule contributes to the model; a body atom that branches on whether some atom is currently undefined lets the rule’s own output depend on the in-progress undefinedness of the model it is helping to compute. That is a non-monotone self-reference the well-founded semantics has no fixpoint for — the classic reason WFS forbids reading Can as a value inside the very fixpoint that produces it. undetermined(A) inside a derive would let a rule fire because A is not yet decided and thereby change what A is decided to be: circular, and unsound. So the operator is refused outside the check plane, structurally, not by convention.

What “structurally” obliges of the implementation. Three properties, each of which a narrower refusal would have failed:

1. One enforcement point, not one per caller. The refusal fires at the entry of the rule-body reference-resolution pass — the only place the operator’s intermediate becomes an executable read of the undetermined region — and that pass takes the body’s plane as a REQUIRED argument. A body lowering added later cannot admit the operator by forgetting to wire a refusal, because there is no plane value meaning “unstated”. This covers the standpoint bridge body, whose rules derive into a target standpoint and so contribute to the fixpoint.
2. At any container depth. The refusal searches the whole atom, so a spelling nested inside a negation, an aggregate, a modal, or a temporal atom is refused as the top-level spelling is. not determined(A) matters in particular: the operator’s own lowering already spells determined as a negation, so the written not makes it doubly negated — semantically identical to the undetermined(A) one spelling away, and equally refused.
3. The names are reserved, not merely captured. Recognition claims a single-segment undetermined(...) / determined(...) call before name resolution runs, so a user declaration of either name would be silently unreachable and its own call sites refused with a message about membership atoms — describing a program the author never wrote. Both names therefore join the reserved-intrinsic list, alongside the identifier-lexed reflection intrinsics, and such a declaration is refused at the declaration (OE0704).

Semantic anchor (Lean). The K3 “definitely” modal this operator exposes is confined to consumers by construction. spec/lean/Argon/Reasoning/Checks.lean (on the RFD 0086 slice-1 branch) already partitions atoms into the wfTrue region and the wfPossible ∖ wfTrue region and defines bodyHoldsPossible/bodyHoldsK3 over the converged wfPossible/wfTrue of P.ground. undetermined(A) denotes membership of A’s ground instance in wfPossible P.ground ∖ wfTrue P.ground — a predicate over the converged model, well-defined precisely because the check plane reads P.ground after it exists. There is no corresponding well-defined denotation inside the fixpoint’s own iteration, which is the mechanized statement of why the derive-plane use has no meaning to give it.

D3 — Exhaustiveness over undetermined membership (a coverage warning)

A check body that branches on undetermined(...) can leave a hole: some membership atom’s Can-ness routes to no clause, so the check’s firing verdict is still Can on that path. A three-valued coverage analysis over the check body detects it and warns (OW0744):

not exhaustive over undetermined membership in C; the default applies.

When the analysis is armed (the firing rule, stated precisely). OW0744 fires only on partial handling — a body that uses a determinedness operator yet leaves a Can path unrouted. The precise rule:

1. Arming is per-body. The coverage analysis runs on a check declaration iff some clause of that check contains undetermined(...) or determined(...). A check body that uses no determinedness operator is not armed and never warns — its Can disposition is the RFD 0086 slice-1 severity-derived default, which is a deliberate, sound fallback, not an exhaustiveness defect (see the consistency decision below and Example 4).
2. Once armed, every membership atom is in scope. For an armed check, the analysis considers every membership atom M the body depends on — not only the ones an operator names. Using a determinedness operator anywhere in a body is the modeler signalling intent to dispose of undecidability explicitly; the analysis then holds the whole check to that intent. Starting a case analysis on one membership and staying blind to another standoff-capable membership in the same check is exactly the hole OW0744 catches.
3. The uncovered-path test. For each membership atom M of an armed check, warn (once, naming M) if the conservative analysis finds — or cannot disprove — a feasible body path where (a) M is Can, (b) that uncertainty leaves the check’s overall firing verdict Can, and (c) no clause routes that path to a definite outcome: fire, don’t-fire, an explicit report clause, or an explicit acceptance of the default (a clause routing undetermined(M) to the check’s own default disposition — e.g. undetermined(M) => block on an Error check — which silences the warning by making the fallthrough intentional and visible). Mere occurrence of undetermined(M)/determined(M) does not establish coverage; the guard must cover the relevant Can path.

The analysis is syntactic and conservative (see Maintainability — this is the identified rot-prone hot spot, deliberately kept dumb). When unsure it warns — it never proves coverage it cannot see. Warning-only, so a conservatism bug never blocks a build.

Why per-body and not per-atom: per-atom arming would make OW0744 nearly vacuous (guarding undetermined(M) already routes M’s only interesting Can state, so the atom you guarded is covered by construction) and would forbid the flagship cross-atom warning of Example 3 — the useful signal is precisely “you handled one membership’s undecidability but left another’s unrouted in the same check.” The apparent cost of per-body — adding a guard for M can surface a warning about a sibling N — is the intended behavior: it reminds the modeler that N is also standoff-capable and undisposed, at the price of one clause. The blast radius is bounded to checks that already opted into determinedness handling (a small minority), which is categorically unlike warning on the whole operator-free corpus.

The default for an unhandled path is RFD 0086 slice 1’s severity-derived behavior, exactly (the shared base, item 2): an uncovered Can path on a Severity::Error check blocks (OE1430); on a Warning/Info/#[observe] check it reports at undefined grade; on an => emit check it is not emitted. This is a consistency decision, spelled out so the two designs agree on the fallback: whatever RFD 0086 slice 1 does for a check with no disposition handling, this design does for an un-handled path of an armed check — and, identically, for an un-armed (operator-free) check as a whole. An operator-free body here is behaviourally a plain RFD 0086 slice-1 check: silent, default-dispositioned. A body that handles every path never reaches the default and never warns; the warning is exactly the signal “you began disposing of undecidability here and did not finish, so slice-1 behavior takes over on this path.”

Firing-rule candidates considered (recorded, one chosen).

• Warn only on partial handling, per-body arming. Chosen (the rule above). Fires on armed-but-incomplete bodies; operator-free bodies silent. Consistent with RFD 0086 slice 1’s silent default, low-noise (bounded to opt-in checks), preserves the cross-atom Example 3 signal.
• Warn always (the literal reading of the uncovered-path test with no arming gate). Rejected. Taken literally — “some membership atom’s Can-ness routes to no clause → warn” — this fires on every operator-free check over any computed/defeasible membership, because such a check has, by definition, no routing clause. That warn-spams the entire existing corpus, all of which correctly relies on the sound severity-derived default: measured over the in-repo .ar corpus, of 18 non-fuzz check declarations only ~3 consume genuinely computed or defeasible membership whose verdict can be Can (and a dumb syntactic pass that cannot prove a base-marker type Can-free would flag up to ~5) — and every one of them would warn despite being correct. It also breaks the RFD 0086 symmetry (a plain slice-1 check is silent; an operator-free body here is the same thing) and inverts the failure-direction doctrine: a missed warning here is low-cost (the default is sound and loud where it matters — Error blocks the build), while a spurious warning on every correct check is pure noise that trains modelers to ignore the diagnostic.
• Per-atom arming (analyse only the atoms an operator names). Rejected. Makes OW0744 nearly vacuous and forbids the cross-atom Example 3 warning; see “Why per-body and not per-atom” above.
• Tiered: partial-handling default plus an opt-in strict lint level flagging every implicit fallback. Rejected for now. The house lint machinery (#[allow/warn/deny], [lints], -A/-W/-D) controls the level of an emitted diagnostic (suppress or promote), not an allow-by-default “pedantic” tier that turns a normally-silent condition into a warning. Introducing a strict “flag-every-implicit-fallback” lint is a separable future addition if demand is demonstrated; it must not change OW0744’s default firing rule, which stays the partial-handling rule above.

D4 — Relationship to the declaration-level disposition attribute (decided: Option A)

The rival surface is a declaration-level attribute #[undetermined(block | pass | report)], written above a check, fixing one disposition for that whole check. Two options for how this operator relates to that attribute were recorded. The owner decided for Option A on 2026-07-24: this RFD replaces the attribute; the attribute never lands. Option B is preserved below as the considered-and-rejected alternative.

Option A — this RFD replaces the attribute. The body operator is the one obvious way to dispose of an undetermined verdict; the #[undetermined(...)] attribute is removed (never lands past its draft, pull request #1840). The attribute’s one advantage — grep-able per-check governance (“enumerate every deliberately-lenient check”) — is recovered by making the inferred per-check disposition a reportable surface: the D3 exhaustiveness analysis already computes, for each check, what happens on each undetermined path, so the compiler can emit a per-check disposition summary (a build-time inventory, or ox surface) that a reviewer reads and greps exactly as they would the attribute. Governance moves from a source token to a derived, always-accurate report.

Option B — the attribute is kept as sugar. #[undetermined(block | pass | report)] remains, desugaring to a single body clause: #[undetermined(block)] becomes an implicit trailing undetermined(A) => block over the check’s membership atoms; pass/report likewise. The attribute is then the ergonomic shorthand for the whole-check case, and the body operator is the general form for the cases the attribute cannot express (ladders, mixed routing). One surface desugars to the other; both are documented, one is canonical.

The trade: Option A is one-obvious-way (no two surfaces to drift, no desugar to maintain) at the cost of removing a near-zero-cost, maximally-grep-able governance token and leaning on a report to recover it. Option B keeps the cheap common case cheap and readable but carries two surfaces and a desugar, re-introducing the drift risk the single-surface discipline (RFD 0084’s maintainability doctrine) exists to avoid. The decision is the one recorded above: Option A.

D5 — The argument set and interaction with defeat / aggregation

• Argument set. undetermined(A)/determined(A) take a membership atom A over ONE subject that occurs in the same check body. The static well-formedness rule (D6) refuses a determinedness test over a non-membership atom (a plain relation tuple whose undefinedness is not a computed-membership standoff), over a wider tuple (D1: the open-world region of a k-column predicate would be a k-fold product of the population), or over a term not present in the body — it is not a general “is this atom undefined” operator, it is a guard over the check’s own membership atoms.
• Defeat plane. A membership atom left Can by a mutual-defeat cycle (RFD 0028; OW0740) is exactly the case undetermined(A) names — the two honesty features agree (RFD 0086’s defeat-plane interplay example). The operator reads the converged post-defeat model; it does not compose with or re-run the defeat plane.
• Aggregation. A membership atom nested inside an aggregate body is not lifted (RFD 0086 D5); a determinedness test’s argument is a top-level membership atom of the check body. An aggregated standoff re-registers as OE1430 per RFD 0086 D5 unchanged — the body operator does not reach inside aggregates.

D6 — Registry integration (RFD 0081)

No parallel dispatch. Two rows:

• Static well-formedness of the determinedness test — a new rule validating that undetermined(...)/determined(...) appears only in a check body (the D2 plane-boundary refusal, OE1431), over a membership-atom argument of that body (D5), enters as a driver-wired BODY-axis row (it is a body-walk predicate over rule bodies, the registry’s Axis-1 category).
• The runtime honesty gate (the discharge that emits OE1430, later the point-free refusal, and now evaluates the body’s determinedness tests against the converged model) is the existing inline INVENTORY row from RFD 0086 D6, extended — not a new row. The gate already runs inside the write path over the post-state overlay where the three-valued model exists; evaluating undetermined(A) there is the same read it already performs, so the operator adds discharge logic to that inventoried site without inventing a dispatch table.

The exhaustiveness analysis (D3) is a static BODY-axis pass emitting OW0744; it is a warning-only sibling of the well-formedness row, reusing the same body walk. It is armed per-body (D3): the pass short-circuits on any check whose clauses contain no undetermined/determined operator, so the common operator-free check never enters the coverage analysis at all.

Comparison — the declaration-level disposition attribute vs. this design

Maintainability

The owner asked for this first-class and honest. The body operator costs more to maintain than the attribute; this section states where, and how each cost is contained.

New expression form through the pipeline. undetermined(...)/determined(...) is a new body-atom form that touches parse (a new atom production), lowering (a new Core-IR body-atom variant reading the three-valued model), and discharge (the gate evaluates it). Contrast the attribute: a recognized word and a lookup, no new expression form. Mitigation: one single check-lowering path through the check-rule registry (RFD 0081) — the operator lowers at exactly one site, and the BODY-axis well-formedness row (D6) is the only recognizer. No second surface lowers it.

The check-plane-only boundary as a standing invariant. D2 is a permanent rule: the operator must never become legal in a derive/query body, on pain of unsoundness. An invariant a future contributor could erode by “just allowing it in derives too.” Mitigation: one refusal gate (OE1431, the D6 BODY-axis row) is the sole authority on where the operator is legal, and a drift-style test pins that no other surface lowers the operator — the same discipline RFD 0084 uses to keep one canonical surface. The soundness argument (D2) is recorded in the RFD as the permanent why, so the re-litigation “why not derives?” has a standing answer rather than being re-derived each time.

The exhaustiveness analysis is the rot-prone hot spot. A three-valued coverage analysis over branching bodies is the kind of pass that accretes special cases and silently starts lying (claiming coverage it cannot actually prove). Mitigation: keep it syntactic and conservative — warn-when-unsure, never clever (D3), and armed per-body so it only ever runs on checks that opted into determinedness handling (operator-free checks — the whole existing corpus — never enter it, bounding the blast radius). It never proves coverage it cannot see; a false “not exhaustive” warning costs the modeler one explicit clause, a false “exhaustive” (silence) would hide a default fallthrough — so the analysis is biased to warn. It is warning-only (OW0744), so a conservatism bug never blocks a build; the worst case is a spurious warning, fixed by an explicit clause. This is the deliberate ceiling on the pass’s ambition.

Long-term scope-creep pressure. “Can we test determinedness in derives? in queries? over arbitrary atoms?” will recur. The RFD pre-answers: never, with the D2 soundness argument as the permanent reason. A determinedness read inside the fixpoint is circular under WFS; that does not change with implementation effort, so the answer is stable and the RFD is the citation.

User-code maintainability — both directions. The body operator makes cascading policies readable where the attribute cannot express them at all (a statutory ladder is one legible block instead of an inexpressible intent split across checks). The attribute makes governance readable — one grep enumerates every lenient check — where the body operator recovers that only via a report (Option A) or the retained sugar (Option B). Neither dominates; the trade is expressiveness-in-the-body vs. governance-in-a-token.

Contrast, stated plainly. The attribute’s compiler-side maintenance cost is near zero and it carries no standing soundness invariant. This design’s cost is a new expression form, a standing plane-boundary invariant, and a conservative coverage pass. That cost buys expressiveness the attribute cannot reach. The 2026-07-24 decision paid it: the expressiveness was judged worth the maintenance because each cost above is contained by a stated mitigation — one lowering site, one refusal gate plus a drift-style test, and a deliberately dumb warning-only coverage pass — while the expressiveness gap is not closable at any price, the attribute having no spelling for a ladder or mixed routing at all. The governance the attribute gave up is recovered by the inferred-disposition report (D4 Option A).

Worked examples

Proposed syntax is fenced argon,ignore; no outputs are fabricated. The shared base (RFD 0086 slice 1, pull request #1826) provides the three-valued verdict these bodies read.

Example 1 — the statutory tie-breaker ladder (inexpressible under the attribute)

Scenario. A residency determination has a statutory fallback ladder: decide residency by the primary-residence test; if that is undetermined, apply the domicile test; if both are undetermined, the return cannot be filed and the write is blocked. The attribute cannot state a ladder — it has one disposition for the whole check. The body operator states it directly.

pub type Filer;
pub type ResidentByHome    <: Filer iff { primaryResidenceMonths(self) >= 6 };
pub type ResidentByDomicile <: Filer iff { domicileState(self) == filingState(self) };

pub check residency_required(f: Filer) :-
    Filer(f),
    // primary test undetermined → fall back to domicile
    undetermined(ResidentByHome(f)),
    // domicile also undetermined → no honest verdict: block
    undetermined(ResidentByDomicile(f))
    => Diagnostic {
        severity: Severity::Error,
        code:     "Tax::E1200",
        message:  format!("residency undecidable for {} under both tests; cannot file", f),
    };

Meaning. The check fires (blocks, Severity::Error) exactly when both residency tests are undetermined. A definite resident under either test does not match the body (the guards demand undetermined(...)), so it does not fire. A filer determined by the home test alone is determined(ResidentByHome(f)), so the first guard fails and the ladder passes at the first rung. The cascade — home, then domicile, then block — is one legible body. Under the attribute this intent has no single-disposition spelling; it would have to be split across separate checks with duplicated bodies.

Example 2 — data-quality routing (undetermined reports, definite blocks, one check)

Scenario. Finance wants un-attributed payments on a worklist, but a payment whose cost-center attribution is definitely wrong (attributed to a closed cost center) is a hard error. One check, two dispositions keyed on determinedness.

pub type Payment { amount: Money };
pub type Attributed  <: Payment iff { exists c. costCenter(self, c) };
pub type MisAttributed <: Payment iff { exists c. costCenter(self, c) && closedCenter(c) };

// definite mis-attribution: block
pub check payment_attribution_hard(p: Payment) :-
    Payment(p), determined(MisAttributed(p)), MisAttributed(p)
    => Diagnostic {
        severity: Severity::Error, code: "Fin::E2051",
        message: format!("payment {} attributed to a closed cost center", p) };

// attribution undetermined: report, never block
pub check payment_attribution_report(p: Payment) :-
    Payment(p), undetermined(Attributed(p))
    => Diagnostic {
        severity: Severity::Warning, code: "Fin::W2052",
        message: format!("payment {} has undetermined cost-center attribution", p) };

Meaning. The first check fires only on a definite mis-attribution (guarded by determined(...), so an undetermined attribution never reaches the blocking head). The second routes an undetermined attribution to a Warning report head. Definite violations block; undetermined memberships land on the worklist. The attribute could give each check one disposition, but could not, within a single check, distinguish the definite-block case from the undetermined-report case keyed on the membership’s own determinedness — the body operator makes the routing the body’s job.

Example 3 — the exhaustiveness warning

Scenario. A modeler guards one undetermined path and forgets another.

pub check dependent_deduction_cap(f: Filer) :-
    DependentFiler(f), f.standardDeduction > money(1_250),
    undetermined(ResidentByHome(f)) => /* ... report ... */ ;
    // DependentFiler(f) itself can be `Can` and is not guarded here:
    // OW0744 — "not exhaustive over undetermined membership in DependentFiler;
    //           the default applies" (Severity::Error ⇒ block, per RFD 0086 slice 1)

Meaning. The body handles ResidentByHome’s undetermined case but leaves DependentFiler’s own Can path unrouted. Because the body uses a determinedness operator (undetermined(ResidentByHome(f))), the check is armed, and the analysis then holds every membership atom to explicit disposition — including DependentFiler, which the operator does not name. OW0744 names DependentFiler; that path falls through to RFD 0086 slice 1’s default for a Severity::Error check — block (OE1430). The warning is the signal that slice-1 behavior, not a body clause, governs that path. (This cross-atom warning is exactly what per-atom arming would suppress — see D3.)

Example 4 — the operator-free twin (silent, no warning)

Scenario. The same check without any determinedness operator — the overwhelmingly common shape, and every existing corpus check today. It consumes computed membership (DependentFiler, an iff/derive-defined concept whose verdict can be Can) but never mentions undetermined/determined.

pub check dependent_deduction_cap(f: Filer) :-
    DependentFiler(f), f.standardDeduction > money(1_250)
    => Diagnostic {
        severity: Severity::Error, code: "Tax::E1300",
        message: format!("dependent standard-deduction cap exceeded for {}", f) };

Meaning. No operator ⇒ the check is not armed ⇒ no OW0744, ever, even though DependentFiler(f) can be Can. The Can path takes RFD 0086 slice 1’s severity-derived default — here, Error ⇒ block (OE1430) — silently and soundly, exactly as a plain RFD 0086 slice-1 check does. This is the twin of Example 3: adding one determinedness operator anywhere in this body flips it from silent-default to armed-and-analysed. The warning is opt-in by using the operator; it never spams a check that relies on the honest default.

New-syntax inventory

These codes are allocated, not notional. The block immediately above the honesty gate proved collision-prone as this record warned it would: the default branch landed four unrelated endpoint diagnostics into the next free catalog slots and took the codes with them, one of which was the code the honesty gate had already claimed. All three codes here were therefore re-allocated together, verified free both on the default branch and on every open branch in the repository — checking only the default branch would have moved the collision onto someone else’s unmerged work rather than resolving it. The honesty gate itself is OE1430.

Before / after — expressiveness

Staging

Each slice leaves the tree green and changes nothing for a module with no determinedness test. All slices sit above RFD 0086 slice 1 (the shared base).

• Slice 1 — the operator + the plane boundary. Grammar for undetermined(...)/ determined(...); lowering to a Core-IR body-atom reading the three-valued model; the check-plane-only refusal (OE1431) as the RFD 0081 BODY-axis static row; discharge evaluates the atom against the converged model at the honesty-gate inventory site (RFD 0086 D6). Reuses the slice-1 gate; no new dispatch.
• Slice 2 — the exhaustiveness analysis. The conservative three-valued coverage pass and OW0744, armed per-body (runs only on checks that use the operator; D3); the severity-derived default fallthrough (D3) wired to RFD 0086 slice 1’s behavior for both un-armed checks and armed-but-uncovered paths.
• Slice 3 — the D4 relationship. Option A, as decided (D4): the attribute does not land, and this slice ships the per-check inferred-disposition report that recovers its governance grep-ability. Sequenced last because nothing above depends on it.
• Lean obligation (paired with Slice 1): spec/lean/Argon/Reasoning/Checks.lean gains the denotation of undetermined(A) as A ∈ wfPossible P.ground ∖ wfTrue P.ground over the converged ground model, and a lemma that this denotation is well-defined only over P.ground (the mechanized statement of the D2 check-plane boundary — no denotation inside the fixpoint iteration). Extends the slice-1 bodyHoldsPossible/bodyHoldsK3 partition.

Verification (per slice)

• A module with no determinedness test is byte-identical in check behavior (negative control).
• undetermined(...)/determined(...) in a derive/query body refuses OE1431; assert rejects(OE1431) pins it.
• Example 1’s ladder blocks exactly when both tests are undetermined; a filer determined under either test passes.
• An armed body (one using undetermined/determined) that leaves one membership’s Can path unrouted warns OW0744 and falls through to the RFD 0086 slice-1 default; a fully-covering armed body neither warns nor falls through.
• An operator-free body over a computed/defeasible membership whose verdict can be Can emits no OW0744 and takes the severity-derived default silently (Example 4) — the per-body arming negative control, and the parity check against an plain RFD 0086 slice-1 check.
• Arming is per-body: a body that uses the operator on membership A and leaves a sibling membership B’s Can path unrouted warns naming B (Example 3).
• The drift-style test confirms exactly one surface lowers the operator.

Alternatives considered

(a) The declaration-level disposition attribute (#[undetermined(block | pass | report)] above a check). The competing design (this whole RFD is the contrast). Near-zero compiler cost and maximal governance grep-ability, at the price of one disposition per check — no ladders, no mixed routing. See the comparison table. Rejected here in favour of the in-body operator (see State and D4). RFD 0086 rejects the same surface independently (its Alternative (d), on the ground that a declaration-level word cannot name which classifier or subject is undetermined) and names the in-body determinedness test as the successor shape, deciding only the default that successor deviates from.

(b) A general undefined(atom) operator over any body atom, any plane. Rejected on soundness: outside the check plane it is truth-value reflection into the fixpoint (D2), and over a non-membership atom it names a plain relational absence, not a computed-membership standoff — a different and less meaningful thing. The operator is deliberately narrowed to membership atoms in check bodies.

(c) A fourth severity (Severity::Undetermined). Rejected for the same reason RFD 0086 rejected it (its Alternative (e)): undetermined is a property of a tuple’s verdict at a point, not of the check. A per-tuple body guard is the right granularity; a per-check severity is not.

Open questions

• Per-atom vs. whole-membership granularity. The operator is defined over a membership atom A. Should it generalize to per-atom determinedness within a compound membership (e.g. the individual conjuncts of an iff body), or stay at whole-membership granularity? Finer granularity is more expressive but sharpens the D3 exhaustiveness analysis’s burden. Left open.
• Interaction with RFD 0087 view undefined regions. A check over a lifted view can read the view’s undefined region. Does undetermined(A) over a view-lifted membership atom read the view’s undefined region or the base model’s Can? The boundary between this operator and 0087’s undefined-region semantics must be coordinated before either ships a check over a lifted view. (RFD 0087 is pull request #1821; cross-reference at decision time.)
• The D4 choice (Option A vs. B). Decided 2026-07-24: Option A (see D4).
• Governance report shape (Option A). The attribute does not land, so the report carries the governance: what is the precise surface of the per-check inferred-disposition report — a build-time inventory, an ox subcommand, or both — so it matches the grep-ability the attribute gave up?
• Retroactive amendment re-introducing inconclusiveness. Inherited unchanged from RFD 0086 (its Worked-examples gap): an amend/retract that pushes an already-admitted tuple into a standoff. Orthogonal to the disposition surface, so the adoption of the in-body operator neither settles nor changes it.