Refinement

refinement-clause ::= ('where' | 'iff') '{' refinement-pred (',' …)* '}'
refinement-pred   ::= D1Pred | D2Pred

A refinement attaches a predicate to a concept. The keyword chooses how the predicate relates to membership — the description-logic split between a primitive class (⊑, necessary conditions only) and a defined class (≡, necessary and sufficient conditions). See RFD 0017.

• where { P } — primitive. P is a necessary condition: every member satisfies it, but a supertype instance that merely satisfies P is not thereby a member. Membership is asserted (by construction or insert iof, mutate); P is enforced as an invariant at each membership write and never widens the extent. This is Rust’s where bound lifted to a concept’s members — a constraint, not a definition.
• iff { P } — defined. P is necessary and sufficient: an instance of the supertype is a member if and only if it satisfies P. Membership is derived — the substrate auto-classifies and rejects manual insert iof (mutate, OE0211). Reads as the membership biconditional: “an Adult is a Person iff age >= 18.”

pub type Adult          <: Person  iff   { self.age >= 18 && self.has_id };   // defined: any qualifying Person is automatically an Adult
pub type ExtinctSpecies <: Species iff   { self.living_count == 0 };          // defined: classification derived from state
pub type VettedVendor   <: Vendor  where { self.risk_score <= 30 };           // primitive: vetting is conferred; the score is a necessary invariant on members

D1Pred (substrate-locked): metaEq, isDet, hasAnc, hasDesc, countGeq, forallC, existsC, plus Booleans. D2Pred: QF-LIA, GNFO, enum equality. The elaborator stages D1 ahead of D2 residual.

Mechanically: D1Pred / D2Pred / MixedPred are inductives at spec/lean/Argon/Decidability/Fragment.lean; the staging theorem stage_correct lives at CrossDomain/Staging.lean; the polynomial bound on D1 evaluation (d1EvalCost n φ ≤ d1Size φ · (n+1)^(d1QuantifierDepth φ)) is proven in Complexity/Bounds.lean. The bound grounds the polytime claim Tier ladder makes for tier:structural and tier:closure.

Three-valued membership under OWA. When the governing world assumption is open (World assumptions (CWA / OWA)), 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 — matching SHACL’s sh:Violation discipline and SQL’s three-valued NULL semantics. Under CWA, unknown collapses to false. The mechanization at TypeSystem/Soundness/CwaOwa.lean proves that CWA-true refinement results survive transition to OWA (monotonic knowledge transfer). The symmetric rule for a primitive where invariant: a membership write is rejected only on positive evidence of violation (P evaluates to a definite false); unknown permits the write (mutate, OE0668). unknown means information absence — a referenced field with no recorded value. A predicate that cannot be evaluated at all (an unsupported form, malformed stored data, or a type-mismatched comparison such as ordering a Date against an Int) is not unknown: unsupported forms are refused at build time (OE0660), and anything that slips past the gate fails the operation loudly at runtime — never a silent permit (where) or a silently-empty derived extent (iff). Refinement predicates evaluate on the same exact value tower as every other value position (RFD 0016): exact rationals for Real/Decimal/Money, chronological Date comparison, with no value-dependent enforcement.