RFD 0070 — Derive-backed classification: the shape clause

• State: committed (ratified 2026-07-08)
• Provenance: the semantic core (§4–§6) was discharged in a kernel-checked scratch mechanization over the shipped Argon.Reasoning.Datalog substrate before ratification (statement ledger in Appendix B; the scratch file is deliberately never merged), and the full document passed an adversarial evidence audit prior to ratification — every load-bearing citation verified against the repo, the mechanization, and the external literature.
• Decides: (a) that a shape-defined concept is an ordinary IDB atom of the reasoner’s WFS/AFT fixpoint, with a stated + mechanized realization biconditional; (b) the guardrail floor; (c) the construct count (§7); (d) the Can-membership dispatch policy (§8). Relates to RFD 0017 — Refinement classification: where (primitive) vs iff (defined) (does NOT widen the inline iff fragment), RFD 0045 — The world-assumption write-side: refuse-on-K3-not and the #[world] opt-in (refuse-on-K3-not), RFD 0060 — The Lean substrate mechanization architecture (delimited reflection), RFD 0069 — The shared-live-KB write model: concurrent authoring, coexistence, and resolution (federation two-layer composition), the persisted-derived-read-model proposal (#1493), RP-008 (the open derive-backed realization home; NOT RP-007 — see §10).

1. Motivation

UFO roles and relational phases are condition-defined membership over other entities (participation in a relation, derived classification of related individuals). Argon’s inline iff { P } refinement is per-individual and local by construction (OE0660): it evaluates a predicate over self’s own field state + the static type graph, outside the reasoner fixpoint. It cannot express a relational instantiation condition. This is the documented OWL gap (gUFO: “OWL has no dynamic classification”; OntoUML→OWL reifies a TemporaryInstantiationSituation and emits SWRL for the instantiation condition). Native rule-derived membership closes it.

The ontology-fit analysis fixes the correspondence:

Rule of thumb: intrinsic-and-local → iff {}; relational OR fixpoint-dependent → shape clause. The mechanism follows the condition, not the metatype label. phase/role/relator/rigidity·sortality are package vocabulary (arg_ufo), never language surface (§3.4 no-ambient-vocabulary); the substrate provides only the two neutral mechanisms and never reads a UFO name.

Flagship (acceptance case 1, legally_capable): LegallyCapableNaturalPerson — a person is legally capable iff they hold a contractual capacity and are not under guardianship. Membership turns on other entities (held capacities) and a derived disqualification — outside OE0660 (verified: count{c in self.caps, c in ContractualCapacity} and a HasCap(self) call both refuse OE0660 today). Built + derived: extent = {alice} (bob excluded — non-contractual capacity; carol excluded — guardianship disqualifies).

2. Scope / non-goals

• The inline iff local fragment is not widened. OE0660 stands; RFD 0017’s vacuous-invalidation containment is preserved. This RFD adds a declaration-level surface, not a widened expression grammar.
• Federated shape membership is deferred (a dedicated later design). Shape membership over placed/foreign relations refuses today (the #1450 prototype’s foreign-connector refusal); this RFD does not lift that.
• Bounded self-field aggregates in inline refinements (count over self nav-fields) are out of scope here: that was evaluator lag on the designed-in decidable fragment, fixed separately (#1501, landed via #1505).

3. Design — the shape clause

Declaration-level clause:

pub type LegallyCapableNaturalPerson <: NaturalPerson iff LegalCapacityShape(self);

<ShapePath> resolves to a module-local pub derive (the shape). It desugars to an ordinary concept-headed rule in the rule plane:

derive LegallyCapableNaturalPerson(m) :- LegalCapacityShape(m), NaturalPerson(m);

plus, per named witness, a projection derive. Keyword reuse, not plane merge: the compiler-enforced marker (body shape — an inline { … } block vs a shape-path Ident(…)) selects the plane. The locality difference stays semantic (§7). No new keyword is introduced: both planes share the one iff keyword, the plane selected by the compiler-enforced marker (the ratified framing, §7). (The exact lexing — one-token lookahead — and positional witness binding are #1450-derived surface specifics, prototype-only and implementation-pending; the semantic contract is the desugar target, not the surface bikeshed.)

The synthesized rule is single-source: it is the only rule with head C, and manual insert iof(x, C) is refused (OE0211, on main). A head-collision with another rule must also be refused; the prototype’s OE0678/OE0666 codes for that are #1450-only (NOT on main) — the diagnostic family is pending implementation, the requirement is not. This single-source discipline is what the semantics in §4 rests on.

4. Semantics — membership-as-IDB + the realization biconditional (mechanized)

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 and no hand-rolled alternating fixpoint (that is where the published hybrid-MKNF errors were: Knorr et al. 2011, corrected by Liu & You 2017/2021). Argon reuses its single AFT operator: the substrate’s stableRev on the product bilattice Approx = Set Atom × (Set Atom)ᵒᵈ, whose well-founded fixpoint wfFix P equals the Van Gelder model (wfTrue P, wfPossible P) — a theorem in the substrate (Argon.Reasoning.Datalog.AFT.wfFix_eq).

Realization biconditional (mechanized). Under the single-source discipline, for the synthesized rule C(m) :- Shape(m), Parent(m) and every individual x, membership realizes the surface promise in three-valued (Kleene) logic:

• definitely-true region: iof(x,C) ∈ wfTrue P ↔ iof(x,Parent) ∈ wfTrue P ∧ Shape(x) ∈ wfTrue P;
• not-false (Can) region: iof(x,C) ∈ wfPossible P ↔ iof(x,Parent) ∈ wfPossible P ∧ Shape(x) ∈ wfPossible P;
• K3 value: wfModel P (iof(x,C)) = KleeneAnd (wfModel P (iof(x,Parent))) (wfModel P (Shape(x))).

These are proved over the joint operator on the existing Argon.Reasoning.Datalog substrate (statement ledger in Appendix B). Undefined membership surfaces as Can (RFD 0007); it is never fabricated into Is (RFD 0045-D1; collapse_conclusion_lacks_positive_evidence).

K3-non-corruption (the Both boundary). Within one store a shape-defined concept’s membership is single-source, so the well-founded model is consistent (wfTrue ⊆ wfPossible, substrate wfTrue_subset_wfPossible) and reads into K3 (Is/Can/Not) — never Both. A single-store realization “with Both” would be vacuous (the inconsistent-pair region is empty) and is refused as a statement. Both on shape membership arises only under federation (a default assertion + a standpoint refutation info-join to Both), which is the Liu-You inconsistent-pairs extension and is already carried by the two-layer composition (RFD 0069: L1 accumulate-Both / L2 resolve→K3, CompositionSoundness.lean). Federated shape membership is deferred (§2). This is the shape slice’s discharge of the “a Both leaking into the reasoner corrupts the fixpoint” landmine: the single-source guardrail is the non-corruption guard.

5. Guardrails (the floor — may tighten, not loosen)

1. Per-individual groundedness on the shape head. Every classified variable is bound by a positive per-individual atom (the parent, or a typed shape-head param). An only-negatively-bound classified variable is not range-restricted → refuse OE1303 (acceptance case 4b refuse_ungrounded_head). Semantic content mechanized: a shape-defined individual is never even possibly a member unless already a possible member of the parent — membership derivation invents no individual (Appendix B L11; compile-time enforcement is the syntactic Compiled.CRule.Safe/Safe.head_determined).
2. Aggregation stratified across classifier cycles. A shape whose body aggregates (forall/count) over the concept’s own extent has no well-founded fixpoint; the synthesized rule is folded into the build-time stratify set → refuse via the OE1317 extension (acceptance case 4a refuse_aggregation_cycle). The OE1317 refusal stands on the substrate (self-aggregating recursion has no well-founded fixpoint), not on the survey. As a design prior only: the design-record literature survey reports (medium confidence) that every deployed system stratifies aggregation w.r.t. the classifier cycle and the monotone carve-out is theory-only/unimplemented — corroborating, not load-bearing.
3. Negation-through-classifier → Can + loud cycle diagnostic. Recursion through negation across classifiers is allowed (WFS gives it a model); membership surfaces Can. Argon additionally emits a loud cycle diagnostic — that loudness is Argon’s own silent-wrong-prevention norm (owned, §8), NOT inherited practice: Flora-2 merely surfaces undefined, it does not warn. We can allow what stratify-only systems forbid because Can is native to the envelope. Acceptance case 2 breach_fulfillment (asymmetric chain → definite; symmetric self-guard → Can) and case 5 cwa_owa_pair (Eligible/Blocked standoff → Can; ground breaker → definite).
4. No existence invention in classifier heads. Membership derivation ≠ individual creation (guardrail 1 mechanization).

6. The #165 evaluation-unit constraint (BINDING)

Compositional/stratified evaluation of a program containing shape-defined concepts agrees with the whole-program well-founded model iff no well-founded-undefined (Can) membership atom crosses a split boundary into a position where the consumer projects Can→absent→Not. When a boundary atom is Can and the upper unit materializes only the lower unit’s definitely-true atoms as a completed EDB, the upper unit reads the Can atom as false and over-asserts (issue #165).

• Disagreement is real (mechanized non-vacuity, Appendix B L8): for Plow = {p←¬q, q←¬p}, Pup = {r←¬p}, evaluating Pup over the materialized wfTrue(Plow) derives r as definitely-true, while the whole-program WFM leaves r undefined (Can). Stratified composition strictly over-asserts.
• Agreement condition (assume-cited): compositional evaluation equals the whole-program WFM when every cross-boundary atom is two-valued in the whole-program WFM. This is the AFT-operator splitting theorem — Vennekens, Gilis & Denecker, Splitting an operator: algebraic modularity results for logics with fixpoint semantics, ACM TOCL (DOI 10.1145/1183278.1183284) — which applies directly because Argon’s wfFix is an AFT well-founded fixpoint; and, at the Datalog level, Ross, Modular stratification and magic sets for Datalog programs with negation, JACM 1994 (DOI 10.1145/195613.195646), whose modularly-stratified class (“makes every ground literal true or false”) is exactly the two-valued-boundary hypothesis.

Binding constraint. A Can-bearing shape concept and everything that (transitively, through the classifier) consumes it live in one WFS evaluation unit (one SCC-closure). Cross-unit materialization of derived membership is Can-faithful-or-refuse — never Can→absent. Two seams are bound:

• The unified membership oracle (#1506) must carry the four-valued state (this is why the fix was one oracle, not a shape-only patch); a store-local evaluator refuses where membership is fixpoint-dependent rather than reading absence as Not.
• The persisted-derived-read-model proposal (#1493) must be Can-faithful-or-refuse: materializing only wfTrue and letting a later read treat absence as Not re-creates #165 at the storage layer.

Perf. Defined-membership modules are IVM-ineligible (they already route to the slow rebuild path; strict_cache.rs treats any defined concept as delta-non-simple). Incremental WFS appears solved only in tabling form (Swift 2014); no set-oriented WFS-IVM is reported (design-record literature survey, self-flagged medium-confidence negative — not corroborated here). Working assumption: memoized recompute per undefined-bearing SCC. The #1493 proposal is the materialization complement, subject to the Can-faithful constraint above.

7. Decision 1 — construct count (DECIDED: two planes, one keyword, one marker)

Decision (ratified 2026-07-08): two evaluation planes, one keyword (iff), one compiler-enforced marker — a local decidable plane (iff { P }) and a fixpoint plane (iff ShapeName(self)), distinguished by a visible marker the compiler enforces, not two independent keywords. Strongest alternative (the field’s): uniform membership under WFS — Flora-2 / F-logic collapse the distinction, making every membership condition (including intrinsic per-individual conditions) an IDB predicate in one fixpoint, with no separate local fragment.

Argued against uniformity, from verified/mechanized sources:

• K3-non-corruption — the realization theorem’s own basis. The mechanized single-source / OE0211 discipline (CwaOwa.lean; the design record’s paper realization argument) keeps classification K3-valued: a manually-asserted Is meeting a law-derived Not info-joins to Both, escaping K3 and corrupting the fixpoint. Two planes with separate sources (asserted where; derived iff/shape; no manual insert iof on a defined concept) preserve single-source. Uniform membership — one predicate both assertable and derivable — forfeits exactly the single-source guarantee that L7 and the realization theorem (§4) rest on. This is the strongest rebuttal, and it is mechanized, not stylistic.
• Local decidability / polytime bound. Decidability/Fragment.lean + Complexity/Bounds.lean prove the local fragment bounded (d1EvalCost ≤ d1Size·(n+1)^depth, “locally determined by the root,” cost independent of N, evaluated at elaboration/write time). Uniform WFS membership makes every per-individual intrinsic check a global fixpoint atom, forfeiting the local bound and the write-time invariant enforcement (where invariants at flush, OE0668).
• RFD 0017 containment. 0017’s vacuous-invalidation containment relies on the local fragment NOT coupling to the fixpoint (OE0660); its §Open flags “revisit if the fragment widens.” Uniform membership IS that widening — it forces transitive invalidation to be chased.
• RFD 0060 delimited reflection is FORCED (decidability + sound mechanization); uniform (un-delimited) membership cuts against a committed decision.

Honest framing of the conclusion. These sources force two evaluation planes + a visible compiler-enforced marker — they do NOT by themselves force two surface keywords. The adopted syntax already reflects this: one keyword iff, the plane selected by the body shape. So the precise decision is two planes, one keyword, one marker, not “two forms.” The marker must be compiler-enforced and visible (OE0660 already refuses fixpoint-forms inside inline iff), so the plane a concept lives in — hence its cost class and whether its membership can be Can — is never silently changed by an edit.

True differentiator between the planes (correcting an earlier overclaim). It is NOT “inline iff never yields Can”: inline iff membership IS three-valued under #[world(open)] (RFD 0007; refinement.md). The differentiator is the SOURCE of Can — in the local plane it is open-world DATA ABSENCE (a missing field/relation under OWA); in the fixpoint plane it is FIXPOINT UNDEFINEDNESS (a well-founded-undefined SCC). Different provenance, different diagnostics, different perf.

(LOOM — production rules re-fused with classification, “death by complexity” — is at most an illustrative caution about hiding the plane boundary; a historical analogy, not evidence in this chain.)

8. Decision 2 — Can-membership dispatch on typed surfaces (DECIDED)

The #1450 prototype implements labeled-Can on all four read surfaces; its own design sketch says definite-only. These are not in conflict once the ENVELOPE is separated from the DECISION.

Decision (ratified 2026-07-08): the envelope is four-valued everywhere (never silently drop Can; hidden counts). Decisions requiring a definite type read definite-only. Two parts, distinct warrant:

• THEOREM (sound): never promote Can→Is. A surface requiring Is must not treat Can/Both as Is. Mechanized: cwaCollapse_is_iff (cwaCollapse t = .is ↔ t = .is) + collapse_conclusion_lacks_positive_evidence (CwaOwa.lean); RFD 0045-D1 (“derive is rejected as unsound, not declined”). The MKNF/Flora-2 undefined-tolerating-consumer restriction maps cleanly: a two-valued-requiring consumer restricts to the proven fragment.
• POLICY (Argon house norm — owned, NOT a theorem): refuse Can LOUDLY rather than silently fail closed. The same mechanized chain that proves never-promote also models the silent K3 fail-closed reading: CwaOwa.member/memberOf return Bool, collapsing Can/Both→false with no signal — and that is mainstream practice (OWL open-world entailment, SHACL validation, SQL NULL 3-valued logic all fail closed silently). So silent-fail-closed is theorem-SANCTIONED; loudness is Argon’s silent-wrong-prevention norm layered on top. The alternative was weighed honestly — silent K3 fail-closed is simpler and matches mainstream tools — and the ratified choice is loud-refuse: a dropped Can is never invisible. The never-promote half is theorem; the loud-vs-silent half was the policy call, now decided.

Caveat: #[world(open)] is a live attribute today, but OWA absence→Can relabeling for derived/shape membership is designed-not-wired (post-implementation). Acceptance case 5’s Can envelope is real today via ox derive; its per-world OWA relabeling of shape absence is not demonstrable pre-implementation (a non-member is currently absent, not Can, under #[world(open)]). Document per-case current behavior accordingly.

9. Migration from #1450 (evidence, never a merge base)

#1450 has the mechanism right (desugar to a concept-headed derive on the rule_head_concepts seam) but patches the classification↔catalog incoherence for the shape tag only, across 117 files, with no spec/Lean backing. Salvage by cherry-pick where this RFD agrees. The prerequisite membership-oracle unification is done — merged as #1506 (9f3bc30e2), #1500 closed: one membership oracle so classification_concepts/most_specific_types/dispatch/closed-world-gate/nav-seeding now see rule-head-concept membership that $meta/catalog/ox derive already served; the read-surface disagreement that had been live on main is fixed. The store-local evaluator refuses where membership is fixpoint-dependent.

10. Corrections folded in (Lean leads)

• The design-record survey’s claim “the iff realization theorem is NOT mechanized (RP-007 §4.5)” is imprecise: Argon.TypeSystem.Realization.realize_iff (#166) already mechanizes the local-fragment realization at the abstract level (P : Ind → Prop opaque over the classification State). What remains open there is the value-environment-dependent local realization — and that IS correctly RP-007 §4.5. This RFD does not overturn that citation: RFD 0017 §61/§91 deliberately route the local iff realization theorem to the RP-007 §1.2-hazard-2 / §4.5 value-dependent sub-problem, and that routing stands.
• What is genuinely distinct: the derive-backed realization (a shape body computed by the WFS/AFT fixpoint, not a value predicate over self’s fields) is a different open problem, homed in RP-008 (relational-extension / evaluation-level: “no RuleIR interpreter; Reasoning.State is meta-property only”). This RFD’s mechanization discharges it at the Datalog layer (Program Atom/wfFix), sidestepping RP-008’s missing-interpreter blocker for the classification-atom case. Net: RP-007 §4.5 = local value-dependent iff (RFD 0017’s, unchanged); RP-008 = derive-backed shape (this RFD).

Appendix A — acceptance corpus (verbatim motivating examples)

Held in the track design record at ratification; ships in-repo as the implementation’s acceptance suite (each case = ratified-pending target surface; each -runnable variant = the desugaring verified against the current toolchain):

1. legally_capable — relational phase via shape; extent = {alice} (§1 flagship).
2. breach_fulfillment — mutual-classifier recursion-through-negation; asymmetric→Is, symmetric loop→Can.
3. usc26_singletons — pub fact statutory singletons + a downstream rule joining the shape-defined concept as a classification atom (the OE0226 TypeRef-parity regression class — must stay green). 4a. refuse_aggregation_cycle — OE1317 (aggregation through classifier cycle). 4b. refuse_ungrounded_head — OE1303 (ungrounded shape head — the genuine negative).
4. cwa_owa_pair — CWA/OWA labeling; Eligible = {} Is + {pending} Can; §8 caveat applies.

Appendix B — scratch-mechanization statement ledger (never merged)

Verified against the built Argon lib (0 diagnostics, no sorry, no new axioms) at ratification; the scratch file is deliberately never merged — RP-008’s substrate mechanization re-homes what implementation needs. Status legend: PROVED-scratch / PROVED-substrate (cite) / ASSUME-cite / REFUSE.