RFD 0087 — Fixpoint typed views

• State: discussion
• State detail: not uniformly in discussion — the three-valued standoff policy’s aggregate arm (D3) is the one piece still undecided. Its read-surface arm states the shipped four-valued envelope contract, and the other decisions below are settled as written; a reader should not take the aggregate arm as carried along with them.
• Opened: 2026-07-23
• Decides: that a typed navigation view — a declared concept field whose value is a set computed by walking a relation (f: [T] from Rel.endpoint) — may have a standoff-capable element type T — a shape-clause concept (iff Shape(self, …)) whose membership is a derived rule head the well-founded fixpoint can leave undefined — and that such a view is evaluated inside that fixpoint rather than materialized store-locally at seed time. The trigger is the ability to stand off, NOT a derived extent generally: a braced refinement (iff { P }) also has a derived extent but can never stand off, and is out of scope in both directions (neither lifted nor refused). Settles four things: (1) the single pin-resolution ladder that keys every concept-pinned field read from the base variable’s accumulated concept pins; (2) the raw + gate cell split that keeps a fixpoint-decided extent live and incrementally maintainable; (3) the three-valued (K3) standoff policy at a view boundary — what a view surfaces when an element’s membership is UNDETERMINED (the heart of this RFD; see D3, whose read-surface arm states the shipped four-valued envelope contract and whose aggregate arm is the one piece still undecided) — and, as the carve-out that keeps that policy additive rather than an override, that absence of evidence is excluded from the undefined region only under a closed world: under the closed-world default an unasserted fact is definitely-false and is settled by the reference manual’s membership rule, so the region is the well-founded standoff alone; under an open world the reference manual reads the same absence as unknown, it is undetermined, and it rides the undefined companion alongside a standoff; (4) the explicit contract this feature holds with the per-scope resolution pass, with mapped relation subsumption (RFD 0084), with the incremental defeat/maintenance plane, and with the parallel admission-point-checks RFD on the shared three-valued surface.
• Numbering: 0086 is the admission-point-checks record this RFD coordinates with, and it is now on the default branch (#1822) — the index runs 0085 → 0086 → 0087 with no gap. 0085 on the default branch is the incremental-rule-circuit-compiler record; the instance-relations lane (#1818) still heads its draft 0085 and owes itself a renumber — that lane’s collision to settle, not this record’s.
• Surface policy: no new grammar. The view spelling f: [T] from Rel.endpoint [where P] (RFD 0005 §5.6) is unchanged; what changes is which evaluation plane a view lowers to, decided by construction from T’s ancestry and the presence of a where filter. No user-visible mode selector. The observable surface does change, and the claim must not be read wider than the grammar — the three new observables and the one source break are under Consequences.
• Affects: navigation-view lowering (Module::load in oxc-runtime/src/module_load.rs, plus oxc-instantiate’s lower/rule_ref.rs / lower/ctx.rs); the store-local view materialization on the read path (oxc-runtime/src/catalog_seed.rs, oxc-runtime/src/index.rs::nav_catalog_keeps_value); the concept-keyed field-projection contract (RFD 0005); the well-founded evaluator surface (oxc-reasoning); the K3 $undefined:: companion and check-discharge K3 pass; DERIVATION_SEMANTIC_EPOCH and the RFD 0072 projection-cache derivation commitment; the Lean substrate (Argon.TypeSystem.Soundness.FieldView, Argon.Reasoning.Datalog.WellFounded). Additive on the artifact wire; a lift is a derivation-semantic change and rides an epoch bump.

In plain language — what changes and why

A navigation view is a concept field whose value is not stored but computed by walking a relation:

f: [T] from Rel.endpoint          // f(self) = { x : Rel(… self … x …) and x is a T }
f: [T] from Rel.endpoint where P  // additionally narrowed by predicate P

self.f reads as the set of T-typed things reachable from self across Rel. Deciding which things belong needs two facts: (a) Rel relates self to a candidate, and (b) the candidate is a T.

Today that second fact must be knowable at catalog-seed time. When T is an ordinary declared concept, membership is a seed-time fact and the view materializes locally on the read path — fine. Two other kinds of T have a derived extent, where members are auto-classified rather than inserted, and the seed-time pass has to evaluate that classification early, on each candidate, before the fixpoint has reached its verdict. Only one of the two can actually be undefined when it is evaluated, and the distinction is what the lift keys on:

• Shape-clause concepts (iff Shape(self, …), RFD 0070) are standoff-capable. Membership is a derived rule head, so recursion through negation can leave it neither definitely true nor definitely false. This is the kind the lift and its refusal are for.
• Braced refinements (iff { P }) are not. The body is a predicate over the individual’s own fields and cannot call a rule — OE0660 rejects any other form — so P is always two-valued. A referenced field with no recorded value makes membership definitely FALSE under the open-world reading: an information absence, not a standoff. Such a concept has no undefined region, so a view over it has none to surface.

For the standoff-capable kind, that early evaluation is exactly where honesty breaks, in two distinct ways (see “Today’s behavior on main”): a well-founded standoff on a shape/rule concept makes the store-local read fail closed — the view is not navigable at all — while an open-world absence is silently coerced to a two-valued no. Either way a genuinely UNDETERMINED membership has nowhere to live at the boundary.

The change. A filter-free view over a standoff-capable element type stops materializing store-locally. It lowers, by construction, to a rule that runs in the same well-founded fixpoint as the membership rules:

$field::<C>::<f>(self, x) :- <C>(self), <Rel>(… self … x …), <T>(x).

Now the view’s element membership <T>(x) is decided by the same fixpoint that decides everything else — including the K3 undefined region. A candidate whose T-membership is undefined is neither silently kept nor silently dropped; it surfaces as undefined at the view boundary (D3). The reader sees the standoff instead of a fabricated verdict.

Two mechanisms make this work without a second copy of the data. The pin ladder (D1) decides, when a rule/mutate/test body reads t.f, which single field cell that read keys — same-named fields on different concepts are distinct cells, so the ladder must pick the right one from the concepts t is pinned to. The raw + gate cell split (D2) keeps a fixpoint-decided extent live: the raw walked extent is seeded extent-blind and maintainable by delta, while a per-fixpoint gate clause re-applies the membership test, so the view stays correct as commits arrive without recomputing the walk from scratch.

Question — what could not be expressed (before / after)

Before: this could not be expressed. Now: it can. The distilled index of the examples below. Each row is one concept a modeler wants to state; LEFT is the closest today’s main gets (verified in “Today’s behavior on main”); RIGHT is the proposed spelling (argon,ignore).

Motivation — a worked example the reader can feel

This RFD extends a principle the project has already committed to at three layers. Where an answer is not known, Argon refuses rather than guesses (the build refusals of the OE family); it warns rather than stays silent (the OW family); and it reports undefined rather than coerces (the defeat plane’s undefined-by-decision, where a standoff surfaces as a distinct value instead of being forced true or false). Navigation is the one place that principle has not yet reached: today, walking a relation to a computed concept must fabricate a two-valued membership verdict at read time. Typed views close that gap — a walk to an iff/shape concept can say “undetermined here” and surface it, exactly as the other three layers already do for their own decisions.

A tax model. Person is declared. Dependent and QualifyingChild are computed concepts — membership decided by rules, not asserted:

type Person { ... }

// A qualifying child is decided by age, relationship, residency, support tests —
// a classification, not a stored flag. (RFD 0070 shape/iff clause: the `iff`
// names ONE shape derive; the tests conjoin inside that derive's body, where
// conjunction is `,`.)
pub derive qualifyingChildShape(p: Person) :-
    relatedToTaxpayer(p), underAgeLimit(p), sharesResidence(p);
type QualifyingChild <: Person iff qualifyingChildShape(self);

// A dependent is a qualifying child OR a qualifying relative (another rule).
// Same-head clauses union, so the disjunction is two clauses of one shape.
pub derive dependentShape(p: Person) :- qualifyingChild(p);
pub derive dependentShape(p: Person) :- qualifyingRelative(p);
type Dependent <: Person iff dependentShape(self);

rel Supports(supporter: Person, supported: Person);

type Taxpayer <: Person {
    // The navigation view we want to write: the taxpayer's dependents,
    // reached by walking Supports, filtered to those the fixpoint decides
    // are Dependents.
    dependents: [Dependent] from Supports.supported
}

taxpayer.dependents must be the supported people who are Dependents. Dependent membership is fixpoint-decided: it can hinge on a chain of rules that themselves reference other computed concepts, and — critically — some person’s dependent-status can be genuinely UNDETERMINED (e.g. a residency test that stands off in a negation cycle, or a support fact that is open-world absent for the read-point). A downstream check counts dependents to compute an exemption:

check ExemptionCount { count { d in self.dependents } == self.claimedDependents }

Why membership-dependence matters here, concretely:

• If the view forces undetermined membership to true, an ineligible person is counted, the exemption is overstated, and the check passes on a fabricated extent — a Can-to-Is collapse.
• If it forces undetermined to false, a person whose eligibility is genuinely open is dropped, the exemption is understated, and the check passes anyway on a different fabricated extent — a Can-to-Not collapse.
• The only honest answer is: the view’s extent is itself three-valued at that element, and a consumer that cannot tolerate the standoff must be told, not silently served a two-valued number.

Store-local materialization on today’s main (below) evaluates Dependent membership at seed time. That is the early-verdict trap: it cannot represent the standoff, so — Dependent being a shape/rule concept — it fails closed on it, and the store-local read (view, count, extent) refuses (run-verified exhibit below). This RFD moves the decision into the fixpoint, where the standoff is a first-class value.

The staleness ledger — what the two workarounds cost

Without this feature a modeler who needs taxpayer.dependents has exactly two options today, and both rot. Walk each concretely.

(a) Denormalize the classification into a stored field. Assert a stored Dependent flag (or a stored dependents list) alongside the facts. It is correct the instant it is written. Then a support worksheet is edited — a Supports fact is added, or an age is corrected, or a residency fact flips. Dependent membership is now a function of facts that changed, but the stored row does not know that: it was written by a human (or a one-shot job) and there is no derivation edge from the support fact to the stored flag. The stored Dependent row is now wrong, and every view, credit, and count keyed on it is silently wrong in lockstep. The retraction is a manual obligation with no owner — the fact that justified the row is gone, but the row outlives it. Denormalized classification is a cache with no invalidation.

(b) Hand re-derive the membership rules at each call site. Skip the stored flag; instead, every consumer that needs dependents re-encodes the membership test inline. The Child Tax Credit’s body writes related and underAge and residency; months later the Earned Income Credit’s author writes related and residency — and forgets the age test. Both check bodies are green. Both compute a “dependents” roster. They disagree, and nothing catches it, because there is no single concept they are both obligated to agree with — each is a private re-derivation. This is the identical silent-omission rot that moving rule bodies onto relation-value application removed for rule bodies: one canonical definition, consumed everywhere, instead of N drifting hand copies. Typed views bring the same discipline to navigation — the roster is the concept, walked, not a copy of the concept’s rules pasted at each site.

The feature collapses both failure modes: the roster is a live derivation over the one canonical membership concept, so an edit propagates (no stale cache) and there is exactly one definition to agree with (no drift).

Why the decision must live inside the fixpoint, not after it

A tempting cheaper design is a post-processing filter: run the fixpoint to its verdict, then walk the relation and keep the members two-valued. That fails on mutual recursion between classification and the aggregate a view feeds.

Concretely: a household’s income is the sum over its dependents’ contributions — an aggregate over the dependents view. And a dependency test (a gross-income or support test) references household income. So Dependent membership and the aggregate over dependents depend on each other. A post-processing filter cannot express this: the membership verdict it needs is a function of a value (household income) that is only known once membership is already decided — the filter would have to run after a quantity it is an input to.

Evaluated inside the well-founded fixpoint, the mutual dependence is well-defined. Household income and each dependency verdict are assigned in one fixpoint under K3: where the recursion is productive, each settles to a definite value; where it forms a genuine cycle with no grounding, the cycle resolves to undefined rather than looping or silently picking an evaluation order that biases the answer. K3 is precisely what turns “circular” into “well-defined with an undefined region” — and that undefined region is the standoff this RFD surfaces at the view boundary.

Context — Today’s behavior on main (verified)

Verified against oxc-runtime/src/catalog_seed.rs (the RFD 0005 §5.6 navigation-view projection block, ~L903–1099) and oxc-runtime/src/index.rs::nav_catalog_keeps_value (~L251), re-checked on the default-branch tip 81dfe28dc. (The run-verified exhibit below was executed at an earlier default-branch tip, eac0442a0; each section states the tip its claims were checked against.)

• A navigation view is carried on the wire as PropertyDeclBody.from_relation: Option<(Vec<String>, String)> (the relation path + endpoint) plus from_filter: Option<CborValue> (the optional where term). oxc-ast carries the surface; Argon.TypeSystem.Soundness.FieldView is the Lean reader of the same clause (RFD 0005 §5.6).
• Materialization is store-local, at read-model seed time. For each live concept declaration and each field carrying from_relation, catalog_seed resolves the relation’s catalog key, computes the holder/value endpoint positions (binary: the sole other end; arity >= 3: the unique end <:-comparable with the declaring concept, else a LOUD build-bypass refusal OE1376), reads the relation’s subsumption-closed extent from the catalog, and projects each kept (holder, value) row into $field::<f> and the concept-keyed companions $field::<C>::<f> (RFD 0005 concept-keying, keyed by blake3(decl_concept :: field) so same-named fields on distinct concepts do not alias).
• The element-type filter is evaluated eagerly, per candidate, at seed time. nav_catalog_keeps_value applies the iof T selection (only a strict narrowing T <: E, T != E is a real filter) and the where term. concept_admits_individual at this site admits iff-derived membership — i.e. a narrowing view onto a defined element type is permitted today, and its membership is decided by evaluating the refinement predicate on each candidate at seed time.
• The honesty limit — two distinct failure modes, both verified end-to-end (see the run-verified exhibit below). The boundary is two-valued, but it does NOT collapse a well-founded standoff to a silent Ok(false). Two cases, established by running ox built from origin/main:
  • Field-refinement iff { … } element type (no standoff possible). Membership is always two-valued. A candidate that is definitely-false or open-world-unknown (a refinement field never asserted) is coerced to Ok(false) and silently excluded — the view drops the row and a count over it is silently short (index.rs: “a legitimate Ok(false) — the predicate is definitely false, or a missing-field open-world-unknown — still excludes”). A braced iff body cannot call a rule (OE0660), so it can never itself stand off; the dishonesty here is an open-world-unknown collapsed to false, not a standoff coerced to false.
  • Shape-derived / rule element type (genuine standoff). Membership is fixpoint-dependent. concept_admits_individual returns Truth4::Can for such a concept — “the faithful value is Can, never a fabricated Not” (classify.rs) — and the store-local read path surfaces that Can as a loud runtime refusal, not a silent drop: the navigation-view read, the count, and the extent query all fail closed (“membership in <T> is rule-derived (fixpoint-dependent) and is undetermined for the store-local classifier”). So a computed concept whose membership stands off is not navigable/countable on the store-local plane at all today. Either way there is no representation, at the view boundary, of a candidate whose fixpoint membership is undefined: the standoff case fails closed and the open-world case is silently coerced. The lift gives the plane an undefined region to place a standoff into.
• No fixpoint view exists today. Every consumer (wire/display, mutate-body reads, rule/query/check bodies, and a classifier consuming the view through exists { p in self.f }) reads the store-local $field::… relation seeded above. There is no synthesized fixpoint rule for a view and no raw + gate split; the walk is recomputed at each read-model rebuild keyed on the storage write-generation pair (oxc-runtime AGENTS.md model_cache contract).

Which element types the lift covers — the two iff kinds, side by side

Both programs below declare a view over an iff element type. Both element types have a derived extent. Only the first is touched by this record, and the difference is whether the fixpoint can leave membership undefined.

Covered — a shape clause can stand off.

pub derive qualifying(p) :- ... ;                 // a rule, so a rule head
pub type Dependent <: Person iff qualifying(self);

pub type Household <: Person {
    dependents: [Dependent] from Supports.supported          // LIFTED (D1-D3)
    // minorDependents: [Dependent] from Supports.supported where under13(supported)
    //                                                        REFUSED, OE0683 (D7)
}

qualifying is a rule head, so Dependent(x) is decided in the well-founded fixpoint and recursion through negation can leave it undefined. The filter-free view lifts and surfaces that undefined region; the where-filtered variant is refused, because a filtered view stays store-local and would have to guess.

Not covered — a braced refinement cannot.

pub type Adult <: Person iff { self.age >= 18 };  // a predicate over own fields

pub type Household <: Person {
    adults: [Adult] from Supports.supported                  // UNCHANGED
    over21s: [Adult] from Supports.supported where senior(supported)  // ACCEPTED
}

Adult’s body cannot call a rule — OE0660 rejects any other form — so the predicate is always two-valued and Adult has no undefined region. Both views keep their store-local materialization: no lift, and no refusal. A person whose age is unrecorded is definitely not an Adult under the open-world reading, which is an information absence and is excluded, exactly as the reference manual says.

Why the distinction is load-bearing. Keying the lift and the refusal on “derived extent” instead of “can stand off” makes OE0683 refuse the second program’s over21s — a view that builds and serves correctly today — for a hazard it cannot exhibit. The narrower trigger is one variant narrower and costs nothing: it is DefinedByShape alone.

The limit this RFD removes: a filter-free view over a standoff-capable element type cannot be evaluated honestly on the store-local plane, because the plane has no undefined region to place a standoff into.

Run-verified exhibit (end-to-end, not unit-test-level)

Built from origin/main @ eac0442a0; source → ox build → ox derive/ox query. Dependent is a computed concept via the shape clause (iff qualifyingChild(self), the clause pointing at a pub derive); qualifyingChild sits in a mutual-defeat cycle through defeat (acyclic defeat graph), undefined (Can) for everyone a strict clause misses.

pub type Person;
pub type Taxpayer <: Person;

#[default]
pub derive qualifyingChild(p) :- Person(p);
#[defeats (qualifyingChild(p))]
pub derive rivalContests(p) :- rivalClaim(p);
#[default]
pub derive rivalClaim(p) :- Person(p);
#[defeats (rivalClaim(p))]
pub derive claimSettled(p) :- qualifyingChild(p);

pub type Tiebroken <: Person;                 // a strict clause settles these
pub derive qualifyingChild(p) :- Tiebroken(p);

pub type Dependent <: Person iff qualifyingChild(self);   // computed concept

pub rel Supports(supporter: Person, mut supported: Person) [0..*] [0..*];

pub type Household <: Taxpayer {
    dependents: [Dependent] from Supports.supported       // the navigation view
}

pub derive dependentsOf(h, d)   :- Household(h), d in h.dependents;
pub derive dependentCount(h, n) :- Household(h), n = count(d for d in h.dependents);

Fixture: alice is a Household supporting bob and dave; bob is Tiebroken (settled), dave is not.

Membership genuinely stands off — bob definite, dave undefined (OW0740 warns at build):

$ ox derive qualifyingChild --explain
  +Δ (bob)                                   # definite (Is)
  1 undefined tuple(s) [well-founded standoff — Can]
  Can (dave)                                 # undefined

Every store-local read of the computed concept refuses — the nav-view read, the count, and the extent query all fail identically:

$ ox derive dependentsOf     # `d in h.dependents`
$ ox derive dependentCount
$ ox query --extent Dependent
Error: membership in `Dependent` is rule-derived (fixpoint-dependent) and is
  undetermined for the store-local classifier — … never evaluated
  mid-classification; read it through the reasoner or classify the individual
  directly

Contrast the field-refinement twin (iff { self.qualified == true }, dave.qualified unset): the view materializes and silently drops dave — dependentCount reports 1, and ox query --extent Dependent --with-truth4 shows bob only with no undefined region (an open-world-unknown collapsed to definite-false, not a standoff).

Both are the honesty limit above: the standoff case fails closed; the open-world case is silently coerced. This RFD replaces both with a served definite extent plus a surfaced undefined region (D3).

What this enables

Workflows a modeler faces today and cannot express honestly. Each opens with the situation, gives the code the lift enables, works one undefined case where it matters, then states why the store-local plane (see “Today’s behavior on main”) forces a stale, wrong, or dishonest answer. Each carries one concept: a standoff reaching a scalar aggregate, where the harm is a magnitude — a credit over- or understated (1) — and where it is directional — a compliance ratio whose failure flips to a pass (2); navigation over mapped parent relations (3); one view serving two consumers opposite verdicts (4); the undefined region as a review queue (5); propagation outward through a second navigation hop (6); composition with valid-time reads (7); and the cross-module governance boundary (8). All code is proposed/illustrative — nothing here is implemented.

The shared dichotomy, stated once — and not restated below. For a shape/rule element type the store-local read of a standoff member fails closed: the read refuses, so the roster is not navigable at all. The field-refinement/open-world twin does the opposite — it silently coerces the absence to a definite false and drops the member. Neither is a representation of an undetermined membership. Scenarios 1, 2, 4, 5 and 6 all hit the fails-closed arm. Their closings tag the arm in two words and then say only what is new at that site — which consumer surfaces the refusal blocks, and what the stale workaround costs there. The tag is repeated because a reader landing mid-section needs it; the argument behind it is not. Scenarios 3 and 7 turn on different limits (a seed-time plane cannot decide a fixpoint-defined classification at all; it cannot express a valid-time slice at all), and 8 states its own distinction.

1. Qualifying-child navigation on a tax return

A preparer builds a return. Whether a supported person is a qualifying child is not a checkbox: it is the conjunction of the relationship, age, residency, and support tests, and any one of them can turn on facts entered elsewhere in the engagement (a second household, a support worksheet). The preparer wants to write the roster of qualifying children once and have every credit computation read the concept the statute defines, not a snapshot that goes stale the moment a worksheet changes.

// tax module (model as in Motivation): QualifyingChild <: Person is iff-decided.
type Taxpayer <: Person {
    // The roster, typed by the COMPUTED concept, walked over Supports.
    qualifyingChildren: [QualifyingChild] from Supports.supported
}

// A dozen credits key on this one roster. The Child Tax Credit counts it.
check ChildTaxCredit {
    self.claimedCtc == count { c in self.qualifyingChildren } * perChildAmount
}

The preparer navigates alice.qualifyingChildren; the credit check counts it.

Worked undefined case: a child dave lives part-year in two households and the residency test stands off in a defeasible cycle — each household’s claim defeats the other absent a tie-breaker fact the preparer has not yet entered, so QualifyingChild(dave) is undefined (∈ J ∖ I). The view serves the definite children and rides dave on $undefined::$field::Taxpayer::qualifyingChildren; the CTC count sees a non-empty undefined region and is itself undefined (D3). The return does not compute a credit that silently omits or silently includes a contested child — it surfaces that a tie-breaker fact is missing, the one actionable state for the preparer.

Why today fails — fails-closed arm. Blocked surfaces: the nav-view read, the credit’s count, and the --extent query (run-verified exhibit). The roster is not navigable or countable at all — a hard expressiveness blocker, not a silently wrong number. Workaround cost here: a stored roster flag goes stale on the next support-worksheet edit, and hand re-deriving the tests inside each credit sets the dozen credits drifting against each other.

2. Nondiscrimination roster feeding a coverage-ratio test

A retirement plan must pass a coverage test: the fraction of non-highly- compensated employees benefiting must be at least a statutory multiple of the highly-compensated fraction. Eligibility is decided by enrollment rules — hours of service, entry dates, a waiting period that can itself hinge on a rehire fact. An auditor recomputing the test needs the roster to be the eligibility concept, and needs an undetermined member to make the ratio undefined rather than silently drop out and flip a fail into a pass.

pub derive eligibleEmployeeShape(e: Employee) :-
    completedServiceHours(e), pastEntryDate(e), not excludedClass(e);
type EligibleEmployee <: Employee iff eligibleEmployeeShape(self);

type Plan {
    eligibleParticipants: [EligibleEmployee] from Enrollment.employee
}

check CoverageRatio {
    benefitingFraction(self.eligibleParticipants, nonHighlyComp)
        >= statutoryFloor
           * benefitingFraction(self.eligibleParticipants, highlyComp)
}

Worked undefined case: a rehired employee’s waiting-period credit stands off — the rehire-bridging rule and the break-in-service rule form a negation cycle pending a determination the plan administrator has not entered — so EligibleEmployee(x) is undefined. The ratio aggregates over a set with a non-empty undefined region, and per D3 the ratio is itself undefined: the test does not discharge on a two-valued roster. The auditor sees the test cannot be certified until the one member is resolved. Aggregate-goes-undefined is exactly the signal the auditor needs.

Why today fails, and what is distinct here: the harm is directional, not merely inaccurate. Dropping an undetermined member shrinks the roster, which raises the benefiting fraction, which turns a coverage failure into a pass — and a plan qualification defect discovered on a later audit invalidates the intervening years that were already relied upon. That is the field-refinement/open-world arm, and it is the reason the lift must not reintroduce silent exclusion. Today EligibleEmployee is a shape/rule concept, so it lands on the fails-closed arm instead. Blocked surfaces: the roster read, the ratio’s count, and the --extent query (run-verified exhibit) — the ratio cannot be computed at all, so the test is inexpressible rather than silently wrong. Workaround cost here: denormalization goes stale on any hours or rehire edit.

3. Statutory cross-reference over a mapped parent relation

A statute allows a deduction for “items of the kind described in section X.” The modeler expresses section-X as a computed classification DeductibleItem <: IncomeItem, and income items arrive as specialized child relations (WagesUSA, DividendUSD, …) that subsume into IncomeItem under mapped relation subsumption (RFD 0084, merged) — a child pins a constant end such as currency or source. The return must navigate “the deductible items” across the parent relation and see the child facts through their mapped images.

rel IncomeItem(p: Person, amount: Money, c: Currency);
// Every filler is keyed by the PARENT end it fills (RFD 0084 — the positional
// filler list was removed); `c = USD` pins a parent end to a constant.
rel WagesUSA(p: Person, amount: Money) <: IncomeItem(p = p, amount = amount, c = USD);

type DeductibleItem <: IncomeItem iff describedInSectionX(self);

type Return <: Person {
    // Walks the subsumption-closed parent extent → sees WagesUSA as its φ-image.
    deductibleItems: [DeductibleItem] from IncomeItem.p
}

Worked case (D5): a WagesUSA(alice, 1000) fact contributes the φ-image IncomeItem(alice, 1000, USD). The view walks the subsumption-closed parent extent, so the section-X classification runs over the parent frame with the constant-pinned USD end visible to it (RFD 0084 forbids dropped child ends, so the frame is information-complete). If describedInSectionX stands off on one item, that item rides $undefined::, and the deduction total is undefined rather than silently smaller.

Why today fails: no store-local plane can decide a section-X membership that is itself fixpoint-defined and simultaneously honor the standoff — the seed-time pass has no undefined region (“Today’s behavior”). Hand re-derivation cannot even see the φ-images without re-implementing mapped subsumption per query, and would still collapse the standoff to a two-valued deduction.

4. Authorized signers on an account (the case for consumer-decides)

An account’s authorized signers are decided by a delegation chain — a power of attorney, a corporate resolution — each with an effective window and each revocable. Getting membership wrong in either direction is a concrete harm: eager inclusion of an undetermined signer authorizes access that may not exist; eager exclusion locks out a signer whose authority is merely unconfirmed at read time. The two consumers of the roster — an authorization gate and a display roster — want opposite fail directions, which is why the view itself must not pre-decide.

type AuthorizedSigner <: Person iff hasActiveDelegation(self, account);

type Account {
    signers: [AuthorizedSigner] from Delegation.grantee
}

Worked case: a delegation whose revocation is contested stands off, so AuthorizedSigner(p) is undefined. The display roster shows the definite signers and marks p as a standoff for a reviewer to follow up. An authorization gate reading the same view via exists { s in account.signers } evaluates the existential in WFS: an all-undefined witness set yields undefined (D3), and the gate’s own policy — fail-closed for access — denies. That existential’s undefined verdict shares E4’s prerequisite — undefined-ness propagating through a rule body join, the engine-level lift this record inherits rather than owns (D3) — so the gate half of this scenario is intended behaviour awaiting that lift; the display half, which reads the definite roster plus the distinguishable standoff, needs only this record’s slices. Neither outcome required the view to pre-decide to include p (authorizing access) or drop p (silently locking out and hiding the contest). One view, two honest consumers, opposite treatments of the same standoff.

Why today fails — fails-closed arm; the roster read refuses. Distinct here is whose need goes unmet: there is no store-local extent to serve either consumer, so the two correct and opposite treatments of one undetermined member cannot both be built off one roster — which is precisely the surface-honest, consumer-decides policy this RFD adopts (D3).

5. The undefined region as an auditor’s worklist (defeasible classification)

A classification is often a default with exceptions: an employee is a ProtectedClass participant by default, unless a documented exclusion applies; a taxpayer filing status defaults to one value unless a rebutting fact is on file. This is the defeasible plane — a #[default] rule that a #[defeats] exception can override. When the default rule and the exception both fire and neither is grounded over the other, the classification is in standoff: the defeat plane holds it undefined by decision rather than guessing a winner.

A view typed by such a defeasible concept surfaces exactly the individuals whose membership is in standoff — and that is not a nuisance, it is the deliverable.

// Membership defaults true, but a documented exclusion rebuts it.
type CoveredParticipant <: Employee iff enrolled(self);
#[default] derive covered(e: Employee)             :- CoveredParticipant(e);
#[defeats(covered(e))] derive excluded(e: Employee) :- documentedExclusion(e);

type Plan {
    // The roster typed by the defeasible concept.
    coveredRoster: [CoveredParticipant] from Enrollment.employee
}

Worked undefined case: for most employees the default holds or a clean exclusion rebuts it — definite in or definite out. For three employees an exclusion form is on file and an enrollment record contradicts it, and no rule grounds one over the other, so CoveredParticipant stands off on those three. The view serves the definite roster and rides exactly those three on the undefined companion. An auditor reading the roster does not get a wrong list that quietly picked a side; they get a review queue — “resolve the membership of these three” — which is the one actionable output. The undefined region is the worklist.

Why today fails — fails-closed arm (rule-derived through defeat). Blocked surfaces: the roster read and the extent query. Distinct here is that the refusal destroys the deliverable itself — the three contested employees cannot be listed, so there is no roster to hand the auditor and no worklist to build from it. The defeat plane’s whole point (undefined-by-decision instead of a guess) is unreachable the moment the classification is navigated store-locally.

6. Undefinedness propagates through a navigation chain

Views compose: taxpayer.qualifyingChildren is a set of children, and each child has .educationExpenses. A credit sums education expenses across the qualifying children. When one child’s membership is undetermined, honesty must propagate through the chain — the credit total is undefined, not silently computed over the children who happen to be definite.

// Person (declared in Motivation) carries a stored expense field:
//   type Person { educationExpenses: Money, ... }

type Taxpayer <: Person {
    qualifyingChildren: [QualifyingChild] from Supports.supported
}

// Education credit sums a nested navigation: over each qualifying child, the
// child's education expenses.
check EducationCredit {
    self.claimedEducationCredit
        == sum { c.educationExpenses for c in self.qualifyingChildren }
}

Worked undefined case: bob and carol are definite qualifying children; dave’s residency test stands off, so QualifyingChild(dave) is undefined. The outer view self.qualifyingChildren has a non-empty undefined region (dave). The sum aggregates over a set one of whose members is undetermined — and dave’s expenses could change the total — so the sum is itself undefined (D3), and the credit check does not discharge on a number computed over { bob, carol } alone. The undefinedness at the membership boundary flows outward through the nested read to the aggregate: a chain is only as definite as its least definite link.

Why today fails — fails-closed arm. Blocked surfaces: the nested navigation, the sum, and the extent query. Distinct here is that there is no boundary at which the undefinedness could enter the computation — the store-local plane has no undefined region, so the chain has nothing to propagate along and the credit is not computable at all rather than silently partial.

7. “Who was eligible when the test ran?” — views over a computed concept read as-of a valid time

Compliance tests are asked as of a date: “who was an eligible participant when the coverage test ran in March?” Argon is bitemporal — facts carry valid time, and a read can be taken as-of a valid instant. Membership is a computed concept, so the as-of question is “what was the fixpoint verdict over the facts valid at that instant?” A typed view composes with valid-time reads: the roster read as-of March is the extent the membership rules decide over the March-valid facts, standoffs included.

pub derive eligibleEmployeeShape(e: Employee) :-
    completedServiceHours(e), pastEntryDate(e);
type EligibleEmployee <: Employee iff eligibleEmployeeShape(self);

type Plan {
    eligibleParticipants: [EligibleEmployee] from Enrollment.employee
}

Worked case: a service-hours record is later corrected — the correction is valid from April, but as-of March the uncorrected hours were on file. Read as-of March, self.eligibleParticipants is the membership the rules decide over the facts valid in March; an employee whose March eligibility turned on a fact that was itself in standoff in March rides the undefined companion of the as-of read. The auditor reconstructing the March test sees the roster the engine would have served in March — definite members and the March standoffs — not today’s membership retro-applied.

Why today fails: seed-time materialization bakes a single two-valued extent at read-model build; it has no notion of “the membership verdict over a different valid-time slice,” and it cannot carry a standoff into the as-of answer. A view evaluated inside the fixpoint inherits the fixpoint’s valid-time discipline for free — the walk and the membership test run over the same as-of frame.

8. Cross-module: rules evolve in one module, navigation stays correct in another

A governance boundary: module eligibility owns the classification rules; module reporting navigates them. reporting should not — and by import discipline cannot — re-encode eligibility’s tests; it declares a view typed by the imported concept and walks it. When eligibility tightens a test (adds a new exclusion, adjusts an age limit), reporting’s view is correct on the next build with no edit, because the view is the imported concept walked, not a copy of its rules.

// module eligibility
pub derive eligibleEmployeeShape(e: Employee) :-
    completedServiceHours(e), pastEntryDate(e), not excludedClass(e);
pub type EligibleEmployee <: Employee iff eligibleEmployeeShape(self);

// module reporting  (imports EligibleEmployee, Enrollment)
type Plan {
    eligibleParticipants: [EligibleEmployee] from Enrollment.employee
}

Worked case: eligibility later adds not leasedEmployee(e) to the eligibleEmployeeShape body that defines EligibleEmployee. reporting is not touched; its next build walks the tightened concept and the roster shrinks correctly. If instead reporting had hand-copied the three original tests (workaround (b) above), the tightening would silently not apply — reporting’s roster would keep counting leased employees, drifting from the authority that owns the definition, with no error. The runtime and the build-plane validator consume the checker’s resolved reference to the imported concept (D4), so the cross-module walk keys the same membership the checker accepted — no re-resolution that could go false-ambiguous or silently miss.

Why today fails: not that cross-module navigation is impossible today, but that the only stale-proof cross-module option — a live view over the imported concept — is exactly the standoff-capable walk this RFD lifts; store-local materialization of a shape/rule concept fails closed on any standoff in the imported concept (verified honesty limit) — the read refuses — so reporting cannot both track the authority’s rules and honor a standoff the authority’s fixpoint produces.

Decision — the design (D1–D9)

D1 — The pin-resolution ladder (one ladder, keying every concept-pinned field read)

When a rule / mutate / test body reads t.field, the base variable t may be pinned to one or more concepts by the atoms in scope (C(t), iof(t, C), a declared relation endpoint whose sort is a concept). Same-named fields on distinct declaring concepts are distinct cells (each property id hashes the declaring concept’s qualified path — the RFD 0005 concept-keying, verified in oxc-runtime AGENTS.md). A single ladder maps (pin set, field name) to one cell decision. It is layered so file-local answers short-circuit and only genuinely cross-module or ambiguous cases fall through to the workspace <:-ancestry walk:

The keyed cell always uses the declaration-qualified path, never the bare name, even when the field’s only file-local identity is that cell. The empty pin set is the only early exit (field reads stay bare-named); a size-1 pin set still routes through the full winner classification, so a defined singleton correctly classifies as a gated bare read (D2) rather than serving an unmaterialized keyed read.

The winner’s kind selects the read shape:

• Plain (ordinary-concept) winner → root the read at its concept-qualified stored relation.
• Defined (iff/shape) winner → the winner’s keyed stored-slot plane is fixpoint-materialized (extent not seedable), so a rooted stored read would join an empty relation. The read stays the bare relation gated by the rule’s own membership atom. A lifted view at such a winner roots at the winner’s fixpoint-synthesized key; a WFS-dependent declarer’s unlifted-view cell is raw+gate materialized at load (D2) so the rooted read is live, never vacuously empty.
• Incomparable pins → the read refuses (see D3 / refusal codes). Rules with no field read over the base stay legal — multiple classification is not itself an error.

D2 — Raw + gate cells (keeping a fixpoint-decided extent live)

The problem: a concept whose membership is decided inside the fixpoint has no seed-time extent, so an extent-gated seeding would leave the keyed field relation permanently empty while the wire serves the read. The fix seeds the field candidate row in two forms and defers the membership decision to the fixpoint:

• Raw cell — $rawfield::<C>::<f> seeded extent-blind: every fixpoint-decided concept whose canonical declarer for the field is the walked concept body takes the candidate row with no membership gate (a holder asserted at a descendant is a candidate member of every chain concept by upward closure). Which concepts receive a raw cell is a recorded load-time fact, never a seed-side re-derivation, so the seed pass and the read pass cannot disagree.
• Gate clause — synthesized at Module::load, one fixpoint rule: $field::<C>::<f>(x, v) :- $rawfield::<C>::<f>(x, v), <C>(x). Membership is decided INSIDE the fixpoint here. The raw cell’s own gated name is rule-only — never seeded — or EDB rows would mix into a fixpoint head.

This split is what makes a fixpoint-decided extent incrementally maintainable: the raw cell is an ordinary EDB projection maintainable by delta as facts arrive; the gate is an ordinary fixpoint rule re-evaluated by the same incremental circuits that maintain every membership rule. See D6 for the maintenance contract.

What the split costs, measured. The raw cell is a persisted second extent, and because it is seeded extent-blind it grows with the walked extent rather than the member extent. So a view whose relation walks many candidates to few members pays proportionally the most, and the cost lands in artifact size rather than in time. Measured on the runtime slice at 40,000 walked candidates: the artifact grows 5.7%–7.3% against the same program with a plain element type (+2.6 MB at 200 members, +2.7 MB at 20,000).

Build time moves the other way, and against the expectation that motivated this split’s scrutiny. Store-local materialization filters at seed time by classifying each candidate individually; the lifted form seeds blind and lets the fixpoint decide membership with one set-at-a-time join. The join wins, and it wins wider as the member extent grows: at those 40,000 candidates, ox build is 2.0× faster lifted at 200 members and 3.5× faster at 20,000, because the store-local path scales with the member count (6.75s → 11.82s) while the lifted path is flat (3.38s → 3.42s). Derived-read time shows no difference at that size. A view over a computed concept is therefore cheaper to build than the denormalized workaround it replaces, which is the comparison a modeller actually faces.

These are from-scratch build figures and say nothing about rebuild cost, which is the open question D6 carries: whether the raw cell participates in touched-set narrowing or is re-seeded whole on every rebuild.

D3 — The K3 standoff policy at the view boundary (the decision)

WFS evaluation is three-valued (Kleene / K3, oxc-reasoning executor/aft.rs): a tuple is definitely-true (I), definitely-false, or undefined (J ∖ I — a well-founded standoff: recursion through negation that the alternating fixpoint pins neither true nor false), read back as the MetaValue K3 assignment (WellFounded.lean). The engine already materializes that region as a per-head companion relation — R carries I, $undefined::R carries J ∖ I — and the companion namespace is threaded through the reasoner: the companion-name helper on the query-engine facade (oxc-reasoning/src/query_engine.rs), the stratification boundary that keeps ordinary NAF from reading it as definite (oxc-reasoning/src/compile/stratify.rs, and the OE1365 refusal that guards the unsound case), and the catalog’s exclusion of the namespace from ordinary per-relation treatment (oxc-reasoning/src/catalog/mod.rs).

Absence of evidence is definitely-false only under a closed world. Under the closed-world default an unasserted fact is definitely-false to the derive plane, and a refinement predicate over an unrecorded field is settled by the reference manual’s membership rule (below), not by the fixpoint — so for a closed-world element type the region above is the well-founded standoff, exactly. Under an open world the manual reads the same absence as unknown (spec/reference/src/semantics/world-assumptions.md: “if a fact isn’t derivable, it’s unknown”), and it is undetermined rather than false. That is the shipped meaning of undetermined, not an inference: the check-plane determinedness operator’s undetermined region is the union of the well-founded standoff region with open-world absence of unrefuted evidence, and its mechanized denotation is parameterized by the world, with the standoff-only reading recovered as the closed-world instance (undeterminedAtom and undeterminedAtom_closed_iff_standoff, spec/lean/Argon/Reasoning/Checks.lean).

D3’s region therefore tracks the element type’s world: a standoff alone for a closed-world element type, and a standoff plus an unrefuted-absent candidate for an open-world one. The widening does not change what the derive-plane companion records — $undefined::R carries fixpoint outcomes only, so open-world absence has no companion of its own there, and the derive plane refuses a negation that would read such an absence as definite rather than evaluating it three-valued (OE1367, the open-world twin of OE1365). The check plane carries the union in its own separate region. Which carrier serves an open-world element type at a view boundary is an open question below, not a decision this record makes.

At a view boundary this MUST NOT collapse to a two-valued verdict in either direction. The governing principle, stated here and held in common with the admission-point-checks record (RFD 0086), which states it in its own words as the two forbidden collapses of its three-verdict decision (D1) and as its failure-direction doctrine — that doctrine cites the view boundary’s refusal to coerce as existing precedent, so the agreement runs both ways:

Undetermined never silently coerces to true or false. Each construct that observes an undetermined value declares its own policy for it.

The view construct’s declared policy — surface-honest, consumer-decides:

Concretely, per consumer:

• Set-materialization / wire / display read of self.f — this half of the policy is the shipped read surface, not a proposal. Every derived read is already an epistemic envelope (compiler/crates/oxc-mcp/src/convert.rs): each row carries its four-valued tag (Is / Not / Can / Both) beside a sibling hidden object counting the undetermined (can), over-determined (both) and determined-false (not) rows. A head’s WFS-undefined companion tuples ride that envelope as Can rows by default (derive_classical_envelope / derive_tagged_envelope), and hidden.can is that companion’s own count — a projection of the companion, not an independent computation. The human fail-closed projection is opt-in (project_k3); under it the Can rows drop from the row list while hidden is still reported — the crate’s stated contract is “never a silent collapse”, and no path collapses undetermined to false or over-determined to true. The reference manual carries the same contract as surface law (spec/reference/src/semantics/reasoning.md, the envelope paragraph: drop-but-count). What this RFD adds for a view is only the source of the region — the synthesized $field::<C>::<f> head’s companion — never a new wire field, marker, or projection mode.

• Aggregate / count over self.f (the exemption check in Motivation) — the one arm of D3 that is not already shipped behaviour, and it invents no new discipline. An aggregate whose input set has a non-empty undefined region does not return a fabricated two-valued scalar. It defers to the aggregation-over-undefined discipline that already ships rather than stating a view-specific rule: a fold over a relation whose $undefined:: companion is non-empty is refused whole-relation, loudly, instead of treating undefined as false (ReasoningError::AggregateOverUndefined in oxc-reasoning/src/error.rs, raised from oxc-reasoning/src/executor/aggregate.rs; the diagnostic is OE1332, whose catalog text states the conservative whole-relation scope and names three-valued aggregate intervals as the designed follow-up). So the semantics is: the aggregate is itself undefined at that read unless the undefined region provably cannot change the result — the same conservatism the shipped guard already applies, reached once a lifted view gives the fold an undefined input. This is the per-view policy’s whole point — it lets the standoff propagate to the consumer that can adjudicate it, rather than the view pre-deciding. What approving D3 leaves undecided is confined to this arm: how much partial definiteness the boundary should exploit before declaring the aggregate undefined (Open question 1, the three-valued-interval track). Every other arm of D3 describes behaviour on the default branch.

  Consumer-surface reality — what each aggregate consumer kind experiences. “The aggregate is itself undefined” is the semantics; the concrete surface a modeler meets differs by consumer, because the plane has no undefined-valued scalar. The three consumer kinds:

  • check (three-valued discharge). A check whose body aggregates over a view with a non-empty undefined region does not pass or fail on a fabricated number — it discharges three-valuedly: the check verdict is itself undefined and surfaces through the K3 check-discharge pass. This is the honest, non-refusing consumer.
  • Scalar derive binding the aggregate (OE1332, the runtime refusal raised while ox build maintains the read model). A value derive such as pub derive dependentCount(h, n) :- Household(h), n = count(d for d in h.dependents) binds the count into a scalar n. A scalar cannot hold “undefined”, so the undefined propagates as a refusal: the pre-existing aggregate-over-undefined discipline (OE1332, the #250/#134 track D3 cites) refuses at build rather than folding undefined to false. This is not a new refusal introduced by the lift — it is the existing derive-plane guard, reached once the lifted view gives the fold an undefined input. The steer is to move the consumer to a check (which discharges three-valuedly), or to read the view’s regions directly (definite rows + the undefined companion) and aggregate an intermediate that is itself definite.
  • Direct view read (definite rows + undefined region). A consumer that reads self.f directly (no aggregation) gets the definite-true extent plus the distinguishable $undefined::$field::<C>::<f> region — it never refuses; it inspects the standoff itself.

  The run-verified OE1332 render for the scalar-derive case is in the worked examples (E3), which states the draft it was captured on and cites it.

• Classifier consuming the view via exists { p in self.f }: a bare exists conjunct over a lifted view forces the classifier onto the rule plane (a fixpoint view is not locally decidable). The existential is evaluated in WFS: undefined membership contributes undefined to the existential per K3, not a silent false. A genuine view↔classifier negation cycle resolves as undefined per WFS — neither a refusal nor false.

• where-filtered views (see D7) are out of scope for the lift and stay store-local; a filtered view over a standoff-capable target is refused at build, fail-closed, rather than served a two-valued extent it cannot honestly compute. Over a braced refinement it is accepted.

Relationship to the reference manual — D3 composes with it; no chapter needs amending. The two rules answer different questions, and both are needed.

• The reference manual decides membership. “iff-derived membership is three-valued: success requires positive evidence that the predicate holds. A value whose predicate evaluates to unknown does not satisfy the refinement … Under CWA, unknown collapses to false”; “unknown means information absence — a referenced field with no recorded value” (spec/reference/src/declarations/types-and-refinement/refinement.md:24, the Three-valued membership under OWA paragraph). That rule decides whether an element is a member. A view’s element filter inherits it unchanged; this RFD neither restates nor narrows it.
• D3 decides observability at a view boundary, for the elements the fixpoint leaves undefined. Its two halves land on opposite sides of the manual’s rule and neither contradicts it. Not included is exactly the manual’s verdict — an undetermined element is not in the served extent. Not dropped addresses a question the membership rule does not reach: whether the excluded region must stay readable. D3 says it must, and rides it on the $undefined:: companion. D3 is therefore additive.

The consequence is concrete, and it is conditioned on the world: under the closed-world default a braced-refinement element type over an unasserted field behaves under D3 exactly as the manual says it behaves today. The predicate is unknown, the manual collapses unknown to false under CWA, the value does not satisfy the refinement, it is not a member, and the fixpoint produces no undefined tuple for it — a definite empty extent and a definite count of zero, with no undefined region. D3 changes nothing there. Under an open world the manual does not collapse the unknown, so the same candidate is undetermined and D3 places it in the undefined region rather than excluding it; D3 is still additive there, because it is again following the manual’s verdict on the absence rather than overriding it. What D3 governs is the case the membership rule does not speak to: an element whose membership is decided by rules that recur through negation, where the alternating fixpoint pins the atom neither true nor false.

The truth-values chapter’s set-projection sentence is likewise consistent. “Set / list / record projections: Can-valued cells are omitted from the result set” (spec/reference/src/semantics/truth-values.md:31, K3 fail-closed projection) is scoped to the fail-closed projection of a single-standpoint query to a non-Truth4 type. D3 does not fold undefined elements into the returned set — it routes them to a name-distinguishable companion — so that projection still omits them, and the reasoning chapter already states the obligation the projection sentence leaves implicit: an undefined tuple “surfaces as a Can row, by default — never silently omitted, because an omitted standoff is byte-indistinguishable from a definite Not”, and the fail-closed projection “drops Can rows from the row list but still reports them in hidden.can — drop-but-count, never a silent collapse” (spec/reference/src/semantics/reasoning.md). Drop-but-count is D3’s own discipline one layer down, already surface law and already shipped.

Prerequisite this record inherits rather than owns. spec/reference/src/semantics/reasoning.md states that “A rule body still joins only against definite rows — an undefined atom does not fire downstream rules; propagating undefined-ness through body joins is the engine-level three-valued lift, tracked separately.” The classifier clause above (exists { p in self.f }, worked example E4) and any consumer that joins a lifted view’s undefined region into a further body depend on that lift. No slice in the Staging plan allocates it; it is a prerequisite, and the record does not own it. The two places that show such a consumer — worked example E4 and the authorized-signers scenario’s authorization gate — are marked at the point of use as intended behaviour awaiting the lift, not as output of the slices staged here.

Two build-time refusals are NOT standoffs and stay build errors:

• An unproductive positive view cycle (a view provably empty for every store — an unseeded cycle or acyclic dead-end) is a modeling defect that should be refused at build. This refusal is net-new analysis, not an edge-addition to an existing check. There is no check-plane productivity / positive-cycle graph on the tree for a view-element edge to be added to — established while building the check-plane slice (#1838). The elaborator (oxc-instantiate) does carry one rule-dependency graph — the defeat lint’s positive / negative / defeat edge graph with a Tarjan strongly-connected- component pass (oxc-instantiate/src/lower/defeat_lint.rs, the emitter of OW0740) — but it judges no productivity or emptiness and carries no view-element edges, and stratification lives in the reasoner’s compile step, not as a build refusal for a provably-empty view. Landing this refusal therefore requires building a view-element dependency graph in the check plane from scratch — a distinct, explicitly-staged increment (staged after the runtime slice; see the Staging plan), not an extension of a pre-existing check. Reserved-not-wired (diagnostic OE0684) until that slice lands; whether to build it or defer it is an owner decision (Open questions).
• A view whose lift would be ambiguous or incomparable at a field read (D1) refuses at build (the pin ladder’s Incomparable / Ambiguous).

Rejected boundary policies (see Alternatives): dropping undefined (Can-to-Not), including undefined (Can-to-Is), and a global refuse-on-any- undefined (kills the honest-propagation case the Motivation needs). The chosen policy is surface-honest: the definite extent is always available, the undefined region is always distinguishable, and the consumer declares whether a standoff blocks it — which is exactly the commit-time twin the admission RFD owns for writes (D7).

D4 — Resolution contract (non-goal: rewriting the resolution pass)

The pin ladder consumes the per-scope resolution results; it does not rewrite the resolution pass. The failure this contract forecloses is two coexisting scope models in lower/rule_ref.rs — a second scope-tracking design standing alongside the per-scope reading/declarer oracles. Two models can disagree at a position on whether a name reads as a binder or as a relation application, and the pin ladder’s choice of cell keys on exactly that judgment, so a field read’s canonical cell would depend on which model answered rather than on the program. This RFD’s contract:

• The ladder’s classifier reads the declarer / chain-locality / ancestry oracles the resolution pass already exposes per scope. A name reads as a binder at a position iff a binder for it is in scope at that position; a relation-application analysis is judged per scope. There is exactly one scope model in rule_ref.rs.
• The ladder adds no new resolution semantics. Where it needs a workspace <:-ancestry answer a file-local oracle cannot give (cross-module pin fallback), it calls the existing workspace-walk classifier, mapping its outcome into the cell lattice — it does not re-resolve names.
• Cross-module: the runtime and the build-plane view validator consume the same resolved reference the checker accepted — never a re-resolution, which could go ambiguous (false refusal) or silently miss (under-refusal). This is the import-parity invariant (D7 test obligation).

D5 — Interaction with mapped relation subsumption (RFD 0084)

RFD 0084 (merged) made <: on relations an explicit argument-mapped form: a child contributes, for each parent end, a mapped image φ of its tuple (rename / cast / constant pin), and subsumption is mapped-tuple-inclusion (the image of the child under φ), not positional tuple-inclusion.

A view walks a relation’s subsumption-closed extent (verified: catalog_seed reads the closed extent so a projection includes subsumed children). Therefore a view walking a parent relation sees the φ-images of member facts, not the child tuples:

• The value the view projects at the walked endpoint is φ’s filler for that parent end — a renamed child end, a cast child end, or a constant pin (e.g. WagesUSA(p, amount) <: IncomeItem(p, amount, c = USD) contributes IncomeItem(p, amount, USD); a view over IncomeItem.c sees USD).
• The element-type test <T>(x) and the holder-endpoint resolution run over the parent frame (the φ-image). RFD 0084 D1 forbids dropped child ends, so the parent frame is information-complete — the holder endpoint is always present in the image, and the arity >= 3 holder resolution (verified in catalog_seed) keeps its uniqueness precondition.
• No new mechanism: the view consumes the one canonical resolved-mapping structure RFD 0084 already threads through every plane. This RFD states the interaction; it does not re-lower subsumption.

D6 — Maintenance contract (compatibility with the incremental strict model)

The incremental-maintenance plane — defeat-plane compilation (RFD 0083) and the incremental rule circuit compiler (RFD 0085) — makes the strict model survive commits by delta. The raw + gate split is stated compatibly, without deep integration:

• The raw cell $rawfield::<C>::<f> is an ordinary EDB projection: it is maintained by delta as backing-relation facts arrive/retract, by the same circuits that maintain any seeded relation. No walk recomputation.
• The gate clause is an ordinary strict WFS rule: it is re-evaluated by the same incremental fixpoint circuits (project / map / union) that maintain every membership rule. A change to <C>(x)’s extent flows to $field::<C>::<f> through the gate, incrementally.
• The undefined companion $undefined::$field::<C>::<f> is maintained as the companion of any fixpoint relation — no view-specific maintenance path.

This RFD does not specify the incremental circuit internals; it commits only to the shape (raw = delta-maintainable EDB, gate = fixpoint rule) so that a lifted view imposes no new full-recompute obligation on the maintenance plane.

D7 — Filtered views stay store-local and refuse at build (fail-closed)

The non-goal boundary of the lift. Stated as its own decision because the rest of the record cross-references it by number.

What a where filter can say today. In f: [T] from Rel.endpoint where P, the only variable the clause binds is the PROJECTED ENDPOINT, named endpoint. Each form below was run against the checker rather than read off the grammar: a type test (where endpoint : T2), a rule call (where somePredicate(endpoint)) and a field predicate (where endpoint.age < 13) all check. Every filtered example in this record has been rewritten to that spelling — the earlier examples wrote where somePredicate(self), which does not parse into anything the checker accepts, so a reader copying one hit a refusal on a form the record presented as working. That is a correction to the examples, not a statement that the endpoint spelling is the right long-term surface.

The holder is unreachable — a known gap, tracked. The correction above does not settle what the clause OUGHT to bind. self is the spelling a modeller reaches for, and whether it should work here is genuinely open: the reference manual’s only definition of the keyword makes self the enclosing declaration’s subject (which for a field is the HOLDER), while the elaborator’s own lowering of this very clause renames the endpoint binder to self (making it the projected ELEMENT). The examples that used to appear here read as the second; the synthesized lift rule earlier in this record names the holder self, which reads as the first. Separately from that ambiguity, no spelling at all reaches the holder: the relation’s other endpoints are not bound either, so a condition relating a projected element to the holder’s own state (“the dependents under this taxpayer’s own cap”) cannot be written. Both the ambiguity and the missing capability are recorded in issue 2007, which also states why widening the scope is entangled with narrowing this decision.

• Filtered views stay store-local. A where-filtered view whose element type or filter type-test target is standoff-capable is not lifted; it is refused at build, fail-closed. A filtered view over a braced refinement is accepted and unchanged — it has no standoff to mishandle, so refusing it would reject a program that materializes store-local and serves correctly today. The where machinery (OWA-unknown exclusion, value predicates over the field bag) is not hosted by the fixpoint lowering, and a store-local read of a fixpoint-dependent membership can only fail loud at runtime — check-green / runtime-dead is never admitted.

D8 — One shared principle with the admission-point-checks record, and no shared mechanism

• No shared new dispatch structure with the admission RFD. Both this RFD and the parallel admission-point-checks RFD touch three-valued surfaces. They share exactly one principle (the boxed statement in D3): undetermined never silently coerces, and each construct declares its policy. They do not share a new dispatch mechanism. The view’s policy (D3: surface-honest at the read boundary) and admission’s policy (its own per-check disposition, derived from the check’s declared severity and its observe marker, judged at the admission point of the write under judgment) are independent. Coupling the two into one severity-dispatch substrate is rejected for a stated technical reason (Alternatives): severity is a property of a check declaration, and a view read boundary has no check and therefore no severity to dispatch on, so a shared substrate would have to invent one for the read side — and would then make neither surface changeable without the other. This RFD keeps them decoupled deliberately.

D9 — The lift is a derivation-semantic change: epoch bump plus projection-cache commitment

Lifting a view changes what the derivation means for the same source and the same artifact, not merely how it is computed: a filter-free view over a standoff-capable element type served a store-local two-valued extent before the lift, and serves a fixpoint extent plus an undefined region after it.

So the lift MUST bump DERIVATION_SEMANTIC_EPOCH, and the change MUST be entered in the projection-cache derivation_commitment of RFD 0072. The failure this prevents is specific rather than hygienic: the projection cache is keyed on a derivation-input commitment, so without the epoch entry a cache populated before the lift stays live afterwards and serves the pre-lift model — and because the binary is the same on both sides, no same-binary differential arm catches it. The full statement of the obligation, including what a stale cache would serve, is under Consequences.

Restated non-goals

• The resolution pass is not rewritten (D4). Relation subsumption is not re-lowered (D5). The incremental circuits are not modified (D6).

Worked examples with I/O

Model as in Motivation. alice is a Taxpayer; Supports(alice, bob), Supports(alice, carol), Supports(alice, dave).

E1 — definite membership

bob satisfies every QualifyingChild test (all definite-true). carol fails the age test (definite-false).

query alice.dependents
→ { bob }                        // carol excluded — a real exclusion, not a standoff

Lowering: $field::Taxpayer::dependents(alice, x) :- Taxpayer(alice), Supports(alice, x), Dependent(x). Dependent(bob) ∈ I; Dependent(carol) definite-false; dave below.

E2 — undetermined membership surfaces, does not silently resolve

dave’s sharesResidence test stands off in a negation cycle → Dependent(dave) is undefined (∈ J ∖ I).

query alice.dependents
→ { bob }                        // definite extent
   standoff: { dave }            // $undefined::$field::Taxpayer::dependents — surfaced, not dropped

dave is neither in the returned set (would be Can-to-Is) nor silently gone (would be Can-to-Not). The read reports the standoff region.

E3 — aggregate over a view with a standoff (both consumer surfaces)

The same count-over-dependents aggregate meets two different concrete surfaces depending on the consumer kind (D3 “Consumer-surface reality”). E3a is the check that discharges three-valuedly; E3b is the scalar derive that refuses.

E3a — the check (three-valued discharge, works).

check ExemptionCount { count { d in self.dependents } == self.claimedDependents }

With E2’s store: the input set has definite { bob } and undefined { dave }. count is not served a fabricated scalar — it is undefined at this read (the undefined element could change the count from 1 to 2), so the check verdict is undefined and surfaces per the K3 check-discharge pass rather than passing on count == 1. Under E1’s store (no undefined region) count { d in self.dependents } == 1 and the check discharges normally.

E3b — the scalar derive (OE1332, the runtime refusal raised while ox build maintains the read model).

A value derive binding the same count into a scalar cannot hold “undefined”. The undefined region propagates as a refusal — the pre-existing aggregate-over-undefined guard (OE1332), not a new refusal introduced by the lift:

pub derive dependentCount(h, n) :- Household(h), n = count(d for d in h.dependents);

Run-verified on the runtime implementation draft, #1839 (the model is this RFD’s run-verified exhibit — bob a definite Dependent, dave undefined — with the scalar dependentCount derive added); ox build:

Error:   × projection cache: strict-model derivation: operation failed: incremental
  │ read-model maintainer: OE1332: aggregate folds over
  │ `$field::Household::dependents`, which has well-founded-undefined atoms
  │ (recursion-through-negation left part of its extent neither true nor
  │ false). Folding would silently treat `undefined` as false — refused rather
  │ than computing a biased result. Aggregate over a definite predicate:
  │ stratify `$field::Household::dependents` so it has a settled extent, or
  │ interpose an intermediate `pub derive` that is itself definite (#250
  │ tracks three-valued aggregate intervals).

The steer: move the consumer to a check (E3a, discharges three-valuedly), or read the view’s regions directly (E2 — definite rows plus the undefined companion). A friendlier teaching render specific to the aggregate-over-a-view’s- undefined-region collision is a recorded cheap follow-up (Open questions), not allocated here.

E4 — classifier consuming the view (undefined case blocked on a prerequisite)

type Sponsor <: Taxpayer iff exists { d in self.dependents };

The bare exists over the lifted view re-homes Sponsor to the rule plane. For alice under E1, Sponsor(alice) is definite-true (bob witnesses). Under a store where alice supports only dave (E2’s undefined), Sponsor(alice) is undefined — the existential over an all-undefined witness set is undefined per K3, not false.

The definite half is deliverable; the undefined half is not, and this example states intended behaviour for it rather than what the stack produces. Runtime slice A synthesizes the classifier re-homing clause, which is what puts Sponsor on the rule plane, so the alice/bob reading above follows from this record’s own slices. The dave reading does not: for a standoff in self.dependents to make Sponsor(alice) undefined rather than leave the head underived, undefined-ness must propagate through the classifier rule’s body join, and the reasoning chapter restricts a rule body to joining “only against definite rows — an undefined atom does not fire downstream rules; propagating undefined-ness through body joins is the engine-level three-valued lift, tracked separately” (spec/reference/src/semantics/reasoning.md:57). That lift is the prerequisite this record inherits rather than owns (D3) and no slice in the Staging plan allocates it. Until it lands, the re-homed classifier body sees only the view’s definite rows, so the standoff does not reach Sponsor’s head. Nothing else in this record turns on the lift — D3’s read-surface arm and its aggregate arm both read the view head’s own $undefined:: companion directly, and the Lean obligations of Staging step 1 are statements about that head’s regions — which is why the lift stays out of scope and this example carries the marker instead.

E5 — filtered view over a standoff-capable target refuses at build

type Taxpayer <: Person {
    // where-filtered AND standoff-capable element type → not liftable
    minorDependents: [Dependent] from Supports.supported where under13(supported)
}
→ build error (fail-closed): a `where`-filtered navigation view whose element
   type has a shape-derived membership cannot be evaluated store-locally without
   a possible loud runtime failure; refused at `ox check` / `ox build`.

// The same filter over a BRACED-refinement element type is ACCEPTED:
type Adult <: Person iff { self.age >= 18 };
type Taxpayer <: Person {
    adults: [Adult] from Supports.supported where over21(supported)
}
→ accepted, unchanged. `Adult`'s predicate cannot call a rule (`OE0660`), so it
   is two-valued and never stands off; there is nothing for the refusal to
   protect against.

E6 — imported backing relation / element type

Supports declared in module family, Dependent in module tax, both imported into the module declaring Taxpayer. The runtime and the build-plane view validator both consume the checker’s resolved references for Supports and Dependent — no re-resolution. A cross-module pin that the file-local oracle cannot answer falls to the workspace <:-ancestry walk (D1 L3); the result keys the same cell the checker accepted, so there is no false-ambiguous refusal and no under-refusal.

Rationale — the decision table

Per-decision status, because the record’s single State: discussion header cannot express it. The state model is binary — discussion means not committed, committed means decided and binding — and this record is genuinely mixed: one arm of one decision is open and the rest are settled as written. The header stays discussion because the record as a whole is not binding until that arm closes; this column says which rows are waiting on it.

Diagnostics

These are the allocated code numbers, reconciled with the check-plane slices. Each row is anchored to the implementation lane that carries it rather than to a pull request, so the row survives that pull request merging or closing; none of the four is emitted on the default branch yet.

Coordination held across the three lanes drawing from these ranges — this record, the admission-point-checks lane, and the instance-relations lane (OE0740 / OE0741 for its refusals, plus one warning) — so no code double-allocates. Two range facts, checked against the default branch: the OE026x range is allocated through OE0268, so a fresh allocation there now starts at OE0269; and the OW074x range is allocated through OW0744 (OW0742 duplicate-fact-in-file, OW0743 declaration-shadows-import, OW0744 check-not-exhaustive-over-undetermined), so OW0742, which the instance-relations lane’s warning claim named, is taken and the next free warning slot is OW0745 — a matter for that lane, not this record. This record’s own four codes are unallocated on the default branch and uncontested.

Range fact, checked against the default branch: no code in the OE068x range is emitted or reserved anywhere on the tree. This record claims exactly OE0683–OE0686 as tabulated above; OE0680, OE0681 and OE0682 are not claimed by it, so an older citation naming one of those does not designate any condition in this record.

The view boundary’s runtime honesty is not a refusal: an undefined element rides the $undefined:: companion and is surfaced (D3), reusing the existing K3 $undefined:: machinery and check-discharge K3 pass — no new runtime refusal code. The commit-time twin (an undetermined membership observed at a write’s admission point) is the admission-point-checks record’s construct with its own policy and its own code — OE1430, named by that record, which is now on the default branch with the code allocated and live in the catalogue, alongside OE1431 for the determinedness operator’s plane boundary. Both slots are that lane’s; this RFD does not allocate them and does not contest them.

Alternatives considered

• Store-local materialization for every element type (status quo). Keep evaluating membership at seed time. Rejected for standoff-capable element types: the seed-time plane has no undefined region, so for a shape/rule element type a standoff fails closed (the store-local read refuses — oxc-runtime/src/classify.rs returns Can; the refusal is RuntimeError::MembershipFixpointDependent (oxc-runtime/src/lib.rs, cited by symbol — the line moves with the tip); run-verified exhibit) and only a field-refinement open-world-unknown is silently coerced to Ok(false) (verified in index.rs) — neither can represent the standoff. Retained for ordinary element types and for filtered views (D7) — this RFD narrows, it does not replace.
• Eager coercion of undetermined to a two-valued verdict at the boundary. Either include undefined (Can-to-Is) or drop it (Can-to-Not). Both fabricate an extent; the Motivation shows each produces a different wrong tax answer that passes checks. Rejected — this is the exact dishonesty the RFD exists to remove.
• Global refuse-on-any-undefined at the view boundary. Refuse any read whose extent has a non-empty undefined region. Rejected: it kills the honest- propagation case (E3/E4), where the consumer is the right adjudicator; a standoff is a runtime value, not a modeling defect (unlike the productive-cycle refusal, which is).
• A shared undefined→severity dispatch substrate with the admission RFD. Fold the view’s read-boundary standoff and admission’s write-boundary severity decision into one dispatch mechanism. Rejected on the mismatch of what the two boundaries have to dispatch on: severity is a property of a check declaration, so the write boundary always has one to consult, while a view read has no check and no severity — a shared substrate must therefore invent a synthetic severity for every read, and the invented value, not the modeler’s, would decide what the read surfaces. Coupling also removes independent evolution: a change to either boundary’s policy would have to be made in the shared mechanism and re-validated against the other, so neither can ship or change alone. This RFD keeps the principle shared and the policies + dispatch independent (D8).
• Implementing the three surfaces as one combined change rather than re-deriving each against main. The pin ladder, the raw + gate cells and the K3 boundary can be built together with a per-scope resolution rewrite and a coupled severity dispatch, on a derivation-semantic epoch numbered off a floor other than the default branch’s. Rejected because each of the three couplings is a design this record decides against on its own technical merits: a second scope model in the resolution file makes a field read’s cell depend on which model answered (D4), a coupled severity dispatch forces a synthetic severity onto a read boundary that has none (D8, above), and an epoch numbered off any floor but the default branch’s cannot be checked against the projection-cache derivation commitment that actually ships (D9). A combined change would carry all three; this record takes the epoch bump off the default branch’s floor and keeps the other two contracts as stated.

Consequences

• Derivation-semantic epoch bump and the projection-cache commitment (D9) — the downstream obligation this record carries. Lifting a view changes what the derivation means for the same source and the same artifact, not just how it is computed: a filter-free view over a standoff-capable element type served a store-local two-valued extent before the lift and serves a fixpoint extent plus an undefined region after it. So the lift is a derivation-semantic change and MUST bump DERIVATION_SEMANTIC_EPOCH, and the change MUST be entered in the projection-cache derivation_commitment of RFD 0072. The failure this prevents is specific: the projection cache is keyed on a derivation-input commitment, so without the epoch entry a cache populated before the lift stays valid by its own key and a strict read is served a pre-lift model — and because both sides run the same binary, no same-binary differential detects it (RFD 0072 D5). The obligation therefore has two halves, and neither discharges the other: the epoch bump invalidates pre-lift caches, and the cache-seeded ≡ recomputed differential arm over a lifted-view fixture proves the post-lift cache agrees with recomputation. Both land in the same slice (Staging plan step 5). Whether the bump composes cleanly with the derivation_commitment state on the default branch is confirmed before that slice lands (Open questions).
• Artifact and wire. Additive. The lift adds synthesized relation heads ($rawfield::<C>::<f>, $field::<C>::<f> and its $undefined:: companion) and no new wire field, marker, or projection mode — a view’s undefined region reaches a consumer through the four-valued envelope every other derived read already uses (D3).
• Observable surface — no new grammar, three new observables. The view spelling is unchanged and there is no user-visible mode selector, but the observable surface does change in three ways, and the no-new-grammar claim must not be read wider than the grammar: a filter-free view over a standoff-capable element type becomes buildable where it is not today; its where-filtered variant becomes a coded build refusal; and a field read gains a new observable, the undefined region. A view over a braced refinement is unaffected in every direction.
• Source compatibility — one break, at the filtered case. A narrowing view onto a defined element type is permitted today, its membership decided by evaluating the refinement predicate per candidate at seed time (“Today’s behavior”). Under D7 the where-filtered member of that family becomes a build refusal (OE0683, E5), so source that carries a filtered view over a standoff-capable element type stops building and must drop the filter or narrow the element type to a non-computed concept. Unfiltered views over ordinary and braced-refinement element types keep store-local materialization unchanged and pay nothing.
• Maintenance cost. None new in kind: the raw cell is a delta-maintained EDB projection and the gate is an ordinary fixpoint rule, so a lifted view imposes no full-recompute obligation on the incremental plane (D6).
• Diagnostics. Four codes, none emitted on the default branch: OE0683 (filtered-view refusal) and OE0685/OE0686 (pin incomparability) land with the check-plane slice; OE0684 stays reserved-not-wired until — and unless — the net-new view-element dependency graph is built, which is an open owner decision. The runtime boundary adds no refusal code of its own.
• Mechanization owed. The substrate statements come first (Staging plan step 1): a navView_extent_wf lemma and a navView_no_silent_coerce corollary against Argon.Reasoning.Datalog.WellFounded, homed either in a new Argon/Reasoning/Datalog/NavView.lean or as an extension of FieldView.lean. Until they exist, no runtime slice may land ahead of them.
• Reference manual. Net-new chapter text, no amendment. The refinement chapter’s membership rule and the truth-values chapter’s projection rule both stand as written, and the reasoning chapter’s drop-but-count envelope contract is the surface D3 reuses rather than replaces (D3, Staging plan step 7).
• Not delivered here. Propagating undefined-ness through a rule body join is the engine-level three-valued lift; this record inherits it as a prerequisite, owns it nowhere, and stages no slice for it (D3). Two documented consumers — the classifier of worked example E4 and the authorization gate of the authorized-signers scenario — state intended behaviour that waits on that lift, and are marked as such at the point of use.

Open questions

1. Aggregate-over-undefined granularity (D3/E3). The three-valued-interval track (#250/#134) can sometimes prove an undefined element cannot change an aggregate result (e.g. count >= 1 when the definite region is already non-empty). How much of that partial-definiteness should the view boundary exploit before declaring the aggregate undefined? Conservative default: undefined whenever the undefined region is non-empty and could change the result.
2. Wire shape of the surfaced standoff (D3) — SETTLED by what ships; only the typed accessor is still open. The undefined region rides the $undefined::$field::<C>::<f> companion relation and is read through the normal derived-query surface. Nothing new is needed on the wire: the four-valued envelope already carries a head’s undefined companion tuples as Can rows and already counts them in hidden.can (compiler/crates/oxc-mcp/src/convert.rs; D3), so a lifted view’s region reaches a consumer through the same surface every other derived read uses. The companion is distinguishable by name, which satisfies D3’s “surfaced loudly, machine-readable” guarantee.
   • (a) Canonical surface — SETTLED. The $undefined::$field::<C>::<f> companion is the canonical definition of a view’s undefined region; both the hidden.can count and the truth-4 / --explain Can block are projections of that same companion, not independent computations — so the surfaces cannot drift semantically.
   • (b) Typed SDK accessor — OPEN (no code, no allocation now). Generated SDKs should grow a typed per-view accessor for the undefined region so clients bind to an API rather than hardcoding the $undefined::$field::… naming convention. Staged with whatever slice first teaches the SDK generator about views; not required for the runtime slice.
   • (c) Wire-contract pin — PROPOSED. The companion’s served shape is a compatibility surface. A pin (nav_view_lift_fixpoint) asserts the companion’s name shape and served row shape for the exhibit view Household::dependents, so a future change to the companion breaks a test rather than a client.
3. Final diagnostic allocation. Which concrete codes the in-flight lanes take from the free block — settle jointly before any implementation slice. The admission-point-checks lane is no longer among them: its record has landed on the default branch naming OE1430 for the write-boundary refusal, so the joint settlement is now between this record’s four codes and the instance-relations lane’s, whose warning still owes itself a fresh number (see Diagnostics).
4. Nested views (self.f.g where f and g are both lifted). The design composes in principle (each is a fixpoint relation), but the productivity / cycle analysis over composed view-element edges needs a stated bound. Note the view-element dependency graph this bound is stated over is itself net-new (see D3 / the OE0684 staging item) — the elaborator’s only rule-dependency graph today is the defeat lint’s, which judges no productivity and carries no view-element edges — so this is a design obligation of that net-new slice, not a tweak to an existing analysis.
5. Build vs. defer the unproductive-view-cycle refusal (OE0684). The refusal requires a net-new view-element dependency graph in the check plane (D3; the check-plane slice, pull request #1838, found no productivity graph to extend). Owner decision: build it as its own staged slice (Staging plan step 6) or defer it and leave OE0684 reserved-not-wired. Until settled, an unproductive positive view cycle is not caught at build.
6. Epoch composition with the projection cache (D9). Confirm the lift’s epoch bump composes cleanly with the RFD 0072 derivation_commitment state on current main before the runtime slice lands.
7. Friendlier teaching render for aggregate-over-a-view’s-undefined-region (cheap follow-up, not allocated). A scalar derive counting over a lifted view with a non-empty undefined region refuses with the generic aggregate-over-undefined guard OE1332 (D3 E3b, run-verified). OE1332 names the synthesized $field::<C>::<f> relation, which is correct but not oriented to a modeler thinking in terms of “my count over self.dependents.” A dedicated, view-aware teaching render (possibly its own code later) that names the view and points at the check / direct-read alternatives would be a cheap ergonomic win. Open — do not allocate a code now.
8. Carrier for an open-world element type’s undefined region (D3). D3’s undefined region is world-conditioned, so a view whose element type is marked #[world(open)] has an undetermined candidate that is not a fixpoint standoff: it is an unrefuted absence. The derive-plane companion $undefined::$field::<C>::<f> records fixpoint outcomes only and cannot carry it; the derive plane’s present answer to an open-world absence under negation is a refusal (OE1367), and the check plane keeps the union in a separate region of its own. Three candidates, none decided here: restrict the lift to closed-world element types and refuse an open-world one fail-closed (smallest, consistent with D7’s treatment of the filtered case); widen the derive-plane companion to carry open-world absence, which is the general three-valued open-world propagation OE1367 currently stands in for and is far larger than this record; or serve the view’s region as the union computed at the boundary, which needs its own soundness argument against the companion’s stated meaning. Settle before the runtime K3-boundary slice (Staging plan step 4), since that slice is what fixes the region’s carrier.

Staging plan

Land Lean-first, then check plane, then runtime slices — never a runtime slice ahead of its substrate obligation.

1. Lean (substrate first). Extend Argon.TypeSystem.Soundness.FieldView (already the reader of the from_relation clause, RFD 0005 §5.6) with the standoff-capable element-type case, and state the view-in-WFS semantics against Argon.Reasoning.Datalog.WellFounded: a lifted view’s extent is the wfTrue slice of $field::<C>::<f> and its undefined region is the wfPossible ∖ wfTrue slice (the K3 boundary of D3). New statement plan: a navView_extent_wf lemma (definite/undefined regions coincide with the fixpoint’s I / J ∖ I at the view head) and a navView_no_silent_coerce corollary (an undefined element is in neither the definite-true nor the definite-false region). Home: a new Argon/Reasoning/Datalog/NavView.lean importing WellFounded + FieldView, or an extension of FieldView.lean — decide at slice time.
2. Check plane. The pin ladder (D1) as the single cell-resolution discipline in lower/rule_ref.rs consuming the per-scope oracles (D4); the lift predicate (filter_free && element_membership_dependent) shared by lowering and runtime; the build refusals OE0683 (filtered fail-closed) and OE0685/OE0686 (pin incomparability). The unproductive-view-cycle refusal (OE0684) is not in this slice — it is net-new productivity-graph machinery, staged separately (step 6). Import-parity: the build-plane view validator consumes the checker’s resolved references (D4).
3. Runtime slice A — lowering. Module::load synthesizes the $field::<C>::<f> fixpoint rule, the raw+gate gate clause (D2), and the classifier re-homing clause for a lifted exists; records the raw-gated-cell load-time fact.
4. Runtime slice B — seeding + K3 boundary. catalog_seed emits the extent-blind $rawfield:: cells (D2) and excludes them from the ordinary concept-keyed companion seed; the read path surfaces the $undefined:: companion at the view boundary (D3) instead of the seed-time nav_catalog_keeps_value two-valued drop for lifted views (store-local materialization stays for unlifted views).
5. Runtime slice C — epoch + cache. Bump DERIVATION_SEMANTIC_EPOCH; enter the change in the RFD 0072 projection-cache derivation_commitment; add the cache-seeded ≡ recomputed differential arm for a lifted-view fixture (D9).
6. Check plane (net-new) — unproductive-view-cycle refusal (OE0684). Build a view-element dependency graph in the check plane and refuse a provably-empty positive view cycle. Explicitly staged here, after the runtime slice, because the check-plane slice (pull request #1838) established this is net-new productivity analysis — the elaborator’s only rule-dependency graph, the defeat lint’s, judges no productivity and carries no view-element edges, so there is nothing to extend — not an edge-addition to an existing check (D3). Owner decision: build vs. defer; until built, OE0684 stays reserved-not-wired.
7. Book. Document the standoff-capable view surface and the standoff boundary in the reference once the runtime slices are green. Net-new chapter text, not an amendment: the refinement chapter’s membership rule and the truth-values chapter’s projection rule both stand as written (D3 composes with them, see D3), and the reasoning chapter’s drop-but-count envelope contract is the surface D3 reuses rather than replaces.

Index rows

README table row:

| [0087](0087-fixpoint-typed-views.md) | Fixpoint typed views: a typed navigation view (`f: [T] from Rel.endpoint`) whose element type `T` is standoff-capable (a shape-clause concept whose membership is a rule head the well-founded fixpoint can leave undefined; a braced `iff { P }` refinement cannot stand off and is out of scope in both directions) is evaluated IN that fixpoint rather than materialized store-locally — a single pin-resolution ladder keys every concept-pinned field read, a raw (extent-blind EDB) + gate (fixpoint rule) split keeps a fixpoint-decided extent live and delta-maintainable, and the K3 standoff at the view boundary is surface-honest (definite extent served, undefined region rides `$undefined::` and surfaces loudly — never silently included or dropped, the consumer adjudicates); the ladder CONSUMES the per-scope resolution pass (no rewrite, one scope model), a view over a subsumed-parent relation walks the φ-images of RFD 0084, filtered views over a standoff-capable element type refuse fail-closed, and it shares ONE principle with the admission-point-checks RFD (undetermined never silently coerces; each construct declares its own policy) with independent policies and no shared dispatch structure; rides a derivation-semantic epoch bump. The standoff policy's aggregate arm is the one piece still undecided | discussion |

SUMMARY list row:

- [0087 — Fixpoint typed views: standoff-capable navigation views evaluated inside the well-founded fixpoint](0087-fixpoint-typed-views.md)