RFD 0084 — Mapped relation subsumption

• State: discussion
• Opened: 2026-07-22
• Decides: that <: on relations takes an explicit argument-mapped form as its only surface form — a child names, for each parent end (by the parent’s end name), what fills it: a child end (a rename), a child end widened to a parent supersort (a cast), or a constant (a pin) — and that the bare positional form (<: Parent) is removed: it is refused at the declaration with a catalogued diagnostic, with no deprecation window and no lint stage. Settles how the mapped form interacts with every plane that already consumes relation subsumption: end mutability (RFD 0076), the retract/amend cascade (RFD 0076), relation-value application dispatch (#1805, #1806), reflection, coverage, and the incremental rule circuits (RFD 0018 / RFD 0021 lineage). This RFD is a successor amendment to RFD 0005; it generalizes that RFD’s positional check to the mapped form and retires the bare spelling. The bare form’s meaning is preserved as the identity instance of the general rule — but it is no longer a writable surface form; the identity mapping survives only as an internal representation and as the migration bridge (D10).
• Surface policy: one surface form (explicit mapped). No bare form, no deprecation window, no lint. In-repo bare sites migrate mechanically in the enforcing slice; the external ontology-library corpus migrates via an ox-migrate rewrite at its next toolchain upgrade.
• Affects: relation declaration grammar; the elaborator subsumption checks (Argon.Substrate.RelationSubsumption — arityEqual, endpoint covariance); the relation-value application dispatch lowering (Argon.Reasoning.Datalog.RelationApplication); the reflection plane ($specializes, the relation tier); the write-path end-mutability and cascade gates (RFD 0076); the artifact wire format (additive, optional-on-decode; non-identity edges gated by a core-IR version stamp so a too-old decoder refuses loudly).

In plain language — what changes and why

A relation in Argon is a named table of tuples — Loc(p, c) says person p is located in city c. Subsumption (<:) says one relation’s tuples flow into another’s: every child tuple is also a parent tuple. Today <: only works when the child is shape-identical to the parent — same number of ends, same order, compatible sorts — and the pairing is positional and implicit: Home(p, c) <: Loc silently pairs Home’s first end with Loc’s first, and so on, by position alone.

That is too rigid for a very common modeling situation: a narrow relation that should participate in a general family under a translation. Consider a general “income item” relation carrying a currency, and a specific “US wages” relation that is always in dollars and therefore does not carry a currency end at all:

pub rel IncomeItem(p: Person, amount: Int, c: Currency);
pub rel WagesUSA(p: Person, amount: Int);

Today you cannot write WagesUSA <: IncomeItem — the shapes differ (two ends vs. three). Your only option is to hand-write a separate derive rule that fills in the dollar constant. But that rule is not a subsumption edge, so the relation family loses WagesUSA as a member: any code that dispatches over “everything that is an IncomeItem” (the relation-value application feature landing in #1805) silently never sees US wages. A member drops out of the family and nothing tells you. That silent omission is the rot this RFD removes.

The change. Every <: clause states, explicitly, exactly how the child’s ends land on the parent’s, and may fill a missing parent end with a constant:

pub rel WagesUSA(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

Each filler is keyed by the parent’s end name (p, amount, c) and states where that end’s value comes from: parent p from child p, parent amount from child amount, and the parent’s c end — which the child does not have — pinned to the constant USD. Now every WagesUSA(p, a) tuple contributes IncomeItem(p, a, USD) to the family, exactly as a hand-written rule would, but as a real subsumption edge — so WagesUSA is a family member and dispatch finds it. The clause can also cast a child end whose sort is a subsort of the parent’s end (a = friend as Person), so a relation over a narrower type can join a family declared over a wider one.

The bare form is removed. pub rel Home(p, c) <: Loc; no longer compiles; it is refused with a catalogued diagnostic. The equivalent must be written explicitly, keyed by the parent’s end names: pub rel Home(p, c) <: Loc(p = p, c = c);. There is therefore one surface form for subsumption, not two.

Why remove it rather than keep it as a shorthand? The relation corpus is written predominantly by automated tooling and read/reviewed by people, so the reader-over-writer trade favors self-describing declarations. Bare positional pairing silently re-pairs the wrong ends if the parent’s ends are reordered — the exact silent-failure class this design exists to eliminate — whereas the explicit form keys each filler to the parent end by name, so the pairing is anchored to names and robust to reordering on either side. (A positional filler list — a bare token per parent position — was considered and rejected for the same reason: it re-pairs under a parent-end reorder exactly as the bare form does; only parent-name keying is mechanically reorder-safe. See Alternatives (d).) And two spellings for one idea guarantee style drift in a machine-written corpus. Nothing outside this repository depends on the bare form (the language is pre-1.0), so every in-repo bare site — reference-book examples, the conformance corpus, fixtures — is migrated mechanically in the same change that turns on the refusal, and an ox-migrate rewrite handles the external ontology-library corpus at its next toolchain upgrade. The identity mapping is preserved internally (it is what a migrated bare site elaborates to), and a theorem proves that migration is meaning-preserving (D10), so removing the bare surface path is safe.

Querying the family — and knowing which member answered. Once relations join a family, you ask questions over the whole family at once. Sometimes you want the merged result (“every income item, in dollars”) — a plain query on the parent relation gives it. Other times you need the witness: not just that a tuple is in the family but which member relation it was declared in (“every income item and the relation it came from”). The canonical surface for that is a trailing via on the parent atom:

pub derive incomeSource(p: Person, a: Int, c: Currency, k: Relation) :-
    IncomeItem(p, a, c) via k;

IncomeItem(p, a, c) is the ordinary parent-union query; via k additionally binds k to the member relation each tuple was declared in. Given WagesUSA(alice, 100) and InterestUSD(alice, 30) it binds k to WagesUSA and InterestUSD respectively — each row once, tagged with its source. Constant pins live in the parent frame, so IncomeItem(p, a, USD) via k selects only the USD members.

via is canonical because the parent frame is information-complete: D1 forbids dropping a child end, so every value a member carries reaches the parent frame through the declared mapping (renames and reorders relocate values, pins add constants). Its meaning is the generalized specializes atom, which names both frames in one atom and is via’s exact desugar target:

pub derive incomeSource(p: Person, a: Int, c: Currency, k: Relation) :-
    specializes( k(_fresh…) , IncomeItem(p, a, c) );   // what `IncomeItem(p,a,c) via k` desugars to
    // (the member frame's width is the selected member's own arity — this
    //  family mixes 2- and 3-place members, so no fixed wildcard count can spell it)

Parent(args) via k desugars exactly to specializes(k(_fresh…), Parent(args)) — one semantics, one desugar point. The obvious hand-rolled alternative — enumerate the family reflectively with the bare specializes(k, IncomeItem), k(p, a, c), then apply each member — returns every row twice (once under its member, once under the family parent, because the parent literally contains a copy of every member’s tuples) and leaves the argument shape implicit. via reads each member’s own extent once and fixes the parent frame explicitly, with no new machinery: it reuses the same dispatch the family membership feature already builds (D6).

Question

<: on relations, since RFD 0005, requires the child to be positionally shape-identical to the parent: equal arity (arityEqual, OE0150), covariant endpoint sorts position-by-position (OE0151), refined cardinality (OE0152), compatible metarel (OE0153). The induced semantics is tuple-inclusion: child’s extent is a subset of parent’s extent, tuple-for-tuple.

This forbids the single most common non-trivial modeling shape: a narrow relation participating in a general family under a translation — an end renamed, an end absent-because-constant, an end at a subsort. Today that shape must be expressed as a hand-written derive rule, which is not a subsumption edge and therefore loses family membership: the relation-value application dispatch of #1805 (specializes(r, Family), r(args)) enumerates subsumption children and never finds the derive-backed relation. The omission is silent — the worst failure mode for a knowledge base.

<: takes an explicit argument-mapped form, keyed by parent end name — renames (parentEnd = childEnd), constant pins, and subsort casts — as its only surface form; the bare form and the positional filler list are both removed and refused. What does the elaborator check, how does the mapping thread through every plane that consumes subsumption, and how do the in-repo and external corpora migrate off the bare form?

Context

The open-family motivation

RFD 0005 records the driving demand as a sub-relation whose endpoints narrow and whose tuples flow to the parent, and notes the fallback cost precisely: “the modeler has to write a derive rule by hand, losing the structural property and the elaborator’s covariance check.” That fallback loses more than the covariance check now that #1805 makes family membership operational: a derive rule is invisible to specializes, so a family whose members are meant to be open-ended (add a new income kind, an audit rule over the whole family keeps working) silently excludes every member that needed a translation. The mapped form makes the translation itself a subsumption edge, so the member stays in the family.

Substrate readiness

The substrate carrier is unchanged from RFD 0005: SubsumptionAxiomBody is generic over sub_id/super_id UUIDs. What a mapped edge adds is not a new axiom kind but a per-edge argument mapping — metadata that says, for each parent position, which child end (possibly cast) or which constant fills it. The subsumption-closure logic is unchanged in shape; the extent contribution of a child is computed through the mapping rather than by identity.

What “mapping” is, precisely

A mapped edge child(e₁ … eₙ) <: parent(f₁ … fₖ) carries, for each parent end fⱼ (j ∈ 1..k), a filler written fⱼ = … that is exactly one of:

• a child-end reference — fⱼ = eᵢ, contributing child end eᵢ’s value at parent end fⱼ (a rename, stated by both names);
• a cast child-end reference — fⱼ = eᵢ as S, where S is the parent’s declared sort at fⱼ and child’s sort at eᵢ is a subsort of S (childSort(eᵢ) <: S); the value is the child end’s, admitted at the wider parent sort;
• a constant pin — fⱼ = κ, a literal value κ of the parent’s declared sort at fⱼ, contributing κ at that end for every child tuple.

Each filler names the parent end it fills by name, and a child-end reference names the child end by name too, so the mapping is anchored to names in both directions: reordering the child’s ends leaves each eᵢ resolving to the same end, and reordering the parent’s ends leaves each filler still filling the same fⱼ — the resolved parent position updates, the mapping’s meaning does not. This is the property both the removed bare form and the rejected positional filler list (Alternatives (d)) lacked: bare and positional pairing both re-pair silently under a same-sort parent-end reorder.

There is no bare surface form. child <: parent (no filler list) is refused (D1). The identity mapping — every parent end fⱼ filled by the child end at the same position (parent(f₁ = e₁, …, fₖ = eₙ), requiring n = k and reducing to RFD 0005’s checks exactly) — survives only as an internal representation: it is what a migrated bare site elaborates to, and the object of the migration-soundness theorem (D10). It is never written by a human or by tooling as surface syntax.

Decision

Ten decisions, one section each. The plane-interaction rows (D3–D9) are the heart of the RFD and are stated one decision per row; D6 is the user-facing family-query surface — the canonical trailing via, whose meaning is the generalized specializes atom — that the dispatch seam (D5) exists to serve.

D1 — Surface grammar and the well-formedness gates

Extend the relation <: clause with a required parenthesized filler list. Each filler is keyed by the parent’s end name — parentEnd = filler-value — so the mapping states, per parent end, where that end’s value comes from:

rel-subsumption ::= '<:' TypePath '(' filler ( ',' filler )* ')'
filler          ::= Ident '=' Ident                  // rename: parent end ← child end
                 |  Ident '=' Ident 'as' TypePath     // cast:   parent end ← child end, widened
                 |  Ident '=' Literal                 // pin:    parent end ← constant

The left Ident of every filler is a parent end name, resolved against the parent’s declared ends; the right side is the value that lands there — a child end name (a rename), a child end name widened with as (a subsort cast), or a literal (a constant pin). The filler list is required. A <: clause with no filler list — the bare form child <: parent — is refused (gate (h) below); there is no bare surface form.

Because each filler names the parent end it fills (not a position in the list, and not a bare child-end token whose parent slot is implied by order), the mapping is anchored to names in both directions. Reordering the parent’s ends leaves every filler naming the same parent end — the mapping’s meaning is unchanged, only the parent position each filler resolves to updates. Reordering the child’s ends leaves every child-end reference resolving to the same end by name. This is the property the earlier positional filler design (fillers as a bare token list, filler i filling parent position i) lacked: a positional list re-pairs silently under a same-sort parent-end reorder exactly as the bare form does — the sort-covariance gate cannot catch it because every position still type-checks (see Alternatives (d)). Name-keyed fillers close that gap mechanically.

There is no same-name abbreviation. A parent end filled by a same-named child end is still written in full — p = p, never a bare p. Admitting a bare token as sugar for p = p would reintroduce a second surface spelling (and revive the positional reading the name-keying exists to remove), against the one-surface-form philosophy this RFD holds throughout (Open questions §6, Alternatives (d)).

Well-formedness (elaborator, Argon.Substrate.RelationSubsumption). The following must hold; each violation is a distinct refusal. New codes are allocated notionally as next-free (the current maximum allocated relation code is OE1409, RFD 0076); the numbers below are placeholders the implementation slice pins against the catalog, not commitments.

Rule (c) — no dropped child ends — is decided deliberately: a child end that maps to no parent position would let two child tuples differing only at that end collapse to the same parent tuple with no declared meaning for the collapse. We forbid dropping child ends in this RFD (a would-be projection is instead a separate derived relation the modeler declares explicitly). This is revisited in Open questions as a possible future relaxation with an explicit projection marker.

A child end may be referenced by more than one parent end (a diagonal: parent(f₁ = e, f₂ = e)); this is permitted and contributes the same child value to both ends. A constant may be pinned at multiple parent ends likewise. (What is forbidden by (b) is the reverse — one parent end named by two fillers.)

The specializes keyword synonym takes the filler list too. The subsumption clause has two glyphs — the <: operator and the specializes keyword — which the parser routes through one clause path (compiler/crates/oxc-parser/src/grammar/decls.rs, supertype_clause), the modeler-friendly spelling of spec §6.3 (spec/reference/src/constructs/relations.md). The explicit-only decision is about the mapping being explicit, not the glyph, so it binds both spellings identically: gate (h) refuses a bare clause in either glyph, and the required filler list is written the same way after specializes as after <: (child specializes parent(f₁ = e₁, …, fₖ = eₙ)). The bare comma-separated multi-parent form child specializes R1, R2 — the keyword analogue of bare <: R1, R2 — is refused for the same reason bare <: is; a multi-parent edge is written child specializes R1(…), R2(…) (each parent carries its mapping; Open questions §1). Collapsing the two relation-side glyphs to a single spelling is out of scope here: the specializes keyword is shared with concept subsumption (supertype_clause_concept), so eliminating one glyph is a §6.3-wide surface decision, not one this relation-scoped RFD makes unilaterally. This RFD fixes only that neither glyph escapes the explicit-mapping requirement.

D2 — Semantics: mapped-tuple-inclusion

Subsumption generalizes from tuple-inclusion to mapped-tuple-inclusion. Let the mapping be the function φ that sends a child tuple t = (v₁ … vₙ) to the parent tuple φ(t) = (w₁ … wₖ) where wⱼ = vᵢ if the filler for parent end fⱼ is fⱼ = eᵢ (or fⱼ = eᵢ as S), and wⱼ = κ if the filler is fⱼ = κ. The induced family extent contribution of the child is the image of the child extent under φ:

ext(parent) ⊇ φ(ext(child)) = { φ(t) | t ∈ ext(child) }

The identity mapping recovers ext(parent) ⊇ ext(child) exactly (RFD 0005). Because φ may be non-injective (constant pins collapse the currency end; a diagonal collapses two ends), the image is a set — duplicate parent tuples from distinct child tuples coincide, consistent with set-semantic extents.

Cardinality/metarel through the mapping (D1f). Cardinality refinement is checked at each parent position against the filler: a constant-pinned position contributes a fixed single value per child tuple, so its parent-side count constraint is evaluated against the pin; a child-end position inherits the child end’s cardinality, which must refine the parent’s. Metarel compatibility is checked between child and parent as before; the mapping does not change the metarel classification, only the argument routing.

Lean-first plan.

• Argon.Substrate.RelationSubsumption (RFD 0005) gains the mapping as data on the edge and generalizes arityEqual to arityMapsParent (filler count = parent arity) and endpoint covariance to covariance-through-the-filler (covariantFillers, over the per-position helper entryCovariant). The existing (now-removed-from-surface) positional lemmas are recovered as the identity-mapping specialization — stated as a mappedChecks_identity_eq_bareChecks corollary. With the bare surface form gone, this corollary is no longer a “sugar can’t drift” guarantee; it is the migration-soundness witness — it proves that rewriting a bare site to its identity mapping preserves every accept/refuse verdict, so the mechanical migration and the deletion of the bare check path are semantics-preserving.
• Argon.Reasoning.Datalog.RelationApplication (as merged with #1805/#1806, carrying structural_containment and dispatch_selected_iff) gains the obligation mapped_containment: a mapped child <: parent edge entails φ(ext(child)) ⊆ ext(parent) in a mapped-closed program (MappedClosed, the generalization of structural_containment’s StructurallyClosed from identity inclusion to φ-image inclusion). Its dispatch_selected_iff obligation is restated as mapped_dispatch_selected_iff so that reading the compiled finite-dispatch helper at an admitted selector applies the selected relation through its mapping — the helper still adds no semantic premise; it applies φ.

What slice 1 proves vs. what it assumes. mapped_containment is stated relative to a MappedClosed program — the hypothesis that every declared edge’s φ-image is already contained in the parent’s extent — and discharges the edge→containment step from that hypothesis. It does not prove that an elaborator emits clauses establishing that closure; the emission is the check-plane / dispatch slices’ obligation and is explicitly deferred (see the module’s “Deferred” note). Similarly mapped_dispatch_selected_iff fixes the value-level contract of the dispatch helper (reading it at a selector = applying φ); it is not a proof about generated clauses. The obligation those later slices owe is: the elaborator-emitted mapped clause (D5) computes exactly φ(ext(child)) and nothing more — establishing the MappedClosed premise that slice 1 assumes — and the subsumption-closure over a graph of mapped edges is the composition of the per-edge images.

Dispatch and cascade are the same function (single-authority design). The dispatch expansion (D5) applies φ in the forward direction (child tuple → image), and the cascade/amend translation (D4) withdraws image support when a child tuple is withdrawn — the same φ, read the same direction. The design commitment is that there are not two hand-kept translations. This is recorded as a Lean obligation dispatch_cascade_same_map: the image a dispatch clause materializes for a child delta and the image a cascade withdraws for the withdrawal of that same delta are computed by one φ — the maintenance direction is the delta’s sign, not a second implementation.

What this obligation is, honestly. In the slice-1 Lean, dispatch_cascade_same_map holds by rfl because dispatchAdds and cascadeRemoves are defined as the same function (image m). The rfl is therefore the specification — it records that one φ, applied per delta sign, is the intended design — not a guard. Once the wire/dispatch slice introduces two independent Rust call sites (a forward dispatch materializer and a cascade withdrawer), a definitional identity in Lean carries no anti-drift content over that Rust boundary. The real anti-drift artifact is therefore owed by the dispatch-translation slice (Staging §5): Rust dispatch and cascade must route through one shared translation function (the single-authority pattern of D10.1), and the rfl obligation is only discharged as a genuine guard once both call sites are wired to that single authority — until then it is the spec, not the proof of non-divergence. This is a named obligation on that slice, not a property this slice already secures.

D3 — Plane: end-mutability inheritance (RFD 0076, OE0267/OE0268)

Per-end mutability inheritance (RFD 0076: effective mutability is conjunctive over a relation and its transitive superrelations at each position) must be evaluated through the mapping, position by parent position.

The consequence: OE0268’s weakening check is “for each parent position mapped by a child end, the child end’s mutability refines the parent’s”; pinned positions are exempt from the check because they have no child-side mutability to compare. This is a strict generalization — under the identity mapping it is RFD 0076’s positional check verbatim.

Mechanized (slice 1, Argon.Substrate.RelationEndMutability): the per-position gate is mappedEndAccepts, exhaustive over MappingEntry. constant_pin_freeze_trivial proves the pinned-freeze witness — a constant-pinned position is accepted for every parent posture — and mappedEndAccepts_childEnd_eq_positional / mappedEndAccepts_cast_eq_positional prove a child-end/cast filler computes exactly the positional OE0268 term, so at the identity mapping the gate is RFD 0076’s check verbatim; allPins_accepted lifts the pin case to a whole all-pins mapping.

The RFD 0076 OE0267 declaration-trap (an immutable end whose dependent context is value-sorted can never be released) is evaluated on the child as declared; the mapping does not create a new immutable end, it routes existing ones.

D4 — Plane: cascade (retract/delete) and amend (RFD 0076)

The family extent is a union of images; image tuples are derived, not asserted. Therefore:

• Direction. A child tuple’s withdrawal maps to withdrawal of its image: cascade flows child → image, never image → child. Retracting WagesUSA(alice, 500) removes IncomeItem(alice, 500, USD) from the image contribution, exactly as retracting a derive premise removes the derived conclusion (RFD 0076 gate 4: “subsumed and derived extent deltas”).
• Two children onto one parent tuple. Because φ may be non-injective across edges (two different children may both map onto IncomeItem(alice, 500, USD)), the parent image tuple is live while any contributing child tuple is live. This is ordinary set-union support: the image tuple is a derived conclusion with multiple independent supports; it is withdrawn only when the last support is.
• Parent-side direct assertion vs. image overlap. A directly asserted parent tuple and an image tuple may coincide. They are distinct supports for the same proposition (one asserted, one derived-via-φ), resolved by the standard support-counting the runtime already applies to a tuple that is both asserted and independently derivable (RFD 0076 §“Rule-derived tuples cannot be amended”: “where an asserted tuple is also independently derivable, amendment withdraws the asserted contribution and the tuple remains live by derivation”). A delete/amend on the parent touches only the directly asserted support; the image contribution persists until its child is withdrawn.
• Amend. amend (RFD 0076 §5) names a directly-asserted tuple. An image tuple is derived, so it cannot be the target of amend — the RFD 0076 OE1406 (AmendmentTargetNotAsserted) refusal applies unchanged. Correct the record by amending the child premise; the image recomputes.

The end-mutability gates of RFD 0076 gate 4 already apply the freeze/retraction checks to “parent-relation rows contributed by a child.” This RFD makes explicit that the contributed row is φ(t), not t, and that the freeze witness for a pinned parent position is the constant (D3).

D5 — Plane: relation-value application dispatch (#1805/#1806)

This is the integration seam, and the payoff. The dispatch of #1805 expands a family query specializes(r, Family), r(args) into one strict clause per family member by positional substitution. For a mapped member the emitted clause applies the mapping — static mapping means static expansion; no runtime machinery.

For the WagesUSA <: IncomeItem(p = p, amount = amount, c = USD) edge, the family query

pub derive anyIncome(p: Person, a: Int, c: Currency) :-
    specializes(r, IncomeItem), r(p, a, c);

expands, for the explicit identity members, to the positional clauses of #1805, and for the mapped WagesUSA member to:

anyIncome(p, a, USD) :- WagesUSA(p, a);

The parent’s currency variable c is bound to the constant USD in the head; the child ends p, a are threaded positionally. A cast member emits the child end at the parent’s sort (no coercion node — the subsort relation guarantees admissibility). This is exactly the clause the hand-written derive rule would have carried, but generated from the subsumption edge, so WagesUSA is a specializes child and the family query reaches it. The witnessed user-facing spelling of this query — binding which member answered — is D6’s canonical trailing via (IncomeItem(p, a, c) via k), whose meaning is the generalized specializes(k(memberArgs), Parent(parentArgs)) atom, desugaring onto exactly this expansion.

The mapped_dispatch_selected_iff obligation (D2) fixes the value-level contract this relies on: reading the compiled dispatch helper at the WagesUSA selector is exactly applying WagesUSA through φ. It does not itself prove that the elaborator emits the clause above — the clause generator is the dispatch-translation slice’s work (Staging §5); the obligation is the correctness target that generator discharges.

D6 — Plane: the family-query surface (via canonical, generalized specializes its meaning)

The dispatch of D5 makes a mapped member reachable. The user-facing family query has one canonical surface spelling — the trailing via — and one meaning for it — the generalized specializes atom, which is via’s desugar target and its spec-level semantics. Both lower to the same D5 dispatch seam; via desugars to the generalized atom, which desugars to dispatch. No second evaluator, one lowering path.

Rule of thumb.

• Parent(args) — the plain parent atom — is the union: every family member’s tuple, merged, no witness.
• Parent(args) via k — the parent atom plus via k — is the union plus “which one”: the same tuples, each additionally bound to k, the member relation the tuple was declared in.
• specializes(k(memberArgs), Parent(parentArgs)) — the generalized atom — is via’s meaning written out: its desugar target and spec-level semantics, not a recommended alternative surface spelling.

Decision (2026-07-22) — presentation emphasis; semantics unchanged. Parent(args) via k is the canonical user spelling of a family query. The generalized specializes(k(memberArgs), Parent(parentArgs)) form is the meaning of via — its desugar target and the spec-level semantics — not a recommended alternative spelling. Rationale (load-bearing): D1 forbids dropped child ends, so the parent frame is information-complete — every value a member frame carries is available in the parent frame through the declared mapping (renames and reorders relocate values; pins add constants; nothing is lost). Therefore via plus the parent atom expresses every practical family-query rule, and a member-frame spelling binds nothing the parent atom does not already bind. The member frame becomes independently expressive only if mappings that drop child ends are ever admitted (Open questions §4, the projection-marker relaxation), at which point the generalized form — already fully specified below — is waiting. Until then, teach and write via; read the generalized atom as its definition.

The canonical surface — trailing via.

Parent( args ) via k

reads “every Parent-family tuple args, together with k, the member relation the tuple was declared in.” args is the parent’s argument list — the parent frame, where constant pins live; k binds to the declaring member, each row once. via writes only the parent frame, so a family query never names a relation bare: the arity is carried by Parent(args) at every site. The parent frame is information-complete (Decision above), so every practical family-query rule is a via rule.

via’s meaning — the generalized specializes atom. via desugars, at elaboration, exactly to:

Parent( args ) via k    ≡    specializes( k( _fresh₁ … _freshₘ ) , Parent( args ) )

— the member frame is a list of fresh wildcards (m = the selected member’s arity), so via elides the member frame entirely and writes only the parent frame, binding k to the declaring member. This desugar identity is the template; the example set below pairs each canonical via query with this generalized form written out beneath it, so the equivalence is visible at every example.

The generalized atom specializes(k(memberArgs), Parent(parentArgs)) names both frames explicitly and does three jobs:

• bounds k to Parent’s family — k ranges over the family’s members (reflexively including Parent itself);
• applies k in its own frame — memberArgs is k’s declared argument list (the member’s own shape);
• constrains the image in the parent frame — parentArgs is Parent’s argument list, constant pins included.

Both argument lists are required in the generalized form; wildcards _ are allowed in either frame (and via’s member frame is all-wildcard by construction). The image constraint is what makes pins load-bearing: IncomeItem(a, b, USD) via k (desugaring to specializes(k(_fresh…), IncomeItem(a, b, USD))) selects every family member — of any arity — whose declared mapping can produce USD at the currency position and statically prunes the rest (a member pinning EUR there can never match, so it is dropped from the expansion at elaboration — the D5 static-expansion property, now driving query-side member elimination).

Requiring arguments at every family-query site resolves the bare-relation-reference problem: the bare two-argument form specializes(k, Parent) — a relation standing as a value with no arguments — is deprecated then refused, on the same explicit-only migration pattern as the bare <: (D1 gate (h), Migration): it parses during the check-plane slice, is refused when the enforcing slice lands, no separate lint stage. Relation literals in value position (k != Wages, a relation-valued endpoint) are the residue that argument-carrying forms do not reach and remain the sole bare sites (Open questions §7).

The φ-not-position rule — stated loudly (it governs the meaning via hides). The correspondence between memberArgs and parentArgs in the generalized form is the member’s declared mapping φ_k, never visual position. A variable shared between the two lists flows its value through φ_k — the member’s declared filler map (D1) — not by lining up columns left-to-right. This is the single documented frame convention; it replaces every scattered “column i here means column i there” reading. Writing via means you never touch the member frame, so this trap cannot arise at a via site; it is stated here because the generalized atom — via’s meaning — is where it lives, and where a hand-written member-frame query would meet it.

Query atoms are positional; the declaration is where names key. The name-keyed filler list of D1 is a property of the <: declaration — the one site where a parent-end reorder must not silently re-pair the mapping. A family-query atom (k(memberArgs), Parent(parentArgs)) is an ordinary atom and its argument lists are positional, exactly like every other atom in a rule body; they are not keyed by end name. That is not an inconsistency: an atom’s positions are read in one relation’s own frame, where position is unambiguous, whereas the <: filler list bridges two frames and must survive a reorder of either — which only name-keying delivers. So the declaration carries parentEnd = childEnd fillers, and a query carries positional Parent(v₁ … vₖ); φ_k (fixed once at the declaration by name) is what bridges the generalized form’s two positional lists (the φ-not-position rule above).

Worked example — a mapping that reorders ends:

pub rel Edge(src: Node, dst: Node, w: Int);
// declared mapping REVERSES the endpoints:
//   parent src ← child `to`,  parent dst ← child `from`
pub rel BackEdge(from: Node, to: Node, w: Int) <: Edge(src = to, dst = from, w = w);

BackEdge’s φ sends the member tuple (from, to, w) to the parent tuple (to, from, w). To read every back-edge’s parent image with its witness, write the parent frame — Edge(s, d, w) via k — binding (s, d, w) to the image (to, from, w); φ does the reordering, the surface never mentions it. The trap via spares you lives in the generalized meaning: specializes(k(x, y, z), Edge(x, y, z)) at k = BackEdge looks like a pass-through, but the member frame binds x = from, y = to, z = w while the parent frame constrains the image Edge(to, from, w) = Edge(y, x, z), so Edge(x, y, z) demands x = y and the atom silently collapses to the diagonal (only self-loops match). Because via writes only the parent frame, the reader never lines two frames up positionally and the collapse cannot happen — the reason via is the canonical surface.

Semantics. specializes(k(u…), Parent(v…)) — via’s meaning — holds iff:

1. k is in Parent’s family — reflexive: k may be Parent;
2. k(u…) holds in k’s own extent — the own-extent rule: the tuple’s declaring relation, each row once, reading the pre-closure extent (carried over from the own-extent decision, so no reflexivity × closure duplicate; see the naive idiom below);
3. φ_k(u…) unifies with (v…) — the member image, routed through the declared mapping, equals the parent-frame arguments.

For k = Parent the reflexive arm reads the parent’s own-tuples view — the tuples declared directly on Parent, excluding the RFD 0005 closure images copied up from members — under the identity φ. Constant pins in the parent frame prune members statically (above): where φ_k’s image is incompatible with a pin, the member contributes nothing and is dropped before any row is read.

The naive idiom this fixes. The obvious hand-rolled provenance query is the bare specializes(k, IncomeItem), k(p, a, c) — the now-deprecated bare two-argument specializes followed by a member-framed application — and it is wrong twice, which is why via (and the own-extent semantics behind it) exist:

1. Over-returns — the reflexivity × closure duplicate. $specializes is reflexive (compiler/crates/oxc-reasoning/src/compile/rule.rs, the reflexive-transitive <: closure; compiler/crates/oxc-runtime/src/standpoint.rs documents $specializes as reflexive-transitive), so k ranges over {WagesUSA, InterestUSD, IncomeItem}. But the RFD 0005 closure (compiler/crates/oxc-runtime/src/standpoint.rs: a member tuple is added to its own extent and copied into each ancestor’s extent) has already placed the image into IncomeItem’s extent, so each family row returns twice — once under its member (own extent), once under the reflexive parent (closure copy). Reading own extents (rule 2) returns each row once.
2. Buries the frame convention. k(p, a, c) applies every k at the parent’s three-place frame, but WagesUSA is two-place; which frame a bare application speaks is left implicit. via writes only the parent frame and lets φ bridge, so no frame is left implicit (the φ-not-position rule).

Maintainability — one lowering path. via never has independent semantics: it desugars to the generalized atom, which lowers onto the D5 dispatch. There is nothing for via to drift from — it is the general form with fresh wildcards. The one new named construct behind either spelling is the parent’s own-tuples view (the pre-closure parent extent) for the reflexive k = Parent arm; every other arm is an existing D5 member arm with the selector surfaced as the k binding. A via (or its generalized desugar) query and the equivalent hand-written per-member derive compile to the identical circuit (D9).

via collision check (why via, not from/[k]). via was chosen because it is the sole spelling collision-free in rule-body position:

Example set — each example a pair: the canonical via spelling first, its generalized specializes meaning desugared directly beneath.

The two spellings in each pair produce identical rows by construction — via desugars to the generalized atom, and both lower along one path onto the D5 dispatch, so there is nothing for via to drift from (see Maintainability — one lowering path above). Read the second line of each pair as the definition of the first, not as an alternative surface to write. _fresh… is the fresh, all-wildcard member frame via elides (m = the selected member’s arity; the desugar identity above).

pub rel IncomeItem(p: Person, amount: Int, c: Currency);
pub rel ForeignIncome(p: Person, amount: Int, c: Currency) <: IncomeItem(p = p, amount = amount, c = c);
pub rel WagesUSA(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

// (1) IDENTITY family.
IncomeItem(p, a, c) via k                          // canonical
specializes( k(_fresh…) , IncomeItem(p, a, c) )    // the same query, desugared
// Meaning: every IncomeItem-family tuple (p, a, c), with k bound to the member relation that declared it.

// (2) PIN SELECTION — only USD-producing members.
IncomeItem(p, a, USD) via k                         // canonical
specializes( k(_fresh…) , IncomeItem(p, a, USD) )   // the same query, desugared
// Meaning: family tuples whose parent-frame currency is USD, with witness; members pinning another currency are pruned statically.

// (3) REORDERING — φ handled by the declared mapping, not the surface.
Edge(s, d, w) via k                                 // canonical
specializes( k(_fresh…) , Edge(s, d, w) )           // the same query, desugared
// Meaning: every family edge read in the parent frame (s, d, w) = the image (to, from, w), with witness; φ does the reversal, the surface never names it.

// (4) WILDCARD parent frame — the parent frame may carry `_`.
IncomeItem(_, a, USD) via k                         // canonical
specializes( k(_fresh…) , IncomeItem(_, a, USD) )   // the same query, desugared
// Meaning: amount only, USD image, with the declaring member as witness.

pub rel Engagement(firm: Firm, client: Client);
pub rel AuditEngagement(firm: Firm, client: Client)      <: Engagement(firm = firm, client = client);
pub rel ConsultingEngagement(firm: Firm, client: Client) <: Engagement(firm = firm, client = client);

// (5) MULTI-WITNESS — two witnesses on one client, compared. Auditor independence.
// NOTE — the two derive rules in each pair below are ALTERNATIVE SPELLINGS of
// one query, shown together for comparison; in a real program write one of them
// (two co-resident rules with the same head would union — both would fire).
pub derive independenceViolation(firm: Firm, client: Client) :-  // canonical
    Engagement(firm, client) via k1,
    Engagement(firm, client) via k2,
    k1 != k2;
pub derive independenceViolation(firm: Firm, client: Client) :-  // the same query, desugared
    specializes( k1(_fresh…) , Engagement(firm, client) ),
    specializes( k2(_fresh…) , Engagement(firm, client) ),
    k1 != k2;
// Meaning: a firm may not both audit and consult for one client. The witnesses must be DISTINCT members.
// The parent query alone cannot express it: the union self-joined on (firm, client) is satisfied by two
// engagements of the SAME kind — only the witness distinguishes which member each row was declared in.
// Reflexivity caveat (semantics 1): k1/k2 range reflexively, so k = Engagement — the parent's own-tuples
// view (own-extent rule; "For k = Parent …" above) — is itself a witness. This example assumes Engagement
// carries NO bare own-tuples (every engagement is declared in a member), so k1 != k2 means two proper
// members. Where the parent does carry own-tuples, a bare Engagement + one member would satisfy k1 != k2
// and over-return; guard k1/k2 to proper members there.

// (6) WITNESS-AS-JOIN — the witness is an ordinary join key, shared across atoms.
pub derive sameCategory(p1: Person, p2: Person, kind: Relation) :-      // canonical
    IncomeItem(p1, _, _) via kind,
    IncomeItem(p2, _, _) via kind,
    p1 != p2;
pub derive sameCategory(p1: Person, p2: Person, kind: Relation) :-      // the same query, desugared
    specializes( kind(_fresh…) , IncomeItem(p1, _, _) ),
    specializes( kind(_fresh…) , IncomeItem(p2, _, _) ),
    p1 != p2;
// Meaning: two distinct people whose income was declared in the SAME family member `kind` — the witness
// bound once and reused as a join key across both atoms.

Every pair names the parent relation with its full argument list on both lines, so no relation ever stands bare (the overloading-proof property; Open questions §7).

Interactions.

• Negation. not (Parent(args) via k, …) is an ordinary safe-negation body; the atom obeys the usual bound-variable / range-restriction rules, and k is a body variable like any other.
• Aggregates. The witness is a first-class grouping key: count{ a } group by k over IncomeItem(p, a, c) via k counts per declaring member — per-member aggregation without naming each member.
• Multiple atoms. Two witnessed atoms compare their witnesses: IncomeItem(p, a, c) via k1, IncomeItem(p, b, d) via k2, k1 != k2 finds a person with income from two distinct family members. Ordinary term comparison on the bound relation-identity values.

specializes repositioned. The generalized specializes atom is the spec-level meaning of via and the uniform reflection instrument over both tiers (concepts and relations); it is the same reflection atom (D7), argument-carrying in both slots. via is the canonical user surface over it. Because a family-query site names the parent relation literally, the family is statically known and the OE1386-family refusals that guard reflective relation-application over an unknown or ill-typed dynamic selector are unreachable here — there is no dynamic selector to reject.

Staging. Slice D delivers via (and its generalized desugar) over IDENTITY families — implementable on the merged relation-value application immediately, since identity members need only the existing dispatch and the parent own-tuples view. The pin / mapped cases (examples 2–4 above) activate when the wire, check-plane, and dispatch-translation slices land (Staging §3–§5), because they require the per-edge mapping to be stored, checked, and lowered through φ. Slice D is otherwise the canonical via surface desugaring onto the dispatch seam and adds no evaluator; see Staging §6.

D7 — Plane: reflection ($specializes, the relation tier)

$specializes and the relation reflection tier must carry the mapping — the edge is no longer fully described by (sub_id, super_id). Add per-edge mapping metadata: for each parent position, a tagged filler (child-end index / cast / constant literal). The wire encoding is additive and optional-on-decode: a legacy decoder that does not know the mapping field reads an edge as the identity mapping (which is correct for every bare edge, the only kind a legacy producer emits), consistent with the house discipline for reflection additions (RFD 0076 §4 reflection; the armMutability additive precedent). A reflective reader that does understand mappings can enumerate the fillers; a $specializes consumer that only needs membership sees the edge unchanged.

Because a post-RFD producer can emit a genuinely non-identity edge that a legacy decoder would silently misread as identity, the mapping field rides the same artifact core-IR posture as RFD 0076’s per-end is_mut: additive within a version whose stamp lets a stricter deployment distinguish artifacts that use mapped edges. (See Migration for the exact bump discipline.)

D8 — Plane: coverage / OE1404 and resurrection guards

Any plane that consumes subsumption to compute a closure — coverage checks, the RFD 0076 OE1404 cascade-coverage gate, resurrection guards — consumes the image φ(ext(child)), not the child extent. Concretely:

• The RFD 0076 cascade coverage gate (OE1404, “an immutable end of an incident tuple is not explained by the retraction set”) walks incident tuples of the parent including image tuples; for an image tuple the “dependent context” is the image’s, and the freeze witness for a pinned position is the constant (D3), which is never a retractable individual, so a pinned position never demands coverage. A child-end position demands coverage of the child’s individual, mapped through φ.
• Resurrection / no-reuse guards (RFD 0076 §“erasure channel”) read the image’s frozen fibers; a pinned fiber has a constant witness that no identity resurrection can launder, closing that residue trivially for pinned positions.

D9 — Plane: incremental circuits (RFD 0018 / RFD 0021 lineage / RFD 0018 IVM)

A mapped member compiles to standard incremental operators: a rename is a column permutation (a projection with reordering), a constant pin is a constant-fill (map) node, a cast is a no-op tag-widening. The image φ(ext(child)) is therefore a project ∘ map node over the child relation, feeding the parent’s union — all monotone, standard DBSP operators (RFD 0018). No new operator kind is introduced; a mapped edge is incrementally maintained by the same machinery as a hand-written projecting derive rule, which is what it compiles to (D5).

D10 — Maintainability by construction

Maintainability is a design axis of this RFD, not an afterthought: the goal is that mapping-related drift is impossible to introduce, not merely unlikely to survive review. Most of these commitments are compile-enforced (one structure, one code path, exhaustive wildcard-free matches, loud refusals); the equality obligation (#5) is the exception — in slice 1 it is a definitional specification, and becomes a real guard only once the dispatch slice routes both directions through one shared translation function (see #5). Six commitments, each a decision the slices implement:

1. One canonical mapping representation, one owner. The parsed <: Parent(f₁ = m₁, …, fₖ = mₖ) clause elaborates, once, to a single resolved-mapping structure — each parent-end name fⱼ resolved to its parent position, and a MappingEntry stored per parent position (so name-keying is a resolution-time concern; the stored structure is position-indexed). Every consumer (end-mutability inheritance D3, cascade/amend translation D4, dispatch expansion D5, reflection metadata D7, coverage D8, incremental lowering D9) reads that one structure. No plane re-derives the mapping from surface syntax. This follows the callable-catalog / freeze-role precedent (single resolution authority, all other views downstream): there is exactly one place the mapping is computed and exactly one shape it is stored in.

2. One surface form ⇒ one code path. There is a single surface form (explicit mapped), so there is only ever a resolved mapping to consume — no “unmapped subsumption” branch anywhere downstream. Every consumer handles exactly one case (a resolved mapping); identity is just a mapping whose every entry is the positional ChildEnd, and it exists only as the internal image of a migrated bare site, never as a second surface path to keep in sync. Where the previous design achieved one code path by desugaring a second surface spelling, this design achieves it more strongly by having no second surface spelling. The mappedChecks_identity_eq_bareChecks corollary (D2) is the internal bridge that licensed deleting the old bare check path: it proves the identity mapping run through the general checker computes exactly the old positional Booleans, so removing the bare path changes no verdict (it is the migration-soundness witness of D2/Migration, not a sugar-drift guard, since no sugar remains).

3. Exhaustive, wildcard-free matches over MappingEntry. The entry enum is ChildEnd { index } | Constant { literal } | Cast { index, to_sort }. Every consumer matches it exhaustively, with no wildcard arm. Adding a fourth mapping form (e.g. the D1c projection relaxation) then fails compilation at every site that must handle it — the compiler enumerates the work, not a reviewer.

4. Refusals over silent adaptation. Any shape the mapping rules (D1) do not cover refuses at the declaration with a catalogued diagnostic — never inferred, never defaulted, never silently adapted. On the wire the mapping field follows the house three-state discipline: present-and-understood, present-and-too-new (refuse loudly — D7/Migration), or absent = the explicit legacy identity state (an old artifact emits only bare edges, so absence is identity, decidably). Absence is a defined state, not a guess.

5. Single-authority translation obligation. The dispatch translation (D5) and the cascade translation (D4) are the same φ applied per delta sign, recorded as the dispatch_cascade_same_map obligation (D2). In slice 1 this obligation is definitional (holds by rfl because both directions are the one image function) — it is the specification of the intended design, not yet a drift guard. The guard is owed by the dispatch-translation slice (Staging §5), which must route Rust dispatch and cascade through one shared translation function (D10.1) so the two directions cannot be independently hand-maintained; only then does the rfl become an anti-drift proof rather than a statement of intent (see D2, “What this obligation is, honestly”).

6. Per-plane drift-impossibility. Each plane interaction names what makes drift impossible rather than unlikely:

   Plane	What makes drift impossible
   End-mutability (D3)	Inheritance reads the resolved mapping’s entries; a pinned position has no mut field to compare, so the OE0268 check is total over entry kinds (exhaustive match) — a new entry kind cannot silently skip the weakening check.
   Cascade/amend (D4)	Uses the same φ as dispatch (obligation D2#dispatch_cascade_same_map); there is no separate withdrawal-mapping to keep in sync. Slice-1 status: the obligation is definitional (rfl) — the spec of that intent; the drift guard is realized when the dispatch slice routes both Rust call sites through one shared translation function (Staging §5).
   Dispatch (D5)	The emitted clause is generated from the resolved mapping, not re-parsed from the <: clause; the generator is the sole producer, mapped_dispatch_selected_iff its correctness pin.
   Reflection (D7)	The reflected fillers are a projection of the same resolved mapping; a legacy-decode path is the one defined absence state, not an inferred fallback.
   Coverage / OE1404 (D8)	Coverage walks image tuples produced by the same φ; a pinned position’s constant witness is derived from the Constant entry, so coverage cannot disagree with dispatch about what a pinned fiber contains.
   Incremental (D9)	The circuit nodes are compiled from the resolved mapping (rename→permute, Constant→map, Cast→widen); no operator kind is bespoke, so IVM maintenance cannot drift from the batch image.

The through-line: one mapping structure, one code path, exhaustive matches, and loud refusals make most desynchronizing edits fail to compile. The equality obligation is the weaker link — definitional in slice 1, a genuine guard only after the dispatch slice funnels both directions through one shared translation function (#5) — so it is named as an obligation on that slice rather than claimed here. The aim is that a future edit that would desynchronize two planes fails to compile (or, for the equality axis, fails the obligation once the single-authority wiring lands), rather than passing silently and being caught (or not) by review.

Worked examples

Syntax note: the mapped <: form is carried by this design record; parser, elaborator, and dispatch support land with the slices in Staging, so these blocks are illustrative here and gate-verified once those slices are in.

1 — WagesUSA, end to end

pub type Person;
pub type Currency;
pub const USD: Currency;

// The general family relation — carries a currency.
pub rel IncomeItem(p: Person, amount: Int, c: Currency);

// A specific member that is always in dollars, so it carries no currency end.
pub rel WagesUSA(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount, c = USD);

// An explicit identity member for contrast — same shape as the parent.
pub rel ForeignIncome(p: Person, amount: Int, c: Currency) <:
    IncomeItem(p = p, amount = amount, c = c);

// A family query over everything that is an IncomeItem.
pub derive anyIncome(p: Person, a: Int, c: Currency) :-
    specializes(r, IncomeItem), r(p, a, c);

Dispatch (D5) generates, per family member:

// identity member — positional, exactly RFD 0005 / #1805
anyIncome(p, a, c) :- ForeignIncome(p, a, c);
// mapped member — the currency end is pinned to the constant in the head
anyIncome(p, a, USD) :- WagesUSA(p, a);

Given facts:

insert WagesUSA(alice, 500);
insert ForeignIncome(bob, 300, EUR);

Results table for anyIncome:

WagesUSA is a genuine specializes(_, IncomeItem) child, so the family query reaches it — the omission the hand-written derive rule caused (this RFD’s motivation) does not occur.

2 — Sort cast (friend as Person)

pub type Person;
pub type Friend <: Person;        // a Friend is a kind of Person

pub rel Knows(a: Person, b: Person);
// Friendship holds between two Friends but participates in the general Knows
// family; the child ends are cast up to the parent's Person sort.
pub rel Friendship(a: Friend, b: Friend) <: Knows(a = a as Person, b = b as Person);

Every Friendship(x, y) contributes Knows(x, y) with x, y admitted at Person. The cast is checked by covariance (childSort <: parentSort, D1d — Friend <: Person), needs no runtime coercion, and compiles to a tag-widening no-op in the incremental circuit (D9).

3 — An audit rule over the mapped family

// A static check over the whole IncomeItem family — reaches mapped members
// because they are real subsumption children.
#[static]
pub check IncomeItemNeedsCurrency(r: TypeRef) :-
    specializes(r, IncomeItem),
    not rel_end(r, 3, _)            // a member missing the currency end...
    => Diagnostic {
        severity: Severity::Warning,
        code: "Example::W_UncurrenciedIncome",
        message: "An IncomeItem family member declares no currency end; \
                  confirm its subsumption clause pins one.",
    };

WagesUSA satisfies the audit precisely because it does pin the currency (c = USD); a would-be member that neither carried nor pinned a currency would be flagged. The audit sees mapped members only because the mapped form keeps them in the family — a hand-written derive rule would make them invisible to this check.

4 — Refusal gallery (one per new gate, notional codes)

pub rel IncomeItem(p: Person, amount: Int, c: Currency);

// D1b — the parent `c` end is left uncovered (no filler names it).
pub rel Bad1(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount);
//                                     refused MappedSubsumptionParentEndCoverage (notional)

// D1a — `qty` names no declared parent end of IncomeItem (p, amount, c).
pub rel Bad1b(p: Person, qty: Int) <: IncomeItem(p = p, qty = qty, c = USD);
//                                    refused MappedSubsumptionUnknownParentEnd (notional)

// D1b — the parent `amount` end is named twice (double cover).
pub rel Bad1c(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount, amount = amount);
//                                    refused MappedSubsumptionParentEndCoverage (notional)

// D1c — child end `note` is referenced by no filler (dropped child end).
pub rel Bad2(p: Person, amount: Int, note: Text) <: IncomeItem(p = p, amount = amount, c = USD);
//                                    refused MappedSubsumptionUnmappedChildEnd (notional)

// D1d — child end sort does not widen to the parent position sort.
pub rel Bad3(p: Person, amount: Text) <: IncomeItem(p = p, amount = amount, c = USD);
//                                        refused MappedSubsumptionEndpointVariance (generalizes OE0151)

// D1e — the pinned literal has the wrong sort for the parent position.
pub rel Bad4(p: Person, amount: Int) <: IncomeItem(p = p, amount = amount, c = 42);
//                                     refused MappedSubsumptionPinSort (notional)

// D3 / OE0268 — the child weakens an immutable parent position it maps onto.
pub rel Locked(mut a: Person, b: Person);
pub rel Loosened(mut a: Person, mut b: Person) <: Locked(a = a, b = b);
//                              ^^^^^ refused OE0268 — child may not weaken an
//                                    immutable parent position through the mapping.

Alternatives considered

Migration

Source migration is required and mechanical. Removing the bare form is a breaking source change, taken deliberately (Alternatives (c)). It is bounded and one-time:

• In-repo bare sites (reference-book examples, the conformance corpus, fixtures) are migrated in the same slice that turns on the refusal (Staging §4a). The rewrite is mechanical: a bare child <: parent becomes child <: parent(f₁ = e₁, …, fₙ = eₙ) where f₁ … fₙ are the parent’s declared end names and e₁ … eₙ are the child’s own end names, paired position-for-position in declaration order — the identity mapping, read directly off the two declarations (both name lists are in scope at the migration site). The rewrite presupposes equal arity n on both sides (fⱼ = eⱼ for j = 1 … n); that precondition is inherited unchanged from the bare form it replaces, whose positional pairing already requires child arity to equal parent arity (a mismatch is the pre-existing arity refusal, not a migration case). The specializes-keyword spelling of a bare clause (child specializes parent) migrates the same way, to child specializes parent(f₁ = e₁, …, fₙ = eₙ) (D1, gate (h) is glyph-agnostic). mappedChecks_identity_eq_bareChecks (D2) proves this rewrite preserves every accept/refuse verdict, so it is a semantics-preserving textual transform, not a re-authoring.
• External ontology-library corpus. An ox-migrate rewrite performs the same identity-argument-list expansion for the out-of-repo ontology corpus; that corpus’s migration is already queued for its next toolchain upgrade. Because the language is pre-1.0 there is no other external consumer of the bare form.
• Deprecation lint considered and rejected. A warn-only stage that kept the bare spelling compiling during a window was weighed and rejected: with no dependents there is nothing a window protects, and it would only prolong the two-spelling regime the removal exists to end. The refusal lands directly, with the in-repo migration in the same change.

Wire/reflection is still additive within the toolchain. The reflection/wire mapping field (D7) carries the resolved mapping. Because every surface edge is now mapped, a producer always emits an explicit mapping; the identity mapping is emitted for migrated bare sites exactly as for any other. A legacy decoder that predates the field reads an edge as the identity mapping — correct only for the identity edges a legacy producer could emit; a post-change producer emitting a genuine non-identity edge rides a core-IR version stamp under the same discipline as RFD 0076’s per-end is_mut, so a decoder too old to understand a non-identity mapping refuses loudly rather than silently misreading it as identity (the RFD 0076 major-bump rationale applies whenever a non-identity edge is present).

Open questions

1. Can a child map to multiple parents? A relation may today have multiple <: edges. With mappings, each edge carries its own φ; the child’s extent contributes an image to each parent independently. Nothing in the semantics forbids it, but the interaction of different mappings to different parents with the RFD 0076 conjunctive mutability inheritance (a child end mapped to an immutable position in one parent and a mut position in another) needs an explicit rule. Provisional stance: the child end’s effective mutability is conjunctive over every parent position it maps onto across all edges; confirm at mechanization.

2. Constant pins under bitemporal amendment of the constant’s meaning. A pin USD is a compile-time constant reference. If the referent of USD (say a Currency individual) is itself subject to bitemporal correction/amendment (RFD 0076 §5), does the pinned fiber’s freeze witness track the correction? The pin is a value, not an independent assertion, so provisionally the image tuple simply reflects whatever USD denotes; but whether a pin may reference a mutable individual at all, versus only a const, is open.

3. Do the bare positional checks (OE0150–OE0154 / arityEqual + positional covariance) survive as a runtime path? Answered: no — subsumed. With the bare surface form removed, there is no declaration that reaches a positional-only checker, so checkSubsumption/arityEqual/endpointsCovariant are not retained as a live elaborator code path. Every edge is elaborated to a resolved mapping and run through checkMappedSubsumption, and the meanings of OE0150–OE0154 are subsumed by the general gates: arity (OE0150) → arityMapsParent; endpoint covariance (OE0151) → covariantFillers; cardinality (OE0152) and metarel (OE0153) are threaded through the mapping unchanged; acyclicity (OE0154) is reused verbatim. The bare Lean predicates remain only as the target of mappedChecks_identity_eq_bareChecks — they are the specification the identity mapping is proved to compute, i.e. the migration-soundness witness, not an executed check. Any performance question is therefore about the single general checker; there is no second path to benchmark against.

4. Relaxing D1c (dropped child ends) with an explicit projection marker. This RFD forbids dropping a child end. A future relaxation could admit child(a, b, drop c) <: parent(x = a, y = b) with a marked projection (drop naming the child end that maps to no parent end), defining the collapse semantics (image is the projection; two child tuples differing only at c coincide in the parent). Deferred — it needs its own coverage/cascade story because the collapse loses the child identity the cascade direction (D4) relies on.

5. Diagonal mappings and cardinality. A child end referenced at two parent ends (parent(f₁ = e, f₂ = e)) — does the parent’s per-position cardinality interact soundly, or should a diagonal be refused pending a worked cardinality rule? Provisionally admitted (D1); flagged for the check-plane slice.

6. Must the identity mapping be written out even when trivial — and may a same-name filler abbreviate? Answered: written out in full; no abbreviation. A shape-identical child must still write the full filler list keyed by the parent’s end names (Home(p, c) <: Loc(p = p, c = c)), and a filler whose child end shares its parent end’s name is still written p = p, never a bare p. Two abbreviations were weighed and rejected: (i) omitting the list entirely for the identity case (that is the bare form, Alternatives (c)); and (ii) admitting a bare token p as sugar for p = p (that is the positional filler form, Alternatives (d) — the very spelling whose silent re-pair under a parent-end reorder motivated parent-name keying; a bare token has no parent-end key and so re-pairs positionally). Either would reintroduce a second surface spelling this RFD removes. Recorded plainly so no later “convenience” change re-adds an implicit identity form or a bare-token filler: the identity mapping is an internal representation only, and every surface filler carries its parentEnd = key.

7. Arity overloading would be blocked by bare relation references — a forward constraint, mostly settled by D6. If relation-name overloading (Loc(a, b) and Loc(a, b, c) as one name) is ever wanted, arguments disambiguate the overload at almost every site: an ordinary atom carries its arity, a mapped <: edge carries it in the filler list, and the family-query form (D6) carries it in both the member frame k(memberArgs) and the parent frame Parent(parentArgs). The bare specializes(k, Loc) two-argument form — a relation standing as a value with no arguments — was the dominant remaining bare site; that is now decided. D6 makes the argument-carrying family-query surface canonical — the trailing via (Parent(args) via k), whose parent atom carries its arity, with the generalized specializes(k(memberArgs), Parent(parentArgs)) (both argument lists required) as its meaning — and the bare two-argument specializes(k, Parent) is deprecated then refused on the same explicit-only migration pattern as the bare <: (D1 gate (h), Migration). The previously-provisional answer here — “a future overloading design would need an argument-carrying specializes form” — is therefore no longer provisional for specializes: the argument-carrying forms are the surface, and the bare form is removed on the same schedule. The residue is relation literals in value position (k != Wages, a relation-valued endpoint): these still stand bare and are the sole sites a future overloading design must settle with an arity-qualified literal spelling. Any surface that renders relation values (diagnostics, provenance columns, reflection output) would need arity-qualified display from day one. Recorded so the constraint is weighed before the D6 slice ships its rendering, and so overloading is not attempted without settling the remaining relation-literal sites first.

8. Divergent-map subsumption diamonds. Answered: refused until motivated. A relation may reach the same ancestor through more than one chain of subsumption edges. When every chain composes to the same mapping onto that ancestor, the diamond is harmless — a child fact frames to one ancestor row no matter which path is read — and stays legal. When two chains compose to different mappings, there is no single answering frame. Worked example: an ancestor A(x, y) with two intermediates that swap the ends,

   rel A(x: Person, y: Person)
   rel Left(a: Person, b: Person)  <: A(x = a, y = b)   // straight
   rel Right(a: Person, b: Person) <: A(x = b, y = a)   // swapped
   rel D(p: Person, q: Person) <: Left(a = p, b = q), Right(a = p, b = q)
   

   D(alice, bob) composes to A(x = alice, y = bob) via Left and to A(x = bob, y = alice) via Right: it would occupy two different rows in A, and a family query over A follows the first path in the subsumption-image closure — so it silently reports one framing and drops the other. Silent under-report is the worst failure shape, so the divergent diamond is refused at declaration (OE1424, in the declaration pass over the resolved per-edge mappings); the message names the child, the ancestor, and both paths with their composed mappings in parent-name-keyed filler form. This makes the closure’s first-path selection exact by construction (every diamond that reaches evaluation agrees on every path). Both-images support — the child genuinely occupying both ancestor rows, one per divergent path — is a deliberate future relaxation: it needs a provenance model for one-row-per-path and a cardinality story, so it is deferred rather than guessed. A modeler who wants it files a feature request; until then, reconcile the fillers so the compositions agree, or remove one edge.

Staging

Mirrors the callable A/B/C slice pattern (#1805/#1806) and builds directly on #1805’s dispatch seam:

1. RFD accepted — this record; the explicit-only surface policy, the identity mapping as internal-representation-and-migration-bridge, and the plane-interaction decisions are fixed.
2. Lean mechanization — Argon.Substrate.RelationSubsumption gains the mapping data, arityMapsParent, covariantFillers, and the mappedChecks_identity_eq_bareChecks corollary (the migration-soundness witness); Argon.Reasoning.Datalog.RelationApplication gains mapped_containment and the restated mapped_dispatch_selected_iff.
3. Wire / metadata slice — the per-edge mapping field on the subsumption edge, additive and optional-on-decode (D7), with the core-IR version discipline (Migration).
4. Check-plane slice — parser + elaborator: the filler grammar (D1), the new refusals (D1a–e notional codes), and the through-mapping cardinality/metarel checks (D2). Reflection tier exposes the fillers. The mapped form is accepted here, but the bare form still parses (as the identity mapping) so this slice is non-breaking on its own.
   1. Bare-form removal + in-repo migration slice (its own slice) — turns on the D1 gate (h) refusal for the bare form and, in the same change, migrates every in-repo bare site (reference-book examples, conformance corpus, fixtures) to the explicit identity form by reading each child’s own end names off its declaration. Kept a distinct slice because it is the only breaking step and pairs the refusal with the migration atomically; the external ontology-library ox-migrate rewrite is prepared here and applied at that corpus’s next toolchain upgrade (Migration). No deprecation lint — the refusal is direct.
5. Dispatch-translation slice — the mapped-clause generator (D5) over #1805’s expansion, and the incremental-circuit lowering (D9). This is the slice that delivers the motivating payoff: mapped members become live specializes children.
6. Family-query surface slice (callable-port slice D) — the generalized specializes(k(memberArgs), Parent(parentArgs)) grammar (both argument lists required), the canonical via surface (Parent(args) via k ≡ specializes(k(_fresh…), Parent(args))), the parent’s own-tuples view for the reflexive k = Parent arm, and the deprecate-then-refuse schedule for the bare two-argument specializes(k, Parent) (D6). This slice splits by mapping kind:
   • IDENTITY families now — the generalized atom and via over identity members need only the merged relation-value application (#1805 dispatch) plus the own-tuples view, so they are implementable immediately on the merged work; both frames coincide under the identity φ.
   • Pin / mapped cases later — pin selection, image constraints, and reordering mappings (D6 examples 2–4) require the per-edge mapping to be stored (§3 wire), checked (§4 check-plane), and lowered through φ (§5 dispatch-translation), so they activate only once those slices land. The surface is otherwise the canonical via spelling desugaring onto the dispatch seam and adds no evaluator. Depends on #1805 (member arms) and #1806 (the selector gates it renders unreachable at family-query sites).

References

• RFD 0005, Relation subsumption — the bare positional form this RFD generalizes; its elaborator checks (OE0150–OE0154) become the identity-mapping instance.
• RFD 0076, Mutability of relation ends — the end-mutability inheritance (OE0267/OE0268), the retract/amend cascade, the additive-reflection and core-IR-version discipline this RFD reuses.
• #1805, Relation-value application — finite-domain dispatch over first-class relation values — the dispatch seam mapped members plug into; the module Argon.Reasoning.Datalog.RelationApplication and its structural_containment / dispatch_selected_iff obligations.
• #1806, Relation-value application check-plane gates — the gate galleries the mapped-subsumption refusals extend.
• RFD 0018, Production reasoner: the incremental DBSP engine — the incremental operators a mapped member compiles to (project / map / union), D9.
• Argon.Substrate.RelationSubsumption (spec/lean/Argon/Substrate/RelationSubsumption.lean) — the elaborator-check predicates generalized here.