RFD 0086 — Admission-point checks: honest verdicts over undetermined membership

• State: committed. The decision is fixed; implementation has landed in part on a branch and not yet on the default branch — the honesty gate (Slice 1) is implemented in pull request #1826 and is the base the remaining slices build on. Per-slice status is marked under Staging, and every transcript in this record says which binary produced it.
• Opened: 2026-07-23
• Decides: two user-facing semantics for a check whose violation body reads membership in a computed concept (an iff/shape-defined concept, or an asserted descendant of one). (a) Admission scoping — a membership-gated check is judged at the admission point of the data it governs (the valid-time instant a write asserts from, or the all-times view for an unqualified write), not against a single global snapshot; each check has a firing closure naming which writes and events can trigger it, so a write outside every closure runs no check discharge. (b) The honesty gate — when a membership-gated check’s verdict for a tuple hinges on membership the well-founded fixpoint leaves undetermined (three-valued Can — a negation/defeat standoff or an open-world absence), the check does not silently pass and does not fire as a false accusation; the outcome is a first-class inconclusive verdict whose disposition is decided per check, derived from the check’s declared severity: a blocking check refuses the write (fail-closed, OE1430), and a reporting check reports at undefined grade. A point-free judgment of membership that varies by valid-time point is refused as having no single honest answer. That refusal is unimplemented and deliberately carries no diagnostic code here; the slice that implements it allocates one.
• Affects: the runtime write gate and on-demand check surfaces (oxc-runtime); the check-rule registry (RFD 0081) — the runtime honesty gate enters as an audited inventory row; the well-founded-semantics mechanization (spec/lean/Argon/Reasoning/Checks.lean). No grammar change and no Core-IR extent representation change — the gate reads the existing three-valued model, and the disposition comes from a severity the modeler already writes.
• Builds on: RFD 0025 (check discharge; K3 “fire on is only”), RFD 0017 / RFD 0070 (defined-concept membership), RFD 0063 (the bitemporal read point), RFD 0081 (the check-rule registry), and the defeat plane’s undefined-by-decision cycles (RFD 0028).

In plain language

Argon lets you declare a check — a rule that says “this must never be true; if it is, refuse the write, or at least report it.” Separately, Argon lets you declare a concept whose membership is computed rather than typed in: an Adult is a Person iff age >= 18; an employee has badge access iff a chain of rules says so. Membership in such a concept is derived from evidence.

The problem this RFD closes: what does a check mean when its body asks “is x a member of computed concept C?” and the answer is not yet decided? Argon’s semantics are three-valued and open-world. A membership question can come back undetermined — the evidence is absent, or the classifying rules sit in a negation/defeat standoff that the well-founded semantics resolves to undefined (Can), not to true or false. Two naive behaviors are both wrong:

• treat undetermined as “not a member” and fire the check → a false accusation (“you have no badge access, therefore you violated the badge-required rule”) when the truth is simply unknown;
• treat undetermined as “member, no problem” and let the write commit → the system admitted a write whose legality it could not actually decide.

Today’s Argon does the second thing, silently. (See Context — this is measured, not assumed.) Admission-point checks make a third choice: undetermined is a first-class verdict, and each check declares what to do with it. A blocking check refuses the write, loudly, and tells the modeler to establish the classifying evidence or break the standoff. A reporting check reports it at undefined grade without blocking. Which of the two a check gets is read off the severity the modeler already declared — there is no new annotation to learn. That much is implemented and executed below.

The second half is when membership is judged. A computed concept’s extent changes over valid time (someone becomes an Adult on a birthday; evidence carries a validity window). A membership-gated check must therefore be judged at the write’s own valid-time point — the instant the write asserts from — not against the union of every valid time at once. When a modeler asks such a check on the all-times view and the membership genuinely varies by point, there is no single honest answer, and that is refused too, pointing the modeler at a specific point to ask instead.

Everything else — checks whose bodies touch no computed membership — is untouched. They keep the classic commit-time behavior exactly.

When an undecided membership stops you, and when it does not

The whole behaviour change lands at one moment: a write. Nothing about it is a build-time or check-time refusal, and none is proposed.

Exactly one cell moves. Three properties bound it:

• The declared severity chooses. Refusing versus reporting is decided by the word already on the check (D3). There is no new switch, and no global policy.
• Only what the write introduces. A tuple already undecided before the write cannot block it — the gate differences pre against post, so a standoff elsewhere never wedges an unrelated write (D3, delta discipline).
• The refusal is atomic. It is judged against a throwaway post-state overlay, so on refusal nothing has reached the committed store.

What this deliberately cannot give you: advance warning. Whether a check becomes undecidable depends on the data, not the program, so no amount of build-time analysis can tell a modeler “this check will stand off.” The design accepts that and spends its guarantee on the write instead — a loud refusal naming the check, the subject and the undecided membership, in place of a silent commit under a constraint nobody evaluated.

Question — what a modeler cannot state today

The distilled index of the examples below. Each row is one thing a modeler wants to state; LEFT is the closest the default branch gets, verified against the re-run probe in the next section; RIGHT is what the design gives, tagged with implementation status.

Context — the probe, re-executed

The soundness claim above is measured, not assumed, and it was re-measured for this revision against a compiler built from the current default branch. Every transcript in this record appears in this section, and each is verbatim output from that binary, or from the honesty-gate branch’s binary where a transcript is labelled as such. No transcript in this record is reconstructed from memory. Artifact paths are shown package-relative for readability; the runs used an absolute path, and where a long diagnostic is cut the cut is marked ….

What changed since the first revision. The re-run reproduced the defect, but three surface details in the original transcript no longer hold and are corrected here: source files carry the .ar extension (the original probe was written .ox); diagnostics and mutation names now render module-qualified (badge::badge_required, not badge_required); and the hiring write emits three events rather than one, because this probe’s inserted individual carries two mutable fields and each field assignment is its own event (the original inserted a fieldless individual). Event counts in these transcripts are a function of the program, not of the defect. One structural detail also changed: a content-carrying file may no longer open with mod NAME; to name itself — a module takes its name from its file stem, and mod NAME; now means only “a sibling NAME.ar exists”. The probe is therefore laid out as a package.

The program

A package with ox.toml naming src/root.ar as its entry. src/root.ar holds nothing but mod badge; mod report; mod strict;. The three modules are the three exhibits: badge carries the undetermined case, strict the two definite cases, report the reporting-severity case. All were built and run as one package; per-module sources are shown where each exhibit is discussed.

badge puts a computed classification in a negation cycle so that the well-founded semantics genuinely cannot settle it. keys_a (“has badge access”) holds by default for an employee, unless conflict_a; conflict_a holds exactly when keys_b does; keys_b holds by default unless conflict_b; and conflict_b reads keys_a back. No head directly defeats itself, so the defeat graph is acyclic and the program is admitted — but the rule-dependency graph cycles through negation, so neither head has a stable two-valued warrant and both surface undefined for every employee. This is the documented way to construct a genuinely inconclusive membership; it is not a contrived error state.

// src/badge.ar
use std::core::type;

pub type Person { mut employee: Bool, mut payrolled: Bool }
pub type Employee <: Person iff { self.employee == true };
pub type Payrolled <: Person iff { self.payrolled == true };

#[default]
pub derive keys_a(p) :- Employee(p);

#[defeats(keys_a(p))]
pub derive conflict_a(p) :- keys_b(p);

#[default]
pub derive keys_b(p) :- Employee(p);

#[defeats(keys_b(p))]
pub derive conflict_b(p) :- keys_a(p);

pub derive on_roster(p) :- Employee(p);

pub derive in_payroll(p) :- Payrolled(p);

pub query roster() -> on_roster;

pub query badge_holders() -> keys_a;

pub check badge_required(p: Employee) :-
    Employee(p), not keys_a(p)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Badge::E001",
        message:  format!("employee {} has no badge access", p),
    };

pub check roster_member_is_payrolled(p: Employee) :-
    on_roster(p), not in_payroll(p)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Payroll::E004",
        message:  format!("roster member {} is absent from payroll", p),
    };

pub mutate hire_bob() { insert Person { employee: true, payrolled: true }; }

The compiler admits the program — the first thing worth reporting, because it means the check really does get to run over an undetermined read rather than being refused beforehand. It warns, at length, that the two heads are undefined:

$ ox build .
workspace: elaborated 4 module(s) into one artifact
  ⚠ warning: OW0740: the public heads `badge::keys_a`, `badge::keys_b` form a
  │ mutual-defeat cycle: each head's live attacker derives, in turn, from that
  │ same head through its positive support (a rule-dependency negative cycle
  │ through defeat). This is NOT the identity cycle of two heads directly
  │ defeating each other (refused earlier by OE0718) — the defeat graph here
  │ is acyclic. Such a cycle has no stable two-valued warrant, so under the
  │ well-founded semantics these heads are UNDEFINED (neither definitely true
  │ nor definitely false) and surface as `Can` rows rather than a definite
  │ `Is`/`Not`. This is the canonical semantics, not an error — no evaluation
  │ order changes it. The warning names the mutually-defeating heads so an
  │ author expecting a definite verdict knows they read `Can`. To get a
  │ … (the remainder of the warning explains how to break the cycle)

wrote ./target/root.oxbin (54 events, 47184 bytes)

What the default branch does with an undetermined read — verbatim

Running the hiring write, and enumerating the declared queries with their four-valued row tags:

$ ox query target/root.oxbin --mutate badge::hire_bob --with-truth4
Badge::E001

  ☞ Badge::E001: [undefined] employee #i1 has no badge access [#i1]
  help: fired by check `badge::badge_required`

ran badge::hire_bob: 1 ops, 3 events emitted
query badge::badge_holders: 1 row(s)
  [Can] (#i1)
query badge::roster: 1 row(s)
  [Is] (#i1)
query report::clearances: 0 row(s)
query report::roll: 0 row(s)

Reading it. badge_holders enumerates keys_a, and its one row is tagged [Can] — the undetermined verdict, confirmed at the read surface rather than inferred. badge_required is declared Severity::Error, and its body not keys_a(p) is therefore also undetermined for #i1 — not definitely true. Under RFD 0025 D4 (“fire on is only”) an undefined violation does not fire, so it never reaches the D2 delta guard that a Severity::Error check blocks on (D3: severity drives blocking, and only a firing violation guards); it is delivered instead through the observe channel (RFD 0025 D6) — the residue the well-founded-semantics mechanization names undefinedObservations. So the violation surfaces as one [undefined]-graded note (☞ is the observe channel) — and the mutation commits (3 events emitted).

That is the hole. The check governs exactly this write; its verdict for this employee hinges on a membership the fixpoint left undetermined; and there were two honest options — refuse the write, or report the undecided verdict at a grade that gates — and it took neither. It admitted the write, and the Severity::Error the modeler wrote had no gating effect on the undetermined tuple.

The same check, the three determinacy cases, side by side

The claim needs a control: the gate is not simply absent. src/strict.ar is the same check shape and the same severity over a classifier that does settle — has_badge follows from a plain computed Cleared, with no cycle:

// src/strict.ar
use std::core::type;

pub type Worker { mut employee: Bool, mut cleared: Bool }
pub type Staff <: Worker iff { self.employee == true };
pub type Cleared <: Worker iff { self.cleared == true };

pub derive has_badge(p) :- Cleared(p);

pub check staff_badge_required(p: Staff) :-
    Staff(p), not has_badge(p)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Badge::E002",
        message:  format!("employee {} has no badge access", p),
    };

pub mutate hire_unbadged() { insert Worker { employee: true, cleared: false }; }
pub mutate hire_badged()   { insert Worker { employee: true, cleared: true }; }

A definite violation is refused, on the default branch, today:

$ ox query target/root.oxbin --mutate strict::hire_unbadged --extent strict::Staff
Badge::E002

  × Badge::E002: employee #i1 has no badge access [#i1]
  help: fired by check `strict::staff_badge_required`

Error:   × mutation `strict::hire_unbadged` rejected by check guard: 1 new
  │ violation(s) at `Severity::Error`

A definite non-violation commits, as it should:

$ ox query target/root.oxbin --mutate strict::hire_badged --extent strict::Staff
ran strict::hire_badged: 1 ops, 3 events emitted
extent(strict::Staff): 1 individual(s)
  #i1

So the write gate works and refuses on the error severity. Hold severity, check shape, and write shape fixed, vary only whether the classifier settles, and the third case — the badge module’s transcript above — silently commits. The defect is precisely and only the undetermined case; nothing about the gate’s plumbing is at fault.

The honesty gate on the same program — verbatim

The surviving half of this record is implemented on the honesty-gate branch (pull request #1826). Built from that branch and run against the identical package:

$ ox query target/root.oxbin --mutate badge::hire_bob --with-truth4
OE1430

  × OE1430: check `badge::badge_required` cannot be discharged for #i1: its
  │ firing verdict depends on membership `badge::keys_a` left undetermined
  │ (`Can`) by the well-founded semantics [#i1]
  help: fired by check `badge::badge_required`

Error:   × mutation `badge::hire_bob` rejected by check guard: 1 new violation(s) at
  │ `Severity::Error`

The refusal names the check, the subject, and the membership that could not be decided. It arrives through the same write-gate rejection channel as the definite violation above — the outer “rejected by check guard” line is identical in both — so a caller already handling a refused write needs no new error path, and assert rejects(OE1430) pins it in a negative-enforcement test. The write commits nothing — the command exits on the refusal, so the query enumeration that follows it in the default-branch transcript does not run at all.

The two definite cases are byte-identical to their default-branch transcripts on this branch. The gate changes exactly one of the three outcomes.

Blast radius — what one silently-admitted write becomes

The asymmetry between refusing and admitting is the whole argument, and it is not a rhetorical one. Follow the default-branch transcript above in three steps.

Step 1 — the write nobody decided is admitted. 3 events emitted. The only trace is the ☞ [undefined] note. It is printed, so it is not invisible at a terminal — but it is not an error and does not gate. The command exits 0 (measured), so a batch importer that checks exit status sees a clean run.

Step 2 — the undecided question is laundered into a definite fact. In the same transcript, in adjacent stanzas:

query badge::badge_holders: 1 row(s)
  [Can] (#i1)
query badge::roster: 1 row(s)
  [Is] (#i1)

badge_holders is still honest — [Can], undetermined. But on_roster derives from Employee alone, and #i1 is now a definite Employee, so the roster row is [Is]. Nothing downstream of on_roster can tell that this individual entered the population through an undecided gate. The undetermined verdict did not propagate; it was dropped at the admission boundary, and everything past that boundary reads a definite fact.

Step 3 — a later check is now confidently wrong. roster_member_is_payrolled is a second Severity::Error check over the same roster. Its body reads nothing undetermined — on_roster(#i1) is the [Is] row above, and in_payroll follows from the payrolled field the write asserted directly — so it renders a confident verdict, and in the transcript that verdict is a pass: it emits nothing at all. The only Severity::Error verdict the system now states about #i1 with any gating force is a pass. An operator reading the run sees one advisory note and one clean blocking check, and concludes the hire is compliant. The badge question was never answered; it was skipped, and the next check inherited the skip as a pass.

Extend those three steps to a running deployment and the cost is not local: payroll accruals fan out from Employee on the next period close; headcount and access-audit checks count an admitted population; every derived roster lists the hire. Unwinding it is not a delete, because the store is event-sourced — the hire event is durable history, and the accruals and roster memberships derived from it are their own committed facts with their own valid-time extents. Correction means issuing compensating events and reconciling everything that read the bad state in between, at a cost that scales with how long the bad event sat unnoticed. Refusing at the gate costs one rejected write and a fix to the evidence.

The failure-direction doctrine. The two directions of being wrong are not symmetric, which is why the default is fail-closed. A wrong admission is silent, compounds in durable history, and is read as settled by every consumer. A wrong refusal is loud at the write and fixable at the source: supply the classifying evidence, break the standoff so the concept settles, or lower the check’s severity to say the undetermined case is not a stop. Argon already applies this doctrine elsewhere — the open-world lints refuse to let a mutual-defeat cycle pass unremarked (OW0740 in the probe is one), the defeat plane names an undecided head undefined by decision rather than resolving it false, typed views refuse a silent coercion across a view boundary. A check reading undetermined membership was the last place the language still guessed silently.

Decision

Terms used below. A membership-gated check is a check whose violation body consumes membership in an iff/shape-defined concept — directly (x : C, not x : C, or the predicate spelling C(x)) or through the nominal upward closure (an asserted <:-descendant of a defined concept is membership-dependent). The admission point of a write is its valid-time instant (an operation-level at/since), else the all-times view. A standoff is a membership verdict that the well-founded semantics leaves undefined at a point — a negation/defeat cycle, or open-world absence of evidence.

D1 — The three verdicts, never collapsed

For each candidate violation tuple, discharge of a membership-gated check distinguishes three outcomes, and never folds one into another:

Inconclusive is a set of violation tuples, not of membership atoms: the head tuples that fire under a possible reading of the body (each positive atom needs only to be well-founded possible; each negated atom needs only that its subject is not well-founded true) minus the tuples that fire under the definite (is-only) reading. The membership-atom residue wfPossible ∖ wfTrue is what drives a tuple into that difference, lifted to the check head — the driver of the verdict, not the level at which the verdict is defined. The two forbidden collapses are: “undetermined ⇒ not a member ⇒ fire” (the false accusation) and “undetermined ⇒ silent pass” (the admitted-undecidable write, the Context exhibit).

Inconclusive is not the observe-channel residue, and the difference is the whole soundness content of the gate. The residue an Error check degrades to the observe channel today is the difference against the two-valued pass, whose positive atoms are read against well-founded truth; it is a strict subset of the inconclusive set. A tuple whose firing hinges on a positively undetermined membership fires under the possible reading but never enters the two-valued pass at all — so it carries no observe note, and a gate enforced over the observe residue would let it through silently. The mechanization states that containment (undefinedObservations ⊆ inconclusive) precisely so the two are not conflated: the gate is enforced over the inconclusive set.

D2 — Admission scoping (the firing closure)

A membership-gated check is judged at the admission point of the write under judgment, over the facts and rules visible at that point — not against a single committed base snapshot. The discharge reuses the existing point-parameterized read seam (the bitemporal read point of RFD 0063); it introduces no parallel evaluator.

Each membership-gated check has a firing closure: the transitive set of relations, concepts, and rule heads whose change can alter the check’s firing verdict, computed through the compiled rule bodies (the check body’s atoms, plus everything those atoms derive from, plus the membership classifiers’ cones). A write is judged against a check iff the write lands inside that check’s closure.

Scoping matters for two reasons. Precision: a module with no membership-gated check pays nothing; a write untouched by any check’s closure pays nothing. Honesty of time: a valid-timed write is judged against membership as of its own instant, so “was this employee an adult when the contract was signed” is asked at the signing date, not against the union of all dates.

Standpoint scoping is part of both the view and the check’s identity: a standpoint-scoped pub check discharges only over its standpoint’s view at the admission point, and its inconclusive-tuple bookkeeping is keyed by (check path, standpoint) — a scoped check’s inconclusive tuple never collides with a base check’s, and a sibling standpoint’s dated evidence cannot make a base check point-variable.

D3 — The honesty gate (disposition of an inconclusive verdict)

Only inconclusive tuples the judged write newly introduces are dispositioned — the same delta discipline the classic guard applies to violations. A tuple already inconclusive over the pre-state does not wedge an unrelated write.

The disposition of a new inconclusive tuple is decided per check, derived from the check’s declared severity. This table is implemented, and the two rows a transcript can exercise today are executed in the Context section.

The refusal contract. A block disposition that fires returns a classified refusal (OE1430) naming the check, the undetermined membership, and the subject, and assert rejects(OE1430) pins it in a negative-enforcement test — as the executed transcript in the Context section shows.

Rationale for per-check over a global default (measured in “Why disposition is per check”). A global fail-closed default (Alternatives (a)) is sound but too blunt: it converts every modelling gap in a long-lived open-world knowledge base into a hard write-stop, including cases the modeler has consciously accepted. A global pass default is the status-quo hole. Deriving the disposition from the declared severity keeps the sound default for the checks that must gate, keeps the reporting behavior for the checks that must not, and states the choice at the constraint itself — in a word the modeler was already required to write, so the disposition cannot drift away from the severity it belongs to.

D4 — Point-free honesty

Status: unimplemented. No refusal for this exists in the compiler on the default branch or on the honesty-gate branch; the gate as implemented judges at the all-times view unconditionally. Everything in this subsection is intended behavior, not measured, and no transcript for it appears in this record because none could be produced honestly.

This subsection names no diagnostic code, on purpose. An earlier revision reserved one by writing it here, and the default branch then allocated that number to an unrelated refusal — a code named only in a design record is a reservation nothing enforces, so the next entry allocated from the same range takes it. The slice that implements this refusal allocates its own code and records it in the diagnostic catalogue, which is the only place a code is owned.

A point-free (all-times) judgment of membership that varies by valid-time point is refused: the all-times view admits every valid time at once, so point-variable membership has no single honest verdict. Point-variability has three sources over the check’s membership cone:

1. committed evidence on a cone relation/concept/field carrying a bounded (non-all-time) valid-time window;
2. a rule-validity window on a cone rule clause (RFD 0056);
3. a clock-reading classifier (a cone rule reads the wall clock, e.g. today()).

A concrete point stays exact: judging at point t pins any clock reading to t’s own civil day, so a clock-reading classifier is decidable at the point. The refusal fires on three surfaces — the write path (an unqualified write landing in a point-variable check’s closure), the check-debug surface (ox derive <CheckName>), and the on-demand stored-check ask (one point-variable check refuses the whole ask, naming the check) — and is classified so assert rejects(...) observes it under whichever code the implementing slice allocates. The remedy the diagnostic teaches: ask the check at a specific valid-time point (at <t>).

D5 — Aggregated membership

The three-valued lifting (D1) is top-level over the body’s atoms; a membership atom nested inside an aggregate body is not lifted there. The reasoner already refuses to fold an aggregate over a relation carrying undefined atoms (OE1332 AggregateOverUndefined, pre-existing). Under admission, when that refusal lands on a membership-gated relation, it is re-registered as OE1430 so an aggregated standoff refuses in the same classified register as a top-level standoff, rather than surfacing as a generic reasoning error. It never folds undefined-as-false, never fires, never silently passes.

D6 — Registry integration contract (RFD 0081)

This feature does not introduce a parallel dispatch mechanism. It integrates with the check-rule registry exactly as that RFD prescribes — its one rule is a row in the one auditable table, tagged by axis and wiring. Because the disposition is read from the declared severity, there is no new declaration surface to validate statically, so this feature contributes no driver-wired row:

• The runtime honesty gate itself (the write-gate discharge that emits OE1430, and later the point-free refusal) enters as an inline INVENTORY row, not a driver-dispatched rule. This is exactly the registry’s category for runtime backstops (its inventory row for the program-global tuple-target resolver, OE0266): placement is semantic — the gate runs inside the write path over the post-state overlay, where the three-valued model exists — and cannot move into the check-pass walk without recomputing the model. The inventory row makes the gate visible in the same table (its codes, its axis-of-reach, the write-gate site) without pretending it is statically enumerable.

The contract in one line: the registry owns “where every check-pass rule runs”; admission adds one audited inventory row and invents no dispatch table of its own.

D7 — Resolution-pass boundary (non-goal)

This RFD’s discharge is a consumer of name resolution, never a rewriter of it. The prior implementation lineage of this feature (Alternatives (b)) died in a three-way collision in which admission, a typed-views lane, and a scope-tracking lane each rewrote per-scope name/severity state in the same resolution surface. To foreclose that, the boundary is stated as a hard non-goal:

• Reads, never rewrites. Admission reads resolved concept identities, the resolved <: ancestry (for the upward membership closure), resolved rule-head identities (for the firing closure), and the resolved standpoint owner of each scoped clause. It never rewrites a resolution verdict, never re-keys the resolver’s per-scope state, and never introduces a second scope-identity carrier alongside the resolver’s own.
• Severity is read from the declaration, not dispatched through resolution. The block/report disposition (D3) is computed from the check’s declared severity — present on the check declaration — and from nothing the resolution pass owns. Admission adds no “severity-dispatch” rewrite to the resolver.
• One identity key, and it is admission-local. The inconclusive-tuple delta index is keyed by (check path, standpoint) and lives entirely in the write gate. It is not a new per-scope identity type shared with resolution or with any other lane; if a future lane needs a shared per-check identity carrier, that is a separate reconciliation (Open questions), not a dependency of this RFD.

Rationale

Two load-bearing choices above are argued from the same probe: why the disposition is per check rather than one engine-wide policy, and why the judgment is scoped to an admission point rather than a whole-store commit-time pass.

Why disposition is per check, not one global policy

Two checks in the same program can want opposite treatment of an equally undetermined verdict, and this is measurable rather than asserted. src/report.ar is the counterpart to badge: the identical negation-cycle construction, so the classifier is equally undetermined, but the check is Severity::Warning because it states a vetting standard rather than a legal bound — blocking every engagement while a clearance objection is unresolved would stop the business.

// src/report.ar
use std::core::type;

pub type Contractor { mut engaged: Bool }
pub type Engaged <: Contractor iff { self.engaged == true };

#[default]
pub derive cleared_a(p) :- Engaged(p);

#[defeats(cleared_a(p))]
pub derive objection_a(p) :- cleared_b(p);

#[default]
pub derive cleared_b(p) :- Engaged(p);

#[defeats(cleared_b(p))]
pub derive objection_b(p) :- cleared_a(p);

pub derive engagement_roll(p) :- Engaged(p);

pub query roll() -> engagement_roll;

pub query clearances() -> cleared_a;

pub check clearance_notice(p: Engaged) :-
    Engaged(p), not cleared_a(p)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "Vetting::W010",
        message:  format!("contractor {} may lack a security clearance", p),
    };

pub mutate engage_dana() { insert Contractor { engaged: true }; }

On the default branch the two checks are indistinguishable. badge_required (a hard bound that must block) and clearance_notice (a standard that must not) produce the same shape of outcome over equally undetermined membership — an ☞ [undefined] note, and a committed write:

$ ox query target/root.oxbin --mutate report::engage_dana --with-truth4
Vetting::W010

  ☞ Vetting::W010: [undefined] contractor #i1 may lack a security clearance
  │ [#i1]
  help: fired by check `report::clearance_notice`

ran report::engage_dana: 1 ops, 2 events emitted
query badge::badge_holders: 0 row(s)
query badge::roster: 0 row(s)
query report::clearances: 1 row(s)
  [Can] (#i1)
query report::roll: 1 row(s)
  [Is] (#i1)

That is what “one global policy” looks like in practice: it is already in force, it is fail-open, and it is right for clearance_notice and wrong for badge_required. Flipping it to a global fail-closed would invert the error — right for the hard bound, and a business-stopping refusal for the vetting standard. Neither setting can serve both, because the two checks differ in what a non-decision costs, and that is a property of the constraint, not of the engine.

The severity-derived default resolves exactly this, and it is implemented. On the honesty-gate branch, the same two writes, on the same package, diverge with no annotation anywhere: badge::hire_bob refuses with OE1430 (transcript above), while report::engage_dana produces output byte-identical to the default-branch transcript just quoted — it commits, and reports at undefined grade. The distinction comes from the declared severity alone.

Where the severity-derived default stops, and this record stops with it. A third case exists: a check that is a hard bound and has a cohort the team has consciously decided to admit, mid-migration. Severity cannot say that, because severity is one word for the whole check, and a per-check disposition cannot condition on which classifier is undetermined or on which subject. Deciding that finer surface is deliberately out of scope here — it is the subject of the in-body determinedness-test record (design record; its number is allocated when the file lands, so this cites the record rather than a number that does not yet resolve), whose implementation stacks on this record’s honesty-gate branch. What this record decides is the default that such a surface deviates from, and that default is the severity above.

Why admission-point scoping matters

Honesty about the verdict is one half; the other is honesty about which data, at which time, a check is judged over. Two mis-scoping failures follow from a whole-store, commit-time discharge. Wrong time: a valid-timed write (“this filer’s return, as filed on 2025-04-15”) is judged against the union of every valid time at once, so a membership that changed during the year has no single truth across that union and the check either picks one arbitrarily or throws; the honest question is “was this filer a dependent as of the filing date”. Wrong reach: a commit-time whole-store pass re-litigates every check on every write, so a write in an unrelated module pays for — and can be blocked by — a check whose governed data it never touched.

D2’s firing closures and admission-point discharge address both: judged only against writes inside a check’s closure, and at each such write’s own valid-time instant. This half of the design is not implemented — the honesty gate judges at the all-times view — so the transcripts above exercise the verdict axis only.

Worked examples

The Context section carries the executed exhibits. These examples restate the same mechanisms in a domain a reader is likelier to recognize — a tax filing — and cover the case the probe cannot: the unimplemented time axis.

None of the source below has been run: it is written against a schema that exists only in this record, and Example 4 additionally describes unimplemented behavior. Every block is therefore fenced argon,ignore and every outcome is stated as intended, paired with the executed transcript from the Context section that supports it, or marked as unsupported where none exists.

Example 1 — a statutory hard bound (blocking is the only defensible default)

Scenario. A tax authority publishes a deduction cap: a filer who counts as a dependent for the year may not take the standalone standard deduction above a capped amount. “Dependent” is not typed in — it is computed by section rules from claimed-support and residency evidence, exactly the kind of classification an auditor expects the system to derive, not accept on assertion. The cap is a hard legal bound; a deduction that exceeds it for a dependent filer is a defect the return cannot carry.

pub type Filer { standardDeduction: Money }
pub type DependentFiler <: Filer iff { claimedAsDependent(self) && residencyMonths(self) >= 6 }

pub check dependent_deduction_cap(f: DependentFiler) :-
    DependentFiler(f), f.standardDeduction > money(1_250)
    => Diagnostic {
        severity: Severity::Error,
        code:     "Tax::E1099",
        message:  format!("dependent filer {} exceeds the capped standard deduction", f),
    };

Meaning. The check forbids a computed DependentFiler from carrying a deduction over the cap. Input. Three writes, each recording a filer’s return. What happens, and why:

1. Definite member, over cap. Residency and support evidence definitely establish DependentFiler(f); the deduction is money(1_400). The body fires under is; the write is refused as a classic violation (Tax::E1099). Unchanged from today.

2. Definite non-member. The filer is definitely independent (independent residency established). The body does not fire; the write commits. Unchanged.

3. Undetermined membership. Support evidence is present, but residency is in a standoff — two dated assertions the fixpoint cannot reconcile at the write’s valid-time point — so DependentFiler(f) is Can, and the deduction is money(1_400). Today (Context) this commits silently with an [undefined] note. Under this RFD the check is Severity::Error: admitting a deduction whose legality was never decided is the exposure the invariant exists to prevent, so the new inconclusive tuple refuses the write (OE1430) — blocking is the only defensible default for a hard legal bound. The refusal names the undetermined concept and the subject and points the modeler at the evidence to establish or the standoff to break.

All three outcomes are intended for this program, which was not run. Case 3 is supported by executed evidence in the Context section: the honesty-gate branch refuses the structurally identical badge_required write with OE1430, and the transcript there is verbatim. An earlier revision of this record quoted a refusal render with a RFD 0025 D2 — new violation(s) created header and a subject #i2827; that string does not match what the branch emits and has been replaced by the actual transcript in the Context section.

If the modeler’s answer is instead that an unresolved-residency filer should be reported rather than refused, that is a reporting severity — Example 2.

Example 2 — the reporting middle (a worklist, not a write-stop)

Scenario. Finance requires that every payment carry a cost center for attribution. Cost-center assignment is a computed classification (Attributed — an iff concept deciding, from vendor and project evidence, which cost center a payment rolls up to). This is a data-quality standard, not a legal bound: finance wants a worklist of un-attributed payments, but blocking payroll because an attribution is momentarily undetermined would be operationally unacceptable.

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

pub check payment_needs_cost_center(p: Payment) :-
    Payment(p), not Attributed(p)
    => Diagnostic {
        severity: Severity::Warning,
        code:     "Fin::W2050",
        message:  format!("payment {} has no cost center", p),
    };

Meaning. A Severity::Warning check flags any payment lacking a cost center. Input. A payroll batch in which one payment’s attribution is undetermined (the vendor-to-cost-center evidence is in a standoff at the write’s point). What happens: the payment commits; the undetermined membership appears in the check’s report at undefined grade — distinct from a definite “no cost center” and from a clean pass. Why: a reporting-severity check never blocks (D3); its job is to hand the ops team a worklist, and undetermined entries belong on that worklist marked as undecided (chase the evidence) rather than definitely missing (assign one). Payroll runs; the worklist grows by one honest, correctly-graded item.

This one is executed, in a different domain: the Context section’s report::clearance_notice is the same shape — a Severity::Warning check over an equally undetermined classifier — and its transcript shows exactly this outcome (☞ Vetting::W010: [undefined] …, then ran report::engage_dana). On the honesty-gate branch that output is byte-identical to the default branch’s, which is the point: the reporting disposition is not new behavior, it is the behavior that becomes a decision once the blocking disposition exists beside it.

Example 3 — defeat-plane interplay — folded into the Context probe

This example previously restated the negation-cycle program that the Context section now builds, runs, and quotes end to end. It is cut rather than duplicated. The one point worth keeping separate is the agreement between two honesty features: the defeat plane already names such a cycle undefined by decision (OW0740, quoted in the Context build transcript) instead of quietly resolving it false, and the honesty gate carries that same refusal-to-guess across the check boundary. An undecided head stays undecided everywhere, and no consumer may collapse it — which is exactly what the default branch’s [Can] membership row beside its [Is] roster row shows going wrong today.

Example 4 — admission over valid time — INTENDED, UNIMPLEMENTED

Nothing in this example has been executed, and no evidence supports it beyond the design argument: the point-free refusal does not exist in the compiler on any branch and has no allocated diagnostic code, and the honesty gate as implemented judges at the all-times view unconditionally, so the refusal described here does not happen today. Read it as the design’s stated intent for the time axis, not as behavior.

Scenario. A filer’s residency changed mid-year: independent through the spring, dependent from the summer. An auditor asks whether Example 1’s deduction cap was satisfied on the return as filed. Because residency membership varies across valid time, the answer depends entirely on which instant the question is asked at.

// dated to the filing instant — a single, honest verdict:
insert Filer { standardDeduction: money(1_400) } at 2025-04-15;

Meaning. A write dated at 2025-04-15 judges DependentFiler membership as of that day. Input / what happens:

• the dated write is judged at 2025-04-15 — one honest verdict (member or not on that day), dispositioned by Example 1’s rules;
• an unqualified write whose firing closure includes the point-variable residency evidence is refused: the all-times view admits every valid time at once, and point-variable membership has no single honest answer there. Why: rather than silently pick a valid time or fold the variation away, the gate refuses and the diagnostic teaches the remedy — ask the check at a specific point (at <date>). This is the time-axis twin of D3’s verdict honesty: D3 refuses to guess what the membership is; D4 refuses to guess when it is being asked.

An honest gap — retroactive amendment (deferred, see Open questions)

Scenario. A filer’s return was admitted last year with a definite DependentFiler non-membership. This year an amendment retracts one of the residency assertions the classification rested on — and the retraction pushes that already-admitted filer’s membership into a standoff, making a verdict that was once definite now undetermined for data that is already committed history.

D3 dispositions only inconclusive tuples the judged write newly introduces; a tuple already inconclusive over the pre-state does not wedge an unrelated write. But the amendment write is not unrelated — it is the write that created the new inconclusiveness, over data admitted earlier. Whether the gate should refuse the amendment (treating the newly-introduced inconclusiveness as this write’s to dispose), report it, or admit it and re-open the earlier admission for review, this RFD does not decide. It is recorded as an Open question rather than resolved by invented semantics.

Alternatives considered

(a) Global fail-closed default, no per-check policy. Undetermined always refuses, everywhere, with no per-check override. Sound and simple. Rejected as the sole mechanism: in a long-lived open-world knowledge base, undetermined membership is a routine transient (evidence not yet arrived), and a global stop converts every such gap into a hard write failure with no modeler recourse short of editing the check. This RFD keeps fail-closed as the default for blocking checks and lets a check opt out by declaring a reporting severity, so the sound behavior is the default and the alternative is visible at the declaration. (A global pass default is the status-quo soundness hole and is not reconsidered.)

(b) The dropped prior implementation lineage. An earlier, unlanded implementation of this feature carried the same core semantics (three verdicts, admission-point discharge, point-free honesty) but grew a second, richer verdict machine on top: a dedicated per-check identity type, a severity-dispatched interception layer with a separate “hinge”/“standoff” representation, and a total membership-reach walk that propagated through defeat and analytical edges and composed with the defeat plane rather than refusing it. That shape collided with two sibling lanes — a typed-views lane and a per-scope-discipline lane — because all three independently represented per-scope/per-check verdict state and the well-founded-undefined boundary in the same resolution surface, producing an irreconcilable set of failures that could not be landed piecemeal. This RFD neutrally records that shape as a considered alternative and does not adopt it: it keeps the verdict representation minimal and admission-local (one (check path, standpoint) delta key, the possible-minus-definite lifting, and a declared refusal for the defeat-plane composition rather than a total reach walk), and states the resolution-pass boundary (D7) precisely so the collision cannot recur. Whether a shared per-check identity carrier is eventually warranted is an open question, deferred to a cross-lane reconciliation, not a dependency here.

(c) Fire on undetermined (treat Can as a member for blocking). Rejected: this is the false-accusation collapse — it refuses a write for a violation that is not established, only possible, indistinguishable to the modeler from a real violation.

(d) A per-check disposition attribute (#[undetermined(block | pass | report)] on the declaration). An explicit per-check word for what an inconclusive verdict does, overriding the severity-derived default. Rejected: the attribute sits on the declaration, so — exactly like severity — it is one word for the whole check and cannot condition on which classifier is undetermined or on which subject. The case that motivates a finer surface is a blocking check with a consciously admitted cohort mid-migration, and a declaration-level word cannot name that cohort; it can only widen the admission to every undetermined tuple the check sees, which is the status-quo silent pass with an annotation on it. The successor shape is a determinedness test written in the check body, where a predicate over the subject is expressible — the in-body determinedness-test record (design record). This record decides only the default such a surface deviates from.

(e) A new severity level (Severity::Undetermined). Rejected: undetermined is a property of a tuple’s verdict at a point, not of the check; a check has one severity and many tuples, some definite and some undetermined. A fourth severity would force the modeler to classify the check by an outcome only some of its tuples have, so the undetermined tuples’ disposition is derived from the existing severity (D3) rather than becoming a severity of its own.

Consequences

• New surface — none. This record changes no grammar. The behavior change is carried entirely by the Severity a modeler already writes on the check, so there is no new keyword, attribute, or body form to learn, and no existing source file needs an edit to opt in.
• Diagnostics. OE1430 (standoff refusal at the write gate) — exists, in the diagnostic catalogue and emitted, on the honesty-gate branch. The point-free refusal (point-variable check judged point-free) — does not exist on any branch, and holds no allocated code. The aggregated-standoff re-registration OE1332 → OE1430 (D5) is likewise unimplemented.
• Behavior change for existing modules. A membership-gated Severity::Error check whose verdict stands off today admits the write silently; under the honesty gate the same write refuses (OE1430) — the two verbatim transcripts of that difference are in the Context section. A module accepting that risk lowers the check’s severity to Warning/Info or marks it #[observe], which is what the emitted diagnostic’s help text tells the modeler to do. A module with no membership-gated check is byte-identical in check behavior and pays no admission work.
• Write-path cost. Admission-point discharge and firing-closure computation run only for writes landing inside a gated check’s closure (D2); everything else is untouched.
• Mechanization. The three-valued surface D1 rests on is formalized in spec/lean/Argon/Reasoning/Checks.lean on the honesty-gate branch (pull request #1826), not yet on the default branch: the possible reading (bodyHoldsPossible, wfViolationsPossible), inconclusive as its difference against the definite set wfViolationsK3, the containments that make the three verdicts a partition, the strictly-weaker standing of the observe residue (undefinedObservations ⊆ inconclusive), and the no-collapse partition theorem itself. This record points at those definitions and does not restate them; where record and mechanization differ, the mechanization governs. What remains unformalized is the point dimension: the mechanized sets are taken over one global well-founded model, so D2’s admission-point discharge and D4’s point-variability refusal have no Lean statement.

Open questions

• Shared per-check identity carrier. D7 keeps the delta key admission-local. If a future typed-views or scope-discipline lane needs a shared per-check identity type, is that a cross-lane reconciliation RFD, and does it subsume this key? (Deferred; not a dependency here.)
• Audit surface for deliberate lenience. A reporting severity on a membership-gated check is a decision to admit undecidable writes, and it reads identically to a reporting severity chosen for any other reason. Should a build surface an inventory — a count, or a lint — so a reviewer sees every path that admits an undecided verdict in one place? Not decided here.
• Disposition for a check whose severity is inherited rather than written. RFD 0025 D5 makes severity: a required field and records no free-standing default; the one way a check carries a severity it did not write is the amendment from RFD 0026 — a check implementing a trait member whose signature pins a severity may omit the field and inherit the pin (a divergent restatement is OE0676). Does the undetermined disposition track the inherited pin, or is such a check’s undetermined disposition always report until the implementor states a severity of its own? (This RFD assumes it tracks the inherited severity.)
• Point-variability of a rule-validity window vs. dated evidence. D4 targets the full firing closure for dated evidence but only the firing-pattern names for a clock-reading cone. Is the rule-validity-window source (D4.2) closer to the dated-evidence case or the clock case for closure targeting?
• On-demand whole-ask refusal granularity. D4 refuses the whole on-demand check_violations ask when one check is point-variable. Should it instead return per-check results with the point-variable ones marked, rather than refusing the batch?
• Retroactive amendment re-introducing inconclusiveness (Worked examples, gap). An amend/retract write can push an already-admitted tuple from a definite verdict into a standoff — the amendment is the write that newly introduces the inconclusiveness, but over data admitted earlier. D3’s delta discipline dispositions inconclusiveness a write newly introduces, which names the amendment as the disposing write; but whether the honest outcome is to refuse the amendment, report it, or admit it and re-open the earlier admission for review is undecided. This RFD does not invent that semantics; it flags it for a follow-up decision.

Staging

Slices are independently reviewable; each leaves the tree green and changes no behavior for a module with no membership-gated check. Status is marked per slice.

• Slice 1 — DONE. The three-valued verdict plus fail-closed blocking, unqualified only: the membership-gated partition, the possible-minus-definite lifting (D1), and the write-gate honesty gate for Severity::Error checks at the all-times view (OE1430). No admission-point selection yet (all-times only), no point-free gate. Closes the hole measured in Context for the common case. Registry: the runtime gate lands as the inventory row (D6). Implemented on the honesty-gate branch (pull request #1826), including the reporting-severity path; transcripts in the Context section.
• Slice 2 — NOT STARTED. Admission-point discharge and firing closures. Point-parameterized discharge (D2) over the bitemporal read seam; the firing-closure computation and write-targeting; standpoint scoping and the (check path, standpoint) delta key.
• Slice 3 — NOT STARTED. Point-free honesty: the point-variability detector (three sources), the refusal (code allocated by this slice) on the write / debug / on-demand surfaces, and the concrete-point clock pin.
• Slice 4 — NOT STARTED. Aggregated membership: the OE1332 → OE1430 re-registration (D5) and the defeat-plane-composition refusal.
• Lean obligation — MET on the honesty-gate branch, not yet on the default branch (paired with Slice 1). spec/lean/Argon/Reasoning/Checks.lean on that branch adds the possible reading of a check body (bodyHoldsPossible — positive atoms against wfPossible, negated subjects merely ∉ wfTrue), its firing set wfViolationsPossible, and inconclusive := wfViolationsPossible ∖ wfViolationsK3 — the violation-tuple-level set of D1, with the membership-atom case (wfPossible ∖ wfTrue lifted to the check head) recorded on the definition rather than being its statement. Discharging the no-collapse obligation: wfViolationsK3_subset_possible (definite violations are contained in the possible ones), wfViolations_subset_possible and undefinedObservations_subset_inconclusive (the observe residue is part of the gate’s subject, never the whole), and honesty_partition, which states that the definite violations, the inconclusive tuples and the complement of the possible firing set cover every candidate head tuple, and that the inconclusive set is disjoint from each of the other two — the two forbidden collapses of D1, plus exhaustiveness. Before that branch the file formalized only wfViolations over wfTrue and the negation-driven undefinedObservations residue; neither a possible reading nor an inconclusive set existed, which is why an implementation enforcing over the observe residue alone would have missed positively undetermined membership. Still unformalized, and not part of this obligation: any point-scoped statement — the mechanized sets are over one global model, so D2 and D4 have no Lean counterpart. Per the Lean-first rule for substrate semantics the mechanization, not this record, is the authority on those definitions.

Verification (per slice)

• A module with no iff/shape-defined membership in any check body is byte-identical in check behavior and pays no admission work (negative control).
• The Context section’s program refuses OE1430 on the hiring write under Slice 1, and a reporting-severity check over equally undetermined membership still commits and still reports at undefined grade. Both are executed and quoted above; both are pinned by runtime tests on the honesty-gate branch, alongside the two definite cases as controls.
• The refusal reaches assert rejects(OE1430) through the same rejection channel as a classic violation (pinned on that branch).
• Remaining, for slices not started: admission-point discharge judged at a dated write’s own valid-time instant, and a write outside every firing closure running no discharge; point-variable point-free → refused on the write, check-debug, and on-demand surfaces; aggregated standoff OE1332 → OE1430.