RFD 0093 — iof denotes membership, whole

• State: discussion
• Opened: 2026-07-25
• Decides: that iof(x, C) denotes an individual’s membership in C, whole — asserted classification, <: closure, predicate-refinement-derived membership, and rule-derived membership alike — and that extent and meta follow it. C(x), x : C, and iof(x, C) become three exact spellings of one question — for a bare or module-qualified concept path; the self::-qualified path is a separate, unfixed defect (issue #1904). Undefined membership remains the third truth value and must not collapse to false.
• Does not fix — and these are protected from the fix, not overlooked by it: meta(x) == C stays narrower than iof under upward <: closure (the metatype yields <:-minimal classifiers, by design); x :: C and self::-qualified iof stay refused; the self::-qualified type test stays broken, as issue #1904. Detail in Non-goals.
• What is being asked for is the semantic decision (D1), not a mechanism. Two mechanisms deliver identical semantics and both are live: (a) make $iof rule-derived, through generated bridge rules from each concept’s own membership atom — the form D2–D5 are written against; or (b) rewrite constant type positions at elaboration and materialize the relation once at a stratum boundary above every read. Either way iof, extent, and meta answer full membership, the individual-tier seed scan goes away, extent(t) becomes a projection over $iof, and $meta’s individual tier becomes an antichain over $iof. Where D2–D5 name bridge rules they are describing mechanism (a) concretely enough to be argued about, not ruling out (b).
• Affects: the reflection materializer (compiler/crates/oxc-runtime/src/standpoint.rs, compiler/crates/oxc-runtime/src/catalog_seed.rs); the rule-body atom-resolution and ad-hoc lowering paths (compiler/crates/oxc-instantiate/src/lower/rule_ref.rs, compiler/crates/oxc-instantiate/src/lower/adhoc.rs); the bare-name type-test lowering it is made to agree with (compiler/crates/oxc-instantiate/src/atom_lower/mod.rs); the extent desugaring (compiler/crates/oxc-instantiate/src/atom_lower/source.rs); the reasoner’s stratification and incremental-maintenance model (compiler/crates/oxc-reasoning/); and the specifying chapter spec/reference/src/declarations/meta-calculus.md. It does not affect the Lean mechanization — see D6.
• Relates to: RFD 0023 (the reflection intrinsics), RFD 0017 (refinement classification), RFD 0027 (the meta-property plane and the catalog tiers), RFD 0070 (derive-backed classification).

In plain language — what is wrong, and what this restores

Argon lets a modeller define a concept by a rule instead of by assertion:

pub derive IsRegistered(p: Person) :- Registered(p);
pub type Voter <: Person iff IsRegistered(self);

Nobody writes down who the voters are. The reasoner works it out. This is a shape-defined concept (RFD 0070); the shape clause must name a pub derive.

Now read that membership back. The reference manual says x : T is sugar for iof(x, T) — the same question, spelled two ways. They do not agree:

• Voter(p) finds the voter.
• p : Voter finds the voter.
• iof(p, Voter) finds nobody, silently, with no diagnostic.
• meta(p) == Voter finds nobody, silently. Worse, meta(p) reports that person’s most-specific type as Person — a true statement replaced by a less true one.
• not iof(p, Voter) matches everybody, including the genuine voter, because the relation it negates over is empty.

Every one of those is executed with real output in Demonstration.

The cause is mechanical. iof reads are served by enumerating a relation named $iof that the runtime builds when it loads the store — before the reasoner runs. A shape-defined concept’s members are decided by the reasoner. The builder cannot see them, so it writes no rows, and $meta, which is computed from the same scan in the same pass, inherits the hole.

The thesis of this record is that the meaning was never in doubt. Three design records and a Lean theorem already define iof as membership including derived membership; the materializer’s own source comment claims the inclusive reading. The narrow behaviour is a hole in one builder, not a narrower definition.

The remedy belongs to the relation, not to the read sites. A fix confined to constant type positions makes iof(x, Voter) and iof(x, t), t == Voter answer differently — the same question, two answers; that shape is recorded and rejected in Alternatives. So the remedy goes where the hole is. The form D2 is written against is a generated rule per concept C saying “if C(x), then x is an instance of C”, with the reasoner — which knows the answer — filling the relation in. Every spelling then reads the same complete relation and they agree because they are looking at the same thing. Which pass computes that relation is still open (front matter); what this record asks for is agreement that the relation must be complete.

Two records were opened on this defect and they remain alternatives. The other is RFD 0092 — Membership-plane authority: fail-closed reads of derived membership (pull request #1874), which refuses an asserted-plane read of a derived-membership concept rather than answering it. The two share a diagnosis and differ on the remedy across the whole surface, including meta(x) == C: under the design below meta is derived from $iof like everything else, so that spelling is fixed rather than refused. RFD 0092 is argued at full strength in Alternatives.

Question

Does iof(x, t) mean “x’s membership in t”, or “x appears in the seed-time-materialized $iof relation for t”? These coincide for every concept whose membership is asserted or predicate-refinement-derived, and diverge for a shape-defined concept, where the second answers empty and the first does not. Which is the definition, and which is an implementation?

Context

Two membership planes

The seed plane. When a store is loaded, catalog_seed populates per-type extent relations from committed events — iof assertions plus <: closure — then runs the refinement-honesty pass, which composes each predicate-refined concept’s extent from its parent’s extent intersected with the refinement predicate. That pass exists precisely so derived membership is visible to ordinary reads (seed_base_catalog_in_frame_filtered in compiler/crates/oxc-runtime/src/catalog_seed.rs, the refinement-composition block):

// Refinement composition (refinement-honesty pass): for each
// concept with a refinement_predicate, compute its honest
// extent (parent extent ∩ predicate-true) and populate the
// catalog under the refined name. This lets rule bodies
// mention refined concepts like `Adult(p)` and get the
// semantically-correct set, not the (typically empty) set
// of individuals explicitly iof-asserted as Adult.

The seed plane is not lazy; it goes out of its way.

The rule plane. A shape-defined concept carries no refinement predicate (compiler/crates/oxc-protocol/src/storage.rs:298-308, the DefinedByShape variant: “The concept carries NO refinement_predicate (it is None)”; the invariant is enforced locally in the elaborator, lower_concept_decl in lower/concept.rs). Its membership is a synthesized concept-headed rule evaluated in the reasoner’s well-founded fixpoint. The refinement-honesty pass has nothing to compose, so the concept is absent from the seed plane’s extent map entirely (catalog_seed.rs:840):

// #1859 — a SHAPE-DEFINED concept (`type Thing <: Base iff
// isThing(self)`, RFD 0070) has no static or refinement-honesty extent:
// its membership is decided in the reasoner fixpoint. The
// refinement-honesty pass above classifies only `iff <predicate>`
// (`Defined`) concepts (a shape concept carries NO refinement
// predicate), so a shape concept is absent from `concept_extent_of_
// internal`, and the concept-keyed field-projection loops below would
// emit ZERO `$field::<Thing>::<field>` rows.

and names the failure mode at catalog_seed.rs:852: (checked-clean, silently-wrong).

Seed-time materialization cannot reach the rule plane for a structural reason, not an oversight: the reasoner has not run when the seed runs, and running it there would invert the dependency, because the fixpoint reads the seeded relations.

$iof and $meta are built by one scan, on the seed plane

Both reflection relations are materialized in one function, materialize_reflection_relations (compiler/crates/oxc-runtime/src/standpoint.rs:49), called once, from the seed, before the fixpoint (the tail of seed_base_catalog_in_frame_filtered).

The individual tier scans the per-type extents already in the catalog (the individual-tier loop of materialize_reflection_relations, standpoint.rs:74-110) and, in the same loop, accumulates a per-entity type set that $meta then reduces (standpoint.rs:64-65):

// Also accumulate the per-entity iof type SET (`iof_by_entity`), which
// `$meta` (below) reads to pick each entity's most-specific type(s).

$meta’s individual tier is that set filtered to its <:-minimal elements (the $meta reduction in the same function, standpoint.rs:159-174). This is why meta(x) == C and x :: C are broken by the same mechanism as iof, not by a second one: there is one scan, one source, and one hole. meta(x) == C is therefore a third silently-empty spelling. x :: C would break identically but never reaches evaluation — it is already refused (below), so it is a latent instance rather than a live one.

The catalog tier (the metatype-tier block of the same function, standpoint.rs:186-284) is different in kind, and the difference matters to the design. Its rows come from declarations only:

// Rows derive from DECLARATIONS only
// (catalog-closed, never from the ABox), so NAF over them is
// stratification-safe — the same justification as `$implements`.
// `meta` here is exact (a declaration has exactly one resolved
// introducer per the §3.4 gate), so the `<:`-minimality pass the
// individual tier needs does not apply.

Two further row sets — the reflective-sort extents and the declared type×type X : T rows — feed $iof only, never $meta, because “a type may be declared an instance of several higher-order types, so meta(X) … stays the §3.4 introducer”. The catalog tier is not an antichain over $iof and is not meant to be. D4 respects this; the naive reading does not, and Demonstration measures the discrepancy.

$specializes (the $specializes block of the same function, standpoint.rs:286-370) is the reflexive-transitive closure of the declared <: graph, type-tier only, both columns Value::Name. It is catalog-closed and stratification-safe for the same reason.

extent has no relation of its own

extent(t) is not a stored relation. It desugars to the reserved-head iof atom (lower_source in compiler/crates/oxc-instantiate/src/atom_lower/source.rs):

// RFD 0023 D4 — the explicit extent form `for e in extent(t)`:
// `extent(t)` lowers (expr_lower) to `App(Var("extent"), [t])`. Iterate
// it as the entity column of the `iof` relation restricted to type `t`
// — i.e. the reserved-head atom `iof(binder, t)`.

So extent inherits iof’s hole exactly, and fixing iof fixes extent with no separate work. Its command-line surface already fails closed: ox query --extent over a shape-defined concept refuses with RuntimeError::MembershipFixpointDependent (the RuntimeError variant in compiler/crates/oxc-runtime/src/lib.rs, raised from concept_admits_individual in compiler/crates/oxc-runtime/src/classify.rs and from select_member_impl in compiler/crates/oxc-runtime/src/store_read.rs). That refusal becomes unnecessary under this design and is retired by the slice that derives $iof.

How each read surface is served today

The bare name is kept honest by an early lowering that never reaches the reflection atom (atom_to_atom_ir in atom_lower/mod.rs):

#![allow(unused)]
fn main() {
return AtomIR::Predicate {
    path: vec![name],
    args: vec![operand],
};
}

The qualified type test is not a silent-empty bug. An earlier revision of this record recorded it as one, and as an open question about which plane it evaluates on. That was wrong, and the correction matters because it removes an item from the defect list rather than adding one. x : pkg::C is refused, by name, at check — before any lowering decision is reached:

OE0223: unresolved type `rfd93q::Voter` in type-test atom (a `c : T` atom
is membership in `T`'s extent; `T` must be a declared concept)

The lowering path behind it is fail-closed too: a qualified path falls through to AtomIR::TypeTest { ty: TypeExpr::Unknown } (the fall-through arm of the same function), which the rule compiler refuses as not-yet-evaluable, so the build aborts rather than deriving an answer. This surface therefore needs a better message, not a new diagnostic and not a semantic decision. The message currently says the type is unresolved, which is misleading when the concept plainly exists and only the spelling is unsupported.

x is C is a different construct entirely. is is a keyword, but it introduces the optional-payload test (is Some / is None) and the reasoning-outcome suffix (is unknown, and the refused is both / is ambiguous / is timeout) — see rule_atom and atom_suffix in compiler/crates/oxc-parser/src/rule_atom.rs. p is Voter does not reach the type-test path at all; it is read as a relation-valued application and refused with OE1386. Open question 1 records the audit this needs; no claim in this record covers it.

The book already contradicts itself

Three sites in one chapter, spec/reference/src/declarations/meta-calculus.md. Two promise full membership:

• :115 — “The rule-atom form x : T … is syntactic sugar for iof(x, T).”
• :123 — “extent has the signature extent(t: TypeRef) -> Set<Entity> … Returns the set of entities x such that iof(x, t) holds at the current state.”

One describes the asserted-only relation:

• :143 — “$iof (entity × type, closed under supertypes; this carries both tiers — the individual-tier rows from pub fact T(x) assertions and the catalog-tier type×type rows from each : T instantiation clause, the latter closed upward over the target type’s <: ancestors)”

The third sentence names two sources, neither of them the rule plane, and it is the only denotational statement the chapter makes about $iof. A reader who takes :115 and :123 at face value and a reader who takes :143 at face value will disagree about what the language does, and both will be citing the specification.

The meaning is already ratified elsewhere

• spec/rfd/0023-reflective-type.md:89 introduces the intrinsic as the general membership predicate — iof(x: Entity, t: TypeRef) -> Bool // sugar: x : T — with extent(t: TypeRef) -> Set<Entity> at :91, and gives the Lean characterization at :104: x ∈ extentOf u t ↔ x ∈ u ∧ iof x t. No materialization clause appears in the definition.
• spec/rfd/0017-refinement-classification.md:36 defines derived membership in terms of iof: “Membership is derived: extent(C) = { x : iof(x, parentᵢ) ∧ P(x) }”. If iof meant asserted-only, the equation would be ill-formed.
• spec/rfd/0070-derive-backed-classification.md:48 settles the shape case: “A shape-defined concept C is an ordinary atom iof(x, C) of the reasoner’s well-founded / AFT fixpoint — uniform with every other ground atom. There is no separate classifier fixpoint”. Line :143 records the biconditional as a proved surface promise: “L5 | parent/body split = surface promise iof(x,C) ↔ iof(x,parent) ∧ shapeBody | PROVED-scratch”.
• spec/lean/Argon/TypeSystem/Realization.lean:13-15 states the realization biconditional for the refinement case, and realize_iff (:82) proves it.
• Appendix C already states fixpoint-evaluated membership normatively: OE0258 (spec/reference/src/appendix-c-diagnostic-codes.md:139) — “Membership is the individual’s full classification (asserted iof UNION derived iff, <:-closed …)”; OE0240 (:121) and OE0241 (:122) — “membership evaluated in the fixpoint … including shape-defined members whose extent is never asserted”.

Demonstration

Every command with its output. One package, no mutations. Voter is shape-defined; alice is registered, hence a voter on the rule plane. Adult is an ordinary asserted concept holding bob, as a control.

Row sets, row counts, event counts, diagnostic codes, and message text are reproduced as emitted, and every output below was re-executed against an ox built from the main line this record is written against — none is inherited from an earlier revision. Four things are trimmed for readability and are the only edits: the module-path prefix on queries from a single-file package, the at vt=… wall-clock suffix an ad-hoc read prints, the multi-line help: body under a diagnostic, and the artifact byte size — which varies with the package name and carries no argument.

On the code fences in this record. The package immediately following is the only block fenced as checkable Argon. It checks clean, and that result comes from a local run: the documentation-example gate roots its scan at the reference manual’s source tree (run_check_doc_examples in compiler/xtask/src/doc_examples.rs joins spec/reference/src and walks only that tree), so it executes no fence in this directory. No block below is machine-verified by continuous integration.

Every other relational block anywhere in this record is an excerpt or is pseudo-relational, and carries a bare or ignore-flagged fence on purpose. Do not promote them: they are not self-contained and would not check. Were such a block moved into the reference manual, the gate would run ox check on it exactly as written, and an excerpt does not stand alone.

use std::core::type;
use std::core::rel;

pub type Person;

pub rel Registered(mut p: Person);

pub derive IsRegistered(p: Person) :- Registered(p);

pub type Voter <: Person iff IsRegistered(self);

pub type Adult <: Person;

pub derive ViaConceptAtom(p: Person) :- Voter(p);
pub derive ViaSugar(p: Person) :- p : Voter;
pub derive ViaIof(p: Person) :- iof(p, Voter);
pub derive ViaNegatedIof(p: Person) :- Person(p), not iof(p, Voter);
pub derive ViaMetaEq(p: Person) :- Person(p), meta(p) == Voter;
pub derive ControlAssertedIof(p: Person) :- iof(p, Adult);
pub derive ControlAssertedAtom(p: Person) :- Adult(p);

pub derive Nonminimal(x: Entity, c: TypeRef) :-
    iof(x, c), iof(x, d), specializes(d, c), d != c;
pub derive DerivedMeta(x: Entity, c: TypeRef) :-
    iof(x, c), not Nonminimal(x, c);

pub query q_concept_atom() -> ViaConceptAtom;
pub query q_sugar() -> ViaSugar;
pub query q_iof() -> ViaIof;
pub query q_negated_iof() -> ViaNegatedIof;
pub query q_meta_eq() -> ViaMetaEq;
pub query q_control_iof() -> ControlAssertedIof;
pub query q_control_atom() -> ControlAssertedAtom;
pub query q_nonminimal() -> Nonminimal;
pub query q_derived_meta() -> DerivedMeta;

pub fact Person(alice);
pub fact Registered(alice);
pub fact Person(bob);
pub fact Adult(bob);

ox check reports ok; ox build writes the artifact; ox query enumerates every declared query:

$ ox check .
ok
$ ox build .
wrote ./target/root.oxbin (31 events)
$ ox query .
query q_concept_atom: 1 row(s)
  (#i7582462787275748164)
query q_control_atom: 1 row(s)
  (#i8648907253816210642)
query q_control_iof: 1 row(s)
  (#i8648907253816210642)
query q_derived_meta: 11 row(s)
  (std::core::type, Metatype)
  (Voter, std::core::type)
  (Voter, TypeRef)
  (Adult, std::core::type)
  (Adult, TypeRef)
  (Person, std::core::type)
  (Person, TypeRef)
  (Registered, TypeRef)
  (Metatype, Metatype)
  (#i7582462787275748164, Person)
  (#i8648907253816210642, Adult)
query q_iof: 0 row(s)
query q_meta_eq: 0 row(s)
query q_negated_iof: 2 row(s)
  (#i7582462787275748164)
  (#i8648907253816210642)
query q_nonminimal: 1 row(s)
  (#i8648907253816210642, Person)
query q_sugar: 1 row(s)
  (#i7582462787275748164)

#i7582… is alice; #i8648… is bob.

The defect, four ways. q_concept_atom and q_sugar find alice. q_iof finds nobody. q_meta_eq finds nobody. q_negated_iof finds both people, including the genuine voter. The control is clean in both directions: q_control_iof and q_control_atom both return bob, so iof is not broken — it is broken for exactly one class of concept.

Reading $iof directly shows the missing row:

$ ox query . --eval 'pub derive q(p, t) :- iof(p, t);'
ad-hoc query: 12 row(s)
  (std::core::type, Metatype)
  (Voter, std::core::type)
  (Voter, TypeRef)
  (Person, std::core::type)
  (Person, TypeRef)
  (Registered, TypeRef)
  (Adult, std::core::type)
  (Adult, TypeRef)
  (Metatype, Metatype)
  (#i7582462787275748164, Person)
  (#i8648907253816210642, Person)
  (#i8648907253816210642, Adult)

(#i7582…, Voter) is absent. And $meta gives alice’s most-specific type as Person:

$ ox query . --eval 'pub derive q(x, t) :- meta(x) == t;'
ad-hoc query: 8 row(s)
  (std::core::type, Metatype)
  (Voter, std::core::type)
  (Adult, std::core::type)
  (Person, std::core::type)
  (Registered, std::core::rel)
  (Metatype, Metatype)
  (#i7582462787275748164, Person)
  (#i8648907253816210642, Adult)

The antichain reformulation, measured. q_nonminimal and q_derived_meta are D4’s rules written in ordinary Argon and evaluated by the ordinary reasoner. On the individual tier they reproduce $meta exactly: (alice, Person) and (bob, Adult), the same two rows the built-in $meta gives, with bob’s Person row correctly suppressed as non-minimal. On the catalog tier they do not, in both directions — q_derived_meta emits four TypeRef rows that $meta withholds, and misses (Registered, std::core::rel) which $meta has. That is exactly what that block’s own comment says it should do, and it is why D4 is scoped to the individual tier. This discrepancy was found by running the rules, not by reading them.

$specializes is reflexive, measured. D2’s bridge rules turn on this, so it is read off the relation rather than off the comment:

$ ox query . --eval 'pub derive q(a, b) :- specializes(a, b);'
ad-hoc query: 14 row(s)
  (Voter, Voter)
  (Voter, Person)
  (Adult, Adult)
  (Adult, Person)
  (Person, Person)
  (Registered, Registered)
  (TraitRef, TraitRef)
  (TraitRef, Entity)
  (Entity, Entity)
  (Metatype, Entity)
  (Metatype, Metatype)
  (Metatype, TypeRef)
  (TypeRef, Entity)
  (TypeRef, TypeRef)

(Voter, Voter) is present, so the <:-closure bridge rule subsumes the direct one.

The refusals, confirmed. Each is fail-closed today and stays that way:

$ ox check .          # with `pub derive V(p: Person) :- p : rfd93q::Voter;`
OE0223: unresolved type `rfd93q::Voter` in type-test atom (a `c : T` atom
is membership in `T`'s extent; `T` must be a declared concept)
$ ox build .
Error: 1 error(s); build aborted

$ ox check .          # with `pub derive V(p: Person) :- Person(p), p :: Voter;`
OE0223: unresolved predicate `p :: Voter` in rule body

$ ox check .          # with `pub derive V(p: Person) :- iof(p, self::Voter);`
OE0227: in rule `membership::V`, the path `self::Voter` resolves to nothing —
searched enum constants, metaxis values, declared types, declared relations,
and declared individuals (this module and the workspace); a multi-segment path
is never a variable

$ ox query . --eval 'pub derive q(p) :- Person(p), not (meta(p) == Voter);'
Error: ad-hoc query could not be prepared: unsupported term shape in atom: MetaCall

$ ox query . --eval 'pub derive q(p) :- Person(p), p is Voter;'
Error: OE1386: the relation-valued variable `p` in rule `q` is applied without
pinning which relations it can stand for

$ ox query . --extent Voter
Error: query_extent: membership in `Voter` is rule-derived (fixpoint-dependent)
and is undetermined for the store-local classifier — it is computed by the
reasoner (`select … from Voter(x)` / a `derive` body), never evaluated
mid-classification (#1314); read it through the reasoner or classify the
individual directly

A trap, recorded so no later reader repeats it. The ad-hoc surface (ox query --eval) resolves a bare concept constant unqualified, while the store holds the module-qualified name. So an ad-hoc read naming a concept constant can disagree with a declared rule containing the identical atom:

$ ox query . --eval 'pub derive q(p) :- iof(p, Adult);'
ad-hoc query: 0 row(s)

Adult is an ordinary asserted concept and the declared rule over the same atom returns bob. The zero here is the ad-hoc path failing to resolve the constant, not a membership answer. Every load-bearing number in this record therefore comes from a declared query head. Ad-hoc reads are used only where the type position is a variable (iof(p, t), meta(x) == t), which binds rather than resolves a constant and is therefore safe; those are read as a dump of the relation, never as a membership verdict.

The whole surface, measured. The package above is one shape. The conformance sweep in pull request #1903 evaluates all fifteen spellings against all five shapes by execution. Its table, with this record’s scope marked — bold is a defect, and the fixed/not-fixed split is called out below it:

Reading it: member means the spelling returns the same individuals the concept atom C(x) returns; non-member means it returns the complement, which is right for a negated spelling.

What the sweep does and does not establish. Its oracle is the concept atom. So it measures agreement between spellings, and it does that by execution rather than by inspection — which is what makes the disagreements incontrovertible. It does not establish that the concept atom is itself correct; that rests on the ratified meaning cited above, not on the sweep. Read the table as a disagreement census, not as a correctness proof.

• Two whole columns split, and they are the same column twice. The shape clause, and the shape clause reached through an import. Seven defect cells each. D2 closes all fourteen.
• One whole row is empty, in every column. x : self::C — including the asserted column, where nothing is derived and there is no hole for D2 to fill. Five cells, issue #1904, not fixed here.
• empty by spec is not a defect. meta(x) == C under upward closure asks for minimal classifiers, and D4 preserves that; see Non-goals.
• The braced column is the control. It agrees everywhere the shape-clause column splits, which is what proves the reasoner boundary is the cause rather than the reflection intrinsic.

That control is executed here rather than taken from the table. Membership by a braced refinement is decided by a field value, and a field is only writable through a mutation, so the two individuals are enrolled by a scenario:

pub type Person { mut registered: Bool }
pub type BracedVoter <: Person iff { self.registered == true };

pub mutate enroll(p: Person, r: Bool) {
    insert iof(p, Person);
    update p: Person set { registered = r }
}

pub derive BracedAtom(p: Person) :- BracedVoter(p);
pub derive BracedIof(p: Person) :- iof(p, BracedVoter);
pub derive BracedNegatedIof(p: Person) :- Person(p), not iof(p, BracedVoter);
pub derive BracedMetaEq(p: Person) :- Person(p), meta(p) == BracedVoter;

With alice enrolled registered and bob unregistered:

$ ox run-scenario .
scenario: applied 2 mutation(s) from ./demo.toml
query q_braced_atom: 1 row(s)
  (#i7582462787275748164)
query q_braced_iof: 1 row(s)
  (#i7582462787275748164)
query q_braced_meta_eq: 1 row(s)
  (#i7582462787275748164)
query q_braced_negated_iof: 1 row(s)
  (#i8648907253816210642)

All four agree: the concept atom, the reflection read, and the metatype read all return alice, and the negated read returns exactly bob. Compare the shape-clause package above, where the same four spellings give the member, nobody, nobody, and everybody. The only difference between the two programs is how membership is decided.

A downstream consumer of extent, executed. The direct reflection read is not the only casualty: a rule that joins against an extent derives nothing, one step removed from the read, which is how the hole escapes notice. Over the same vocabulary, with two ballots:

pub type Slip;
pub rel Ballot(mut b: Slip, mut owner: Person);

pub derive CountedBallot(b: Slip) :- Ballot(b, p), p in extent(Voter);
pub derive ControlCountedBallot(b: Slip) :- Ballot(b, p), p in extent(Adult);
pub derive ExtentMember(p: Person) :- p in extent(Voter);
pub derive ControlExtentMember(p: Person) :- p in extent(Adult);
pub derive AtomCountedBallot(b: Slip) :- Ballot(b, p), Voter(p);

pub fact Slip(slip1);
pub fact Slip(slip2);
pub fact Ballot(slip1, alice);
pub fact Ballot(slip2, bob);

$ ox check .
ok
$ ox build .
workspace: elaborated 2 module(s) into one artifact
wrote ./target/root.oxbin (31 events)
$ ox query .
query membership::q_atom_counted: 1 row(s)
  (#i768220427304451167)
query membership::q_control_counted: 1 row(s)
  (#i2503042279537445241)
query membership::q_control_extent: 1 row(s)
  (#i8648907253816210642)
query membership::q_counted: 0 row(s)
query membership::q_extent: 0 row(s)

#i7682… is slip1 (alice’s), #i2503… is slip2 (bob’s). The extent read over the rule-decided concept is empty, so the ballot rule counts nothing; the asserted control counts slip2; and the same ballot rule with the concept atom in place of the extent read finds slip1. The intended answer for q_counted is therefore exactly the row q_atom_counted computes.

The type-parametric rule, executed — the case with no literal-spelling workaround. When the type position is a bound variable rather than a written name, no concept atom can be substituted, because the concept is not known statically. This is the shape of every vocabulary-generic rule: one rule intended to hold for each concept in a family, including concepts declared later, in packages that do not exist yet.

pub derive RoleGeneric(p: Person, role: TypeRef) :-
    specializes(role, Person), iof(p, role);

pub derive RoleFamilyGeneric(p: Person, role: TypeRef, family: TypeRef) :-
    RoleGeneric(p, role), specializes(role, family);

// Only writable because this vocabulary happens to be known statically.
pub derive RoleExpanded(p: Person, role: TypeRef) :-
    specializes(role, Person), role == Voter, Voter(p);
pub derive RoleExpanded(p: Person, role: TypeRef) :-
    specializes(role, Person), role == Adult, Adult(p);
pub derive RoleExpanded(p: Person, role: TypeRef) :-
    specializes(role, Person), role == Person, Person(p);

$ ox check .
ok
$ ox build .
workspace: elaborated 2 module(s) into one artifact
wrote ./target/root.oxbin (23 events)
$ ox query .
query membership::q_role_expanded: 4 row(s)
  (#i7582462787275748164, membership::Person)
  (#i7582462787275748164, membership::Voter)
  (#i8648907253816210642, membership::Person)
  (#i8648907253816210642, membership::Adult)
query membership::q_role_family_generic: 4 row(s)
  (#i7582462787275748164, membership::Person, membership::Person)
  (#i8648907253816210642, membership::Person, membership::Person)
  (#i8648907253816210642, membership::Adult, membership::Person)
  (#i8648907253816210642, membership::Adult, membership::Adult)
query membership::q_role_generic: 3 row(s)
  (#i7582462787275748164, membership::Person)
  (#i8648907253816210642, membership::Person)
  (#i8648907253816210642, membership::Adult)

The generic rule is missing (alice, Voter) — for no reason visible in it, since it names no concept — and the rule one join downstream is missing the two Voter-headed triples that follow. It is correct for the asserted concept and silently incomplete for the rule-decided one, so it under-derives once per rule-decided concept in the vocabulary. The hand expansion is not a workaround: it requires the author to enumerate the vocabulary and cannot be written by library code that receives a type as a value. This is the strongest motivation for D1 — under D1 the generic rule returns q_role_expanded’s four pairs.

The metatype’s narrowness, executed as a control. meta yields <:-minimal classifiers, so a member asserted at a strict subtype is deliberately absent under the supertype; this is the empty by spec cell and it is preserved:

pub type Person;
pub type Adult <: Person;

pub derive AtomPerson(p: Person) :- Person(p);
pub derive IofPerson(p: Person) :- iof(p, Person);
pub derive MetaEqPerson(p: Person) :- Person(p), meta(p) == Person;
pub derive MetaEqAdult(p: Person) :- Person(p), meta(p) == Adult;

pub fact Adult(bob);

$ ox check .
ok
$ ox build .
workspace: elaborated 2 module(s) into one artifact
wrote ./target/root.oxbin (16 events)
$ ox query .
query membership::q_atom_person: 1 row(s)
  (#i8648907253816210642)
query membership::q_iof_person: 1 row(s)
  (#i8648907253816210642)
query membership::q_meta_eq_adult: 1 row(s)
  (#i8648907253816210642)
query membership::q_meta_eq_person: 0 row(s)

Membership in Person holds by both the concept atom and the reflection read; the classifier is Adult; meta(bob) == Person is correctly empty.

The self:: row, executed. It needs no derived membership at all:

pub type Person;
pub fact Person(alice);
pub fact Person(bob);

pub derive ViaAtom(p: Person) :- Person(p);
pub derive ViaBare(p: Person) :- p : Person;
pub derive ViaSelf(p: Person) :- p : self::Person;

$ ox check .
ok
$ ox build .
wrote ./target/root.oxbin (12 events)
$ ox query .
query q_atom: 2 row(s)
  (#i7582462787275748164)
  (#i8648907253816210642)
query q_bare: 2 row(s)
  (#i7582462787275748164)
  (#i8648907253816210642)
query q_self: 0 row(s)

A checked-clean program serving an empty answer to a well-formed question about a plainly asserted concept. That is issue #1904, and D2 does not touch it.

The truth-qualifier precondition, executed. D5 makes this a blocker for slice 4:

pub derive IsRegistered(p) :- holdsRegistration(p, r), Registration(r);
pub type Voter <: Person iff IsRegistered(self);

pub derive DefinitelyVoter(p) :- Voter(p);
pub derive UnknownVoter(p) :- Person(p), Voter(p) is unknown;

$ ox query .
query q_definite: 1 row(s)
  (#i7582462787275748164)
query q_unknown: 1 row(s)
  (#i7582462787275748164)

alice holds a registration, so her membership is definitely true; she is returned by both. bob, definitely not a member, appears in neither. The qualifier is not being evaluated. Issue #1902.

Group axioms are already correct and are not what this record is about. The reported defect that prompted it — partition mis-evaluating a shape-defined cover — was fixed by pull request #1873. With Voter and Abstainer both shape-defined and partition Person { Voter, Abstainer }:

$ ox check .          # alice registered — covered
ok
$ ox check .          # `pub fact Registered(alice);` removed — uncovered
Argon::OE0241: `Person` is declared completely covered, but an instance is
in none of its cover members [alice]

Both directions enforced. This record concerns the reflection spelling a modeller writes by hand.

Decision

D1 — iof denotes membership, whole

iof(x, C) denotes an individual’s membership in C: asserted classification, <: closure, predicate-refinement-derived, and rule-derived alike. extent and meta follow it. C(x), x : C, and iof(x, C) are three exact spellings of one question, and answer identically for every concept and every argument shape, including a bound type variable.

Exact is the operative word and is stronger than the first revision’s claim. It means substitution holds: iof(x, Voter) and iof(x, t), t == Voter denote the same set. Any remedy that does not deliver that is not a remedy for this defect, only for its most visible instance.

Scoped to bare and module-qualified concept paths. The sweep finds a separate defect on self::: p : self::C checks, builds, and silently derives nothing, in every shape including a plainly asserted concept where no derived membership is involved. Nothing in this record touches path resolution, so “three exact spellings of one question” holds for C and for pkg::C and not for self::C until issue #1904 is fixed.

D1 is the decision this record asks for. The originating records already fix this meaning (Context, above). Under D1 the seed-time $iof build is an implementation of it, and an incomplete one. The remedy is to complete the implementation, not to narrow the intrinsic.

D2 — The reflection relation carries derived membership

The individual tier of $iof stops being a seed-time snapshot of the per-type extents and starts carrying every concept’s decided membership, rule-decided included. That is the semantic content of D2 and it is what D1 requires.

The mechanism below is one of two, and is not settled. D2 is written against generated bridge rules because that form is concrete enough to argue about — the stratification obligation in D5 and the antichain in D4 are stated over it. The alternative mechanism — rewriting constant type positions at elaboration and materializing the relation once at a stratum boundary above every read — yields the same answers for every spelling and every argument shape, so nothing in Consequences or Measured scope turns on the choice. Reviewers are asked to settle D1; D2’s mechanism is sequenced with slice 4.

In the bridge-rule form: for each declared concept C the elaborator emits bridge rules into the program:

$iof(x, C)     :- C(x).
$iof(x, super) :- C(x), $specializes(C, super).

The second rule folds in <: closure, reading the same catalog-closed $specializes relation the surface specializes intrinsic reads.

Two corrections to the obvious form of these rules, both read off the tree:

• $specializes is reflexive (standpoint.rs:286-290: “for each declared concept t, ancestor_concept_ids_including_self(t) yields t itself plus every supertype”), and the executed rows in Demonstration show (Voter, Voter). The second rule therefore already subsumes the first. The first is kept only so a concept absent from the <: graph still bridges; whether that case exists is an implementation detail for the slice, not a semantic question.
• $specializes’s columns carry the concept name directly (Value::Name), not a wrapped type-reference constructor. The rule joins on the plain name.

The catalog tier stays extensional, unchanged. Its rows are declaration-derived and finite, it is explicitly catalog-closed, and negation over it is already justified as stratification-safe on that ground (the metatype-tier block of materialize_reflection_relations). Deriving it would buy nothing and would put declaration-level rows into a fixpoint that has no need of them.

materialize_reflection_relations’ individual-tier scan (standpoint.rs:74-110) is deleted, along with the iof_by_entity accumulation it feeds.

D3 — extent(t) is a projection over $iof

No change of meaning and no separate work: extent already desugars to the reserved-head iof atom (lower_source), so once $iof is derived, extent(t) is the entity column of $iof restricted to t and is correct for every concept, constant or variable argument alike.

The store-local classifier’s fail-closed refusal (RuntimeError::MembershipFixpointDependent) exists because that surface runs mid-classification and cannot reach the fixpoint. Once the read is served from the derived relation rather than from the classifier, the refusal has nothing left to protect and is retired. Retiring it is part of the slice that derives $iof, not a separate decision — but it is a user-visible widening and is called out as such in Consequences.

D4 — meta is an antichain over $iof, on the individual tier

$meta’s individual tier stops being a second snapshot and becomes:

$nonminimal(x, C) :- $iof(x, C), $iof(x, D), $specializes(D, C), D != C.
$meta(x, C)       :- $iof(x, C), not $nonminimal(x, C).

This is the same <:-minimality the current code computes (the $meta reduction in materialize_reflection_relations), expressed over the derived relation instead of over the seed scan’s accumulated type set. Demonstration evaluates exactly these two rules in ordinary Argon and confirms they reproduce the current individual tier row for row.

Scoped to the individual tier, deliberately. The catalog tier’s $meta is the exact declared introducer, not a minimal element — a type may be declared an instance of several higher-order types, and two catalog row sets feed $iof but not $meta on purpose (the metatype-tier block of materialize_reflection_relations; Context, above). The demonstration measures what an unscoped antichain would get wrong: four spurious rows and one missing one, in a program with three concepts. The catalog tier keeps its existing construction.

D5 — Stratification, and the third truth value

The bridge is positive. $iof(x, C) :- C(x) has no negation, so concept-to-relation-to-concept recursion is monotone: a concept whose rule reads iof of another concept forms an ordinary positive cycle, and the least fixpoint is the intended one. No new stratification obligation arises from the bridge itself.

Negation inside a component is handled by the well-founded semantics, not by refusal. The stratifier already distinguishes the three edge kinds and, on finding negation inside a strongly-connected component, marks that component for well-founded evaluation instead of refusing it (stratify in compiler/crates/oxc-reasoning/src/compile/stratify.rs):

#![allow(unused)]
fn main() {
// Recursion through negation → well-founded semantics.
EdgeKind::Naf => scc_is_wfs[src_scc] = true,
}

So a rule reading not iof(x, C) puts $iof, $nonminimal, $meta, and every concept that bridges into them into one dependency component, evaluated as a single well-founded unit.

This is not new machinery, and the claim that shape membership already works this way is not an analogy. A shape-defined concept’s membership rule is emitted as an ordinary rule declaration (compiler/crates/oxc-instantiate/src/lower/concept.rs, synthesize_shape_membership_rule) and is stratified with everything else; the pipeline has a named pass for shape classifiers caught in negation cycles (shape_classifiers_in_negation_cycles, compiler/crates/oxc-workspace/src/pipeline.rs), and its documentation (the OW0679 block of runtime_rule_failures) records the disposition this design relies on: a shape-defined classifier in a recursion-through-negation cycle “is ALLOWED, not refused”, because “WFS gives the cycle a model (membership surfaces Can)”. It warns (OW0679) rather than refusing. D2 puts the reflection relation into the same regime that already governs the concept it bridges from.

D4’s $meta pair is a weaker case still: $nonminimal does not read $meta, so the two sit in different strata and the negation is ordinary stratified negation, not recursion through it. The demonstration evaluates that pair today, unmodified, with no stratification complaint.

Hard invariant: undefined membership remains the third truth value and must not collapse to false. Where the well-founded semantics leaves iof(x, C) undefined, iof(x, C) is undefined, not iof(x, C) is undefined, and neither derives. A read must not silently substitute false for undefined — that would replace today’s silent over-derivation with a different one, which is the failure class this record exists to close.

The substrate has the representation for this. The well-founded executor materializes the undefined extent as a companion relation rather than losing it (undefined_name in compiler/crates/oxc-reasoning/src/executor/wfs.rs): R holds the definitely-true fragment and $undefined::R holds the rest, explicitly “so a downstream reader … can tell undefined apart from definitely-false”. On the classification side the same distinction is already honoured for exactly this class of concept (concept_membership_local in compiler/crates/oxc-runtime/src/classify.rs), where a rule-headed concept’s undetermined membership reads Truth4::Can and never a fabricated Not.

A bound on that invariant, stated rather than glossed. Three-valued undefined does not yet propagate into derive heads: cross-stratum negation over a well-founded relation is currently refused (OE1365, OE1367; the ReasoningError variants in compiler/crates/oxc-reasoning/src/error.rs, gated at the cross-stratum block of stratify), and the source calls this “the honest interim until three-valued undefined propagates into derive heads”. Aggregation over an undefined extent is likewise refused (OE1332). So today the invariant is upheld by refusal, not by propagation. D2 must not weaken that: where the propagation does not exist, the refusal stays. Making a derived $iof widen the set of programs that hit those refusals is an accepted and expected consequence; making it silently answer them is not.

The surface already has a spelling for the undefined case — is unknown, the well-founded-undefined read (atom_suffix in compiler/crates/oxc-parser/src/rule_atom.rs) — but the reflection atoms do not accept that suffix. Open question 2.

That spelling was broken and is now repaired by RFD 0094. Issue #1902 established that Voter(p) is unknown returned the definitely-true extent because lowering discarded the qualifier. RFD 0094 lowers it to the completed $undefined::Voter companion, orders the consumer after Voter, and refuses recursive reads.

This is not an unrelated ticket. Making membership fixpoint-derived means more concepts can legitimately be undetermined — every shape-defined concept whose defining rule is itself undetermined now has an undefined reflection extent where before it simply had none. The surface for asking “is this membership undetermined?” therefore matters materially more after this change than before.

So issue #1902 is a stated precondition of slice 4, the first behaviour-changing slice — not a follow-up. It was fixed before the read surface widens. The same pressure applies to the refusals themselves: this design pushes more programs into OE1365 / OE1367 territory, so the refusal path becomes a surface users actually meet rather than a corner. It has to be a good refusal — a message that names the undetermined concept and points at the qualifier — and not merely a correct one.

Recursion through aggregation stays refused, by the existing gate OE1317 (the aggregate-cycle arm of stratify): an aggregate edge inside a component is collected and refused, because “recursion through aggregation has no well-defined fixpoint”. The bridge rules introduce no aggregation and do not widen this.

No restriction on variable type positions is required for soundness. A free type position — iof(x, t) with t unbound — is sound under this design; it simply ranges over the whole relation. Any restriction imposed on it is for tractability, because a free type position can merge otherwise-independent dependency components into one large well-founded unit. That is a cost question, not a correctness question, and Open question 3 records what bounds it. This distinction is worth stating plainly because the first revision’s design-gated slice implied the opposite.

D6 — The mechanization requires no change

spec/lean/Argon/MetaCalculus/Reflect.lean:183-184 declares membership as an opaque field on the reflection catalog:

/-- `iof x t = true` iff instance `x` is an instance of type `t`. -/
iof : Ref → Ref → Bool

It is a bare Ref → Ref → Bool with no defining equation and no provenance condition — contrast the sibling specializes, which carries preorder obligations. Whether rows arrive by a seed scan or by a bridge rule is exactly the choice of inhabitant supplied for that field.

extentOf is defined from it (Reflect.lean:209-210):

def extentOf (c : ReflectCatalog) (u : List Ref) (t : Ref) : List Ref :=
  u.filter (fun x => c.iof x t)

and every downstream result — iofRel (:204), mem_extentOf (:214), extentOf_subset (:221), catalogTierIof (:242) and its catalogTierIof_eq_iofRel := rfl (:248-249) — is proved through the field and is provenance-agnostic. Realization.lean’s realize_iff (:82) operates on a different abstraction with no seeding assumption.

So this design requires no Lean change. This inverts which option looks conservative, and the inversion is the point. The rejected alternative (Alternatives, below) would have needed a second catalog field — an asserted-plane membership distinct from membership — and would have had to re-point extentOf and every theorem above it at whichever field the surface now meant. A record that presents itself as the smaller change would have been the one to disturb the mechanization.

“No Lean change” is not “no Lean obligation”. The field’s opacity is what makes existing theorems survive, and it is also why D1’s actual semantic content — that membership includes rule-derived membership — is not stated in the mechanization: nothing in Reflect.lean says which inhabitant is the right one, and the strongest backing for the inclusive reading is RFD 0070’s L5, which that record reproduces as PROVED-scratch rather than as a merged theorem. Mechanizing that bridge — relating the generated membership rules’ output to the iof field’s population, so the inclusive reading is a theorem and not only a surface promise — is deferred, not a non-goal. It is deferred without a named owner and without a slice in this record’s plan; no decision here forecloses it, and no claim here rests on it having happened.

One boundary to respect: AxisRelation.lean’s catalog-closure invariants (:182, :224-227) state that the reflective extents read the catalog only. D2 keeps the catalog tier declaration-derived, so those theorems stand. A design that let rule-derived rows feed the reflective-sort extents would not, and is out of scope.

D7 — The book states the meaning once, and the migration is mechanical

meta-calculus.md:143 is corrected to state the meaning — full membership — with the two-source enumeration retained as an implementation note about what the catalog tier builds. :115 and :123 become true instead of aspirational. The Appendix C entries already stating fixpoint-evaluated membership (OE0258, OE0240, OE0241) are cited, not rewritten. The qualified-path type test gets a better OE0223 message, saying the spelling is unsupported in a membership position rather than that the type is unresolved.

Migration is compiler-locatable. Both halves of the trigger are already computed by the compiler, so no new analysis is needed to find every affected site.

Which concepts carry a shape clause. The elaborator decides this from the concrete syntax and records it as the refinement tag (lower_concept_decl in compiler/crates/oxc-instantiate/src/lower/concept.rs, matching on find_shape_clause), and the runtime exposes the answer as a pair — Module::shape_defined_concept_ids and Module::is_shape_defined (compiler/crates/oxc-runtime/src/schema_module.rs:1820 and :1835).

Which body atoms are reflection heads. iof, meta, and specializes are keyword-lexed, not identifiers (compiler/crates/oxc-syntax/src/generated.rs, the from_keyword table), and the elaborator already tests for them by name at the atom-resolution pass (validate_reflection_carrier in compiler/crates/oxc-instantiate/src/lower/rule_ref.rs):

#![allow(unused)]
fn main() {
if matches!(head, "iof" | "specializes" | "meta")
}

The intersection is therefore mechanical: every rule whose body reads a reflection head with a shape-defined concept in the type position can be enumerated at elaboration. The same site is where the first revision’s prototype keyed its rewrite off the bare head string; used for a warning rather than a silent rewrite, that keying is fit for purpose, because a missed carrier under-warns rather than mis-derives.

A warning ships one release ahead of the behaviour change, naming each such site and what its answer will become. For nearly everyone the edit count is zero: a read that silently derived nothing starts deriving correctly, which needs no source change. Only rules that depend on the empty answer change meaning — in practice a negated read used as a universal, not iof(x, C) standing in for “everybody”. Those are the sites the warning exists to find. Open question 4 records that the warning’s exact trigger set is not yet fixed.

Rationale

The meaning is already ratified, and none of the ratifying sites mentions a materialization. The citations — four design records and a Lean proof — are in The meaning is already ratified elsewhere. What follows from them is the argument here: narrowing the intrinsic to match the materializer would retract a proved surface promise to accommodate a seed-order constraint.

The implementation already agrees and already works to make it true. The refinement-honesty pass in seed_base_catalog_in_frame_filtered exists for no other reason than to make derived membership visible through these surfaces, at real cost. The $iof materializer’s own doc comment claims derived members are included (standpoint.rs:16-28). The minimal-classifier path documents the union explicitly. The inclusive reading is the implementation’s stated intent; shape concepts are the one class it structurally cannot reach.

Fixing the relation is smaller than fixing the readers. There is one producer of $iof and an open-ended set of consumers — rule bodies, ad-hoc bodies, the extent desugaring, $meta, the serving reads. Every remedy that teaches consumers to look elsewhere has to enumerate them and stay enumerated as new ones appear; the first revision’s prototype found this the hard way, keying its rewrite on the head string "iof" at each site so that a new reflection carrier would silently miss it. Deriving the relation fixes every consumer at once, including consumers not yet written, because they all read the same relation and the relation is now right.

The precedent ran twice, both times by routing the read to the plane that knows the answer. Issue #1859 → pull request #1860 fixed field projections over a shape-defined concept by materializing rows extent-blind and gating them on the fixpoint membership atom. Issue #1871 → pull request #1873 fixed group-axiom checks by swapping iof for the concept atom; the rule is now recorded in the source (compiler/crates/oxc-instantiate/src/lower/groupaxiom.rs:48): “Membership is tested with CONCEPT atoms, never iof(...): the $iof reflection relation carries asserted classification only, while a shape-defined member’s extent is derived in the fixpoint — the concept atom covers both planes”. Neither was remedied by refusing the read. D2 generalizes the same move to its source: after it, that comment’s premise is false and the comment can be deleted, because $iof no longer carries asserted classification only.

Nothing pins the current behaviour. No test pins iof / extent / $iof against a shape-defined concept on the read side, so no test expectation has to be revised to accommodate the correct answer. The audit: compiler/crates/oxc-runtime/tests/shape_write_gate.rs is entirely write-and-load refusals (OE0211) and contains no extent read at all; compiler/crates/oxc-driver/tests/group_axiom.rs reads iof only against asserted concepts, and its shape-defined case (shape_defined_parent_covering_guard_fires, :681) exists to record the change away from the iof spelling; compiler/crates/oxc-runtime/tests/materialization_impact_proof.rs:437 (cone_reaches_through_shape_defined_membership) exercises shape membership through a concept atom in a check body and queries extents only for plain concepts; and compiler/crates/oxc-driver/tests/shape_defined_field_projection.rs likewise reads through concept atoms. The two tests that do spell iof(x, …) and extent(…) target a non-shape concept.

Alternatives

Rewrite only the statically-known iof(x, C), and refuse meta(x) == C — REJECTED

This was this record’s own first revision, and it is recorded here as rejected, with its reasoning, rather than quietly replaced.

The proposal: at elaboration, when the type position of a membership read is a constant naming a shape-defined concept, rewrite iof(x, C) to the concept atom C(x), positive and under not. Leave a variable type position alone. Refuse meta(x) == C, because the surface does not survive relationalization as one atom — it splits into a join meta(x, $g) plus a filter $g == C, and rewriting the pair needs a second pass, a duplicated wrapper-recursion walk, and a total occurrence test that the prototype could only discharge by matching a substring of a derived debug rendering.

Its attractions were real: one small site, no source break, no epoch bump, and it matched what the two merged fixes for the same root cause did.

It is rejected because rewriting only the statically-known form breaks substitution. After the rewrite, iof(x, Voter) denotes full membership and iof(x, t), t == Voter denotes asserted-plane membership. Those are the same question, and they would return different sets. iof is not an incidental predicate — the manual sells it as first-class and type-value-polymorphic, and the value-polymorphic use is the reason RFD 0023 D4 introduced the reflection relations at all (0023-reflective-type.md:89-91). A first-class predicate over which equals cannot be substituted is not a predicate a modeller can reason about, and no amount of documentation repairs it. The proposal would have converted a uniform wrong answer into a non-uniform one, which is harder to find and harder to explain.

The refusal of meta(x) == C falls with it, for a different reason: it was adopted because the pair rewrite was fragile, and the pair rewrite is fragile because it is a rewrite. Once $meta is derived from $iof there is no pair to rewrite and nothing to refuse. The spelling is fixed.

Two findings from that revision’s prototype survive as evidence and are kept: the size and fragility of the relationalized-pair rewrite (which is why no design should try it), and the head-string keying of the rewrite sites (which is why per-site remedies do not stay correct).

A second intrinsic exposing the asserted-only plane — CONSIDERED AND DECLINED

Add asserted_iof(x, C) (or similar) so a modeller who genuinely wants the asserted plane can ask for it, with iof freed to mean membership. This looks like a tidy separation of concerns and it was considered on those terms.

It is not adopted. The reasons, in order of weight:

• It is not load-bearing for the fix. D2 delivers correct iof, extent, and meta without it. It is an addition, and additions to a language surface need their own justification.
• No concrete need has been produced. Not one use case has been written down that requires distinguishing asserted from derived membership at the read surface.
• The write path already reaches asserted membership by construction — it writes assertions — and OE0211 refuses precisely where the two planes would diverge, so the place where the distinction has operational meaning is already governed. (OE0211 is narrower than a general plane-divergence gate: it refuses all insert/delete iof on any defined concept or defined-ancestor, while the construct door refuses only shape-defined targets, and it is runtime-only. The point stands for the read surface.)
• It would cost a reserved name, which iof does not. iof, meta, and specializes are lexed as keywords (compiler/crates/oxc-syntax/src/generated.rs, the from_keyword table), so they can never collide with a user identifier. extent is already the exception — it lexes as an identifier and has to be carried on two allow-lists (compiler/crates/oxc-workspace/src/hygiene.rs, fn is_ambient; compiler/crates/oxc-check/src/references.rs, REFLECTION_INTRINSICS). An asserted_iof would be identifier-lexed too, expanding both gates and taking a plausible user identifier out of circulation, for a facility nobody has asked for.

If a provenance need does appear, it can be served without a new keyword — through the reflection relation surface, an attribute, or a standard-library predicate — and it should be decided then, against the real use case, rather than speculatively now.

Fail-closed refusal everywhere — RFD 0092

The alternative record’s position, at full strength: the two planes are a real architectural fact, and the honest response to a read that cannot be answered on the plane it is issued against is to refuse it, not to silently reroute it. RFD 0092 introduces one authority predicate naming which plane owns a concept’s membership, and a diagnostic refusing an asserted-plane read of a derived-membership concept.

Its case is strong on three counts. It is uniform: a refusal needs no static concept, so it covers the variable and runtime forms that a rewrite cannot reach — which was decisive against the rejected alternative above, and is not decisive against D2, because D2 is also uniform. It is loud: a refused program is strictly better than one that derived the wrong answer, and Argon’s diagnostic culture prefers refusal to silent adaptation. And it is cheap: no stratification argument, no incremental-maintenance work, no epoch bump, no change to what the reasoner computes.

The reasons this record prefers D2:

• It keeps iof meaning one thing. Under a refusal, iof means asserted-plane membership and x : T means full membership, while the manual documents them as synonyms — a permanent two-meaning split every reader must learn, and a :115-versus-:143 contradiction resolved in favour of the narrower sentence.
• It needs no source break. A refusal turns programs that check today into programs that do not, and the count is not small: every iof read over a shape-defined concept, correct or not.
• It retracts a proved surface promise. RFD 0070’s L5 is recorded as proved; a refusal makes the surface narrower than the theorem, and the mechanization would have to be re-pointed to say so (D6).
• It gives up on the value-polymorphic use RFD 0023 D4 exists to enable, rather than delivering it.

The counter-case is honest and is why this stays a live alternative: D2 is a silent change to what an existing program derives, in a direction no user can have intended but may have built on, whereas a refusal makes the modeller choose. D7’s warning-one-release-ahead is the mitigation, and a mitigation is not the same as not having the problem.

Do nothing

Rejected. The failure is checked-clean and silent — the source’s own words (catalog_seed.rs:852) — and in the negated direction it does not merely under-derive, it over-derives. A wrong answer with no diagnostic is the failure mode Argon’s loud-gate contract exists to exclude.

Move all membership to the rule plane and delete the seed plane’s classification

One plane, so the question cannot arise. Rejected as out of scope: the seed plane’s assertion closure and refinement honesty exist for reasons outside this record — mid-classification write gates read them — and moving them would restructure the write path. D2 does not require it.

Measured scope: what this record closes, and what it does not

The consequences below are counted, not estimated. A conformance sweep evaluates every membership spelling against every program shape by execution and records the answer each gives — five shapes (membership asserted; braced predicate refinement iff { … }; shape clause iff Derive(self); upward <: closure; the shape-clause concept imported across a module boundary) by fifteen spellings, seventy-five cells. It is proposed in pull request #1903.

Nineteen cells are defects. They fall into exactly three groups:

So this record closes fourteen of nineteen. The remaining five are an independent defect that survives it: the sweep finds p : self::C empty even in the asserted shape, where no derived membership exists to be missed, which is what establishes it as unrelated to the hole D2 fills.

Fourteen defect cells is not fourteen behaviour changes: the defect count sizes the diagnosis, and a much smaller flip count sizes the migration. The breakdown, and the one honest limit on it, are in Consequences.

The sweep also isolates the cause. The braced-refinement shape agrees on every spelling — a braced refinement is composed on the seed plane before the reasoner runs, so its members reach the reflection relation. Only the shape clause splits. That contrast is the control, and it is why the remedy is aimed at the reasoner boundary and not at the reflection intrinsic in general.

Non-goals — the behaviours that must be protected from the fix

These are the most likely way to over-implement this record. An implementer reading “every spelling agrees” could reasonably try to make them agree too. They must not. Neither is a defect, and neither is closed, softened, or widened by anything here.

1. meta(x) == C under upward closure is empty, and that is correct. The metatype yields an individual’s <:-minimal classifiers. When a member is asserted at a strict subtype of C, its minimal classifier is that subtype, so C is absent — the individual is a member of C and is not most-specifically classified by it. The sweep records this cell as differing by specification, not as a defect. meta asks a narrower question than iof by design, and D4 preserves that: the antichain is over $iof, so it inherits $iof’s completeness without inheriting its breadth. Making this cell agree would delete the metatype’s reason to exist.
2. The two refusals stay refusals. x :: C is refused, and iof with a self::-qualified path is refused (OE0227). Neither becomes an answer under this design, in any shape. x :: C is the metatype-equality sugar and is refused before evaluation; widening it is a separate decision with its own surface consequences. The self:: refusal is the fail-closed half of issue #1904 — the reflection intrinsic rejects a path the type test silently accepts, and of the two behaviours the refusal is the correct one. Fixing that issue by making the type test refuse would be consistent with this record; making iof silently accept would not.

Recorded explicitly because silence invites scope creep in both directions.

Consequences

• Every membership spelling agrees, for a bare or module-qualified concept path. C(x), x : C, iof(x, C), extent(C), and meta(x) == C return the same answer for the same concept, for a constant or a variable type position — with the two non-goals above, and with self:: still excluded pending issue #1904.

• Programs that silently derived nothing start deriving correctly. No source change needed; this is the intended effect.

• The behaviour change is two cells, not fourteen. This distinction is the whole migration story and the defect count badly overstates it. Of the fourteen cells this record closes, twelve go from empty to correct: a read that derived nothing starts deriving the right rows. No rule can meaningfully depend on those — an empty relation contributes nothing to a positive body, so there is no behaviour to preserve. Two cells genuinely flip: not iof(x, C) in the shape-clause shape and in the imported shape-clause shape, which today match every individual and will match only genuine non-members. That is the dangerous cell and the only one: a rule that reads as an exclusion but has been silently behaving as a pass-through changes meaning. D7’s warning exists for exactly these two.

  One honest limit on that count: the sweep measures negation over three spellings only — the concept atom, the type test, and iof. A negated extent or metatype read (not (x in extent(C))) is not in the table and would flip the same way. The claim “two measured cells” is exact; the claim “two possible negated reads” is not, and D7’s trigger set (Open question 4) must cover the unmeasured spellings too.

• ox query --extent over a shape-defined concept stops refusing and starts answering. A widening, not a break, but a visible behaviour change for any tooling that treats the refusal as a signal.

• $iof moves on more events. It currently moves only on membership assertions; the archived incremental-maintenance model records exactly that (archive/rfd/0079/architecture/07-commit-pipeline-reuse.md:100, .../15-materialization-impact-proof.md:164). A derived $iof moves on any commit that moves a shape concept’s extent, so the impact model must be extended or its proof narrowed. This is work, and it is the largest single cost of this design.

• A dependency component can get larger. A free type position can merge otherwise-independent components. Sound, but a cost — Open question 3.

• The catalog tier is untouched, so its stratification-safety justification and the Lean catalog-closure invariants stand.

• The mechanization is untouched (D6).

• The seed gets smaller. The individual-tier scan and the iof_by_entity accumulation are deleted under either mechanism.

• Derivation-semantic epoch. The first behaviour-changing slice bumps it. DERIVATION_SEMANTIC_EPOCH (compiler/crates/oxc-runtime/src/lib.rs) is 10 on the main line today, and pull request #1784 advances it to 11, so the first slice here takes 12 or later. The number is read off whatever the main line carries when the slice lands, never assumed.

Slice plan

Each slice is independently reviewable and independently revertible. Only the slices marked as such change what a program derives.

1. Executable oracle — pins today’s wrong answers. A fixture per spelling (iof, not iof, meta ==, extent, constant and variable type position, ad-hoc and declared, shape-defined and asserted control) asserting the answers the toolchain gives now, wrong ones included, each annotated with the answer it will give after. No behaviour change; no epoch bump. This lands first so every later slice’s effect is a diff against a recorded baseline rather than a claim.

2. Canonical concept semantics. One statement, in the specifying chapter and in the mechanization’s prose, of what concept membership means and which relation denotes it — the D1 statement, with the D5 third-truth-value invariant. Documentation and the corrected meta-calculus.md:143. No behaviour change; no epoch bump.

3. Typed intrinsic and intermediate-representation boundary. Give the reflection reads a typed representation and keep the metatype-equality atom whole through relationalization instead of splitting it into a join plus a filter, so lowering can later decide on it as one thing. This is the slice that makes D4 implementable without the pair rewrite the rejected alternative foundered on. Internal representation only; no epoch bump, subject to the artifact hash moving, which the projection cache already discriminates on (derivation_commitment in compiler/crates/oxc-oxbin/src/projection_cache.rs).

4. Derived $iof. The bridge rules, the deleted individual-tier scan, the stratification wiring. First user-visible change; epoch bump — 12 or later. extent follows for free (D3), and the --extent refusal is retired here. D7’s warning ships one release before this slice.

   Preconditions, both blocking. (a) Issue #1902 — the is unknown truth qualifier returns definitely-true members — is fixed or the qualifier is refused, per D5: this slice widens the region of legitimately undetermined membership, so the read surface for undetermined membership must be honest before the region grows. (b) Open question 2 is settled: the incremental maintainer’s handling of the undefined extent across commits. Neither is a follow-up.

5. Derived $meta. The antichain rules, individual tier only. Epoch bump. Kept separate from slice 4 because it is the slice with a measured discrepancy against the catalog tier and should be reviewable against the demonstration’s numbers on its own.

6. Optimization. Bounds on the free type position, incremental-maintenance work for the widened $iof impact set, and whatever the measurements from slices 4 and 5 justify. No semantic change; no epoch bump. Last, deliberately: the design must be correct before it is fast, and the tractability restrictions D5 declines to impose for soundness belong here or nowhere.

Open questions

1. Does x is T belong to this surface at all? It does not appear to share the : lowering path: is introduces the optional-payload test and the reasoning-outcome suffix (rule_atom and atom_suffix in compiler/crates/oxc-parser/src/rule_atom.rs), and p is Voter is refused as a relation-valued application (OE1386). No claim in this record covers it. Settled by: an audit of the is suffix grammar against the membership surface, deciding whether x is T should be a membership spelling, a refusal with a message pointing at x : T, or left as it is. Required before any statement about “every membership spelling” is complete.
2. How does the incremental maintainer preserve the third truth value across commits? D5 makes undefined a real state of the reflection relation. The batch evaluator represents it as a companion relation ($undefined::R, undefined_name in compiler/crates/oxc-reasoning/src/executor/wfs.rs), but the incremental circuits carry signed weights, so a cell moving between undefined and false must not become indistinguishable from one that never moved — and the companion relation must be maintained, not recomputed. Related: whether the reflection atoms should accept the is unknown suffix so the undefined case is readable at all (atom_suffix in compiler/crates/oxc-parser/src/rule_atom.rs); today they do not. Settled by: a statement of how the undefined extent is maintained incrementally, plus a differential test that moves a cell into and out of undefined across commits and compares against full re-derivation. This gates slice 4.
3. What bounds a free type position? iof(x, t) with t unbound is sound (D5) but can merge otherwise-independent dependency components into one well-founded unit, turning a set of small evaluations into one large one. Settled by: a measurement of component size against a corpus with free type positions, and a decision on whether to bound it — by requiring a $specializes or equality constraint on t, by a cost-based warning, or not at all. This is slice 6 and must not become a soundness argument.
4. What is the warning’s exact trigger set? D7 says a warning ships one release ahead. The obvious trigger — a reflection head with a shape-defined concept in the type position — over-fires on positive reads that need no edit and under-fires on a variable type position that could range over a shape concept. Settled by: a trigger specification plus a measured false-positive rate against the example corpus, before the warning ships.
5. Do the bridge rules interact with defeasible or standpoint-scoped membership? The bridge is stated over C(x) unqualified. Whether it should bridge per standpoint, and how it composes with a defeated membership conclusion, is unexamined here. Settled by: an audit against the defeat-plane and standpoint surfaces before slice 4.
6. Should the mechanized type-test atom gain an evaluation semantics? typeTest and metaEq are recorded as correct-to-fail (spec/lean/Argon/Reasoning/EvalProgram.lean:73-74, :1375-1380), and the surface stays honest only because the bare-name lowering never reaches the atom. D6 shows this design does not force the question, but it does not answer it. Settled by: a decision at the substrate layer, which has precedence over the surface for evaluation semantics.
7. Who fixes the self::-qualified path, and in which direction? Issue #1904 is five of the nineteen measured defect cells and is explicitly out of this record’s scope, but it bounds this record’s headline claim (D1) until it is resolved. The direction is not obvious: the type test accepts the path and silently answers nothing, the reflection intrinsic refuses it (OE0227), and those cannot both be right. Settled by: a ruling on whether self:: resolves or is refused, applied to both spellings at once. Independent of slices 1–6, but the “three exact spellings” claim is not fully true until it lands.
8. What does #[world(open)] change? Under an open world an empty membership answer may be unknown rather than wrong. The OE0240 and OE0241 entries record the open-world softening as designed and not wired. Settled by: a ruling on whether shape-defined non-membership under an open world reads as Not or as Can, and whether D5’s third truth value and the open-world unknown are the same state or two.

References

• RFD 0017 — Refinement classification: where (primitive) vs iff (defined) (0017-refinement-classification.md)
• RFD 0023 — Reflective TypeRef (0023-reflective-type.md)
• RFD 0027 — The meta-property plane (0027-meta-property-plane.md) — the catalog tiers the $iof / $meta metatype rows implement
• RFD 0070 — Derive-backed classification (0070-derive-backed-classification.md)
• RFD 0092 — Membership-plane authority: fail-closed reads of derived membership (the alternative record; pull request #1874)
• Pull request #1903 — the membership-spelling conformance sweep: five program shapes by fifteen spellings, seventy-five cells, each evaluated by execution. The source of every count in Measured scope.
• Issue #1902 — is unknown returns definitely-true members. A blocking precondition of slice 4 (D5).
• Issue #1904 — the self::-qualified type test silently derives nothing. Five of the nineteen measured defect cells; not closed by this record, and it bounds D1.
• spec/lean/Argon/MetaCalculus/Reflect.lean — the opaque membership field and extentOf
• spec/lean/Argon/TypeSystem/Realization.lean — the realization biconditional
• spec/lean/Argon/Reasoning/EvalProgram.lean — the correct-to-fail atom ledger
• Issue #1859 → pull request #1860 — field read on a shape-defined-typed parameter
• Issue #1871 → pull request #1873 — group-axiom checks evaluate membership in the fixpoint