RFD 0027 — The meta-property plane: axis bindings, catalog tiers, value-position resolution, and substrate-neutral modifiers

• State: committed — implemented end-to-end (S0 #276, S1+S2 #283, S3 #287, S4 = this arc’s final PR; bugs #242/#243/#229 closed)
• Opened: 2026-06-11
• Decides: how metaxis declarations and metatype axis bindings become real — validated at elaboration, persisted on the wire, materialized as catalog relations, and queryable in rule bodies (meta(t).rigidity == rigidity::anti_rigid); one unified name-resolution pass for value positions in rule bodies (axis values, enum constants, individuals, qualified names — closing a family of silent mis-evaluations); metatype-tier $meta/$iof rows (settles #229); a Value::Symbol carrier shared with enum constants (fixing enum type-erasure); and the substrate-neutral modifiers abstract and fixed that replace every compiler read of user axis vocabulary (the OE1327 "sortality"/"sortal" magic strings, the §7.5 dynamic-iof gate, §10.2 static-discharge rigidity, RP-004 VT-persistence defaults). Settles audit findings ufo-01/ufo-02/ufo-03/ufo-04 and issue #148’s constants half; motivated by the first external user collision (Tiago’s ArgUFO overlay, 2026-06-11). PR #209 parked citing a planned “RFD 0027 ambient-vocabulary cleanup” that was never written; this RFD takes the number and completes that program.

Prior state (verified at aa7a7d0e): metatype axis bindings parse and are then dropped — lower_metatype_decl emits axes: Vec::new() (oxc-instantiate/src/lower.rs:2870; same for metarels at :2897); the metaxis value set {anti_rigid < semi_rigid < rigid} is persisted nowhere (MetaxisDeclBody.value_type hardcoded Null, lower.rs:2844-2845); there is zero validation — pub metatype weird = { nonexistent_axis::bogus_value }; passes ox check and ox build clean. $meta/$iof materialize individual-tier rows only (oxc-runtime/src/lib.rs:3923-4040, gap note at :4012-4014); meta(Person) == kind silently derives nothing (#229). In rule bodies, any multi-segment path lowers to a variable named by the joined path (atom_lower.rs:1649-1655 path_term), so rigidity::anti_rigid trips OE1303 as an “unbound variable” — and the same resolver hole makes enum constants work on comparison-RHS only, individuals in predicate-argument position silently match everything, and qualified predicate atoms silently derive zero rows. The trait coverage gate decides instantiability by token-scraping the literal strings "sortality"/"sortal" from metatype declarations (oxc-driver/src/trait_conformance.rs:398-399) — an unqualified match any module’s axis can satisfy, and a one-letter typo silently disables the gate. The book Note (04-meta-calculus.md:44) claims the language “ships” the rigidity/sortality/identity_provision axes.

Question

pub metaxis and the metatype binding form exist so that vocabularies can classify their own types along their own dimensions — the meta-calculus is atom 1 of the language. The book already commits to the semantics: axis values “are not labels — the reasoner reads them” (crash-course §1), and the storage chapter commits axis values as (axis, target, value) meta_property events (“No UFO axis is a column”, 18-storage.md:7). The Lean storage model carries them (Storage/AxiomBody.lean:96-132). The implementation honors none of it.

The first external user hit the gap within a day of the trait arc shipping. Tiago’s ArgUFO overlay — UFO built as user-space vocabulary, exactly what the no-ambient-vocabulary doctrine (#208, #213) prescribes — writes:

pub derive isAntiRigid(t: TypeRef) :-
    meta(t).rigidity == rigidity::anti_rigid

and gets OE1303 naming rigidity::anti_rigid as an unbound variable. No phrasing works: the constant doesn’t resolve, the metatype tier isn’t materialized, and the binding isn’t even in the artifact. Meanwhile the compiler itself does read axis vocabulary — by magic string — in the one place it needs an answer (OE1327 instantiability), which is the same bug class the §3.4 gate (#213) eliminated one level down.

Two questions, then. (1) What is the correct end-to-end design for declared meta-properties — declaration, validation, persistence, materialization, query surface? (2) Where is the boundary between user axis vocabulary and substrate semantics — what may the compiler read?

Design lineage

The vault records both questions being answered before, halfway:

• argon-ontology-neutrality/rigidity-removal-storage (sub-RFC, accepted 2026-04-30): tore the built-in Rigidity/SortalDependence enums out of the legacy kernel — “the largest remaining UFO leak in nous” — replacing them with a generic per-target meta_properties: BTreeMap<AxisId, Vec<MetaValue>>, with MetaValue::Symbol interned per (axis, value-name) pair. The (axis, target, value) event shape descends from this. But the cluster kept legacy helpers (is_rigid()/is_sortal()/provides_identity()) that read the axes by string — the storage went neutral, the semantics did not. The OE1327 magic strings are that compromise carried forward.
• Beyond-OntoClean research (vault scratch, 2026-04-18): the useful meta-property space is open-ended — Fine’s essence-vs-modality refinement of rigidity, unity as a parameterized family (topological/morphological/functional/intentional), Mizoguchi role-ness and context-dependence, Lowe individuation-dependence, BFO’s dependence typology. No finite axis list a substrate ships can be right. Rigidity/sortality are formal-ontology-neutral (UFO/BFO/DOLCE all use them) but they are still ontological commitments — and the substrate does not need them; it needs their operational shadows.

This RFD completes the neutrality program: the 04-30 sub-RFC neutralized the data; this RFD neutralizes the semantics.

D1 — One value-position name-resolution pass

Every term position in a rule body (predicate arguments, comparison operands both sides, compute operands, head arguments) resolves names through a single pass, in priority order:

1. Bound rule variable (appears in a positive body atom or is a head parameter).
2. Enum constant — Status::Active, qualified or imported.
3. Axis value — rigidity::anti_rigid, where the first segment resolves to a visible pub metaxis and the second to a value in its declared domain.
4. Type reference — single-segment and qualified type names (TypeRef constant).
5. Declared individual — bare or qualified (alice, people::alice).

Refusals are loud:

• A multi-segment path that resolves to nothing is a hard error (new OE), never a variable.
• A bare identifier used both as a rule variable and resolving to a declared constant is a hard ambiguity error naming both candidates (the lesson of Rust’s bindings_with_variant_name, promoted from lint to refusal): rename the variable or qualify the constant.
• The existing path :: Ident metaEq sugar (07-rules.md:128) applies only when the left side is a bound term, after constant resolution fails to claim the path — the resolution order above is the documented disambiguation for A::B (already flagged ambiguous at 07-rules.md:155).

This single pass closes five verified symptoms at once: axis values as OE1303 “variables” (Tiago); enum constants failing on comparison-LHS while working on RHS; x == alice refused (#148); knows(x, carol) silently treating carol as a wildcard and over-deriving (the worst member — silent wrong results, zero diagnostics); and qualified individuals refused. Qualified predicate atoms deriving zero rows (rule compile keys joined paths, catalog keys short names) is the predicate-position sibling fixed in the same slice.

D2 — Declarations become real: wire + validation

• MetaxisDeclBody persists the domain: unordered(values), chain(values) (declaration order is the order; the book’s a < b chains), or typed(TypeExpr, refinement?). The Lean AxisDomain shape (MetaCalculus/Axis.lean:38-48) already models this; the Lean storage mirror does not and gains it.
• MetatypeDeclBody.axes / MetarelDeclBody.axes are populated with resolved bindings: axis = qualified NameRef (post-#213 discipline — the wire does not carry bare text), value = symbol (enumerated domains, bound with ::) or literal (typed domains, bound with =, e.g. weight = 1.0; :: vs = follows the existing grammar and the RFD 0017 note that = belongs to typed domains).
• Validation at elaboration (new diagnostics, meta-calculus OE19xx range): unknown axis; value not in the axis’s declared domain (or literal fails the typed domain’s refinement — the OE0606 precedent); axis tier mismatch (for type axes bind only on metatypes, for rel only on metarels); duplicate axis in one declaration (OE1903, already specified in Wellformed.lean).
• Per-target assertions ride the existing MetaProperty event ((axis, target, value) — the channel MLT’s #[order(N)] already emits), now actually consumed (D3).
• Lean storage mirrors for MetaxisDeclBody/MetatypeDeclBody/AxisBinding are added; the Rust doc-comment claiming “Mirrors Argon.Storage.AxiomBody.AxisBinding” currently cites a declaration that has never existed and becomes true.

D3 — Catalog tiers: metatype-tier $meta/$iof and the $axis relation (settles #229)

• The runtime Module indexes concept_id → metatype_id at load (ConceptDeclBody.metatype_id is already resolved on the wire since #213; it currently has zero non-test readers).
• $meta and $iof gain metatype-tier rows: (type, metatype) for every declared type, plus the tower the book’s worked examples promise (meta(Person) == kind, meta(kind) == Metatype, 04-meta-calculus.md:95-99). Catalog-closed ⇒ NAF-safe, the same justification as $implements. This also unblocks MLT’s CL-rules (iof over types) as a side effect.
• A new catalog relation $axis(target, axis, value) materializes the effective axis assignments: metatype-level bindings (D2) unioned with per-target MetaProperty assertions, per-target assertions taking precedence, functional per (target, axis) — a conflicting pair is a load-time error, not a silent choice.
• Valence: single-valued per (target, axis). The legacy design admitted Vec<MetaValue> (the vault’s mode metatype binding two nature values); in the IS/CAN/NOT calculus that case is correctly “the metatype does not determine the value” — a CAN, i.e. no binding — rather than two simultaneous ISes. Multi-valued axes are a recorded non-decision: revisit with a concrete consumer, against the vault lineage. Cross-axis condition clauses from the legacy engine likewise stay out until someone needs them.

D4 — The query surface

• meta(t) over a type evaluates via the metatype-tier $meta join (it already lowers correctly; the rows now exist).

• Sort-directed projection. base.name where base is reflective: a TypeRef-sorted base resolves name as a declared field on the type (the documented meta(bar).x walk-up, 05-constructs.md:158-173 — unchanged); a Metatype-sorted base resolves name as a visible metaxis and lowers to a $axis join. No overload collision: fields live on types, axes live on metatypes. Tiago’s rule works as written:

  pub derive isAntiRigid(t: TypeRef) :-
      meta(t).rigidity == rigidity::anti_rigid
  

  t binds via the catalog $meta join; .rigidity joins $axis; the right side is a constant (D1). meta(t).rigidity == r with r free binds r. An unbound axis (the metatype binds nothing for it) yields no row — ordinary Datalog absence.

• Chain comparisons. For chain domains, </<=/>/>= compare by declared position (crash-course §1 promises exactly this). Comparing symbols of different owners, or of an unordered domain, is a loud compile-time error where statically known and a loud runtime refusal otherwise — never an enum-variant-order fallback.

• Type-tests over reflective sorts are catalog atoms. t : TypeRef ranges over all declared types; m : Metatype over all declared metatypes (the predicate forms of the promised extent(TypeRef)/extent(Metatype), 04-meta-calculus.md:109). Both bind positively, catalog-closed. This legalizes Tiago’s second attempt rather than refusing it. x : Entity stays refused for now, with a diagnostic that names the supported sorts and the catalog-atom binding idiom (its extent spans individuals ∪ types and needs its own design).

D5 — Value::Symbol: one carrier for axis values and enum constants

A new runtime value sort:

#![allow(unused)]
fn main() {
Value::Symbol { owner: NameRef, name: SmolStr, ord: Option<u32> }
}

• Identity is (owner, name) — the interned-(axis, value-name) design from the 04-30 sub-RFC. ord is populated from chain domains at build (None for unordered/enum owners); equality ignores it; ordered comparison requires Some on both sides and equal owners, else refuses loudly.
• Enum constants migrate to the same carrier. Today’s enum runtime carrier is a type-erased CBOR tag ({tag: "<variant>"}) under which two enums sharing a variant name compare equal — a live defect this RFD fixes rather than duplicates. Pre-release, no artifact compatibility is owed; the corpus regenerates.
• Full sort cost, paid in full (no hollow rendering): CBOR encoding in the event log; CLI render_value renders owner::name; serve JSON renders a typed envelope with the qualified owner path (the #182 pattern); oxc-gen emits branded TS types per owner with exact (de)serialization; Lean wire mirror + drift coverage.

D6 — Substrate-neutral modifiers: abstract and fixed

The compiler never reads a user axis name. Anywhere. The substrate’s three genuine needs reduce to two ontology-neutral, PL-precedented bits, declared as modifiers:

• Placement. Both modifiers attach to metatype declarations (pub abstract fixed metatype category = { … };) — the metatype is the behavior bundle — and abstract is additionally allowed per-type (pub abstract type Vehicle { … }, the UML/PL convention). No override semantics: a type introduced by an abstract metatype is abstract, full stop.
• Polarity: dynamic by default, fixed is the opt-in restriction. The §7.5 gate governs re-classification of existing individuals, not construction; for a data-systems language, membership churn is the normal case and is today’s behavior throughout the examples. The restriction is the constraint you declare — the same posture as check. (The keyword is fixed; sealed was rejected as colliding with the closed-hierarchy meaning in Kotlin/Scala/C#.)
• Consequences for the book. The Note at 04-meta-calculus.md:44 (“the language ships the rigidity/sortality/identity_provision axes”) is deleted. Anti-rigid admission “through the axis assignment” is rewritten: admission comes from the absence of fixed; identity_provision has zero substrate consumers and becomes pure user vocabulary like everything else. ArgUFO writes pub abstract fixed metatype category = { sortality::non_sortal, rigidity::rigid }; — the modifiers carry the behavior, the bindings carry their ontology, and importing a package can never change mutation semantics because its author named an axis rigidity.
• StaticDischarge.lean’s Rigidity inductive (:38-50) is re-grounded as the Kripke-semantics justification of fixed (rigid designation = fixed classification), not as a privileged axis.

D7 — Lean obligations

Surface settled (this RFD); per the workflow table the substrate semantics go Lean-first:

1. Canonical model = the ternary axis relation (target, axis, value) with per-(target, axis) functionality — the (axis,value)-point instantiation of State C A cannot express chains or typed domains; the relation reading covers all three domains uniformly. This resolves the deferred wiring note in IsCanNot.lean:48-50 (the A-instantiation becomes a derived view of the relation).
2. Chain-order semantics for symbol comparison; refusal semantics for cross-owner/unordered comparison.
3. Catalog-closure of $meta (both tiers), $axis, and the reflective-sort extents, with the NAF-safety corollary — the #221 (Catalog.conformant_iff) pattern, including a decidable checker and non-vacuity witnesses on a concrete catalog.
4. Decidability: axis atoms, metatype-tier reflection atoms, and reflective-sort type-tests are D1-tier (catalog joins); the classifier admits them.
5. Modifier semantics: fixed ⇒ the mutation-boundary refusal theorem (no iof delta on fixed-introduced types in any successful mutation — extends the RFD 0015/0019 mutation semantics); abstract ⇒ the OE1327 oracle reads a wire flag (decidable, no string predicate); the static-discharge soundness hypothesis re-stated over fixed.
6. Wire mirrors (D2) under @[language_interface], acknowledging the known drift-gate limitation that structures are prose-aligned — the mirrors are still written, and the lying comment dies.

D8 — Diagnostics inventory

New codes in the meta-calculus range (numbers assigned at implementation against the live catalog; the trait arc’s OE1322→OE1326 renumbering is the cautionary precedent): unknown axis in binding; axis value not in domain / literal fails typed-domain refinement; axis tier mismatch; unresolvable multi-segment path in rule value position; variable/constant ambiguity; cross-owner or unordered symbol comparison; insert/delete iof against fixed; instantiating an abstract type; Entity type-test refusal (help names the supported idioms). Amended help texts: OE1303’s “variable(s)” wording when the offender is an unresolved path (point at the path, not at range restriction); OE0223 on reflective sorts (now legal per D4 — the remaining refusal case is Entity).

Alternatives considered

• std-shipped well-known axes (std::meta::rigidity, …): rejected. Re-creates the #208/#213 leak one level up — a blessed package whose names carry compiler semantics — and the beyond-OntoClean record shows no finite list is right. The book Note that implied this dies.
• Per-value marker attributes on axis declarations (#[dynamic_classification] on anti_rigid): rejected — the substrate bit is per-value in that encoding, the declaration site becomes clutter, and importing a vocabulary still changes substrate behavior.
• Keep the magic strings: rejected; it is the audited bug (ufo-01), behaviorally confirmed — a typo silently disables a soundness gate.
• Multi-valued axes (Vec<MetaValue>): deferred with the K3 ‘can’ reading as the principled alternative; see D3.
• Static-by-default polarity for classification mutability: rejected for data-systems pragmatics — it makes the common case ceremonial and breaks every existing example; the ontological reading is recovered exactly by declaring fixed.
• A separate axis-value sort distinct from enum constants: rejected; two symbol-like sorts with different equality and rendering rules is incoherence by construction, and the enum carrier needed the fix anyway.

Sequencing

1. S0 — D1 resolution pass + the two filed silent bugs (individual-as-wildcard, qualified predicates). Independent of everything else; converts silent-wrong to loud immediately.
2. S1 — D2 wire + validation + Lean storage mirrors.
3. S2 — D3 catalog tiers ($meta/$iof metatype tier, $axis), closing #229.
4. S3 — D4 query surface + D5 Value::Symbol (including the enum migration), full rendering chain.
5. S4 — D6 modifiers + consumer migration (OE1327, §7.5 gate, static discharge, VT defaults)
   • the book rewrite (Note deletion, §7.5, §12.4, crash-course).
6. Lean (D7) leads each slice’s semantics per the workflow table; the mutation-gate theorem lands with S4.

Each slice is loud-complete on its own: no slice ships a parsed-but-inert surface.

Relationship to existing issues

• #229 — settled by D3 (metatype-tier rows) + D4 (the classifier admits catalog-level bodies).
• #148 — the constants half is settled by D1; the equality-binding half stands.
• #209’s “RFD 0027” parking reference — this document.
• Audit register: ufo-01 (magic strings → D6), ufo-02 (hollow wire → D2/D3), ufo-03 (phantom Lean mirrors → D2), ufo-04 (the boundary ruling → D6), gs-09 (axis sugar diagnostics → D1/D8), plus the enum type-erasure finding (→ D5).
• #150 — the new codes land catalog-first; no raw-string emissions.