Mechanization provenance
This index maps each language feature to the Lean module(s) that mechanize it and the spec section it lives in. It is generated from the feature registry, and CI verifies that every cited module exists — a feature naming a vanished mechanization fails the build.
| Feature | § | Lean module(s) | RFD |
|---|---|---|---|
| Module extraction (⊥-locality) | §3 | Locality/Locality.leanLocality/ScopedConservativity.lean | — |
mod, use, visibility, multi-file build, ox.toml package | §3 | CoreIR/Path.lean | 0022 |
| The meta-calculus (metaxis / metatype / metarel) | §4 | Substrate/MetaCalculus.lean | — |
abstract / fixed declaration modifiers | §4 | Runtime/ModifierGates.lean | 0027 |
Concepts (type baseline; declared classifying vocabulary) | §5 | — | 0038 |
Facts pub fact / strong negation pub not_fact | §5 | Storage/AxiomEvent.lean | 0010 |
| First-class relations | §5 | Substrate/RelationSubsumption.lean | 0005 |
Relation subsumption R2 <: R1 | §5 | TypeSystem/RelationExtension.lean | 0005 |
struct / enum data declarations | §5 | Substrate/Construct.lean | — |
Field intents T / T? / Truth4Of<T> | §6 | Foundation/Truth4Of.lean | 0007 |
Generics, collections ([T] / Set / Map / Option), function types | §6 | Syntax/TypeExpr.lean | — |
Instance-of : clause (cross-level) | §6 | MetaCalculus/IsCanNot.lean | — |
Mutable fields mut + update | §6 | Runtime/MutationSemantics.lean | 0006 |
Numeric tower — Top/Bot, exact Decimal/Real, result widening | §6 | Runtime/AggregateExact.lean | 0016 |
Refinement: iff (defined) vs where (primitive) | §6 | TypeSystem/Realization.lean | 0017 |
Specialization <: (subtyping) and a concept hierarchy | §6 | TypeSystem/Subtyping.lean | — |
| World assumptions — CWA default + per-concept OWA opt-in (`#[world(open | closed)]`) | §6 | Schema/WorldAssumption.leanTypeSystem/Soundness/CwaOwa.lean |
Aggregates count / exists / sum / min / max / avg | §7 | Runtime/AggregateExact.lean | 0011 |
Defeasibility — honest heads + defeat directive (#[default] / #[defeats] / #[label]) | §7 | Reasoning/Defeasibility/Transform.leanTypeSystem/Soundness/Defeasibility.lean | 0028 |
Defeasibility — proof tags (+Δ / +∂) | §7 | Reasoning/Defeasibility/Transform.lean | 0028 |
Modal box / diamond (fixed-default) | §7 | Reasoning/Modal.lean | — |
| Recursion-through-negation (well-founded semantics) | §7 | Reasoning/Datalog/WellFounded.lean | — |
Removed defeasible strength triple (#[strict] / #[defeasible] / #[defeater] / #[priority]) | §7 | — | 0028 |
| Rule-atom forms: predicate, comparison, NAF, type-test, field projection | §7 | Reasoning/Rule.lean | — |
Sinks (pub sink, emit) | §7 | — | 0015 |
Stable models (#[brave]) | §7 | Reasoning/Stability.lean | 0003 |
Temporal rule atoms (since, until, ever, …) / FOL quantifiers | §7 | Reasoning/Temporal.leanDecidability/Temporal.lean | — |
Universal quantifier forall v: T where Body, Head | §7 | Reasoning/Rule.lean | — |
#[comptime] build-time lifting | §7 | Substrate/Comptime.lean | 0002 |
check (consistency observers) | §7 | Reasoning/Checks.leanReasoning/StaticDischarge.lean | 0025 |
derive (recursive head-population) | §7 | Reasoning/EvalProgram.leanReasoning/Stratification.lean | — |
fn (pure compute) | §7 | CoreIR/Lowering.lean | — |
mutate — Datalog-style body | §7 | Runtime/MutationSemantics.lean | — |
mutate — imperative body | §7 | Runtime/MutationSemantics.lean | 0015 |
query (read-only) | §7 | Runtime/EngineModuleStore.lean | — |
| MLT level theory as an unprivileged package | §8 | — | 0043 |
Reflective rule-body intrinsics (iof / meta / specializes / extent) | §8 | MetaCalculus/Reflect.lean | 0023 |
TypeRef reflective type-as-value | §8 | Storage/CatalogProjections.lean | 0023 |
| Decidability tier ladder (classifier + per-tier admittance) | §9 | Decidability/Tier.leanDecidability/Classifier.leanDecidability/Admittance.lean | — |
| Decidability — Expressive tier | §9 | Decidability/Expressive.lean | 0003 |
Decidability — Fol tier (unsafe logic { }) | §9 | Decidability/FOL.lean | — |
| Decidability — Metaorder tier | §9 | Decidability/MetaOrder.lean | — |
| Decidability — Modal tier | §9 | Decidability/Modal.lean | — |
| Decidability — Structural / Closure / Recursive tiers | §9 | Decidability/Structural.leanDecidability/Closure.leanDecidability/Recursive.lean | — |
| Polynomial bound on type-graph (D1) evaluation | §9 | Decidability/Complexity/Bounds.leanDecidability/Domain1/Eval.lean | — |
Bridge rules pub bridge | §11 | Standpoint/Federation.lean | — |
| Federation policies (paraconsistent / strict / weighted) | §11 | Standpoint/Consistency.lean | — |
| Sheaf semantics (categorical) | §11 | Locality/SheafEquivalence.lean | 0008 |
Standpoint declarations, lattice <:, standpoint-block scoping | §11 | Standpoint/Visibility.lean | — |
| Standpoints and four-valued federation (Truth4) | §11 | Standpoint/Federation.leanFoundation/Truth4.lean | — |
Truth4 (is / not / can / both) | §11 | Foundation/Truth4.lean | — |
Macros — declarative pub macro, procedural #[procmacro] | §12 | Substrate/Macro.lean | 0037 |
| Traits (behavioral contracts + dispatch) | §12 | TypeSystem/Conformance.leanSubstrate/Trait.lean | 0026 |
ox build → .oxbin (preamble, four version axes, validation, content hash) | §16 | BuildArtifact/Oxbin.leanBuildArtifact/Validation.lean | — |
Bitemporal stamps + time-travel (query … as_of) | §17 | Runtime/AsOf.lean | — |
Forks, hot reload, retention / forget capability | §17 | Runtime/Capability.lean | — |
In-language tests (the test declaration) | §17 | Storage/AxiomKind.lean | 0048 |
Runtime serving ox runtime serve (/v1) | §17 | Conformance/Envelope.lean | 0014 |
| Two-layer incremental cache (compile + runtime) | §17 | Runtime/SalsaContract.lean | — |
Module / Store, execute_mutation, query_* | §17 | Runtime/EngineModuleStore.lean | — |