RFD 0009 — std::mlt library scope

• State: discussion
• Opened: 2026-05-28
• Last revised: 2026-05-29 (added #[order(N)] assertion decorator + completed decorator set per discussion with Tiago Sales; fixed @[…] → #[…] sigil throughout to align with §14.2)
• Decides: scope of the std::mlt library that provides Multi-Level Theory (Carvalho-Almeida 2018) as a parallel std::* package on Argon’s neutral substrate; surface syntax for decorators (relational AND assertion forms); the Datalog rules CL-1..CL-7 enforcing MLT well-formedness; per-rule diagnostic emission for OE1903–OE1907.

Question

Argon’s substrate is committed to MLT-as-library (RFD-relevant memory: “Higher-order theories as stdlib libraries”). The substrate provides the higher-order type primitives required (universe polymorphism via metaxis, level-indexed quantification via metatype) and now carries the five MLT primitive metarel kinds (MLTMetarelKind per the just-landed Argon/MetaCalculus/MLTKinds.lean). What’s needed is the library that operationalizes MLT — decorators, Datalog enforcement rules, diagnostic emission.

What should std::mlt v0.1 ship, and how should it be wired into the build pipeline?

Context

Why a library, not substrate

Per user strategic commitment: “MLT is a library, not substrate. The atoms of the language allow for MLT to be implemented, as we have higher-order type primitives, but MLT must be a library.” This preserves Argon’s neutrality. UFO, BFO, DOLCE, ML2 all ship as parallel std::* packages; the language doesn’t favor one foundational ontology over another. The substrate’s responsibility ends at exposing sufficient primitives.

This commitment is verified for MLT specifically by the just-landed substrate sufficiency scaffold:

• instanceOf, specializes admitted via the inheritance lattice + IsCanNot machinery.
• categorizes, partitions, subordinates admitted via MLTMetarelKind carriers.
• Order arithmetic semantics live in Argon/MetaCalculus/Wellformed.lean as parametric Props over an abstract T.

What’s missing: the library that instantiates these primitives against modeler-written declarations and emits enforcement rules.

What MLT requires from a library

Per Carvalho-Almeida 2018 (Theorem-based MLT axiomatic theory) and Vault’s “MLT as a Library, Not Substrate” deep-dive:

1. Decorators on metatype declarations that express MLT primitives at the surface. Two distinct kinds — relational (declare a cross-level relation between types) and assertion (declare a claim the compiler verifies against the derived fixpoint). Sigil is #[…] per Procedural macros; both kinds appear at declaration position.

   Relational decorators — desugar to canonical metarel-instance events; the relation participates in CL-1..CL-7 enforcement:

   • #[categorizes(T)] — the metatype’s instances are proper specializations of T; implies order(M) = order(T) + 1. (Carvalho-Almeida §3.2.)
   • #[partitions(T)] — #[categorizes(T)] + members of the metatype pairwise disjoint and jointly exhaustive of T’s extent. (Carvalho-Almeida §3.3.)
   • #[subordinate_to(M)] — same-order subordination per Carvalho-Almeida §3.4. (Spelled subordinate_to per Higher-order modeling, not subordinates — the §3.4 relation reads “A is subordinate to B”.)
   • #[power_type_of(T)] — the metatype is the powertype of T per Cardelli 1988; every instance of T is also an instance of M. (Carvalho-Almeida §3.5.)

   Assertion decorators — desugar to a check rule verifying a claim against the derived fixpoint; fail-loud at runtime if the assertion conflicts with the iof chain, vacuous when the chain is incomplete:

   • #[order(N)] — modeler asserts has_order(Self, N); the elaborator emits an implicit check rule that fires OE1905 OrderInconsistency if the derived order disagrees. See § Decorator kinds — assertion vs. relational below for the full design.

   Tier decorators — module-level annotations that narrow the decidability tier:

   • #[order_bound(N)] — module declaration; caps every concept’s order at N. Lowers the module from tier:metaorder to a polynomial tier under the bound. (See Higher-order modeling, Tier ladder.)

2. Datalog enforcement rules (kernel-native, fired automatically), per the Vault’s “Hybrid A+B” design pattern:

   • CL-1 Categorization: violation_categorization(X, T₂, T₁) :- categorizes(T₂, T₁), iof(X, T₂), ¬subclass(X, T₁). Emits OE1903.
   • CL-2 Partition disjointness: violation_partition_disjoint(Ind, T₃ₐ, T₃ᵦ) :- partitions(T₂, T₁), iof(T₃ₐ, T₂), iof(T₃ᵦ, T₂), T₃ₐ ≠ T₃ᵦ, iof(Ind, T₃ₐ), iof(Ind, T₃ᵦ). Emits OE1904.
   • CL-3 Order consistency: violation_order(X, T) :- concept_order(T, N), iof(X, T), concept_order(X, M), M ≥ N. Emits OE1905.
   • CL-4 Categorization inference: subclass(X, T₁) :- categorizes(T₂, T₁), iof(X, T₂). (Positive rule, no diagnostic.)
   • CL-5 Subordination requirement: violation_subordination(A, B) :- subordinates(A, B), (order(A) ≠ order(B) ∨ order(A) < 2). Emits OE1906.
   • CL-6 Powertype completeness: violation_powertype(T) :- power_type_of(M, T), iof(X, T), ¬iof(X, M). Emits OE1907.
   • CL-7 MLT compositional consistency (Carvalho-Almeida Theorem 5): a closure rule that propagates categorizes/partitions/subordinates interactions per the §3.4 composition table.

3. Diagnostic codes OE1903–OE1907 wired into oxc-diagnostics and emitted from oxc-instantiate (or a follow-on pass) when CL-1..CL-7 detect violations.

4. Library API surface modelers reach for:

   • use std::mlt::* brings the decorator set #[categorizes] / #[partitions] / #[subordinate_to] / #[power_type_of] / #[order] / #[order_bound] into scope.
   • std::mlt::well_formed!() build-time check macro that runs CL-1..CL-7 (plus the user’s #[order] assertions, if any) and fails the build on violation. Modelers serious about MLT correctness add this to their root module.
   • std::mlt::order(e: Entity) -> Option<Nat> library function — query a concept’s derived order at runtime; None when the iof chain is incomplete enough that order isn’t yet determined. (Operationally lowered to a one-shot query over the has_order/2 predicate per RP-003 §4.3.)

What std::mlt does NOT do

Per the strategic commitment, MLT-as-library means:

• The library does NOT extend the substrate. No new atoms.
• The library does NOT enforce MLT globally — only modules that use std::mlt opt in. Other modules see iof/specializes as usual without categorization arithmetic.
• The library does NOT subsume UFO, BFO, DOLCE — those are parallel std::* libraries with independent enforcement.

Decision

Scope of v0.1

Three landings, each independent:

Phase 1 — Decorator parser + lowering (~1-2 weeks)

• New oxc-parser recognition for the v0.1 MLT decorator set on type/metatype declarations:
  • Relational (lower to metarel_decl axiom events): #[categorizes(T)], #[partitions(T)], #[subordinate_to(M)], #[power_type_of(T)].
  • Assertion (lower to implicit check rules): #[order(N)].
  • Tier (module-level, narrows decidability tier): #[order_bound(N)].
• oxc-instantiate lowers each decorator according to its kind:
  • Relational → canonical metarel_decl axiom event via Argon.MetaCalculus.MLT.declOfKind.
  • Assertion → synthesized check declaration; for #[order(N)] on concept X, the check is check OrderMatches { has_order(X, N) } keyed to OE1905 OrderInconsistency.
  • Tier → module-attribute on the elaborated program; the classifier reads it and narrows the tier.
• Diagnostic emission for surface mis-use (decorator on a non-applicable position, bad argument shape, conflicting decorators on the same declaration). Reuses OE0708 ReservedAttributeName only when collision is genuine; the MLT-specific positional checks ride on a new fingerprint.
• Sigil is fixed at #[…] (Procedural macros); the prior draft of this RFD used @[…] which was a typo against the rest of the spec.

Phase 2 — CL-1..CL-7 Datalog rules + OE1903–OE1907 (~3-4 weeks)

• oxc-reasoning admits the seven CL-* rules as built-in rules (compiled at runtime, not modeler-written).
• evaluate_to_fixpoint (or its semi-naive successor — depends on RFD 0003 backend dispatch) computes the violation predicates.
• oxc-runtime lifts violation tuples to OE1903–OE1907 diagnostics at query-time-of-affected-rule.
• Lean-side: extend Argon.MetaCalculus.Wellformed’s parametric predicates to a runtime-evaluable form; prove correctness against Carvalho-Almeida 2018’s axioms.

Phase 3 — std::mlt package + integration tests (~1-2 weeks)

• Ship std::mlt as a workspace package with use std::mlt::* bringing in decorators.
• Integration test exercising the Vault’s “biological taxonomy” canonical example (Animal → AnimalSpecies → DogBreed, order 0/1/2).
• Documentation: short tutorial showing modeler-facing usage.

Total v0.1 effort: ~5-8 weeks across Phase 1+2+3.

Implementation pattern — “Hybrid A+B”

Per Vault’s MLT design synthesis: enforcement is two-layered.

• A — Compile-time decorator expansion: #[categorizes(T)] on metatype M desugars to a canonical metarel categorizes(M, T) declaration that lands in the events list. Pure source transformation; no runtime cost. Assertion decorators (#[order(N)]) similarly desugar at compile time, but to a synthesized check rule rather than a metarel-instance event.

• B — Runtime Datalog evaluation: CL-1..CL-7 rules fire continuously during query evaluation, detecting violations as they arise. Lazy by construction (a violation only matters when a query touches the affected predicate). Diagnostics emit at query time, not at build time.

This hybrid lets the build complete even if MLT violations exist (graceful degradation for in-progress modeling), while ensuring runtime queries fail loud if a violation is reachable.

Decorator kinds — assertion vs. relational

The two decorator kinds carry different semantic weight and warrant different mechanical treatment.

Relational decorators (#[categorizes], #[partitions], #[subordinate_to], #[power_type_of]) introduce a fact into the model: “this metatype is in this cross-level relation with that type.” They desugar to canonical metarel_decl events that participate in the CL-1..CL-7 enforcement closures. The diagnostic surface for these is the closure rules — a violation is detected when the modeler’s facts are mutually inconsistent under MLT’s axioms (Carvalho-Almeida §3.2–§3.5).

Assertion decorators (#[order(N)]) introduce a claim into the model: “this concept has this property.” They desugar to implicit check rules that fire at runtime against the derived fixpoint. The diagnostic surface is the check rule itself — a violation is detected when the modeler’s claim conflicts with what the iof chain actually derives.

#[order(N)] — design

use std::mlt::*;

#[order(2)]
pub type AnimalSpecies : TaxonomicRank <: Species  // claimed 2; derived order(AnimalSpecies) = 2 ✓

#[order(1)]
pub kind Dog : AnimalSpecies <: Animal             // claimed 1; derived order(Dog) = 1 ✓

let Lassie : Dog                                    // individuals don't need #[order]; order = 0 always

Semantics. On a concept declaration X with #[order(N)], the elaborator synthesizes a check rule equivalent to:

check OrderMatches { has_order(X, N) }   // mlt::E0007 in the library namespace; routed to OE1905 in v0.1

The has_order(_, _) predicate is std::mlt’s stratified-aggregate derivation over the iof DAG (RP-003 §4.3, lines 226–240):

• has_order(x, 0) for any individual x;
• has_order(t, n) for type t when n = 1 + max{m | iof(t’, t) ∧ has_order(t’, m)} (well-founded by iof acyclicity).

Three possible outcomes at check time:

The vacuous-pass case is the load-bearing one for incomplete-model checking — a modeler partway through wiring up the iof chain can assert #[order(2)] and the build won’t fail just because the chain isn’t done; it only fails when the chain explicitly contradicts the assertion. As the model grows toward completeness, more #[order] assertions become checkable, and any divergence shows up immediately.

Why this matters (ergonomics). Three concrete wins motivate the assertion decorator over inference-only:

1. Incomplete-model verification. Modelers iterate. A partial iof chain doesn’t yet derive order, but the modeler has a belief about what the final order should be. #[order(N)] records that belief and turns it into a checkable invariant the moment the chain reaches completeness.
2. Self-documenting models. A reader can see a concept’s intended tower position at a glance without traversing iof predecessors. This compounds in large models where the iof chain crosses module boundaries.
3. Agent guidance. LLM-driven modeling is a primary v0 use case (per Argon’s stdlib-libraries design memo and design notes). Explicit assertions give the agent something to be checked against; pure inference gives the agent nothing to falsify. Agents reason better when their claims are observably refutable.

Why this design, not a procmacro. RP-003 GAP-3 calls for eventually re-homing all MLT decorators as pub macro declarations in std::mlt once the procmacro system is implemented (§14.2). For v0.1, parser-recognized attributes are simpler and ship sooner; the surface (#[order(N)]) is identical either way. Migration is internal.

Applicability. #[order(N)] is valid on:

• Concept declarations (pub type, pub kind, and any user metatype-introduced declaration). Asserts the concept’s tower position.
• Individual declarations (let X : T). Trivially asserts N == 0; mostly redundant since individuals always have order 0, but admitted for symmetry.

It is not valid on:

• struct/enum declarations (no metatype, category error parallel to meta()).
• Relation declarations (relations don’t carry order in MLT; the relation’s metarel does).

Mis-application emits OE1908 OrderAssertionMisplaced (a new code reserved by Phase 1).

Order ceiling at 2 for v1

Per Vault’s “Orca domain census” finding: real-world MLT patterns max out at order 2 (Animal → AnimalSpecies → DogBreed; no order-3 patterns required). v0.1 caps support at order 2:

• concept_order predicate ranges over {0, 1, 2}.
• OE1905 emits for order ≥ 3 declarations.
• MLT* orderless types (universe polymorphism per Sozeau-Tabareau 2014) defer to v2.

This bound makes polynomial decidability concrete: D1Pred over a bounded type graph is polynomial; OE1905 enforcement is O(n²) in the type graph’s edge count.

Rationale

Why ship std::mlt rather than fold it into the language

Three reasons:

1. Neutrality preservation. UFO and BFO have ontological commitments MLT doesn’t (UFO commits to a rigidity/sortality taxonomy; BFO commits to continuant/occurrent). If MLT were substrate, every Argon program would inherit MLT’s claims even when modeling a non-MLT ontology. Library-form means opt-in.

2. Substrate parsimony. Adding MLT to the substrate would grow the five atoms to six. The substrate’s clean five-atom architecture (memory: “Argon substrate atoms fixed: five atoms; mutate not mutation; no event atom; standpoints first-class”) is load-bearing for the meta-calculus story; growing it for one foundational ontology breaks the symmetry.

3. Future foundations. ML2, MLT*, DeepTelos all extend MLT in different directions. Library form lets each ship as a parallel package (std::ml2, std::mlt_star, std::deeptelos); substrate form would force one to be canonical.

Why decorators rather than a new keyword

Carvalho-Almeida’s notation uses categorizes as a relation name. The decorator form #[categorizes(T)] mirrors this exactly: “the metatype is categorized by T.” A keyword form (pub categorization Foo of T) would invent surface syntax that doesn’t appear in the literature.

Decorators also compose naturally with other attributes (#[categorizes(T)] #[disjoint] pub metatype M). A keyword form forces a single grammar position.

Why Datalog enforcement rather than compile-time

Several MLT constraints (CL-1, CL-3 in particular) require closing over the full extent of iof — instances asserted across the module. Compile-time evaluation can’t see runtime-asserted facts (added via mutations). Datalog evaluation fires lazily at query time, catching violations including runtime-added ones.

The downside: violations don’t surface until queried. A modeler can build a broken MLT module that passes the build. The catch is the build-time std::mlt::well_formed!() macro: it pre-runs CL-1..CL-7 against the build-time fact catalog and fails the build if violations exist. Modelers serious about MLT enforcement add this macro to their root module.

Why the OE1903–OE1907 codes are reserved but not yet emitted

The codes were reserved in grammar.toml when RFD 0006 landed (field mutability). The reservation predates this RFD because the diagnostic codes are part of the broader Argon diagnostic registry, not specific to std::mlt. Their EMIT SITES land with Phase 2; reservation is already in place.

Alternatives considered

Alt 1: ship MLT as part of substrate

Add categorizes/partitions/subordinates as substrate atoms; bake CL-1..CL-7 into the elaborator.

Rejected per user strategic commitment. See “Why ship std::mlt rather than fold it into the language” above.

Alt 2: ship std::mlt v0.1 with only the surface (decorators), defer Datalog

A “syntax-only” v0.1: parser admits decorators, but enforcement is documentation-only (“violations are the modeler’s responsibility”).

Rejected as too weak. Decorator-only would let broken MLT modules pass the build silently — the worst-of-both world (visible syntax claiming MLT compliance with no actual checking). Phase 2’s Datalog enforcement is what makes the library credible.

Alt 3: ship Phase 1 + 2, defer the std::mlt package wrapper (Phase 3)

Decorators + Datalog rules + diagnostics ship as part of the language; the std::mlt package is a thin re-export layer added later.

Rejected because it leaks MLT-specific names (categorizes, subordinates, etc.) into the language’s prelude. Keeping them library-prefixed (std::mlt::categorizes) maintains the neutrality claim.

Alt 4: full Carvalho-Almeida axiomatization (Theorems 1-8) in Lean before shipping

Mechanize every Carvalho-Almeida theorem in Argon/Locality/MLTAxioms.lean before allowing the Rust library to claim MLT compliance.

Rejected as too ambitious for v0.1. The substrate-sufficiency scaffold (MLTMetarelKind + classify_declOfKind theorem) discharges the expressibility claim; full axiomatization is a separate research effort (~24-38 person-months per Vault’s D-132 estimate). Defer to v0.2 or beyond.

Consequences

Wire format

No new axiom kinds. #[categorizes(T)] and its relational siblings desugar to canonical metarel_decl events; #[order(N)] desugars to a synthesized check declaration that emits a CheckDecl event keyed to OE1905. No new body types.

Lean changes

Phase 2 lands a Argon/Locality/MLTRules.lean (~400-600 LOC) that:

• Defines the seven CL-* rule shapes against Argon.MetaCalculus.MLTKinds.
• States the soundness theorem (CL-rules detect exactly the violations of Carvalho-Almeida’s axioms).
• Proof handle: parametric predicates in Wellformed.lean already capture the violation semantics; this module instantiates them against runtime tuples.

Rust changes

Phase 1: oxc-parser decorator recognition + oxc-instantiate decorator-to-metarel lowering. ~300-500 LOC.

Phase 2: oxc-reasoning admits built-in rules; oxc-runtime lifts violation tuples to diagnostics. ~800-1200 LOC.

Phase 3: std::mlt package declaration in packages/std-mlt/ with re-exports. ~100-200 LOC.

Diagnostic surface

The #[order(N)] assertion is the first MLT diagnostic emitted from Phase 1 (the synthesized check rule fires under runtime evaluation but the check declaration itself lands in Phase 1’s parser/elaborator output). All other MLT diagnostics land with Phase 2’s CL-rule evaluator.

Per RP-003 GAP-4, the OE19xx codes are scheduled to migrate to the library namespace (mlt::E0001–mlt::E0008); v0.1 retains OE19xx for continuity with the rest of the diagnostic registry and tracks the migration as an open question below.

Documentation

Reference book §13 (or §5.x — placement TBD) gains a subsection on MLT-as-library, citing Carvalho-Almeida 2018. The §17 ARS substrate description references MLT as one of the foundational ontologies the substrate admits via library composition.

Open questions

• Phase 2 evaluation dispatch: CL-1..CL-7 are Datalog rules. They should run on the same executor as user-written derives. But CL-1..CL-7 are built-in, not modeler-written — should they be loaded as part of the runtime’s bootstrap, or shipped in a special “kernel” rule set? Affects how RFD 0003 (per-stratum backend dispatch) handles them.

• Cross-library MLT consistency: if a module uses both std::mlt and std::ufo, do their iof/specializes semantics align? UFO inherits MLT semantics by reference (per Vault’s “UFO Design Limitations”); BFO does not. The interaction needs RFD-level treatment.

• Order arithmetic via Lean universe inference vs explicit predicate: Vault’s Phase B1 + B2 work proposes mechanizing T2 substrate (Tarski-cumulative universes) so Lean’s elaborator infers order(T) automatically. v0.1 sticks with the explicit concept_order predicate; T2 mechanization is a separate research effort.

• MLT orderless types*: universe-polymorphic types per Sozeau-Tabareau 2014. v0.1 caps at order 2; MLT* unlocks unbounded order. Defer to v0.2.

• Powertype keyword deprecation: per Vault, pub powertype Name (categorizes|partitions) Target { instances } is currently hard-reserved in kind.rs:657 but marked for removal. The pattern system + decorator approach in this RFD obsoletes that surface. Removal unblocks pub metatype powertype = { ... } from user code. Coordinated removal with this RFD’s Phase 1.

• MLT decidability under unbounded order: at order ≥ 3, decidability becomes uncertain (Carvalho-Almeida 2018 is silent past order 2). If v0.2 admits MLT*, the decidability classifier needs an MLT-specific tier or a refinement to the existing metaorder tier.

• Backward compatibility of iof semantics: in MLT, iof(x, T) includes order arithmetic. In other foundational ontologies (UFO continuant, BFO universals), iof is order-agnostic. Module-local use std::mlt::* should NOT retroactively change iof semantics for non-std::mlt-using modules — but the runtime evaluator runs CL-1..CL-7 globally. Resolution: scope CL-1..CL-7 to predicates declared with MLT decorators (a metarel_decl.is_mlt_primitive flag added by Phase 1 decorator lowering).

• OE19xx → mlt::E* namespace migration (RP-003 GAP-4): the diagnostic codes in this RFD use the language-level OE19xx range, inherited from when MLT was substrate-embedded. Per the MLT-as-library commitment, library-namespaced codes (mlt::E0001–mlt::E0008, with the mlt:: prefix matching 09-higher-order.md:20) are the consistent endpoint. v0.1 keeps OE19xx for continuity with the existing registry; the migration is a coordinated rename across oxc-diagnostics, the Lean wellformedness module, and appendix-c-diagnostic-codes.md. Open question: do we migrate before or after Phase 2 emit sites land?

• Assertion-decorator pattern as a reusable mechanism: #[order(N)] is the first assertion-style decorator. The same pattern is the natural shape for forthcoming ontological libraries — #[potency(N)] in std::potency (deep-instantiation level), #[stratum(N)] in std::ml2, etc. Should std::core expose a generic assertion-decorator builder (a procmacro helper) so each library doesn’t re-implement the lowering? Or do we accept boilerplate per library and re-evaluate when a third library wants this pattern? v0.1 hard-codes #[order]’s lowering; revisit after std::potency is sketched.

• Vacuous-pass behavior under incomplete iof chains: #[order(N)] passes vacuously when has_order(X, _) is undefined at check time. This is the right default for incomplete-model development — but it means a modeler can ship a build with unverified assertions. Mitigation: the well_formed!() macro could escalate vacuous passes to warnings (OE1909 OrderAssertionUnverified) so modelers see what’s not yet covered. Decide whether to land that escalation in Phase 1 or defer.

• #[order(N)] on individuals: let Lassie : Dog #[order(0)] is admitted but redundant (individuals always have order 0). Should the elaborator reject as a useless annotation (W0001-style warning) or silently accept? Argument for accepting: agent-generated models may always emit it for symmetry; the redundancy is harmless. Argument for warning: signals to the modeler that they may be confused about what #[order] means. Lean toward silent accept for v0.1; revisit if it becomes a source of confusion.

Discussion log

2026-05-29 — #[order(N)] added, decorator set completed

Tiago Sales asked in chat whether the syntax for declaring a type’s MLT order should be a refinement on the meta-calculus (pub type Species <: Taxon where { meta(self).order == 2 }) or an attribute (@[order(2)]). Neither matched the substrate’s actual design — meta(x) returns a Metatype value, not an arithmetic carrier, and @[…] is the wrong sigil. The substrate’s design is that order is computed, not declared: it falls out of the iof chain as a fixpoint over the well-founded has_order/2 predicate.

The follow-up question was the load-bearing one: “is implicit ordering sufficient for the modeler?” Tiago’s argument — that explicit assertions help with incomplete-model checking, documentation, and agent guidance — settled the question. #[order(N)] becomes a std::mlt assertion decorator that verifies the modeler’s belief against the derived fixpoint, fail-loud on conflict, vacuous-pass on incomplete chain.

Changes made to this RFD in the 2026-05-29 revision:

1. Added #[order(N)] to the v0.1 decorator set as the canonical example of an assertion decorator (a new decorator kind alongside the existing relational decorators).
2. Completed the relational decorator set — added #[power_type_of(T)] (was missing) and renamed #[subordinates(M)] → #[subordinate_to(M)] (the §9 spelling, matching Carvalho-Almeida §3.4’s “A is subordinate to B” reading).
3. Added #[order_bound(N)] as the module-level tier decorator (was referenced in §9 / RP-003 but not enumerated in this RFD).
4. Fixed @[…] → #[…] throughout. The @[…] form was a typo against Procedural macros and every example in the reference book.
5. New diagnostic code OE1908 OrderAssertionMisplaced for #[order(N)] on inapplicable declarations (struct/enum/relation).
6. New subsection “Decorator kinds — assertion vs. relational” with the #[order(N)] design in full, including the three-state check outcome table (pass / fail / vacuous) and the ergonomic rationale.
7. New open questions: OE19xx → mlt::E* migration, assertion-decorator pattern as a reusable mechanism for std::potency / std::ml2, vacuous-pass behavior under incomplete chains, and the individual-redundancy question.