RFD 0043 — Theory packages and the neutrality boundary: where ontologies and higher-order theories live

• State: discussion
• Depends on: RFD 0030 (package dependencies — path deps, the on-ramp), RFD 0027 (meta-property plane — the neutral axis machinery a theory rides), RFD 0042 (the re-checkable emission boundary — the event-emission gate a theory’s decorators emit through), RFD 0037 / 0040 (the macro atom + procedural layer — the authoring surface), RFD 0009 (MLT — the first theory re-homed)
• Amends: RFD 0009 (relocates MLT out of std to a first-party package) · RFD 0042 (realizes its “blocks the genuine, builtin-free re-home of the MLT decorators” clause)
• Blocks: the genuine re-home of the MLT decorators (#483); ArgUFO authorable end-to-end (milestone #8)

Question

Where do higher-order type theories and foundational ontologies live, and what may std contain?

Today the asymmetry is the tell: UFO is an external package (correct — the substrate ships no ontological category), but MLT is embedded in std and expanded by privileged compiler builtins — ambient theory vocabulary at four layers. MLT and UFO are the same kind of thing: a committed theory the substrate is deliberately neutral about. The doctrine already says “no ambient ontology vocabulary” and “higher-order theories ship as libraries” — but those are two rules without one operational test, and the MLT leak slipped through the gap between them.

So: what is the single test that decides whether a thing belongs in the substrate, in std, or in a package — and where, concretely, does a theory like MLT live?

Context

The leak surface runs four layers. MLT-specific vocabulary is wired into:

1. the compiler directive registry — categorizes et al. registered as known directives with hard-coded arg-shapes (oxc-instantiate/src/directives.rs);
2. the lowering path — lower_relational_mlt_decorators / lower_order_decorator natively emit MetaProperty (oxc-instantiate/src/lower.rs);
3. std itself — std/mlt/ is include_str!-embedded and elaborated in a fixed order after std::core (oxc-instantiate/src/lower.rs);
4. the diagnostic registry — OE1903–OE1907 reserved for MLT’s specific violations (oxc-diagnostics, oxc-syntax/grammar.toml);
5. the substrate mechanization — MetaCalculus/MLTKinds.lean names categorizes/partitions/subordinates carriers (its Wellformed.lean predicates are already parametric/neutral — the names are the residue).

The neutral substrate the theories need already exists. RFD 0027 gives axes the compiler never interprets; the meta-calculus exposes a generic metarel carrier, iof/specializes, reflection, and MetaProperty events; RFD 0042 adds (in progress) the re-checked event-emission gate a decorator emits through. None of this names a theory.

The packaging on-ramp already exists. RFD 0030 shipped [dependencies] name = { path = "…" } end-to-end — transitive closure, cycle/collision diagnostics, package-qualified module paths, a two-package acceptance test. A non-std package on disk is buildable and dependable today; the include_str! embed is how std is distributed, not a constraint on path deps. (Versioning, a registry, a lockfile, [workspace], and ox new/add/publish do not yet exist — that is a separate cargo-parity arc, below, and it does not block this RFD.)

Decision

D1 — The neutrality test

A capability belongs in the substrate or std only if it passes the reflect-not-smuggle test:

std (and the substrate) may reflect a commitment the substrate has already made. It may not smuggle a commitment the substrate deliberately withholds.

The competing-theory rule is its corollary: a competing formalization exists exactly where the substrate withheld commitment, so if multiple credible theories occupy the same layer, none of them belongs in std — shipping one privileges a theory.

Applied to the current std set (each verified against its header / the substrate it rides):

The same verdict puts UFO, BFO, DOLCE, potency, and ML2 in packages — none in std, none built-in.

D2 — Three layers

• Substrate (intrinsic, inert, neutral): the meta-calculus — a generic metarel carrier, axes the compiler never interprets (including a neutral ordinal axis a level-theory rides), iof/specializes, reflection, MetaProperty events, the partition/disjointness mechanism, and the RFD 0042 re-checked event-emission boundary. The substrate names no theory.
• std (neutral, non-theory utilities): everything that passes D1. No higher-order type theory, no foundational ontology.
• Packages (theories and ontologies, none privileged): MLT, UFO, BFO, potency, ML2. Each declares its own metarels, authors its decorators as library #[procmacro]s emitting MetaProperty through the RFD 0042 gate, expresses its semantics as derive/check rules, and emits its own diagnostics via RFD 0025 check-discharge.

There is no “higher-order type utilities” tier in std: anything generic enough to be theory-neutral already is the substrate (generic metarel + ordinal axis); anything more specific smuggles a theory’s commitments.

D3 — The packages/ directory

First-party libraries that are not std live in a new top-level packages/ directory (this RFD authorizes the new top-level directory). A package there is an ordinary ox package with its own ox.toml, depended on as name = { path = "packages/name" } and imported as use name::…. packages/ is visibly distinct from examples/: packages/ holds publishable libraries; examples/ holds demonstrations. The future registry’s naming aligns with packages/ (the three-layer story maps to substrate / std / registry, ≈ language / stdlib / crates.io).

D4 — MLT re-homes to packages/mlt as an unprivileged package

Delete the four-layer privilege (D1 context items 1–5): the directive-registry entries, the lower_* builtins, the std/mlt/ embed + its fixed elaboration order, the OE1903–OE1907 codes, and the MLT names in MLTKinds.lean (leaving the neutral parametric mechanism). packages/mlt declares its metarels, authors #[categorizes(T)] et al. as #[procmacro]s emitting MetaProperty, and emits its own diagnostics via RFD 0025. User source is unchanged — #[categorizes(T)] is spelled identically; only the (already-required) import and the now-unprivileged provenance differ.

The re-home is two-phase, because its two halves have different dependencies:

• Phase 1 — emission/classification neutrality (independent; do now). The RFD 0042 EmittedArtifact::Event boundary + routing an emitted MetaProperty into the event stream where the shipped D3 load re-checks (OE0622–OE0624) gate it; delete the privilege; the packages/mlt skeleton (metarels + #[procmacro]s). This closes #483’s emission scope by construction and touches none of the reasoning fixpoint — its files are the emission boundary, the lowering-deletion sites, the diagnostic registry, and packages/; not oxc-reasoning’s disjointness/classifier semantics.
• Phase 2 — reasoning-time function (converges with the substrate keystone). MLT functioning: the declarable-disjointness primitive (the OE1904-Reserved mechanism, downstream of the CWA/OWA write-side ruling), the ordinal axis, and the reflective #[static] checks that express partitions ⇒ disjoint + cover and the order arithmetic. These are not macro work — they are the shared substrate keystone that also makes ArgUFO authorable (milestone #8). They are designed once, in the keystone arc’s own RFD and tracker (see Consequences), and consumed by packages/mlt. The full acceptance test (D6) is met only here.

D5 — Package soundness-proof home

A package’s soundness proofs travel with the package, and must not pollute the substrate’s proof corpus:

• In-repo first-party packages home their Lean under spec/lean/Packages/<Name>/ — in the same lake build (so they are CI-gated and held to the same no-sorry / no-uncited-axiom discipline as the substrate), but namespaced out of Argon/ so the Argon/↔Rust @[language_interface] drift gate and the substrate theorem corpus stay pure. packages/mlt’s categorizes ⇒ order+1 / partitions ⇒ disjoint+cover soundness lives at spec/lean/Packages/Mlt/, proved against the neutral substrate it imports.
• External packages carry their proofs in their own repository, importing the substrate Lean as a lake dependency.

This sets the precedent for every theory package (UFO, BFO, potency).

D6 — Acceptance: an unprivileged package authors a full type-theory

The neutrality proof is that a package with zero compiler privilege authors a complete type-theory:

• Phase 1: packages/mlt’s #[procmacro] decorators expand end-to-end, emit MetaProperty events that are re-checked at load by the substrate’s own gate, classify on their true tier, and round-trip an .oxbin — with no builtin, no std embed, no reserved diagnostic code. The criterion is parity, not byte-identity: the metarel path moves (std::mlt::categorizes → mlt::categorizes), so the emitted event’s axis_id interns a different string and cannot be byte-identical to the old builtin output (unlike the relation-property re-home, which stayed at std::rel). Parity = the semantically-equivalent re-checkable event (correct axis metarel, target, value), load re-check clean, .oxbin round-trip.
• Phase 2: packages/mlt’s #[static] checks enforce its well-formedness (disjointness, order) at reasoning time over the neutral substrate primitives, emitting its own diagnostics.

Rationale

Why reflect-not-smuggle over competing-theory alone. “No competing theory” is true but secondary — it explains why a layer is neutral (a competitor exists precisely because the substrate withheld commitment) but does not, on its own, justify keeping std::kripke (modal logic has competing semantics — neighborhood, algebraic, topological). The primary fact is that the substrate already committed to Kripke frames in its mechanized modal/standpoint semantics; std::kripke reflects that commitment honestly. The test has to be about what the substrate committed to, with competing-theory as the diagnostic for “did it withhold here?”. That ordering is what makes “keep kripke, drop mlt” a consequence of doctrine rather than a judgment call.

Why packages/, not std and not external-only. std-membership is the privilege we are removing. External-only (like UFO today) loses the in-CI neutrality proof. An in-repo first-party package gets both: zero privilege and a CI-gated proof that the substrate is neutral — co-evolving with the substrate work that unblocks it.

Why two-phase. The emission re-home is genuinely independent of the reasoning substrate; gating it on the keystone would stall a clean, provable win behind a multi-session research arc. Splitting also exposes the real shape: MLT is a second forcing function for the keystone (alongside ArgUFO), not the owner of it. One disjointness primitive, designed in the keystone, consumed by every theory — never a parallel mechanism invented inside the macro arc.

Why package proofs under spec/lean/Packages/. The substrate’s quality bar (no sorry, drift-gated, one lake build) is worth extending to first-party theory proofs, but the substrate’s purity (the Argon/↔Rust contract, the neutral theorem corpus) must not absorb theory-specific lemmas. A sibling namespace in the same build is the only option that keeps both.

Consequences

• std is purged of theory vocabulary. MLT moves to packages/mlt; UFO/BFO/potency/ML2 follow the same path. std::kripke/std::fin/std::rel/std::core stay, justified by D1. (std::kripke’s “elaborate after std::core and std::mlt” wiring simplifies to “after std::core”.)
• #483 closes its emission scope by construction (Phase 1) — the strongest neutrality statement we can make: an unprivileged package authors decorators that emit re-checked substrate events with no compiler involvement. #517 (the MLT signature disagreement) becomes a package-internal naming choice aligned to the neutral substrate.
• The reasoning-time keystone (Phase 2) is owned by the substrate keystone arc, not this RFD. The declarable-disjointness primitive (CWA/OWA write-side ruling), the reflective #[static]-check plane, and the set-valued metaxis work are one coordinated substrate cluster currently spread across the macros, tiago-meta, and design-review threads, all editing oxc-reasoning / the classifier / the meta-plane. They share one design and one tracker (a converged keystone epic), with packages/mlt Phase 2 and ArgUFO as its two independent forcing functions. This RFD references that arc; it does not design it.
• The package registry / ox publish / lockfile / [workspace] / ox new/add is a distinct cargo-parity arc. Path deps (RFD 0030) already carry the re-home. MLT is the forcing function for “the first published package” once the registry lands; it does not block here.
• D5 sets the package-proof precedent for every future theory package.

Alternatives considered

• Keep MLT in std, just delete the builtins (library-surface-stub + privileged-native-expander). Rejected: relocates the surface while the privileged expander stays — a hollow re-home, and std-membership is itself the privilege. RFD 0042 already commits to the genuine version.
• MLT external-only, like UFO. Workable, but forfeits the in-CI neutrality proof and the co-evolution with the substrate work. In-repo first-party (packages/) dominates.
• A neutral “higher-order type utilities” tier in std. Rejected: any such util generic enough to be neutral already is the substrate; anything more specific smuggles a theory (see D2).