Get Started

This is the entry point for new users learning pr4xis. It is a three-step tutorial sequence — each step is a short, focused page you can complete in 10 minutes or less. By the end you will have pr4xis built locally, made your first query against the engine, and written your own minimal ontology! block.

The sequence

1. 01 — Install — clone, build, run the test suite. Verifies your environment.
2. 02 — First Query — interact with the engine through the CLI chatbot or the WASM browser demo, and learn how to read the trace.
3. 03 — Your First Ontology — write a minimal ontology! block of your own, and watch the categorical machinery validate it.

Each page links forward to the next, and back to this index. You can also jump straight in if you already know what you need.

After the tutorial

Once you have completed the three steps, the next layer of docs depends on what you want to do:

• Use pr4xis as a library in your own service or research project → Architecture
• Add a real ontology from a published paper → Build an ontology from a paper
• Compose two ontologies with a verified functor → Compose via functor
• Write a domain axiom → Write axioms
• Understand the categorical machinery deeply → Concepts, Foundations
• See the most distinctive concrete result → Gap detection

If you get stuck, file an issue — broken queries are bug reports, not user error.

• Document date: 2026-04-14

01 — Install

The first step in the Get started tutorial sequence. After this page you will have pr4xis built locally and the test suite green.

Prerequisites

• A Rust toolchain — version 1.85 or later, edition 2024. The simplest install is via rustup.
• git.
• About 1 GB of free disk space for the build artifacts (the target/ directory grows during compilation).

If you use Nix, the project ships with devenv configured. After cloning, devenv shell drops you into a fully-configured environment with the right Rust version, cargo-nextest, treefmt, and other dev tools already on the path. You do not need to install Rust separately.

Clone and build

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo build --workspace

The first build pulls dependencies and compiles the seven workspace crates. Expect 2-5 minutes on a modern machine, longer on first run.

Verify with the test suite

cargo test --workspace

This runs the entire test suite — more than 7,000 tests across the workspace, including category laws, functor laws, axiom checks, and property-based tests via proptest. A release run on a multi-core machine takes a few minutes. You should see something like:

test result: ok. <N> passed; 0 failed; ...

If anything fails, that is the bug report. File an issue with the failing test name and your toolchain version. Pre-existing test failures are not normal — the workspace is meant to be green at every commit on master.

Optional: run the property-based tests with more iterations

The default proptest budget is 256 cases per property, which is enough for routine CI but may miss subtle counterexamples. To run with a larger budget:

PROPTEST_CASES=10000 cargo test --workspace

This is slower (5-10 minutes) but exercises a much wider input space. Use it before submitting a PR that touches reasoning-system code or category-law-checking infrastructure.

Fetch the WordNet data

The English ontology is built from a WordNet XML file that is not checked into the repository, so a fresh clone does not have it yet. The CLI in 02 — First Query needs it and will refuse to start without it. Fetch it once:

pr4xis update wordnet

If you use Nix, the dev-data dev script wraps the same pr4xis update step. The file lands at crates/domains/data/wordnet/english-wordnet-2025.xml; set WORDNET_XML if you keep it elsewhere.

What you have now

• A working pr4xis workspace built from source
• The full test suite passing
• A target/ directory with the pr4xis-cli and pr4xis-web binaries
• The full source for the domain ontologies under crates/domains/src/
• The WordNet data fetched and ready for the CLI

Next

Continue with 02 — First Query to interact with the engine, either through the CLI chatbot or the WASM browser demo.

• Document date: 2026-04-14

02 — First Query

The second step in the Get started tutorial sequence. After this page you will have made your first interaction with the pr4xis engine, in your browser, with the same WASM build that runs in production.

This page assumes you have already completed 01 — Install.

Option A (recommended): Local WASM via dev-web

dev-web is a workspace-provided dev script that builds the WASM bundle, watches crates/ for changes, and serves the chat surface locally with live reload. The interaction runs entirely in your browser tab — sandboxed, no local process to manage, exactly the same code path as the production pr4xis.dev demo.

dev-web

You will see something like:

Building WASM...
Starting pr4xis-web with live reload...
  /                — WASM chatbot
  /decks/technical — presentation
Watching crates/ for changes — WASM rebuilds automatically.

Open the URL it serves — dev-web prints the address and port on startup (currently http://localhost:4096). The page loads the English ontology (~107K WordNet concepts compiled into the WASM binary at build time) and gives you a chat input.

If you don’t have dev-web on your path, you are not in the dev shell. Run devenv shell first if you use Nix, or fall back to Option B below.

Try a few queries

is a cat a mammal
define telescope
is a guitar a string instrument

The system tokenizes each input, parses it through the Lambek pregroup grammar, looks up the entities in the WordNet taxonomy, and answers from the loaded category. The trace pane shows every step the engine took.

What you should expect

The chat surface is a working surface, not a polished product. Three classes of behavior you will see:

1. Clean derivation. The query parses, the entities resolve, the taxonomy traversal answers. The trace shows every step.
2. Honest “no” with a reason. The query parses, but the answer doesn’t follow from the loaded ontology. The system says so. This is correct behavior — pr4xis cannot make up answers that aren’t in its axioms.
3. Grammar gap. The query doesn’t fit the current pregroup parser coverage. The system says so. This is a bug report — file an issue with the exact input.

The third case is the one we care most about closing. Pr4xis will get better the more grammar gaps users surface.

Option B: The CLI chatbot (no browser)

If you cannot use dev-web for any reason, the same engine ships as a CLI:

cargo run -p pr4xis-cli

This starts a chat loop in your terminal. It loads the English ontology from the WordNet XML you fetched in 01 — Install; if that file is missing it stops with a message pointing you at pr4xis update wordnet. With the data in place it runs the same engine on the same ontology and gives the same answers — it prints the response text for each query rather than the browser’s live trace pane. Useful for headless servers, CI debugging, or anywhere a browser isn’t available.

Option C: The hosted demo

If you don’t want to run anything locally at all, open pr4xis.dev. Same WASM build as Option A, hosted as a static site. Loads the English ontology at startup (a few seconds), then accepts the same queries.

Inspecting the trace

The browser surfaces (Options A and C) render a structured trace for each query. The trace is a sequence of PipelineTraceEntry records, one per pipeline stage:

1. Tokenize — input → TypedToken[]
2. Parse — tokens → Lambek pregroup reduction
3. Interpret — parse tree → Montague semantic form
4. Speech act classification — what kind of thing the user said
5. Metacognition — which response strategy fits
6. Entity lookup / taxonomy traversal / common ancestor / etc. — the actual reasoning
7. Realization — semantic answer → human-readable text

When something goes wrong, the trace is where you look first. Every entry tells you which ontology produced it, which operation was performed, and whether it succeeded.

What you have now

• A working interaction with the pr4xis engine
• A sense of which queries land cleanly and which don’t
• A way to see the full reasoning trace for any query

Next

Continue with 03 — First Ontology to write your own minimal ontology! block.

• Document date: 2026-04-14

03 — Your First Ontology

The third step in the Get started tutorial sequence. After this page you will have written a minimal ontology! block, run its tests, and seen the categorical machinery validate your definition.

This page assumes you have completed 01 — Install and 02 — First Query.

What we’ll build

A toy ontology of musical instrument families. Three concepts (string, wind, percussion) that subsume an Instrument parent. Small enough to read in one sitting; complete enough to show every part of the macro pattern.

For a real-world authoring workflow against a published source paper, see Build an ontology from a paper. This page is the toy version that gets you familiar with the macro syntax.

Step 1: Make a place for it

Inside the workspace, create a new directory and module:

mkdir -p crates/domains/src/social/music_intro
touch crates/domains/src/social/music_intro/{mod.rs,ontology.rs,tests.rs}

Add the module to crates/domains/src/social/mod.rs:

pub mod music_intro;

Step 2: Write the ontology

In crates/domains/src/social/music_intro/ontology.rs:

pr4xis::ontology! {
    name: "MusicalInstruments",
    source: "tutorial example, not a published paper",

    concepts: [Instrument, String, Wind, Percussion],

    labels: {
        Instrument: ("en", "Instrument", "A musical instrument family."),
        String: ("en", "String", "Instruments that produce sound via vibrating strings."),
        Wind: ("en", "Wind", "Instruments that produce sound via vibrating air columns."),
        Percussion: ("en", "Percussion", "Instruments that produce sound by being struck."),
    },

    is_a: [
        (String, Instrument),
        (Wind, Instrument),
        (Percussion, Instrument),
    ],
}

The ontology! proc macro (pr4xis::ontology, re-exported from pr4xis-derive) expands this into:

• A MusicalInstrumentsConcept enum implementing Concept (Guarino 2009 — closed-world named objects)
• A MusicalInstrumentsCategory struct implementing Category (Mac Lane 1971 Ch. I §1)
• A MusicalInstrumentsRelation struct + MusicalInstrumentsRelationKind enum implementing Arrow — every is-a row becomes a Subsumption-kinded morphism (Awodey 2010 §1.3)
• An Ontology impl whose fn axioms() returns the structural axioms for every kind in use — for Subsumption the catalog (OBO-RO; Smith et al. 2005) emits NoCyclesOnKind (Tarski 1941) + AntisymmetricOnKind automatically
• A fn meta() -> Provenance carrying the name: + source: for trace attribution

Everything is type-checked: a typo in a concept name fails at compile time, not at test time.

Step 3: Write a test

In crates/domains/src/social/music_intro/tests.rs:

use super::ontology::*;
use pr4xis::category::laws::assert_category_laws;
use pr4xis::category::{Arrow, Category, Concept};
use pr4xis::ontology::Ontology;

#[test]
fn category_laws() {
    assert_category_laws::<MusicalInstrumentsCategory>();
}

#[test]
fn ontology_validates() {
    MusicalInstrumentsOntology::validate()
        .unwrap_or_else(|c| panic!("validation failed: {}", c.meta().description.as_str()));
}

#[test]
fn string_is_an_instrument() {
    let m = MusicalInstrumentsCategory::morphisms();
    assert!(m.iter().any(|r| r.source() == MusicalInstrumentsConcept::String
        && r.target() == MusicalInstrumentsConcept::Instrument
        && r.kind() == MusicalInstrumentsRelationKind::Subsumption));
}

In mod.rs:

pub mod ontology;

#[cfg(test)]
mod tests;

pub use ontology::*;

Step 4: Run the tests

cargo test -p pr4xis-domains music_intro

You should see three passing tests:

test social::music_intro::tests::category_laws ... ok
test social::music_intro::tests::ontology_validates ... ok
test social::music_intro::tests::string_is_an_instrument ... ok

If they pass, your category obeys identity and associativity (Mac Lane 1971), your subsumption edges form a valid DAG (NoCyclesOnKind + AntisymmetricOnKind from the catalog), and your encoding of “string is an instrument” is queryable as a kinded morphism.

If a test fails, the returned Counterexample names the specific law or axiom that failed. Fix the encoding and re-run — usually the issue is a cycle in is_a: or a typo in a concept name.

What just happened

You wrote three lines of taxonomy data and got back:

• A category with verified composition and identity laws
• Subsumption edges with verified NoCycles + Antisymmetric axioms inherited automatically from the structural-axioms catalog
• A type-checked concept enum
• A test suite that re-runs every law on every commit

That’s the value of ontology! — most of the categorical machinery is auto-generated from the declarative spec, and the parts that aren’t are auto-tested.

What you can do next

• Add parthood. What are the parts of a string instrument? (body, neck, strings, tuning pegs.) Add a has_a: sugar clause to the macro. The catalog will attach NoCyclesOnKind for the Parthood kind automatically. If you need WeakSupplementation (Casati & Varzi 1999), add it as a hand-written domain axiom in your Ontology::axioms() impl.
• Add a quality. What measurable property does an instrument have? (pitch range in Hz.) Implement the Quality trait for a marker struct and wire it as type Qual = … in your Ontology impl.
• Compose with another ontology. Pr4xis already has a music ontology at crates/domains/src/natural/music/. Write a Functor from MusicalInstrumentsCategory to the music category. Run check_functor_laws to verify identity + composition preservation.
• Add a domain axiom. “A string instrument has at least one string.” Implement Axiom (with verify() + citation()) and push it onto the vec returned by Ontology::axioms() alongside the catalog’s structural axioms.

For each of these, see the matching how-to guide:

• Compose via functor
• Write axioms
• Build an ontology from a paper — the real-world authoring workflow

What you have now

• A complete ontology! block in the workspace
• A test suite that exercises the category laws, the structural axioms from the catalog, and a worked example query
• A starting point for adding your own real-world ontology — the macro pattern is the same, just with more concepts and more kinds of edges

Where to go from here

• Concepts — what the categorical machinery you just plugged into actually means
• Architecture — the five-layer stack and how ontology! fits into it
• Build an ontology from a paper — the next-level authoring workflow
• Domain catalog — the existing ontologies you can use as patterns

• Document date: 2026-05-14

Build an Ontology from a Paper

This page is the contributor’s authoring guide for adding a new ontology to pr4xis from a published source. Tracked in #44.

Before you start

Open one of the existing ontologies and read the source. The biology ontology at crates/domains/src/natural/biomedical/biology/ontology.rs is the canonical reference example — small enough to read in one sitting, complex enough to show all the patterns. Compare it to its source paper (Alberts et al., Molecular Biology of the Cell, 6th ed.) by reading both side by side. The mapping from “what the paper says” to “what the ontology! block contains” is the workflow you will follow.

The workflow

Step 1: Pick a source

Authoritative, citable, and finite. Examples:

• A textbook chapter (Alberts on cells, Sola on quaternions, Riehl on category theory)
• A standards document (W3C OWL spec, ECMA JSON spec, IEC color spec)
• A peer-reviewed paper (Lambek 1958 on pregroup grammars, Conant-Ashby 1970 on the Good Regulator Theorem)
• A foundational technical reference (Mac Lane’s Categories for the Working Mathematician)

Avoid: blog posts, Wikipedia pages, AI summaries, your own notes. The point of pr4xis is that every axiom traces to a source you can put in a bibliography.

Step 2: Extract the concepts

Read the source carefully and list the named things it talks about. These become the variants of your Concept enum (Guarino 2009 — closed-world named objects). For the biology ontology, the source paper named: cell, tissue, organ, organism, stem cell, fibroblast, columnar epithelial cell, etc.

Two rules:

• One name, one concept. If the paper uses two names for the same thing, pick one and note the alias in a comment. If it uses one name for two things, that’s a context-dependent concept and you’ll need a ContextDef to disambiguate (see Concepts).
• Concepts, not values. “Cell” is a concept; “10 micrometers” is a value (a Quality attached to a concept, not its own entity).

Step 3: Extract the relations

For each pair of concepts, ask: does the source say one is a kind of the other? a part of the other? a cause of the other? an opposite of the other? Each answer becomes a kinded morphism, and the structural-axioms catalog attaches the right axioms automatically (OBO-RO; Smith et al. 2005):

• Subsumption (is_a): “a fibroblast is a kind of cell” → (Fibroblast, Cell) — catalog attaches NoCyclesOnKind + AntisymmetricOnKind
• Parthood (has_a): “a cell membrane is part of a cell” → (CellMembrane, Cell) — catalog attaches NoCyclesOnKind
• Causation (causes): “stem cell division causes cell differentiation” → (StemCellDivision, CellDifferentiation) — catalog attaches AsymmetricOnKind + IrreflexiveOnKind (Lewis 1973; Reichenbach 1956)
• Opposition (opposes): “M1 macrophages are the functional opposite of M2 macrophages” → (MacrophageM1, MacrophageM2) — catalog attaches SymmetricOnKind + IrreflexiveOnKind

The source is the authority. If the source says it, the relation goes in. If the source doesn’t say it, the relation does not go in — even if it “feels obvious”.

Step 4: Write the ontology! block

The macro takes a declarative spec and emits the full implementation. Skeleton:

pr4xis::ontology! {
    name: "MyOntology",
    source: "<Author, Title, Year, Edition>",

    concepts: [ParentConcept, ChildConcept, Part, Whole, /* … */],

    labels: {
        ParentConcept: ("en", "Parent concept", "One-line description."),
        // … one row per concept …
    },

    is_a: [
        (ChildConcept, ParentConcept),
        // … one row per is-a relation in the source
    ],

    has_a: [
        (Part, Whole),
        // … one row per part-of relation in the source
    ],

    // Omit any sugar clause the source doesn't motivate.
    // For arbitrary kinded morphisms, use `edges: [(Source, Target, Kind)]`.
}

The macro generates the MyOntologyConcept enum (Concept impl), the MyOntologyCategory struct (Category impl), the MyOntologyRelation + MyOntologyRelationKind (Arrow impl with kind tagging), an Ontology impl whose fn axioms() returns the catalog’s structural axioms for every kind in use, and a type-level fn meta() -> Provenance carrying the name: + source: for trace attribution. Run cargo test -p pr4xis-domains to verify the laws hold.

Step 5: Add the citation

Create a citings.md file alongside ontology.rs (per #57, once that lands) listing every source the ontology stands on. For each source: full citation, DOI or URL, and one-line annotation of which concepts or axioms it grounds. The README of the ontology directory points at the citings file.

Step 6: Add Quality types where the source quantifies

If the source paper says “neurons fire when the membrane potential exceeds −55 mV”, the threshold is a Quality attached to the Neuron concept. Implement the Quality trait for a marker struct, wire it as type Qual = … in your Ontology impl, and write a unit test that exercises the value.

Step 7: Add domain axioms

Structural axioms (no cycles, antisymmetric subsumption, symmetric opposition, …) are inherited automatically by the macro via structural_axioms_for::<Self::Cat>() in Ontology::axioms(). Domain axioms are the constraints that come from the source paper: “neurons cannot have more than one axon”, “an enzyme catalyzes exactly one reaction class”, “a chess king moves at most one square per turn”, “if a whole has a proper part, it has another disjoint part” (Casati & Varzi 1999 WeakSupplementation). Implement each as an Axiom impl (with verify() returning a typed Verdict and a citation() to the source) and push it onto the vec returned by Ontology::axioms().

Step 8: Compose with other ontologies

If your new ontology shares concepts with an existing one, write a functor. Example: if you’re adding a hematology ontology and pr4xis already has a biochemistry ontology, the cells in your hematology ontology need to map to the biochemistry’s cellular processes. Create a HematologyToBiochemistry functor, implement map_object and map_morphism, and run check_functor_laws. If the laws pass, the composition is verified — your ontology can now be queried alongside biochemistry through the composed functor.

Step 9: Run the full suite

cargo test --workspace

If anything that was passing is now failing, you have introduced a contradiction with an existing ontology. Either the new source disagrees with the old source (in which case both are documented and the disagreement is explicit), or your encoding has a bug. Diagnose and fix.

What to skip

• Don’t encode “common sense” that isn’t in the source. Even if it feels obvious. The point of pr4xis is that every claim is sourceable. If you encode common sense, you will eventually contradict someone else’s source.
• Don’t encode terminology debates. If the field has multiple naming conventions, pick the one the source uses and document the others as aliases.
• Don’t encode contested facts. If the source itself flags a claim as disputed, encode it as a disputed: true quality, not as a hard axiom. (This pattern is in flight — see existing ontologies for examples.)

Where to get help

• Look at existing ontologies first. crates/domains/src/natural/biomedical/biology/ontology.rs is the reference. Pick another close to your domain and pattern-match.
• The ontology! proc macro source at crates/pr4xis-derive/src/ontology.rs documents every supported field; the surrounding lib.rs carries an example.
• Concepts explains what each reasoning system means, with worked examples.
• Architecture explains where the ontology fits in the larger stack.

When you’re done

Open a PR. The CI will run cargo test --workspace, check formatting, run clippy, and verify the WASM build. If all pass, your ontology is in.

Related

• Compose via functor — how to write a cross-domain functor
• Write axioms — how to write a domain axiom that the engine enforces
• Concepts — the categorical machinery you’re plugging into
• Glossary — every term defined
• #44 — the issue this doc closes

• Document date: 2026-04-14

Register a Source

This page is the operator’s guide for telling praxis about an external source — a published artifact the engine should reason about (a statute text, a lexicon dump, a regulation) — and managing its on-disk copy from the command line.

A registered source has three pieces, all at the workspace root:

• A manifest entry in praxis.toml that names the source, its version, its SourceTaxonomy type, and the authoritative URL.
• A lock entry in praxis.lock that pins the source’s content digest so any drift between the registered identity and the on-disk bytes is detected at startup by the LockManifestAgreement axiom.
• The on-disk artifact at the path RegistryEntry::local_path() derives from the type — e.g. crates/domains/data/wordnet/english-wordnet-2025.xml for the registered Language source.

The runtime side is the engine’s data-provisioning subsystem (pr4xis_domains::applied::data_provisioning); the operator side is the pr4xis update CLI.

The manifest — praxis.toml

One [sources.<name>] block per registered source. Schema:

[sources.<name>]
version     = "<publication identifier>"
type        = "<SourceTaxonomy leaf concept>"
url         = "<https URL of the authoritative source>"
description = "<one-line human description>"

• name is a snake-case identifier. Convention: <short>_<section> for statutes (sox_1514a, air21_42121), <short>_<rule> for procedural rules (frcp_rule_17), <plaintiff>_v_<defendant>_<year> for case law.
• version is free-form — calendar year, amendment cycle, edition. Not semver; legal corpora are publication-date identified.
• type must be a leaf concept name from the SourceTaxonomy ontology (Language, UsFederalStatute, Regulation, ProceduralRule, CaseLaw, …). Unknown types fail closed at startup.
• url is the authoritative source URL. For US federal statutes that means LRC USLM XML on uscode.house.gov/download/releasepoints/... per 1 U.S.C. § 204 (the Office of the Law Revision Counsel is the statutory codifier; USLM is its published XML form). For case law it means the issuing court’s published opinion (typically PDF). For other sources, the standard cites the canonical edition. Secondary republications (Cornell LII for statutes, justia.com for cases) are not authoritative — encode the canonical source.

The reference example is the WordNet entry:

[sources.english_wordnet]
version = "2025"
type    = "Language"
url     = "https://github.com/globalwordnet/english-wordnet/releases/download/2025-edition/english-wordnet-2025.xml.gz"

The lock — praxis.lock

Two layers of pinning:

• [hashes] — <name>@<version> = "blake3:<hex>". The content digest of the bytes praxis expects on disk at local_path(). This pin is the persisted form of a typed IntegrityClaim (W3C Subresource Integrity): it binds the source to its expected content hash rather than trusting any self-asserted label. LockManifestAgreement verifies every manifest entry has a matching hash and that the local file (when present) re-derives to it.
• [canonical_text."<name>@<version>"] (optional, source-specific) — for sources whose authoritative format praxis cannot yet read end-to-end (e.g. case-law PDFs whose figures or non-text content require future image-understanding work), a hand-transcribed plain-text approximation lives under data/canonical_text/, with sha256 + provenance flags. provenance = "training_reconstructed_<date>" marks the file as a transcription pending verification against the authoritative source; provenance = "verified" marks it as a fetched-and-confirmed copy. This is an explicit, machine-readable record of the gap — not a workaround. Statutes don’t need this: USLM XML reads end-to-end through the loaded W3C XML 1.0 parser + USLM lens.

The [structural."<name>@<version>"] block is a legacy codegen input retained for sources whose loader hasn’t yet been wired into the build-time codegen path. For statutes, M4.δ.2.b wired the USLM XML loader into build.rs, so the source-driven path consumes USLM XML directly — [structural.*] is being deleted for statutes per task M4.δ.2.e. See Build an Ontology from a Paper for the declarative authoring path that’s parallel to source-driven ingestion.

The CLI — pr4xis update

The CLI’s data-provisioning surface. All flags work the same for every registered source.

pr4xis update

Fetches every registered source, verifies bytes against praxis.lock, writes verified output to local_path(). Runs through every entry regardless of per-entry failures so you get a full report. Re-running after a successful fetch short-circuits via local re-verification, so invocations are idempotent.

pr4xis update

Output is one line per source:

  [ok]      english_wordnet: already verified
  [fetched] english_wordnet: 47 MB written to crates/domains/data/wordnet/...
  [fail]    foo_source: verification failed — content-digest mismatch

pr4xis update <name>

Single dataset by registered name. Useful when only one source needs refreshing.

pr4xis update english_wordnet

Unknown names fail fast: pr4xis update: unknown dataset: foo.

pr4xis update --check

Read-only mode: verify the current on-disk state against the lock without touching the network. --check always wins over --force — pr4xis update --check --force ignores force and only verifies. Useful in CI air-gapped steps and pre-commit hooks.

pr4xis update --check

pr4xis update --force

Re-fetch even when a valid local copy already exists. Useful when the upstream URL has new content under the same version label (unusual for legal corpora, common for development manifests).

pr4xis update english_wordnet --force

pr4xis update --list

Print every registered source with its current state. Includes the schema-derived information — version, taxonomy kind, content-type, on-disk path:

Registered datasets:
  english_wordnet@2025 [Language] An open lexical database of English.
    remote: https://github.com/globalwordnet/english-wordnet/releases/...
    local:  crates/domains/data/wordnet/english-wordnet-2025.xml
    content-type: XmlLmf
  usc_title_18@pl-119-90 [UsCodeTitle] Crimes and Criminal Procedure.
    remote: https://uscode.house.gov/download/releasepoints/us/pl/119/90/xml_usc18@119-90.zip
    local:  crates/domains/data/legal/uscode/...
    content-type: UslmXml
  …

Individual sections (18 U.S.C. § 1514A SOX, 49 U.S.C. § 42121 AIR21, etc.) are not separate datasets — they are URN-addressable slices of the registered title. To resolve one at runtime: UsCode::loaded().section_by_urn("/us/usc/t18/s1514A").

pr4xis update --offline

Refuse to touch the network. Local files are still verified; an absent file reports as MissingAndOffline rather than fetching. Useful for air-gapped builds.

pr4xis update --offline

Flag precedence: --check (read-only) always wins over --force. --offline blocks network access; if a local file exists it is still verified, and verification failure is reported as VerificationFailed (not MissingAndOffline, which is reserved for actually-absent files).

pr4xis update --lock

Regenerate praxis.lock pins, preserving comments and key ordering; values are written in the tagged blake3:<hex> form. Two modes:

• --lock alone: downloads every (or one named) registered entry, bypasses identity verification, writes the bytes to disk, computes the content address, and rewrites the corresponding [hashes] line — the path to pin a source for the first time, or to re-pin after the upstream bytes legitimately change.
• --lock --offline: the custody re-pin — no network. Every on-disk source must first verify against its existing pin (under whatever algorithm that pin names); only then are the [hashes], [byte_exact_signatures], and [canonical_signatures] entries rewritten under the emit algorithm. Any mismatch aborts the whole run before praxis.lock is touched.

--lock is mutually exclusive with --check (read-only).

pr4xis update --lock                 # re-pin every registered source
pr4xis update english_wordnet --lock # re-pin one source

Use --lock deliberately — it trusts the freshly fetched bytes rather than checking them against an existing pin, so it should run only when you intend to update the recorded identity.

Planned: pr4xis source add / remove / list (M6)

A separate source subcommand for mutating the registry — adding a new entry, removing an existing one, or listing without going through update — is task M6 in the milestone plan, not yet implemented. Today the registry is read-only from the CLI’s perspective; pr4xis update --list prints it but cannot edit it, and new entries are added by hand-editing praxis.toml. When M6 lands, hand edits will remain valid (the file is the source of truth either way) and pr4xis source add <name> --version <v> --type <leaf> --url <url> will automate the common case.

Adding a new source

End-to-end. The current workflow is hand-edit-then-verify; mutating subcommands (pr4xis source add / remove / list) are planned as M6 — registry CLI mutators and not yet implemented. Manual edits are the canonical path until then.

1. Choose a leaf in SourceTaxonomy under crates/domains/src/formal/meta/source_taxonomy/ontology.rs. If no existing leaf fits the jurisdictional or genre specificity of your source, add a new leaf first — the taxonomy is closed-world and unknown types fail registration at startup.
2. Append a [sources.<name>] block to praxis.toml with the four required fields. Use the authoritative URL. (M6 will let pr4xis source add <name> --version <v> --type <leaf> --url <url> do this; today it’s a hand edit.)
3. Pin the digest in praxis.lock’s [hashes] block — run pr4xis update <name> --lock to fetch the bytes and write the tagged blake3: pin for you.
4. Run pr4xis update <name> to fetch and verify. The CLI writes the verified bytes to local_path(). Subsequent runs are no-ops unless you pass --force.
5. Verify with cargo test — the data-provisioning ontology runs LockManifestAgreement (along with seven other axioms) over the registered set; any drift fails.

Note that the runtime registry is OnceLock-cached per process, so a running process only sees entries present at first load. After hand-editing praxis.toml you need to restart any long-running praxis process to pick up the new entry.

What’s automated end-to-end today

The reference instance is WordNet (sources.english_wordnet): registered → manifest+lock pinned → pr4xis update fetches .xml.gz from GitHub Releases → decompresses → writes .xml → verifies → engine consumes via build-time codegen. Every step is machine-driven and reproducible.

The registered US statutes are whole U.S. Code titles in USLM XML published by the LRC (Office of the Law Revision Counsel) per 1 U.S.C. § 204 at uscode.house.gov/download/releasepoints/.... usc_title_18 (Crimes), usc_title_49 (Transportation), and usc_title_28 (Judiciary, including the Federal Rules of Civil Procedure / Evidence / Appellate Procedure / Bankruptcy Procedure as appendices) are registered at release point pl-119-90. Individual sections like 18 U.S.C. § 1514A (Sarbanes–Oxley § 806) and 49 U.S.C. § 42121 (AIR21) are URN slices of the registered title, not separate sources — UsCode::loaded().section_by_urn("/us/usc/t18/s1514A") returns the typed Statute via the bytes ⇄ Statute composed lens (M4.λ.3.b, shipped).

The end-to-end pipeline for a registered USLM XML title:

• The bytes are fetched as a .zip from uscode.house.gov, verified against praxis.lock, unzipped, and the usc<N>@<release>.xml file lands at local_path().
• The bundled W3C XML 1.0 parser (crates/domains/src/social/software/markup/xml/parser/) reads it into a typed XmlDocument — the same parser the M5.ω audit confirmed is 100% xmlconf-conformant.
• The USLM ontology (uslm/) types the document tree, with every concept’s identity grounded in the loaded LRC USLM XSD (M4.ε.5.a — XSD-grounded USLM ontology). Container kinds, subdivision kinds, additional containers, and the codegen tokenizer config all derive from the XSD’s substitutionGroup="level" membership (Batches D + E of M5.ω).
• The UslmStatuteLens (M4.λ.3.b) projects each <section> to a typed Statute value with citations, valence, obligations, evidence requirements, and proof standards — all loaded, not hand-coded.
• The build-time codegen (crates/domains/build.rs) materializes per-title runtime modules at us_code::title_N::*; downstream code looks up sections by URN via the UsCode corpus loader (M4.ε.3).

pr4xis update usc_title_18 today: fetches the LRC USLM XML zip, unzips, verifies, and the build script’s USLM lens projects every section in the title to a typed Statute. The audit modules consume the typed values directly — no Option<&str>, no PDF text extraction, no hand-transcribed approximations.

PDF is for case law, not statutes. The M4.γ PDF loader (shipped) is the path for court opinions (e.g. CourtListener / PACER bulk PDFs). The legal-evidence pipeline reads statutes from USLM XML and case law from PDFs — two distinct loaders, two distinct authoritative formats.

Related

• Build an Ontology from a Paper — the declarative authoring path (the ontology! macro), parallel to source-driven ingestion
• Architecture — where data-provisioning sits in the engine stack
• Glossary — Manifest, Lock, Registered source, SourceTaxonomy, Data provisioning

• Document date: 2026-05-16

Compile & Decompile

This page is the operator’s guide for the two legs of the praxis compiler: pr4xis compile, which turns every registered source into a verifiable .prx archive, and pr4xis decompile, which turns an archive back into the exact original source bytes. The completeness meter (pr4xis decompile --meter) is the honesty report over the whole set: per source, what round-trip fidelity is declared and what is actually achieved.

Both commands operate on the registry (praxis.toml) and the lock (praxis.lock); compile consumes the source files that pr4xis update provisions, so run that first (or pass --update).

What compile produces

pr4xis compile

emits one content-addressed .prx.gz per registered OWL vocabulary, U.S. Code title, and WordNet language into the build cache at <workspace>/.prx-cache/. Two artifact families come out, serving two different consumers:

• The compact runtime caches — .prx-cache/usc-compact/ and .prx-cache/wordnet-compact/. These are the parse-once fast-load archives the runtime loaders read: UsCode::loaded() and english_loaded() load a pinned compact archive in milliseconds instead of re-parsing the source XML in every process. The compact codec is dependency-free bit-packing, so its content addresses are portable — stable across toolchains and targets.
• The distribution envelopes — .prx-cache/ontologies/ (OWL), .prx-cache/usc/, and .prx-cache/wordnet/. These rkyv envelopes carry the typed ontology graph plus a content-addressed concrete-syntax complement; they are what pr4xis decompile reads to regenerate the source. Their content address (a MerkleRoot over the rkyv bytes) is a build output, so it is pinned per toolchain rather than portably.

Each line of output names the artifact, its size, and its content address:

  compiled  cito@2.8.1  …  bytes  2fa4c96c12ea…
  compiled  usc_title_18@pl-119-90  …  bytes  ed47add31553…
  …
26 archive(s) (10 compact), … bytes total → /…/.prx-cache
verified 26 archive(s) against praxis.lock pins (0 unpinned, no fast path).

A registered, pinned source that is not on disk is an error, not a silent skip — the “forgot to run pr4xis update” failure is reported by name. pr4xis compile --update provisions the missing sources first instead of erroring; CI provisions separately.

--compact — the fast CI mode

pr4xis compile --compact

emits (and verifies) only the compact runtime caches, skipping the heavy, toolchain-coupled envelopes. This is the CI check: it re-derives and verifies the committed [compact_archive_signatures] pins for all U.S. Code titles — including the giants the unit-test budget caps out of — in seconds.

The pin / verify discipline

praxis.lock carries two archive-pin sections alongside the source [hashes]:

• [archive_signatures] — the MerkleRoot of each rkyv envelope.
• [compact_archive_signatures] — the portable content address of each compact archive. The runtime’s fail-closed load gate checks the installed compact bytes against this pin; a title (or the English archive) takes the fast path only when it is pinned here.

The discipline mirrors pr4xis update’s [hashes] handling:

• Default = verify (CI-safe, writes nothing). Every emitted archive’s content address must equal its committed pin. Any drift fails closed with the offending sources named:

  pr4xis compile: praxis.lock pin drift (1 archive(s)) — re-run `pr4xis compile --lock`
  after confirming the change is intended:
    cito@2.8.1 [archive_signatures]: emitted 9f3a… ≠ pinned 2fa4…
  

  An unpinned archive is reported but never fails — it simply gets no fast path until it is pinned.

• --lock = the deliberate re-pin (maintainer write mode). Writes each emitted archive’s content address into the corresponding lock section, preserving comments and key ordering. Run it locally after a source or codec change you have confirmed is intended — never in CI:

  pr4xis compile --lock
  

So a source file, codec, or envelope-layout change that silently alters any archive is caught by the next plain pr4xis compile; the only way the pins move is a human running --lock on purpose.

What decompile gives you

pr4xis decompile cito                       # → cito-2.8.1.owl
pr4xis decompile usc_title_18 --out t18.xml # → t18.xml
pr4xis decompile english_wordnet            # → english-wordnet XML

decompile is the inverse leg: it resolves the registered source by name (pr4xis update --list shows the names), loads the envelope compile wrote into .prx-cache/, regenerates the original source bytes, writes them to --out (or <name>-<version>.<ext> in the current directory), and prints the achieved round-trip fidelity:

decompiled cito@2.8.1 → cito-2.8.1.owl (… bytes)
  round-trip fidelity: ByteExactGraphFaithful (regenerated from the ontology graph alone)

Routing is registry-derived, not byte-sniffing: the source’s content type selects the reconstruct leaf (OWL RDF/XML, USLM XML, or WN-LMF XML) inside one uniform decompile op. Every reconstruction passes a content-address honesty gate — the regenerated bytes must re-derive the recorded source address, or the load is refused.

The law this realises, proven per source by the test suite over the real bytes:

hash(decompile(compile(source))) == hash(source)

Today 17 registered sources carry a .prx compile/decompile pair — 6 OWL vocabularies, 9 U.S. Code titles, and 2 LMF lexicons (the English WordNet and the bundled US legal lexicon) — and each round-trips byte-for-byte.

There are two fidelity tiers, both byte-exact:

• RawBytesComplementFloor — the bytes come back from a stored, content-addressed copy of the source (a constant complement) inside the archive. Real, cryptographically witnessed exactness, but from a stored side-channel.
• ByteExactGraphFaithful — the bytes are regenerated from the typed ontology graph plus a small concrete-syntax complement, with no stored raw blob. This is the tier the per-source lens registrations declare for all 17 sources today.

The completeness meter

pr4xis decompile --meter

prints the honesty report: one line per registered .prx source, stating the tier its round-trip reaches and — for any source still on the floor — the named writer gap that remains:

biro@1.1.1: graph-faithful
cito@2.8.1: graph-faithful
…
usc_title_42@pl-119-90: graph-faithful (declared) — byte-exact proof in the slow / all-sources lane
…
decompile completeness: … graph-faithful, … still on the stored-complement floor (…)

Two properties make it a report you can trust:

• It cannot over-claim. Each row carries both the declared tier (what the source’s registered lens promises) and the achieved tier (what the emitted archive actually carries, as measured by the round-trip harness). A test asserts they agree for every provisioned source, so an archive claiming graph-faithfulness it does not achieve is a test failure, not a meter line.
• It does not guess. A source whose corpus is not provisioned on this machine, or whose size defers it to the slower all-sources test lane, is stated as such rather than credited with a tier the fast harness did not measure.

The meter is non-failing — it never blocks CI. It exists so the remaining distance to a fully graph-only compiler is always stated per source, never averaged away.

Related

• Register a Source — the manifest/lock/pr4xis update workflow that provisions what compile consumes
• Test Architecture — how the compact archives serve as the parse-once fast path for the test suite
• Glossary — .prx, Archive, IntegrityClaim, Fail-closed load gate

• Document date: 2026-06-09

Compose Two Ontologies via Functor

This page is the practical guide for writing a cross-domain functor in pr4xis — the mechanism that lets two ontologies compose with mathematical proof that the composition is sound.

When you need a functor

If you have an ontology that uses concepts from another ontology — explicitly or implicitly — you should write a functor between them. Examples from the existing workspace:

• Pharmacology talks about molecular targets → PharmacologyToMolecular
• Biology talks about bioelectric phenomena → BiologyToBioelectric
• Concurrency talks about events → ConcurrencyToEvents
• Chess talks about state machines → ChessToConcurrency, ChessToEvents

The functor makes the implicit dependency explicit, and proves at test time that the dependency preserves structure.

What a functor must do

A functor F: Source → Target is a Rust impl of pr4xis::category::Functor. It must:

1. Map every object in the source category to an object in the target category.
2. Map every morphism in the source category to a morphism in the target category, with matching source and target.
3. Preserve identities: F(id_x) = id_{F(x)}.
4. Preserve composition: F(g ∘ f) = F(g) ∘ F(f).

If the laws hold, the functor is a categorical theorem that the source domain’s structure faithfully embeds in the target. If they don’t hold, your encoding has a bug or the composition you proposed isn’t actually structural — either way, the failing test surfaces it before the functor ships.

The pattern

Skeleton for a functor between two existing ontologies:

use pr4xis::category::{Arrow, Functor};

use crate::domain_a::{ACategory, AConcept, ARelation};
use crate::domain_b::{BCategory, BConcept, BRelation};

pub struct AToB;

impl Functor for AToB {
    type Source = ACategory;
    type Target = BCategory;

    fn map_object(obj: &AConcept) -> BConcept {
        match obj {
            AConcept::Foo => BConcept::CorrespondingFoo,
            AConcept::Bar => BConcept::CorrespondingBar,
            // … one arm per source concept
        }
    }

    fn map_morphism(m: &ARelation) -> BRelation {
        BRelation {
            from: Self::map_object(&m.source()),
            to: Self::map_object(&m.target()),
            kind: /* map kinds analogously */ todo!(),
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use pr4xis::category::laws::assert_functor_laws;

    #[test]
    fn test_a_to_b_functor_laws() {
        // Panics with the failing law's name if any law breaks.
        assert_functor_laws::<AToB>();
    }
}

That’s it. assert_functor_laws iterates the functor laws as Axiom impls: for every source concept it maps the identity morphism and checks F(id_x) == id_{F(x)}, and for every composable morphism pair it checks F(g ∘ f) == F(g) ∘ F(f). Each law’s verify() returns a typed Verdict (a proof or a counterexample, never a bool); the assert_* helper pattern-matches it and panics on the first counterexample.

If the test passes, the functor is verified. If it fails, the panic names the specific law that broke (e.g. FunctorIdentityLaw), and you fix the map_object arm that’s wrong. When you’d rather inspect each result yourself instead of panicking, iterate pr4xis::category::laws::functor_law_axioms::<AToB>() and match each Verdict.

Three things to know

1. map_object must be total

Every variant of AConcept must have a corresponding case in the match. The Rust compiler enforces this — exhaustiveness checking is your friend. If the source ontology adds a new concept, the compiler tells you to add a new case to every functor that uses it. This is one of the safety guarantees of writing functors as Rust types instead of as runtime mappings.

2. map_object does not need to be injective

Two distinct source concepts can map to the same target concept. This is how the molecular-bioelectric functor collapses 27 molecular concepts onto 4 unique bioelectric concepts (the 85.2% collapse from Gap detection). The collapse is not a bug — it’s a measurement of how much information the target ontology cannot represent.

If you want to detect collapses, pair your forward functor with a reverse functor and check whether they form an adjunction. The round-trip G(F(x)) will collapse onto a different concept for every concept the source ontology distinguishes that the target cannot.

3. The functor is a theorem, not a translation

A functor is not just “convert objects from A to B”. It is the claim that the conversion preserves structure. If you can write map_object correctly but assert_functor_laws fails, you have not proven the functor — the conversion does not actually preserve composition or identity, which means the source domain’s structure is not faithfully present in the target. The failing test is telling you the proposed embedding doesn’t hold.

When that happens, two paths forward:

• Find a different target. Maybe the source belongs in a different ontology, with different morphism structure.
• Restrict the source. Maybe only a subset of the source’s morphisms map cleanly. Write the functor over the restricted source category; document what’s left out and why.

Either is fine. The wrong move is to fudge the map_object to make the test pass — that hides the structural mismatch instead of surfacing it.

When you also need an adjunction

If you have two functors F: A → B and G: B → A going in opposite directions, you may have an adjunction. Adjunctions enable gap detection — the round-trip G(F(x)) surfaces concepts that one side cannot represent.

To check whether your functor pair is an adjunction, implement the Adjunction trait:

use pr4xis::category::Adjunction;

pub struct ABAdjunction;

impl Adjunction for ABAdjunction {
    type Left = AToB;
    type Right = BToA;

    fn unit(obj: &AConcept) -> ARelation {
        // η_A: A → G(F(A))
        let round_trip = BToA::map_object(&AToB::map_object(obj));
        ARelation { from: *obj, to: round_trip, kind: /* … */ todo!() }
    }

    fn counit(obj: &BConcept) -> BRelation {
        // ε_B: F(G(B)) → B
        let round_trip = AToB::map_object(&BToA::map_object(obj));
        BRelation { from: round_trip, to: *obj, kind: /* … */ todo!() }
    }
}

Then run the gap-analysis pattern from crates/domains/src/formal/meta/gap_analysis.rs against your adjunction. The collapses the analysis surfaces are missing distinctions in your source ontology — fix them with ContextDef::resolve or by splitting the entity, and the gap closes.

Where to look in the codebase

• crates/domains/src/natural/biomedical/adjunctions.rs — the three biomedical adjunctions, with unit and counit implementations and the full law-checking test suite
• crates/domains/src/natural/biomedical/biochemistry/bioelectricity_functor.rs — a clean single-functor example, no adjunction
• crates/pr4xis/src/category/laws.rs — the functor laws as Axiom impls (functor_law_axioms / assert_functor_laws)
• crates/domains/src/formal/meta/gap_analysis.rs — the gap-analysis pattern that uses the adjunctions

Related

• Build an ontology from a paper — the upstream tutorial; if you are writing a functor, you have probably already authored both source and target ontologies
• Write axioms — domain-specific axioms that go beyond the structural laws functors enforce
• Concepts — the categorical machinery, with examples
• Gap detection — the bioelectricity result, the canonical example of an adjunction surfacing a real ontological gap
• Glossary — formal definition of a functor

• Document date: 2026-04-14

Write a Domain Axiom

This page covers how to write a domain-specific axiom that the engine enforces at runtime. For the structural axioms inherited automatically via pr4xis::ontology::reasoning::structural_axioms_for (no cycles on Subsumption / Parthood, antisymmetric Subsumption, symmetric Opposition, etc. — OBO-RO; Smith et al. 2005), see Architecture. This page is about the axioms your domain adds on top.

When you need a domain axiom

Whenever a published source says “this must be true” about your domain, and the truth isn’t already enforced by category laws or the standard reasoning systems. Examples:

• “A chess king moves at most one square per turn” — chess
• “Voltage = current × resistance” — electromagnetism
• “Energy is conserved across drops and rises” — mechanics
• “Heisenberg uncertainty: Δx · Δp ≥ ℏ/2” — quantum
• “Speed of light is the upper bound on velocity” — relativity
• “An enzyme catalyzes exactly one reaction class” — biochemistry

If the source says it, the axiom should encode it. If the engine ever produces a state where the axiom doesn’t hold, the engine should refuse the action that produced it.

What an axiom is

An axiom in pr4xis is a Rust type that implements the Axiom trait:

use pr4xis::logic::Axiom;
use pr4xis::logic::proof::{SimpleProof, SimpleCounterexample, Verdict};

pub struct MyAxiom;

impl Axiom for MyAxiom {
    // `verify` returns a typed Verdict, never a bool:
    //   Verdict = Result<Box<dyn Proof>, Box<dyn Counterexample>>
    // Ok carries a proof witness; Err carries a counterexample. The two
    // are structurally distinct kinds of evidence — core never collapses
    // them into a boolean.
    fn verify(&self) -> Verdict {
        if /* the axiom holds */ true {
            Ok(Box::new(SimpleProof::new(self.meta())))
        } else {
            Err(Box::new(SimpleCounterexample::new(self.meta())))
        }
    }

    // Citation is required — every axiom must trace to published work.
    fn citation(&self) -> pr4xis::ontology::meta::Citation {
        pr4xis::ontology::meta::Citation::parse_static("Smith (1999) J. Foo")
    }

    // `name` and `description` have defaults derived from the type name
    // and return OntologyName / Label; override them only when the Rust
    // identifier differs from the human-readable axiom label.
}

When name, description, and citation are all string literals, the pr4xis::axiom_meta! macro emits the three override methods in one line:

impl Axiom for MyAxiom {
    fn verify(&self) -> Verdict { /* … */ }
    pr4xis::axiom_meta!("MyAxiom", "What the axiom says, in one sentence.", "Smith (1999) J. Foo");
}

Axioms come in two shapes:

1. Unconditional axioms. Statements that must hold regardless of state. “The speed of light is constant in all reference frames.” These are checked at compile time or at startup.
2. State-dependent axioms. Statements that must hold given the current situation. “The total energy of the system equals the total energy at the previous time step.” These are checked by the engine before applying any action.

Most domain axioms are state-dependent — they live as Precondition implementations on the engine, not as pure Axiom impls. The two are related but distinct.

The Precondition pattern (state-dependent axioms)

If your axiom needs to know the current situation to be checked, implement Precondition instead of (or in addition to) Axiom. The trait has one type parameter — the Action — and the situation type comes from Action::Sit. check returns the same typed Verdict an axiom does:

use pr4xis::engine::Precondition;
use pr4xis::logic::proof::{SimpleProof, SimpleCounterexample, Verdict};

pub struct EnergyConservation;

impl Precondition<MyAction> for EnergyConservation {
    fn check(&self, situation: &<MyAction as pr4xis::engine::Action>::Sit, action: &MyAction) -> Verdict {
        let meta = /* a Provenance carrying name + description + citation */;
        let energy_before = situation.total_energy();
        let energy_after = situation.simulate_action(action).total_energy();

        if (energy_before - energy_after).abs() < EPSILON {
            Ok(Box::new(SimpleProof::new(meta)))
        } else {
            Err(Box::new(SimpleCounterexample::new(meta)))
        }
    }
}

Two things to note:

1. The result is a typed witness. Ok carries a Proof, Err carries a Counterexample; each carries its own meta() (name, description, citation, module path), so the trace shows exactly which rule passed or failed and where it comes from — no separate rule/reason string fields are needed.
2. The check is total. Every possible (situation, action) pair must produce a proof or a counterexample. There is no “I don’t know” — if the axiom depends on something the situation doesn’t carry, the situation needs to be enriched, not the precondition.

Wiring the axiom into the engine

When you create an engine, you pass it the list of preconditions:

use pr4xis::engine::Engine;

let engine = Engine::new(
    initial_situation,
    vec![
        Box::new(EnergyConservation),
        Box::new(SpeedLimit),       // another precondition
        Box::new(PositiveDuration), // another
    ],
    apply_action,
);

Every call to engine.next(action) runs every precondition in order. If any return Violated, the engine returns EngineError::Violated with the list of violations and a recoverable engine reference. If all return Satisfied, the apply function runs and produces the new situation.

Property-based testing for axioms

The strongest verification for a domain axiom is property-based: define a property the axiom should ensure, then let proptest generate random inputs and look for counterexamples. Pattern:

use proptest::prelude::*;

proptest! {
    #[test]
    fn energy_is_conserved_for_all_drops(initial_height in 0.0_f64..1000.0) {
        let situation = MySituation::new_at_rest(initial_height);
        let action = MyAction::Drop;
        let result = EnergyConservation.check(&situation, &action);
        prop_assert!(result.is_ok()); // Ok(proof) — the precondition holds
    }
}

The proptest harness will run hundreds of random inputs and shrink any failure to the smallest counterexample, which makes domain bugs much easier to find than hand-picked unit tests.

Citing the source

Every axiom needs a citation. The recommended pattern is a doc comment on the axiom struct:

/// Energy conservation under closed-system mechanics.
///
/// **Source:** Newton's *Principia* (1687), Book I, Definitions and Laws of Motion.
/// Modern formulation: any standard mechanics text, e.g., Goldstein,
/// *Classical Mechanics* (3rd ed., 2002), Chapter 1.
///
/// **Statement:** For an isolated system, the total energy E = KE + PE is
/// constant under all permitted actions.
pub struct EnergyConservation;

The doc comment becomes part of the axiom’s public documentation and is what the trace will show to users when the axiom fires. Make it precise enough that someone reading the failing trace can find the exact paragraph in the source where the axiom comes from.

What NOT to do

• Don’t write axioms for “obvious” facts that aren’t in any source. Pr4xis is not a common-sense engine; every axiom must be sourceable. If you can’t cite it, don’t encode it.
• Don’t use floating-point equality in axiom checks. Use an epsilon comparison or rational arithmetic. Floating-point equality fails for reasons that have nothing to do with the axiom.
• Don’t make axioms catch unrelated bugs. If your EnergyConservation precondition is also catching velocity-out-of-range errors, split them. Each axiom should fail for one reason.
• Don’t make axioms expensive. Preconditions run on every engine action. If checking your axiom requires solving a hard problem, cache the result or restructure the check. The engine is meant to be fast.

Where to look in the codebase

• crates/domains/src/natural/physics/relativity.rs — the SpeedLimit axiom enforcing v < c
• crates/domains/src/natural/physics/energy.rs — EnergyConservation and PhysicalConstraints for KE↔PE transformations
• crates/domains/src/social/games/chess/engine.rs — GameNotOver, PieceExists, OwnPiece, LegalMove
• crates/pr4xis/src/logic/axiom.rs — the Axiom trait
• crates/pr4xis/src/engine/precondition.rs — the Precondition trait

Related

• Build an ontology from a paper — the upstream tutorial; if you are writing axioms, you are extending an ontology you already authored
• Compose via functor — when an axiom from one domain implies an axiom in another, the implication is a functor
• Concepts — the categorical machinery axioms plug into
• Architecture — the engine that runs the preconditions
• Glossary: Axiom, Glossary: Precondition

• Document date: 2026-04-14

The Constitution

pr4xis holds five properties about its own reasoning. They are not features offered to a user and not promises that can be relaxed under pressure — they are the conditions under which a computation counts as pr4xis reasoning at all. A build that violates one of them fails its own test suite.

Each guarantee is stated three ways: the promise it makes, the enforcer in code that makes it true, the violation that would break it. Each ends in a command that re-derives it. Nothing here is asserted; it is checked at test time.

For the literature and reasoning behind the values — the enforcement ladder, what grounds each, and why Consistent — see the research grounding.

Verifiable

• Promise — every claim carries its source. Nothing is asserted without a citation back to an authoritative origin.
• Enforcer — Axiom::citation() is required: no default, no Option. An axiom without a citation is a compile error. Domain vocabulary is loaded from cited sources (praxis.toml + a praxis.lock SHA256), never hand-written into the code.
• Violation — a hardcoded list, a regex over the input, a weight with no axiom behind it.

cargo test -p pr4xis-domains --lib -- citation

A statistical model cannot make this promise: a citation it emits is itself a prediction, with the same ground-truth status as any other token it produces.

Deterministic

• Promise — the same input produces the same output, byte for byte, on every run and across versions.
• Enforcer — transformations are lawful morphisms, and the serialized substrate round-trips byte-exactly. There is no debug-only path and no profile-conditional behavior, so what is tested is what runs.
• Violation — a lossy projection, a cfg-gated shortcut, any branch whose result depends on profile, temperature, or seed.

cargo test -p pr4xis-domains --lib -- byte_exact

A statistical model is stochastic by construction; its output depends on sampling and drifts between versions.

Explainable

• Promise — the system can describe its own structure, and the reasoning path is the answer rather than a story told after the fact.
• Enforcer — self-description is a fixed point: the description pr4xis gives of itself, fed back in, reproduces itself (the eigenform). Nothing in the system lives outside the ontology it can report.
• Violation — an unregistered concept, an unexaminable branch, an explanation reconstructed separately from the computation it claims to describe.

cargo test -p pr4xis-domains --lib -- eigenform

A statistical model’s explanations are post-hoc and need not be faithful to the computation that produced the answer.

Honest

• Promise — what it cannot ground, it leaves ungrounded. It stops rather than confabulate.
• Enforcer — an input with no grounding does not get an invented binding; it is left ungrounded, and a derivation that depends on it does not proceed. End to end, the engine answers from a loaded gloss when it has one and abstains when it does not.
• Violation — filling a gap with a plausible guess; answering past the edge of what is grounded.

cargo test -p pr4xis-chat -- abstain

The schema-level guarantee — that an unknown word is left ungrounded rather than bound to a guess — is checked alongside it with cargo test -p pr4xis-domains --lib -- ungrounded.

A statistical model has no reliable internal signal for “I am making this up,” and always has an output.

Extensible

• Promise — new knowledge plugs in and the other four guarantees still hold. Adding an ontology does not silently degrade the rest.
• Enforcer — ontologies compose by functors whose laws are checked; an integration that does not preserve structure fails the law test instead of merging.
• Violation — a merge that drops or distorts structure; an “extension” that is really a rewrite of what it touches.

cargo test -p pr4xis-domains --lib -- functor_laws

A statistical model extends by fine-tuning, which trades one capability for another without measuring the loss.

Honest is the keystone

The five are not five peers. The other four are credible only because the system can stop.

Verifiable means nothing if, when it cannot verify, it answers anyway. Deterministic, Explainable, and Extensible each assume the system will decline rather than fabricate at the boundary. Remove the ability to refuse and the other four become preferences that hold until they are inconvenient. Keep it, and they become invariants. The defining act is the refusal: the point at which there is no grounded answer and pr4xis says so.

Two readings of the same five

The guarantees above are the product reading — what someone relying on pr4xis gets. The same five are also the engineering invariants the substrate is built on. They are one set seen from two sides.

Self-binding

These five are not documentation about pr4xis written alongside it. They are checked by the tests above, which run in the same suite as everything else. The constitution is part of the substrate it governs: a change that breaks Verifiable or Deterministic does not produce a system that quietly stops meaning what it says — it produces a red test.

The suite classifies itself

The constitution is not asserted about the test suite from outside — the suite declares its own relationship to it. Every test in pr4xis-domains carries the guarantee it witnesses:

#[pr4xis::praxis_value(Honest)]
#[test]
fn an_unknown_word_is_left_ungrounded() { /* ... */ }

and property tests (which the attribute cannot wrap) declare it next to the proptest! block:

pr4xis::register_praxis_value!(prop_mutated_prx_always_rejected, Honest, Verifiable, Deterministic);

The tag carries a primary guarantee (the partition key), optional secondary guarantees for irreducibly multi-witness tests, and a TestKind — Example (a point-claim) or Property (a ∀-claim checked over generated inputs). Tags register into a linkme distributed slice at link time; the constitution_coverage meta-test folds the slice into the partition, and scripts/constitution-gate.sh enforces completeness: it diffs the registered test names against the live cargo test --list, failing if any test is untagged or any tag names a test that does not exist.

The guarantee a test witnesses is decided by one rule — a test witnesses the guarantee whose failure it would detect: if it went red, which property of the system just broke? A wrong citation breaks Verifiable; a non-reproducible result breaks Deterministic; an un-presentable structure breaks Explainable; accepted bad input breaks Honest; a broken functor law breaks Extensible.

Coverage

Re-derived by cargo test -p pr4xis-domains --lib -- constitution_coverage -- --nocapture over all 6,684 tests:

What is a hard guarantee, and what is a diagnostic. The per-test declaration and the completeness gate are hard: it is mechanically impossible for a test in this crate to exist without a declared guarantee, or for the meta-test to claim a coverage it does not have. The percentages are a directional diagnostic, not an objective measurement — a classification of ~6,700 tests into five categories involves judgment at the margins (a fail-closed safety test that also verifies a value; a functor test that asserts both a mapping value and a law), and a chunk of Verifiable is the genuine residual of structural-completeness tests (totality, exhaustiveness, has_N_concepts) that no product-guarantee names cleanly.

Read that way, the numbers tell a real story: Honest concentrates in operational and adversarial-input code (engineering safety guards, legal/compliance gates, game-move and markup validation) and is thin in pure-knowledge domains; Explainable is rare everywhere (self-description is a small, specific mechanism); and Verifiable dominates because most tests, at bottom, assert that a specific claim holds. The thin guarantees are the suite telling us where its own verification is shallow — which is exactly what a constitution that checks itself is for.

From classification to enforcement (the rung)

Counting tagged tests is the weakest useful way to hold a guarantee — it measures the suite, not the system. A guarantee can be held five ways, weakest to strongest: a slogan; a count of tests; a census of tests against the code they cover; a single universal axiom checked over the whole base; or a structural property the compiler refuses to let you violate. The work is to push each guarantee up that ladder, from tested toward enforced.

Five answer-guarantees + one composition guarantee

The values are not all the same kind, and the ontology says so. Five are answer-guarantees — properties of a single answer: Verifiable, Deterministic, Explainable, Honest, Consistent. Extensible is second-order — the property that those five are preserved under composition. It is modeled as a meta-property (Preserves edges pointing at each answer-guarantee), not a sibling of them, and ExtensiblePreservesEveryGuarantee checks that structure while the workspace’s functor-law tests discharge it operationally.

Where each stands, and what enforces it:

These are not slogans: each is a machine-checkable axiom or universal property that fails red if the guarantee is broken. Consistent (the value the formal-methods and ontology-quality literature ranks most foundational, yet which a product framing omits) was backed by a runnable axiom the day it was named.

Backing a value finds bugs. The first time Honest was pushed from tested (hundreds of example tags) to enforced (∀-bytes totality), the fuzz immediately found a real defect the examples never caught: a directory-archive decoder could be driven to a multi-petabyte allocation — a process-abort denial-of-service — by a forged length prefix. The fix (bound the pre-allocation; refuse rather than abort) is a genuine Honest hardening. That is the difference between stating a guarantee and enforcing it: enforcing it is generative — it surfaces exactly where the system is not yet honest.

Concepts

This document explains the conceptual model behind pr4xis — what an ontology is in this system, why category theory is the substrate, and how domains compose. For the layer structure and runtime mechanics, see Architecture. For the academic lineage and source papers, see Foundations.

What is an ontology in pr4xis?

Most ontology systems treat an ontology as a graph of facts — a set of triples saying that A is-a B and B has-part C, queryable via SPARQL or a graph database. pr4xis treats an ontology as a category — a mathematical structure with objects, morphisms, composition, and identity, plus a set of reasoning systems built on top of that structure.

The difference matters because it determines what you can prove. A graph of facts can be queried; a category can be composed with other categories under proof, and the composition can be checked at compile time and test time. If two ontologies share structure, a categorical functor between them is a theorem about that shared structure — not a heuristic, not an alignment score, not a similarity measurement.

Every domain in crates/domains/src/ is an ontology in this stricter sense: an enum of concepts (the objects), an Arrow impl whose morphisms carry Kind tags (Subsumption / Parthood / Causation / Opposition / Equivalence / domain-specific kinds), the structural axioms attached to each kind by the catalog (no cycles, antisymmetric subsumption, symmetric opposition, …), any domain-specific axioms the source paper motivates, and a Provenance carried by fn meta() for trace attribution. The ontology! macro emits all of this from a single declarative block.

Categories

A category has:

• Objects — the things the category is about. In pr4xis, every object is a Concept (Guarino 2009 — a finite, enumerable Rust enum variant).
• Morphisms — directed maps between objects. In pr4xis, every morphism is an Arrow between two concepts, carrying a Kind tag and per-instance provenance (Mac Lane 1971; Awodey 2010).
• Composition — if f: A → B and g: B → C, then g ∘ f: A → C exists and is itself a morphism.
• Identity — for every object A, there is a morphism id_A: A → A.

Two laws govern these:

• Associativity: (h ∘ g) ∘ f = h ∘ (g ∘ f) — the order of grouping does not matter.
• Identity: id_B ∘ f = f = f ∘ id_A — composing with identity changes nothing.

These laws sound trivial but they have a consequence pr4xis exploits everywhere: if your domain model satisfies them, it has no dead states, no unreachable objects, and no broken compositions. The laws are themselves first-class axioms: category::laws::assert_category_laws verifies them for every category in the workspace, and each underlying axiom’s verify() returns a typed Verdict — a Proof when the law holds or a Counterexample that names what broke, never a bare boolean or an error string.

Reasoning systems

A category is a structure. Relation kinds are interpretations of its morphisms that answer specific kinds of questions. The structural-axioms catalog (pr4xis::ontology::reasoning::structural_axioms_for) reads each morphism’s Kind and attaches the right algebraic properties (OBO-RO; Smith et al. 2005; Tarski 1941):

• Subsumption (is-a) — NoCyclesOnKind (a thing cannot be its own ancestor) and AntisymmetricOnKind (if A is-a B and B is-a A, then A = B). Answers “is dog a mammal?”.
• Parthood (part-of) — NoCyclesOnKind. The full CEM WeakSupplementation (Casati & Varzi 1999) is available as a hand-written domain axiom for ontologies that need it. Answers “what are the parts of an esophagus?”.
• Causation (causes) — AsymmetricOnKind (Lewis 1973) and IrreflexiveOnKind. Answers “what caused this event?”.
• Opposition (opposes) — SymmetricOnKind (if A opposes B, B opposes A) and IrreflexiveOnKind (a thing does not oppose itself). Answers “what is the opposite of cold?”.
• Context — disambiguates concepts by context (ContextDef::resolve). A potassium channel in a constitutive context is not the same as a potassium channel in a therapeutic context. Closes gaps that adjunctions surface.

The ontology! macro provides sugar clauses (is_a: / has_a: / causes: / opposes:) for the canonical kinds and a free-form edges: clause for any other kinded morphism the ontology needs.

Functors

A functor is a structure-preserving map between two categories. If F: Source → Target is a functor, then:

• For every object A in the source, there is an object F(A) in the target.
• For every morphism f: A → B in the source, there is a morphism F(f): F(A) → F(B) in the target.
• Identities are preserved: F(id_A) = id_{F(A)}.
• Composition is preserved: F(g ∘ f) = F(g) ∘ F(f).

The third and fourth conditions are the functor laws. If a Rust impl Functor for X passes category::laws::assert_functor_laws, the laws hold and the functor is a categorically valid claim that the source domain’s structure embeds into the target. Like the category laws, each functor law is an axiom whose verify() returns a typed Verdict — a Proof or a Counterexample, not a boolean.

This is what pr4xis means when it says “domains compose with proof”. A functor from Pharmacology → Molecular is not an analogy or a heuristic mapping — it is a verified theorem that pharmacological structure faithfully embeds in molecular structure. The workspace ships more than 95 such functor implementations; to count the current total, run grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/ | wc -l.

Adjunctions and gap detection

When two functors come in opposed pairs, F: A → B and G: B → A, with F going one way and G going the other, the pair may form an adjunction. The technical definition involves natural transformations called unit (η: Id_A → G ∘ F) and counit (ε: F ∘ G → Id_B); the practical consequence is that F and G are “optimal inverses” of each other, even when neither is a true inverse.

The reason adjunctions matter for pr4xis is gap detection. If you take an object A in the source category and apply G(F(A)) — a round-trip through both functors — you get back to the source category. If G(F(A)) ≠ A, the source ontology has a missing distinction: the round-trip collapsed A into something else because the target ontology cannot represent the difference.

Every collapsed entity is a missing distinction the math detected automatically. This is how the bioelectricity adjunction in crates/domains/src/natural/biomedical/ discovered that voltage-gated potassium channels (Kv) serve two functionally distinct roles — homeostatic and therapeutic — that the molecular ontology had collapsed into a single entity. The adjunction surfaced the gap; a ContextDef resolution then disambiguated the two roles, and the gap closed.

For the live percentages of how much information is lost in each round-trip across the biomedical stack, run cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture.

Composition is the point

Categories are the substrate. Functors are the maps between them. Adjunctions are the paired functors that detect what’s missing. Together they answer one question directly: does this composition preserve structure, with proof?

The functor from pharmacology to the molecular ontology is not just an alignment exercise. If the functor laws hold, the composition is a theorem. If they don’t hold, you cannot pretend the two ontologies are saying the same thing — the system tells you exactly which morphism breaks. The biomedical adjunctions go further: a round-trip through the paired functors surfaces a distinction the target ontology cannot represent — the Kv-channel gap detection above is exactly such a case.

This is what pr4xis adds to the existing landscape of formal ontologies. The ontologies have been there for decades; the categorical substrate that makes their composition machine-checkable is the missing piece.

The Self-Model — categories all the way down

Because pr4xis describes its own structure with the same machinery it uses for any other domain, there is a self-model ontology (crates/domains/src/cognitive/cognition/self_model.rs) that models pr4xis’s own architectural concepts — what an ontology is, what a reasoning system is, how they relate — as objects in a category, through exactly the same Ontology trait it uses for biology or chess. Self-reference is modeled categorically as a natural transformation, not as a special case in the runtime.

This is a small but load-bearing detail: it is the reason pr4xis can extend itself without bolting on metaprogramming. Every new capability is just another ontology, and every new capability is automatically composable with everything that came before.

Reading legal text

Legal text is English, but it does not read like English. A statute can redefine a word for its own purposes, and when it does, the redefinition is law, not lexicography: in ordinary English a “person” is a human being, but 1 U.S.C. §1 — the Dictionary Act — provides that throughout the U.S. Code “person” includes corporations, companies, associations, firms, partnerships, societies, and joint stock companies as well as individuals. A reader that brings only a dictionary’s senses to a statute gets the law wrong. pr4xis models this with two pieces: a lexicon in which one word carries many senses, and a precedence order that decides which definition governs a given use.

One word, many senses. The lexicon (crates/domains/src/cognitive/linguistics/lemon/lexicon.rs) follows the W3C OntoLex-Lemon model (2016; McCrae et al. 2017): each written word has exactly one LexicalEntry, and that entry carries many Senses, each pointing at an ontology concept. Lexicon::add_sense appends to the one shared entry — so when the legal layer teaches the lexicon a legal meaning of “person”, the word is not duplicated and its ordinary meaning is not overwritten; both senses live side by side. A sense may carry a domain marker (OntoLex’s dct:subject, e.g. "legal"), and which sense is predominant depends on the domain of the question being asked — Koeling, McCarthy & Carroll (2005) showed the predominant sense of a polysemous word is domain-dependent. The ranking is simple: a sense whose domain matches the query is most salient, a general unmarked sense is the default fall-through, and a sense from some other domain ranks last. Lexicon::resolve(word, domain) returns the winner, and the ordering is not merely asserted: the SenseOrderIsStrictPartialOrder axiom verifies it is irreflexive, asymmetric, and transitive, so “the predominant sense” is always well-defined.

A defined term is a first-class sense. When a statute defines a term, pr4xis records a LegalDefinition (crates/domains/src/social/judicial/statute_structure/definition_scope.rs): the term, the scope it applies to, and the concept it binds the term to. The load-bearing modeling choice is that the defined term’s identity anchors in the legal definition, not in the English word: legal “person” references a concept of its own (usc_title_1:person), distinct from WordNet’s person.n.01. DefinitionLexicon::mint_into then mints each defined term into the shared lexicon as a "legal"-domain sense — alongside, never instead of, the general sense.

The precedence ladder. A term like “person” may be defined at several scopes at once, captured by DefinitionScope:

• Enacted — a definition with stated applicability (“In this section …”, “For purposes of this title …” — 26 U.S.C. §7701). It governs every use inside the subtree its citation names, and its specificity rises with the scope’s depth: a section-level definition is more specific than a title-level one.
• DictionaryAct — 1 U.S.C. §1, the default for the entire U.S. Code.
• OrdinaryMeaning — no statutory definition; the word means what English says it means.

When more than one scope governs a use, the more specific displaces the more general — the general/specific canon from the statutory-interpretation literature (Scalia & Garner 2012, Reading Law §28, lex specialis). So the ladder reads: enacting section > title-wide definitions > the Dictionary Act > ordinary English. pr4xis models this as a priority ordering, not as disjoint namespaces, because resolution is a fall-through — when a rung does not apply, the use falls to the next — and a fall-through is an ordering (Reiter 1980 on default reasoning; Prakken & Sartor 1996 on defeasible rule priorities in legal reasoning). The DefinitionScopePrecedenceIsStrictPartialOrder axiom verifies the ladder is a strict partial order, so a well-defined governing definition always exists.

The ladder is also defeasible — it yields. The Dictionary Act applies “unless the context indicates otherwise”, and §7701 yields where its definition would be “manifestly incompatible” with the provision at hand — the Supreme Court treated exactly this clause as a soft, contextual escape in Rowland v. California Men’s Colony, 506 U.S. 194 (1993). resolve_definition therefore takes a contextual-defeater predicate alongside the candidate definitions: a defeated definition does not abort resolution, it falls through to the next-most-specific governing definition.

“person”, resolved twice. dictionary_act_definitions() ships the twelve Dictionary Act terms — “person”, “whoever”, “officer”, “signature”, “subscription”, “oath”, “sworn”, “writing” (1 U.S.C. §1), “vessel” (§3), “vehicle” (§4), “company” and “association” (§5) — each bound at code-wide scope. Mint them into a lexicon that already knows WordNet’s “person”, and the same word resolves differently per register:

let mut lex = Lexicon::new("en");
lex.add_sense("person", "english_wordnet", "person.n.01", None);
dictionary_act_definitions().mint_into(&mut lex);

lex.resolve("person", Some("legal")); // → usc_title_1:person  (the Title-1 sense)
lex.resolve("person", None);          // → english_wordnet:person.n.01

One entry, two senses, both reachable: the legal register elevates the statutory meaning, the default stays WordNet’s.

This is the definitional layer — which sense a word resolves to, and which definition governs where. The Dictionary Act layer is a hand-coded prototype of what the Title 1 corpus loader will produce, and typed statute-to-statute cross-references (“as defined in section 3(a)” resolving to the cited provision as a first-class edge) are future work.

Related

• Architecture — the five-layer Rust stack and runtime mechanics
• Foundations — academic lineage; every concept above traced to its source paper
• README — the project entry point with the LLM contrast table and the bioelectricity gap-detection result
• Per-ontology READMEs (pending #57) — for what each individual ontology contains
• Per-ontology diagrams (pending #59) — for the visual “neural network of an ontology” view

• Document date: 2026-04-14
• Verification: the category and functor law axioms (category::laws::assert_category_laws / assert_functor_laws) are exercised by cargo test -p pr4xis category; the functor count comes from grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/; the round-trip collapse measurement from cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture; and the legal-text resolution behavior (sense elevation, lex-specialis precedence, the contextual defeater, the “person” example) from cargo test -p pr4xis-domains definition_scope and cargo test -p pr4xis-domains lexicon.

Architecture

pr4xis is a five-layer Rust stack where each layer depends only on the layers below it. Domain knowledge lives in composable ontologies, not in mechanical processing logic — there is no parser-with-special-cases, no rule-engine-with-hardcoded-strings, no if-statements branching on domain values.

This document covers the abstract structure. For specific ontologies — what concepts they contain, what they connect to, what their adjunction discoveries look like — see the per-ontology READMEs (#57) and the per-ontology diagrams (#59).

The five layers

graph TB
    domains["pr4xis-domains<br/>160+ ontologies"]
    engine["**engine**<br/>runtime enforcement"]
    ontology["**ontology**<br/>structural rules"]
    category["**category**<br/>category theory"]
    logic["**logic**<br/>propositional foundation"]
    codegen["**codegen**<br/>build-time generation"]

    domains --> engine
    engine --> ontology
    ontology --> category
    category --> logic
    codegen --> ontology

These five layers are the conceptual frame; the crate also carries supporting modules (entity_ref, xml_grammar, codegen_data) alongside them. To see the actual top-level module list, run ls crates/pr4xis/src/ or read the pub mod declarations in crates/pr4xis/src/lib.rs.

pr4xis::logic — propositional foundation

Depends on nothing. Provides axioms, propositions, logical composition (AllOf, AnyOf, Not, Implies), the three modes of inference (deduction, induction, abduction), and the classical connectives with truth tables. Verified by cargo test -p pr4xis logic.

pr4xis::category — category theory primitives

Depends on logic. Provides entities, relationships, categories, morphisms, functors, natural transformations, adjunctions, and the algebraic structures used throughout the stack: Writer monad (for tracing), Monoid, Semigroup, Applicative, NonEmpty, Cofree comonad, Algebra (F-algebras and recursion schemes), Lens. The category and functor laws live in category::laws as first-class Axiom impls — assert_category_laws and assert_functor_laws exercise them exhaustively and via property-based testing, and each law’s verify() returns a typed Verdict (a Proof, or a Counterexample naming what broke) rather than a boolean or an error string. Verified by cargo test -p pr4xis category.

pr4xis::ontology — structural rules

Depends on category and logic. Defines what things ARE and how they relate. The Ontology trait bundles a category (type Cat), a quality (type Qual), and fn axioms() -> Vec<Box<dyn Axiom>> — the union of structural axioms inherited from the catalog and any domain axioms the ontology adds. The ontology! proc macro is the declarative entry point — author concept names, labels, and kinded edges (is_a: / has_a: / causes: / opposes: / free-form edges:) and the macro emits the Concept enum, the Category impl, the kinded Arrow impl, an Ontology impl whose axioms() calls structural_axioms_for::<Self::Cat>() to inherit the catalog’s structural axioms (no cycles, antisymmetric subsumption, symmetric opposition, …), and a type-level fn meta() -> Provenance used by the engine for trace attribution. Verified by cargo test -p pr4xis ontology.

pr4xis::engine — runtime enforcement

Depends on ontology, category, and logic. Defines how things CHANGE.

stateDiagram-v2
    [*] --> Initial
    Initial --> Checking: next(action)
    Checking --> Violated: precondition fails
    Checking --> Applying: all preconditions pass
    Applying --> NewState: apply succeeds
    Applying --> LogicalError: apply fails
    Violated --> Initial: rollback
    LogicalError --> Initial: rollback
    NewState --> Checking: next(action)
    NewState --> Initial: back()
    Initial --> NewState: forward()

A new next() after back() clears the redo stack and starts a new branch from that point. Verified by cargo test -p pr4xis test_back_forward_roundtrip and cargo test -p pr4xis test_next_after_back_clears_future.

pr4xis::codegen — declarative ontology data delivery

Depends on ontology. The mechanism for getting authoritative ontology data into the runtime. The layer name is codegen after the build-time path, but codegen is one of several delivery options — all of them are functors from the same OntologyBuilder source category, with categorical equivalence proven so that the choice between them is operational rather than semantic.

• Build-time codegen — the reference instance is codegen::wordnet, which converts the WordNet XML dictionary into a compiled English ontology of ~107K concepts emitted as static Rust.
• Runtime async loading — load ontology data from a file or stream asynchronously at runtime, materializing the same OntologyBuilder structure the codegen path produces.
• Memory-mapped files — mmap a precomputed ontology binary directly into memory, getting the data without parsing or copying.

All three produce the same ontology because each is a verified functor from the same source. The choice depends on deployment: build-time codegen for static binaries, async loading for hot reloading or for ontologies too large to embed, mmap for very large ontologies that need to share memory across processes.

For the largest ontologies, the runtime increasingly loads a compact, content-addressed .prx (see Verifiable archives) instead of embedding static Rust: the English dictionary (~107K concepts) and U.S. Code both load this way — in the browser and on the command line — reading back in milliseconds without re-parsing the source. The compact .prx is smaller than fetching the source itself, so the read-back is the fast path and the original parse is the fallback.

The runtime side of delivery — which external sources praxis knows about and how their on-disk bytes get verified — lives under pr4xis_domains::applied::data_provisioning. A workspace-root manifest (praxis.toml) declares each registered source by name, version, taxonomy type, and authoritative URL; a workspace-root lock (praxis.lock) pins the content digest (tagged blake3:<hex>) each source’s bytes must match. The LockManifestAgreement axiom fails closed on any drift between manifest, lock, and the file on disk. The pr4xis update CLI is the operator’s interface to the same subsystem — see Register a Source for the contributor workflow.

Verifiable archives

A loaded source can be frozen into a small, self-contained, content-addressed .prx file. The runtime reads it back in a moment — instead of re-parsing the original source each time — and checks the archive’s fingerprint before trusting it, refusing anything that has been altered; the same .prx can also rebuild the original source byte-for-byte. The ontology that describes this storage — content-addressable nodes, a Merkle DAG, a binary envelope, a source pin, and a load gate — lives in crates/domains/src/formal/meta/ontology_archive/; its runnable axioms exercise the real realisation.

Three pieces hold the property together:

• A byte-exact round-trip. The archived bytes reload to exactly what was packed; the content address re-derived from those bytes is the round-trip gate (hash(out) == hash(in)).
• A fail-closed load gate. On load, the gate re-derives the content address from the node’s own bytes and admits the node only when that re-derived address equals the trusted pin recorded in praxis.lock. It never trusts an embedded self-asserted label; on mismatch, an unverifiable claim, or an absent pin, nothing is installed.
• A typed, multi-algorithm IntegrityClaim. Integrity is a verifiable claim binding a resource to its expected content hash (W3C Subresource Integrity, 2016), carried over a content-hash family that spans SHA-256, SHA-512, and BLAKE3 (crates/domains/src/formal/meta/artifact_identity/) rather than a single hard-coded algorithm.

The first realisation is the OWL leaf (crates/domains/src/social/software/markup/xml/owl/prx.rs): a registered OWL vocabulary, parsed once and frozen into a content-addressed .prx envelope the runtime materialises back without re-parsing the XML. U.S. Code (USLM) text is a second, non-OWL consumer of the same archive machinery — it is verified against the same archive axioms (the same lens round-trip, source-faithfulness, and fail-closed-gate laws), demonstrating that the storage ontology is not tied to OWL.

The same fail-closed discipline carries the compact fast-load path the runtime reads at startup. The English dictionary (WordNet, ~107K concepts) and each U.S. Code title freeze into a compact, content-addressed .prx — smaller than fetching the source — that english_loaded() and usc_loaded() read back in a fraction of a second, each verifying the archive’s content address against a pin in praxis.lock ([compact_archive_signatures]) and refusing a tampered archive before any data is installed. The pr4xis chat CLI takes this pin-verified path for English today; its U.S. Code is still materialised from a build-time codegen static, and the browser embeds the compact English bytes under a build-time Merkle-root check rather than the praxis.lock pin.

The same primitive extends to a content-addressed graph slice (crates/domains/src/formal/meta/praxis_knowledge_graph/): select a subgraph, emit it as a deterministic content-addressed binary, reload it through the fail-closed gate, and re-bind the behavioural nodes by name, with the slice’s outgoing references surfaced as explicit unbound references. Selecting the whole graph is the degenerate case of the same slice. This is the slicing primitive only — the negotiation that would let one node learn what another holds, and any wire transfer between nodes, is a separate, deferred layer, not part of this machinery.

Runtime-loaded knowledge

A .prx is not only something the build produces — a running praxis can take one in. The runtime accepts a content-addressed .prx archive while it runs, verifies it, materialises it into a live ontology, and grounds it into the chat’s lexical surface, so the chat answers from content it was not built with. Three steps carry the path, each in its own module:

• A fail-closed admit. crates/pr4xis-runtime/src/load.rs is the verify-before-interpret gate: load(bytes, trusted_root) decodes the bytes, re-derives the archive’s Merkle root from the content it is about to admit, and accepts the archive only if that root equals the trusted root supplied from outside the bytes (a lock pin, or a caller-provided root). A self-asserted identity is never trusted; on a mismatch the result is a typed LoadError::RootMismatch and nothing is installed.

• Materialisation into a live ontology. crates/pr4xis-runtime/src/ontology.rs turns the admitted archive into a RuntimeOntology. Referential closure is validated first — an edge naming an undeclared node is a typed DanglingEdge error, never a silent skip. The transitive-relation closure (Subsumption, Parthood, Causation) is re-folded once from the archive’s generating edges at materialize time — a stored closure is never trusted — so every later query (reachable_from, is_a, subsumption_meet) is an O(1) lookup into the pre-folded set rather than a traversal, and is_a returns a typed Verdict (a proof or a counterexample carrying the witnessed claim), not a boolean. Identity is the content address: two RuntimeOntologys are equal exactly when their archive roots agree.

• Grounding into English. ComposedReasoner::new(english, loaded) (crates/domains/src/cognitive/linguistics/composed.rs) composes the embedded English model with the loaded ontologies as one LexicalReasoner: each loaded node’s surface form becomes a Lemon lexical entry whose reference is the typed ConceptRef { ontology, name } (McCrae et al. 2017), and word lookup is the union of the English lexicon and the grounded entries. Loaded concepts get ConceptIds in a range disjoint from English’s, and taxonomy questions over them are answered from the loaded ontology’s materialised closure — never by comparing names as strings.

The chat pipeline consumes this through one seam: pr4xis_chat::process_with_reasoner (crates/chat/src/lib.rs) threads a &dyn LexicalReasoner through the answer stages, so “what is X” reads the loaded gloss when X is loaded and abstains exactly as the embedded model already does when it is not. With no corpus loaded the reasoner is English itself (process_with_metadata), and behaviour is unchanged.

The browser demo runs the whole path end to end. Pr4xis::load (crates/wasm/src/lib.rs) takes a name, a typed encoding, and — for a content-addressed archive — the expected root in hex plus the archive bytes as its payload; the core runs load → materialise → install, rebuilding the ComposedReasoner on each load (idempotent by content address — re-loading the same root replaces rather than duplicates). chat() then dispatches through the composed reasoner when at least one .prx is loaded, and through English alone otherwise. A small demo archive ships embedded with its build-baked trusted root, so the path is exercisable without a network.

The current reach is deliberately narrow. This grounding path runs in the browser, for new-format content-addressed .prx archives; the pr4xis chat CLI (crates/cli/src/main.rs) still answers from the embedded English model alone via chat::process. The U.S. Code and OWL corpora that the browser loads at runtime are a different kind of load — they surface through the self-model catalog (self_describe) but are not yet consulted by the chat’s linguistic pipeline.

The Ontology trait

Every ontology in pr4xis is a category whose morphisms carry Kind tags. The ontology! macro emits the category, the kinded morphisms, the inherited structural axioms, and the type-level Provenance metadata used for trace attribution — all in a single declarative block.

graph LR
    O["Ontology trait"]
    C[Category]
    K[Kinded morphisms]
    A[Axioms]
    M[Provenance]

    O --> C
    C --> K
    O --> A
    O --> M

The canonical relation kinds tracked by the structural-axioms catalog (OBO-RO; Smith et al. 2005) are:

• Subsumption (is_a sugar clause) — NoCyclesOnKind + AntisymmetricOnKind (Tarski 1941)
• Parthood (has_a sugar clause) — NoCyclesOnKind; WeakSupplementation available as a hand-written domain axiom (Casati & Varzi 1999)
• Causation (causes sugar clause) — AsymmetricOnKind + IrreflexiveOnKind (Lewis 1973; Reichenbach 1956)
• Opposition (opposes sugar clause) — SymmetricOnKind + IrreflexiveOnKind
• Equivalence — canonical properties (reflexive + symmetric + transitive) per Tarski (1941); when a catalog entry is added it will be inherited the same way
• Context — disambiguation by context (ContextDef, resolve)
• Analogy — structure-preserving maps between ontologies (functors as Analogies)

For what each looks like in a specific domain, see the per-ontology README. For the broader composition story — how ontologies talk to each other through proven functors and how adjunctions detect missing distinctions — see Concepts.

Domain organization

crates/domains/src/
├── formal/        — math, information, calculator, meta (ontology diagnostics)
├── applied/       — sensor fusion, navigation, perception, tracking, space, underwater,
│                    industrial, localization, theming
├── social/        — games, software (HTTP, XML, OWL, RDF, LMF), judicial, compliance, military
├── natural/       — physics, biomedical, hearing, geodesy, colors, music
└── cognitive/     — linguistics, cognition (epistemics, metacognition)

Total: more than 160 ontologies; to count the current total, run find crates/domains/src -name ontology.rs | wc -l.

Design decisions

Domain knowledge lives in composable ontologies. There is no parser-with-special-cases, no rule-engine-with-hardcoded-strings, no if-statements branching on domain values. Every domain is an ontology; every ontology is encoded as Rust code that the type system checks; every claim is a theorem with a proof.

Situations are immutable. Every action produces a new situation. The old one is preserved in the history stack. This enables undo, redo, and branching without mutation.

Preconditions are separate from apply. The precondition layer validates rules; the apply function transforms state. They are checked independently, so a precondition failure never partially applies a state change.

EngineError returns the engine. Both Violated and LogicalError return the engine so the caller can rollback. The system never panics — contradictions are data, not crashes.

Rich enums carry context. Every enum variant carries the data of HOW it got there. No information is lost between state transitions.

Property-based testing is the primary verification. Domain invariants are expressed as properties that hold for all generated inputs, not just hand-picked examples.

The pipeline is a writer monad. Tracing is not a separate concern bolted onto computations; pipelines are built as Writer<PipelineTrace, A> so trace entries accumulate via monoid composition rather than mutation.

Related

• README — the project’s main entry point and pitch
• Concepts — what ontologies are and how they compose via functors
• Foundations — academic lineage; every ontology traced to its source paper
• Per-ontology READMEs and citings — pending #57
• Per-ontology diagrams (“neural network of an ontology”) — pending #59
• Source-of-truth report pipeline (live numbers from CI) — pending #60

• Document date: 2026-04-14
• Verification: the module layout is in crates/pr4xis/src/lib.rs (or ls crates/pr4xis/src/); the ontology count comes from find crates/domains/src -name ontology.rs | wc -l; the layer behaviour from the cited cargo test commands; and the archive machinery under crates/domains/src/formal/meta/{ontology_archive,artifact_identity,praxis_knowledge_graph} and crates/domains/src/social/software/markup/xml/owl/prx.rs.

Test Architecture

Praxis loads ontologies from large external corpora — the 89 MB Open English WordNet, the U.S. Code (Title 42 alone is 113 MB). How the test suite handles those corpora is itself a praxis-aligned design, not an afterthought.

The principle: parse-once is immutability

The .prx artifact exists because parsing a source once and addressing the result by content is the right shape: a source is parsed, compiled to a compact content-addressed .prx, and every consumer loads that immutable artifact instead of re-parsing. The test suite mirrors the same discipline — a corpus is parsed once and shared, never re-parsed per test.

This matters because of how the two test runners differ.

Two runners, on purpose

Nextest’s process-per-test isolation is exactly what you want for the bulk of the suite (crash isolation, per-test timeouts, cargo nextest archive build-once/run-many, cross-binary scheduling). But it means a test that parses a 89 MB corpus in a process-local static re-pays that parse for every test that touches it. With ~30 USC structural tests, that is ~30 redundant 100 MB parses.

So praxis runs each tier under the runner that fits it.

The tiers

1. Fast unit / axiom / proptest — small inline fixtures, in-crate #[cfg(test)]. Runner: nextest. The overwhelming majority of tests.

2. Heavy-corpus producer / round-trip — the few tests that must parse a raw multi-hundred-MB giant (full-title structural invariants, codec round-trips, byte-exact reconstruction). Runner: cargo test, in the workspace-excluded crates/praxis-corpus-tests, where a LazyLock parses each giant once for the whole binary.

3. Product-metric gates — assert the properties the .prx work delivers (compactness, load-speed, losslessness) over the on-disk corpora, so a regression fails CI. Also in praxis-corpus-tests.

4. Consumer — load the content-pinned .prx and assert on the materialized ontology, instead of re-parsing the source. The .prx-cache (below) is the shared cross-process fixture.

crates/praxis-corpus-tests

A dedicated crate, excluded from the default workspace (alongside wasm and e2e). Exclusion is deliberate:

• it depends on pr4xis-domains with test-internals (+ codegen, prx); as a non-member, that feature never unifies into the normal workspace build;
• the giants never re-parse under cargo test --workspace / nextest — they live only in this explicit, cargo test-run lane.

Each giant gets a LazyLock fixture; every test in the file borrows the one shared parse:

static TITLE_18: LazyLock<Option<UslmCorpus>> =
    LazyLock::new(|| load_uslm_corpus("legal/uscode/usc_title_18/usc_title_18-pl-119-90.xml"));

macro_rules! corpus_or_skip {
    () => {
        match &*TITLE_18 {
            Some(c) => c,
            None => { eprintln!("SKIP: not on disk"); return; }
        }
    };
}

#[test]
fn every_section_satisfies_every_axiom() {
    let UslmCorpus { title, .. } = corpus_or_skip!();
    axiom_every_section_has_num(title).expect("…");
    // … all 37 Title-18 tests share this one parse.
}

A corpus absent on a fresh checkout is skipped gracefully — the giants are fetched (pr4xis update), not committed.

The .prx-cache: a content-addressed fixture

pr4xis compile --compact parses each giant once and writes a compact, content-addressed .prx to the cache. The runtime’s loaded() fast path reads that cache through a fail-closed pin gate, with no XML re-parse. This is the cross-process parse-once fixture — the same “compile once, load an immutable artifact” the product ships, reused by the test suite. CI emits it (pr4xis compile --compact) before the test run.

Product-metric gates

The compactness and load-speed numbers the .prx work exists to deliver are asserted, not just observed. usc_compact_gate.rs iterates every on-disk USC title (source-agnostic, via the data-source registry) and gates:

• compactness — the compact .prx.gz is smaller than gzip(source);
• load-speed — materializing from the compact .prx is far faster than parsing the raw USLM XML (asserted on the aggregate with a generous margin, so it gates the regression without flaking on CI jitter);
• losslessness — the compact-loaded section count equals the XML-parsed count, including the 113 MB Title 42.

Running the lanes

# Fast bulk (nextest, all workspace crates):
cargo nextest run --workspace --profile ci --release

# Heavy-corpus lane + the product-metric gates (cargo test, parse-once):
cargo test --manifest-path crates/praxis-corpus-tests/Cargo.toml --release

# Doctests (nextest can't run them):
cargo test --doc --workspace --release

dev-ci runs all of these in sequence (see devenv.nix); CI mirrors it.

Intellectual Foundations

pr4xis draws from and synthesizes several academic traditions. This document traces the lineage and identifies where pr4xis extends existing work. For the runtime mechanics see Architecture. For the conceptual model — what an ontology is in this system — see Concepts.

Distinction-Calculus Lineage (Spencer-Brown → Heim → pr4xis)

Before going section by section through the modern category-theoretic and cybernetic foundations, it is worth naming the older tradition pr4xis sits in: distinction-calculus, the line of thought that treats the act of drawing a boundary as the primitive operation from which everything else is derived.

• G. Spencer-Brown, Laws of Form (1969) — starts with one instruction: “Draw a distinction.” From that single act, all of logic, Boolean algebra, and self-reference emerge. Already cited later in this document under “Distinction (Spencer-Brown)”.

• Burkhard Heim, Syntrometrische Maximentelezentrik (mid-20th century, published posthumously) — a logical framework built from predicates, permutation operators, mereological composition, and goal-oriented “telecenters”. Recently formalized using category theory, modal logic, Kripke semantics, and mereology in A Modernized Syntrometric Logic: Foundations and Applications (heim-theory.com, 2025).

• pr4xis (2025–2026) — composable ontologies in Rust, with category-theoretic functor proofs between domains. The substrate is novel as executable code; the structural ideas have prior art in Heim and Spencer-Brown.

The honest claim: pr4xis is the first executable, machine-checkable instance of this tradition across many domains. It does not adopt Heim’s physical-metaphysical claims (twelve-dimensional spacetime, particle mass formulas, teleological cosmology). The structural overlap with the modernized syntrometric logic is concrete and verifiable: both treat domains as categories with structure-preserving functors between them, use Kripke-style aspect-relative semantics, ground part/whole reasoning in classical extensional mereology, and model self-reference as a natural transformation.

The lineage claim is verified, not asserted. Heim’s 18 syntrometric primitives — distinction primitives (Predicate, Predikatrix, Dialektik, Koordination, Aspekt), structures (Syntrix, SyntrixLevel, Synkolator, Korporator), mereology (Part), teleological/hierarchical concepts (Telecenter, Maxime, Transzendenzstufe, Metroplex), permutation operators (SequencePermutation C, OrientationPermutation c), multi-aspect structure (Aspektivsystem), and self-observation (Reflexivity ρ) — are encoded at crates/domains/src/formal/meta/syntrometry/. Cross-functors verify the lineage at test time:

cargo test -p pr4xis-domains -- syntrometry

The primary Syntrometry → Pr4xisSubstrate functor has four intentional collapses out of 18 concepts — Dialektik, SequencePermutation, OrientationPermutation, and Aspektivsystem each collapse to a substrate parent because their full semantic content lives in dedicated cross-functor targets (Dialectics, Kripke, etc.). 14 of 18 round-trip as fixed points; counit loss is 0%. Seven cross-functors align Heim’s vocabulary with pr4xis’s existing and new ontologies:

• Syntrometry → MetaOntology (pr4xis’s gap-detection meta-ontology)
• Syntrometry → Staging — Futamura (1971) projection levels
• Syntrometry → Algebra — Goguen/Zimmermann ontology composition primitives
• Syntrometry → C1 — Dehaene (2014) Global Workspace Theory; Maxime ↦ Attention, Metroplex ↦ GlobalWorkspace. Heim anticipated the attention/workspace split GWT formalises 34 years later.
• Syntrometry → Dialectics — Heim’s Dialektik ↦ Hegel’s DialecticalMoment; opposition structure is carried by a dedicated Dialectics ontology (Aristotle, Hegel, Marx, Adorno, Priest).
• Syntrometry → Kripke — Aspekt ↦ KripkeFrame, Aspektivsystem ↦ AccessibilityRelation. Heim’s Aspektrelativität is structurally Kripke-style possible-worlds semantics (Kripke 1959, 1963).
• Distinction → Syntrometry — Spencer-Brown (1969) → Heim, the historical direction; ReEntry ↦ Synkolator preserving the self-application edge structure.

Per-functor collapse profiles and gap-analysis numbers live in the per-ontology README.

Modern Foundations (Section by Section)

Category Theory

The mathematical foundation. Category theory studies composition — how things combine while preserving structure.

Key concepts used in pr4xis:

• Objects and morphisms → Concept and Arrow
• Composition → transitive closure in reasoning ontology
• Functors → structure-preserving maps (analogy, translation, ontology evolution)
• Natural transformations → transformations between functors
• Axioms → category laws (identity, associativity, closure) verified exhaustively
• Category of elements (Grothendieck construction) → automatic trace schema derivation
• Discrete fibrations → every presheaf IS a fibration (Riehl 2019)

Category of Elements (El) — the construction that makes traceability automatic. Given a functor F: C → Set, El(F) has objects (c, x) where x ∈ F(c) and morphisms tracking how elements relate. Applied to ontology schemas: El unpacks the schema into individual observable elements, each decorated with PROV-O provenance. T(C) = El(C) +_O O_obs is the trace schema functor.

Key references:

• Saunders Mac Lane, Categories for the Working Mathematician (1971) — the foundational text- Steve Awodey, Category Theory (2010) — modern introduction
• Emily Riehl, Category Theory in Context (2016) — accessible with rich examples- Emily Riehl, Categorical Notions of Fibration (2019) — discrete fibrations = Set-valued functors- Bartosz Milewski, Category Theory for Programmers (2019) — bridge to software engineering
• Brendan Fong & David Spivak, Seven Sketches in Compositionality (2019) — applied category theory- Alexander Grothendieck, SGA1: Revetements etales et groupe fondamental (1961) — original fibered category definition
• Spivak, Functorial Data Migration (2012) — El(I) for database instances
• Spivak, Category Theory for the Sciences (2014) — pedagogical El treatment

Systems Thinking

The conceptual foundation. Systems thinking studies wholes, relationships, and patterns of organization.

Key insight: Category theory and systems thinking are isomorphic — the same structure viewed from different angles. Category theory provides the formal proof layer; systems thinking provides the intuitive conceptual layer. A functor maps between them.

Key references:

• Ludwig von Bertalanffy, General System Theory (1968) — the founding text
• Donella Meadows, Thinking in Systems (2008) — accessible introduction
• Peter Senge, The Fifth Discipline (1990) — systems thinking in practice
• Fritjof Capra & Pier Luigi Luisi, The Systems View of Life (2014) — synthesis across disciplines

Control Systems and Cybernetics

Control theory is the general science of feedback and regulation. Cybernetics is a specific type: control systems that involve communication (Wiener 1948). The distinction matters — not all control is cybernetic, and not all communication is control. pr4xis’s Engine is a cybernetic control loop; metacognition is second-order cybernetics.

Connections to pr4xis:

• Feedback loops → Engine (situation → precondition check → action → new situation)
• Requisite variety (Ashby) → ontology must be as complex as the domain it models
• Autopoiesis → self-creating systems (pr4xis generating its own ontologies via codegen)
• Second-order cybernetics → the observer is part of the system (pr4xis reasoning about itself via OwnToDolce functor)

Three key theorems:

• Requisite Variety (Ashby 1956): a controller must have at least as many states as the disturbances it regulates. V(controller) >= V(disturbances).
• Good Regulator Theorem (Conant & Ashby 1970): every effective controller must be (or contain) a model of its system. THIS IS WHY THE ENGINE NEEDS AN ONTOLOGY.
• Perceptual Control (Powers 1973): systems control their inputs (perceptions), not their outputs (behavior). Behavior is the means, not the end.

Key references:

• Norbert Wiener, Cybernetics (1948) — the founding text; control + communication
• W. Ross Ashby, An Introduction to Cybernetics (1956) — requisite variety, homeostasis- Roger Conant & W. Ross Ashby, Every Good Regulator of a System Must Be a Model of That System (1970) — the regulator theorem
• William Powers, Behavior: The Control of Perception (1973) — perceptual control theory
• Stafford Beer, Brain of the Firm (1972) — Viable System Model (5 recursive control levels)
• Karl Åström & Richard Murray, Feedback Systems (2008) — modern treatment (free online)
• Humberto Maturana & Francisco Varela, Autopoiesis and Cognition (1980) — self-creating systems
• Heinz von Foerster, Observing Systems (1981) — second-order cybernetics
• Gregory Bateson, Steps to an Ecology of Mind (1972) — patterns that connect

DOLCE (Upper Ontology)

The philosophical classification of being. DOLCE provides the taxonomy of existence that pr4xis uses to classify domains.

Why DOLCE over BFO or SUMO:

• DOLCE was designed specifically for linguistic and cognitive engineering — exactly pr4xis’s domain
• Its Endurant/Perdurant/Quality distinction maps naturally to pr4xis’s Situation/Action/Quality
• Its Social Object category captures rules, standards, and institutions — most of what pr4xis models

Key references:

• Claudio Masolo et al., WonderWeb Deliverable D18: Ontology Library (2003) — the original DOLCE specification
• Stefano Borgo et al., DOLCE: A Descriptive Ontology for Linguistic and Cognitive Engineering (2022) — updated formalization (arXiv:2308.01597)
• Barry Smith, Basic Formal Ontology (BFO) — the main alternative (used by US DOD/IC since 2024)
• Ian Niles & Adam Pease, Towards a Standard Upper Ontology (2001) — SUMO

Category Theory Applied to Systems

The synthesis that pr4xis builds on — researchers who have explicitly connected category theory to systems.

Robert Rosen — Life Itself: A Comprehensive Inquiry into the Nature, Origin, and Fabrication of Life (1991). Used category theory to model living systems as “relational” rather than mechanical. Key insight: a living system is characterized by its organization (morphisms), not its material (objects). Directly relevant to pr4xis’s ontological approach — we model rules and relationships, not physical stuff.

David Spivak — Category Theory for the Sciences (2014). Created “ologs” (ontology logs) — category theory applied to knowledge representation. His databases-as-categories framework is conceptually close to what pr4xis does with ontologies. Also: Seven Sketches in Compositionality (2018, with Brendan Fong) — accessible introduction to applied category theory.

Andrée Ehresmann & Jean-Paul Vanbremeersch — Memory Evolutive Systems (MES). Category-theoretic framework for complex adaptive systems that form, maintain, and evolve internal representations. Directly relevant to pr4xis’s metacognition roadmap — the system building internal models and evolving them.

John Baez & Mike Stay — Physics, Topology, Logic and Computation: A Rosetta Stone (2009). Demonstrates that category theory reveals deep structural parallels between physics, topology, logic, and computation. The “Rosetta Stone” metaphor aligns with pr4xis’s use of functors to map between domains.

Brendan Fong & David Spivak — An Invitation to Applied Category Theory (2019). Covers monoidal categories, operads, and hypergraph categories applied to databases, circuits, and signal flow — all systems.

Eugenia Cheng — The Joy of Abstraction (2022). Accessible bridge between category theory and everyday thinking. Relevant to making pr4xis’s formal foundations understandable.

Formal Ontology in Information Science

The discipline of building rigorous ontologies for computational systems.

Key references:

• Nicola Guarino, Formal Ontology in Information Systems (1998) — foundational text
• Thomas Gruber, A Translation Approach to Portable Ontology Specifications (1993) — “an ontology is a specification of a conceptualization”
• Nicola Guarino & Christopher Welty, Evaluating Ontological Decisions with OntoClean (2002) — rigorous methodology for ontological analysis

WordNet

The lexical database that pr4xis uses for the English language ontology.

Key references:

• George Miller, WordNet: A Lexical Database for English (1995) — the original
• Christiane Fellbaum (ed.), WordNet: An Electronic Lexical Database (1998) — comprehensive reference
• John McCrae et al., English WordNet: A New Open-Source Wordnet for English (2020) — the open version pr4xis uses

Categorial Grammar and Compositional Semantics

The formal foundation for pr4xis’s language understanding pipeline. Semantics IS a functor from syntax to meaning — this is not metaphor, it’s the literal mathematical framework.

Lambek Grammar (syntax as category)

Words have types (noun, verb, etc.). Types combine via function application: a transitive verb is a function that takes a noun phrase on the right and returns a verb phrase. The grammar IS a category: types are objects, type reductions are morphisms, and composition is guaranteed by the calculus.

Key references:

• Joachim Lambek, The Mathematics of Sentence Structure (1958) — the founding paper; syntax as algebraic calculus
• Joachim Lambek, Type Grammar Revisited (1999) — pregroup grammars, simplified Lambek calculus

Montague Semantics (meaning via functor)

Every syntactic rule has a corresponding semantic rule. Interpretation IS a functor from the syntax category to a logic category. Compositionality: the meaning of the whole is a function of the meanings of the parts.

Key references:

• Richard Montague, The Proper Treatment of Quantification in Ordinary English (1973) — the founding paper
• Barbara Partee, Montague Grammar (1976) — accessible introduction
• Janssen, Compositionality (1997) — formal treatment of the compositionality principle

DisCoCat (the modern synthesis)

Distributional Compositional Categorical model. The syntax category is Lambek pregroups, the semantics category is vector spaces (or logic), and the interpretation IS a functor preserving composition. This is exactly what pr4xis does — functors between categories — applied to language.

Key references:

• Bob Coecke, Mehrnoosh Sadrzadeh, Stephen Clark, Mathematical Foundations for a Compositional Distributional Model of Meaning (2010) — the DisCoCat paper
• Giovanni de Felice, Categorical Tools for Natural Language Processing (2022, Oxford thesis) — comprehensive modern treatment
• Coecke & Kissinger, Picturing Quantum Processes (2017) — string diagrams (the visual language of DisCoCat)
• Alexis Toumi et al., DisCoPy — open-source Python toolkit for computing with string diagrams and functors

Pregroup Grammars (the algebraic key)

Lambek (1999) showed that parsing is a group-like computation. A pregroup is a partially ordered monoid where every element has left and right adjoints. Word types are products of basic types with adjoints; parsing is contraction of the product to the sentence type.

Why pregroups matter for pr4xis:

• Parsing IS algebra: multiply word types, contract using adjoint laws
• The chart IS a semiring (Goodman 1999): + = all derivations, × = combining spans
• The Montague functor IS a compact closed functor from the pregroup to vector spaces (DisCoCat)
• Pregroups connect to our existing group theory ontology (Rubik’s cube)

Key references:

• Lambek, Type Grammar Revisited (1999) — pregroups replace slash types with adjoints
• Lambek, Pregroups and Natural Language Processing — parsing as group computation- Casadio & Lambek, A Tale of Four Grammars (Studia Logica, 2002) — the hierarchy AB → Lambek → Pregroup- Goodman, Semiring Parsing (Computational Linguistics, 1999) — chart as semiring- Yeung & Kartsaklis, A CCG-Based Version of the DisCoCat Framework (ACL, 2021) — CCG + DisCoCat- Pentus, Lambek Grammars are Context Free (1993) — free group interpretation

Type-Logical Grammar

Types-as-formulas, proofs-as-programs applied to natural language. A derivation of a sentence IS a proof that its types compose correctly. The Curry-Howard correspondence gives us: parsing = proof search, semantics = proof normalization.

Key references:

• Glyn Morrill, Type Logical Grammar (1994) — the standard reference
• Michael Moortgat, Categorial Type Logics (1997) — comprehensive survey
• Stanford Encyclopedia entry on Typelogical Grammar

The Pipeline (all functors)

Text → Tokens → SyntaxCategory → SemanticCategory → PragmaticCategory
         ↑            ↑                 ↑                  ↑
      Lexicon     Lambek grammar   Montague functor    Speech acts

Every arrow is a functor. Every step preserves structure. This is the theoretical foundation for pr4xis’s chatbot — no mechanical parsing, only ontological understanding through functors.

Metacognition and Self-Awareness

The theoretical foundation for pr4xis knowing what it knows and — critically — what it DOESN’T know. A system that can reason about its own ontological gaps.

Second-Order Cybernetics (von Foerster)

First-order cybernetics is “the cybernetics of observed systems.” Second-order cybernetics is “the cybernetics of observing systems” — the observer enters the domain of observation. When pr4xis reasons about why its grammar failed to parse a sentence, it IS second-order cybernetics: the system observing its own observing.

Key references:

• Heinz von Foerster, Observing Systems (1981) — the founding text of second-order cybernetics
• Ranulph Glanville, Second Order Cybernetics (PDF) — comprehensive introduction
• Humberto Maturana & Francisco Varela, Autopoiesis and Cognition (1980) — self-creating systems
• Ernst von Glasersfeld, Radical Constructivism (1995) — knowledge as constructed, not discovered

Meta-Ontology for Introspection (MOI)

An ontological model for tracing metacognitive experiences — what the system knew, when it knew it, and what happened when knowledge was insufficient. Directly applicable to pr4xis’s self-diagnosis of grammar and ontology gaps.

Key references:

• Olivares-Alarcos et al., Towards an Ontology for Robot Introspection and Metacognition (2023) — formal introspection model

Metacognitive Bi-Level Architecture

Metacognition is a two-level system: an object level (actual reasoning) and a meta level (monitors, evaluates, controls the object level). When pr4xis’s grammar fails to parse, the meta level detects the failure, diagnoses the gap, and decides whether to ask for clarification or attempt repair.

Key references:

• Wang & Zhao, Metacognition in LLMs (EMNLP 2025) — metacognitive capabilities and limitations
• Qi et al., Meta-R1: Empowering Large Reasoning Models with Metacognition — metacognitive monitoring and control

Self-Model and Self-Image

Three cybernetic traditions converge on the necessity of self-models:

Representational (Craik → Conant-Ashby → Powers → Metzinger): the system holds an explicit internal model of itself. Conant-Ashby (1970) proves this mathematically: any self-regulating system must contain a model of itself (homomorphism). Powers’ PCT (1973) places self-image at Level 11 (System Concept) — the highest level of perceptual control.

Organizational (Maturana-Varela autopoiesis, 1972/1980): the system does not have a model — it is its self-producing organization. Operational closure: processes produce the processes that produce them.

Reflexive (von Foerster eigenform, 1981; Bateson double description, 1972): the observer must include itself. Self-image = eigenform (fixed point of recursive self-observation). Bateson: valid self-image requires “double description” — self AND context simultaneously.

Key references:

• Kenneth Craik, The Nature of Explanation (1943) — dual internal model (world + self)
• Conant & Ashby, Every Good Regulator of a System Must Be a Model of That System (1970)
• William T. Powers, Behavior: The Control of Perception (1973) — PCT, 11-level hierarchy
• Gregory Bateson, Steps to an Ecology of Mind (1972) — cybernetics of self, double description
• Maturana & Varela, Autopoiesis and Cognition (1980) — operational closure
• Thomas Metzinger, Being No One (2003) — Phenomenal Self-Model (PSM)
• Maxwell Maltz, Psycho-Cybernetics (1960) — self-image as servo reference signal
• Louis Kauffman, EigenForm (2003) — fixed points of self-reference

Self-Description and Knowledge Base Introspection

For a system to describe what it knows, it needs formal vocabularies for self-description.

Key references:

• W3C, VoID — Vocabulary of Interlinked Datasets (2011) — describes what a knowledge graph contains
• W3C, DCAT — Data Catalog Vocabulary v3 (2024) — catalogs of datasets
• Herre & Loebe, A Meta-ontological Architecture for Foundational Ontologies (FOIS 2005) — using ontology’s own categories to describe itself
• Brian Cantwell Smith, Reflection and Semantics in LISP (POPL 1984) — causal connection requirement
• Kephart & Chess, The Vision of Autonomic Computing (IEEE 2003) — MAPE-K, Ksys self-model
• Lewis et al., A Survey of Self-Awareness in Computing Systems (IEEE 2011) — five awareness levels
• IEEE 1872.2, Autonomous Robotics Ontology (2021) — SelfModel as required class
• Nolte et al., Towards an Ontology for Robot Introspection and Metacognition (FOIS 2023) — MOI

Open World Assumption

When a query fails, does it mean “false” or “I don’t know”? The Open World Assumption (OWA) treats absence of knowledge as uncertainty, not falsity. pr4xis must distinguish:

• “Is a dog a mammal?” → YES (positive knowledge)
• “Is a dog a vehicle?” → NO (explicit negative knowledge via taxonomy)
• “Is a quark a boson?” → I DON’T KNOW (absent from ontology — open world)

Key references:

• Open World Assumption — Wikipedia
• Open World vs Closed World — Dataversity

Distinction (Spencer-Brown)

The most fundamental concept. Before categories, before logic, before knowledge — there is distinction. The act of drawing a boundary that separates “this” from “not this.”

Spencer-Brown’s Laws of Form (1969) starts with one instruction: “Draw a distinction.” From that single act, all of logic, Boolean algebra, and self-reference emerge. Von Foerster recognized this as the foundation of second-order cybernetics — the observer draws the distinction between self and observed.

In pr4xis, distinction is everywhere: Concept (this vs not-this), Boundary (inside vs outside), Opposition (A vs not-A), Bit (0 vs 1), Context (this meaning vs that meaning).

Key references:

• G. Spencer-Brown, Laws of Form (1969) — the founding text
• Louis Kauffman, Laws of Form — An Exploration in Mathematics and Foundations- Robin Robertson, Some-thing from No-thing: Spencer-Brown’s Laws of Form- Francisco Varela, A Calculus for Self-Reference (1975) — extending Spencer-Brown to self-referential systems

Information Theory

The science of quantifying, storing, and communicating information. Foundation for the information ontology (Bit, Byte, Reference, Text).

Key references:

• Claude Shannon, A Mathematical Theory of Communication (1948) — the founding paper- Alan Turing, On Computable Numbers (1936) — computability and information processing

Mereology

The formal theory of parts and wholes. Foundation for the mereology reasoning ontology (has-a relationships).

Key references:

• Peter Simons, Parts: A Study in Ontology (1987, Oxford) — the standard reference
• Stanford Encyclopedia — Mereology — comprehensive formal treatment
• Winston, Chaffin, Herrmann, A Taxonomy of Part-Whole Relations (1987) — meronymic relation types

Concurrency Theory

The formal theory of concurrent and parallel computation. Foundation for the concurrency ontology (Agent, SharedResource, Synchronization, Deadlock).

Key references:

• C.A.R. Hoare, Communicating Sequential Processes (1978) — CSP- Robin Milner, A Calculus of Communicating Systems (1980) — CCS
• Carl Hewitt, A Universal Modular ACTOR Formalism (1973) — Actor model

Event-Driven Architecture

Foundational patterns for event-driven systems. Basis for the events ontology (Event, Command, EventLog, Handler, EventBus).

Key references:

• Martin Fowler, Event Sourcing (2005) — pattern description
• Greg Young, CQRS Documents (2010) — Command Query Responsibility Segregation
• Exploring CQRS and Event Sourcing — Microsoft patterns & practices- Guizzardi et al., Events as Entities in Ontology-Driven Conceptual Modeling (2019) — formal event ontology based on UFO-B

RDF and OWL (Knowledge Representation Standards)

The formal foundation for reading and exchanging ontologies. RDF provides the data model (triples: subject-predicate-object). OWL provides the ontology language built on RDF. Together they define how to express and share formal knowledge — what pr4xis reads when loading OLiA, WordNet-LMF, or any published ontology.

RDF (Resource Description Framework):

• Everything is a triple: (subject, predicate, object)
• Subjects are IRIs or blank nodes; predicates are IRIs; objects are IRIs, blank nodes, or literals
• An RDF graph is a set of triples — no ordering, no duplicates
• RDFS adds: rdfs:Class (a set of resources), rdfs:subClassOf (taxonomy), rdf:type (instantiation), rdfs:domain/range (constraints)
• The RDFS class hierarchy: Resource → Class → Datatype; Resource → Literal; Resource → Property

OWL 2 (Web Ontology Language):

• Built on RDF, adds formal logic (Description Logic SROIQ)
• Entities: Classes, Object Properties, Data Properties, Annotation Properties, Named Individuals, Datatypes
• Class expressions: intersection, union, complement, oneOf (enumeration), existential/universal restrictions, cardinality constraints
• Property characteristics: functional, inverse functional, transitive, symmetric, asymmetric, reflexive, irreflexive
• Axioms: SubClassOf, EquivalentClasses, DisjointClasses, SubPropertyOf, ClassAssertion, PropertyAssertion
• Three profiles: OWL 2 EL (polynomial, for large ontologies like SNOMED CT), OWL 2 QL (LOGSPACE, for databases), OWL 2 RL (polynomial, for rule engines)

Key references:

• W3C, RDF 1.1 Concepts and Abstract Syntax (2014) — https://www.w3.org/TR/rdf11-concepts/
• W3C, RDF Schema 1.1 (2014) — https://www.w3.org/TR/rdf-schema/
• W3C, OWL 2 Web Ontology Language Structural Specification (2012) — https://www.w3.org/TR/owl2-syntax/
• W3C, OWL 2 Web Ontology Language Primer (2012) — https://www.w3.org/TR/owl2-primer/
• W3C, OWL 2 Web Ontology Language Direct Semantics (2012) — https://www.w3.org/TR/owl2-direct-semantics/
• W3C, OWL 2 Web Ontology Language Profiles (2012) — https://www.w3.org/TR/owl2-profiles/
• Franz Baader et al., An Introduction to Description Logics (2003) — formal logic underlying OWL- Tim Berners-Lee, James Hendler, Ora Lassila, The Semantic Web (Scientific American, 2001) — the vision

OLiA (Ontologies of Linguistic Annotation)

The formal standard for linguistic data categories. OLiA defines 1,300+ linguistic concepts in OWL/DL — every part of speech, morphological feature, and syntactic category across all natural languages. This is what pr4xis loads to KNOW what a Determiner, Copula, or Interrogative is — not from a hand-coded vocabulary, but from the research-grounded ontology.

Architecture (three tiers):

1. Reference Model (olia.owl) — universal linguistic data categories: MorphosyntacticCategory, MorphologicalFeature, SyntacticCategory
2. Annotation Models — OWL formalizations of specific tagsets (Penn Treebank, Universal Dependencies, EAGLES)
3. Linking Models — rdfs:subClassOf bridges from annotation models to reference model concepts

Key references:

• Christian Chiarcos & Maria Sukhareva, OLiA — Ontologies of Linguistic Annotation (Semantic Web journal, 2015) — the formal paper- Official URI: http://purl.org/olia/
• GitHub: https://github.com/acoli-repo/olia

Lexicon Ontology

The formal structure of a language’s word inventory. A lexicon is not a list — it is a structured mapping from forms to meanings where both sides have internal structure.

Three converging models:

• LMF (ISO 24613): Language → Lexicon → LexicalEntry → Form + Sense. The international standard.
• OntoLex-Lemon (W3C 2016): Three-way bridge: ontology entity ↔ lexical sense ↔ lexical concept. Bridges lexicons and ontologies in RDF/OWL.
• Generative Lexicon (Pustejovsky 1991): Each entry carries four qualia (Aristotle’s aitia): FORMAL (is-a), CONSTITUTIVE (has-a), TELIC (purpose), AGENTIVE (origin).

Open class vs closed class — nearly universal but not absolute. Open class (nouns, verbs) accepts new members; closed class (determiners, pronouns, copulas) is finite and fixed. In some languages adjectives are closed class. In Japanese pronouns are effectively open.

Language-agnostic design — Hebrew uses consonantal roots + vowel patterns (binyanim), not “words.” Chinese has no word boundaries. Turkish agglutinates. The Language trait provides lexical_lookup — each language implements its own segmentation and morphological analysis.

Key references:

• Pustejovsky, The Generative Lexicon (Computational Linguistics, 1991) — structured lexical entries- Jackendoff, Foundations of Language (2002) — the Parallel Architecture; the mental lexicon
• OntoLex-Lemon, W3C Community Report (2016) — lexicon-ontology bridge in RDF/OWL
• OntoLex-Lemon as bridge for WordNets (GWC 2019)
• ISO 24613 (LMF), Lexical Markup Framework (2019/2024) — international standard
• Farrar & Langendoen, GOLD: General Ontology for Linguistic Description (2003)

Spelling Error Ontology

The science of misspelling. Spelling errors are classified on three orthogonal axes — every error is a point in this three-dimensional space.

Axis 1 — Etiology (WHY): Competence errors (the writer doesn’t know the spelling) vs performance errors (the writer knows but mistypes). This maps to the dual-route model of spelling production (Coltheart 1981).

Axis 2 — Linguistic Level (WHAT): Phonological (sounds wrong), Orthographic (sounds right but spelled wrong), Morphological (morpheme boundary error), Visual (letter shape confusion). The POMAS framework (Silliman, Brimo 2013).

Axis 3 — Operation (HOW): Substitution, Deletion, Insertion, Transposition, Run-on, Split. Damerau (1964): >80% of misspellings involve a single operation.

The noisy channel model (Shannon 1948, applied by Kernighan, Church & Gale 1990): spelling correction IS a functor — the inverse of the error channel.

Orthographic Depth Hypothesis (Katz & Frost 1992): shallow orthographies (Finnish, Spanish) produce mostly performance errors; deep orthographies (English, French) produce mostly competence errors.

Key references:

• Damerau, A technique for computer detection of spelling errors (1964) — the four basic edit operations
• Kukich, Techniques for automatically correcting words in text (ACM Computing Surveys, 1992) — seminal survey
• Brill & Moore, An improved error model for noisy channel spelling correction (ACL, 2000) — string-to-string model
• Pollock & Zamora, Collection and characterization of spelling errors in scientific text (1983) — 50K+ errors analyzed
• Coltheart, Dual-route model of reading/spelling (1981) — cognitive architecture
• Caramazza & Miceli, The structure of graphemic representations (1990) — graphemic buffer
• Wing & Baddeley, Spelling errors in handwriting (1980) — serial position effects
• Katz & Frost, Orthographic Depth Hypothesis (1992) — writing system determines error patterns
• Mitton, English Spelling and the Computer (1996) — Birkbeck corpus (36K misspellings)

Ontological Architecture

pr4xis’s architecture is a novel synthesis of five existing ideas that have never been combined:

What is novel: an architecture where domain knowledge lives in composable ontologies rather than in mechanical processing logic. There is no parser-with-special-cases, no rule-engine-with-hardcoded-strings, no if-statements branching on domain values. Cross-domain composition is done via verified functors that preserve behavioral properties, and the architecture is justified by the Good Regulator Theorem.

Key references:

• Guarino, Formal Ontology and Information Systems (FOIS 1998) — defined ontology-driven systems
• Spivak, Ologs: A Categorical Framework for Knowledge Representation (PLoS ONE, 2012)
• Spivak, Functorial Data Migration (2010) — functors between database schemas
• Fiadeiro, Categories for Software Engineering (Springer, 2005)
• Goguen & Burstall, Institutions: Abstract Model Theory (JACM, 1992)
• Gangemi, Ontology Design Patterns for Semantic Web Content (2005)
• Guizzardi et al., UFO: Unified Foundational Ontology (2022) — OntoUML
• W3C, Ontology Driven Architectures (Working Group Note, 2006)
• Pan, Staab et al., Ontology-Driven Software Development (Springer, 2012)

Where pr4xis Extends Existing Work

1. Category theory + DOLCE synthesis. Using category theory as the formal proof mechanism for upper ontological classification. Existing work uses either category theory OR formal ontology; pr4xis combines them with a verified functor.

2. Self-application. Using the system’s own tools (functors) to evolve its own ontology. The OwnToDolce functor is pr4xis reasoning about itself — second-order cybernetics formalized in code.

3. Ontology evolution via functor. When transforming ontologies, create the new one alongside and prove the mapping. This pattern is implicit in categorical database migration (Spivak) but pr4xis applies it to ontological evolution explicitly.

4. Reasoning ontology as reusable patterns. Taxonomy, mereology, causation, equivalence, opposition, context — formalized as generic category patterns that any domain instantiates. Individual patterns exist in the literature; the unified set with axioms and property-based testing is new.

5. Build-time ontology generation. Using Rust’s build system to parse authoritative data sources (WordNet, W3C specs) through ontological understanding (not mechanical parsing) and generate static, tested code. The “no mechanical processing” principle — every data interaction goes through an ontology.

6. Cross-domain functor proofs. Proving that domains ARE instances of abstract ontologies: traffic IS a system (TrafficToSystems), chess IS concurrent (ChessToConcurrency), chess IS event-driven (ChessToEvents), systems ARE concurrent (SystemsToConcurrency), event-driven IS concurrent (EventsToConcurrency). The equivalence triangle System ↔ EventDriven ↔ Concurrent is proven by functor composition.

7. Lambek + Montague + DisCoCat in Rust with property-based testing. Implementing categorial grammar, compositional semantics, and the syntax→semantics functor in Rust with exhaustive category law verification. Existing implementations (DisCoPy) are in Python without formal verification. pr4xis proves the functor laws hold via property-based testing.

Related

• Architecture — the five-layer Rust stack and runtime mechanics
• Concepts — what ontologies are and how they compose via functors
• README — the project entry point with the LLM contrast table and the bioelectricity gap-detection result
• Per-ontology citings.md (pending #57) — once each ontology has its own bibliography, this document becomes the workspace-wide foundations index that the per-ontology files cite into

• Document date: 2026-04-14
• Note on paper paths: This document used to point at docs/papers/*.pdf for several references. Per #57, the PDFs live alongside the ontologies that cite them via per-ontology citings.md files; this document cites sources by author/year only.

Ontology Evolution

Knowledge changes. Scientific understanding deepens, terminology shifts, errors get corrected, fields merge. An ontology that cannot grow without breaking its existing users is a dead ontology. pr4xis treats evolution as a first-class concern, with a single rule:

Transform ontologies via functor. Never rewrite.

This page explains what that means and why it works.

The principle

When an ontology needs to change — concepts added, deprecated, split, merged, or refined — the change is expressed as a functor between the old version and the new one. The old ontology is not deleted; it is preserved alongside the new, and the functor is the mathematical proof that everything provable in the old version is still provable in the new one (or that specific things have been intentionally invalidated, with the ones that change made explicit).

Categorically, this is the same machinery pr4xis already uses for cross-domain composition. A cross-domain functor proves that domain A’s structure embeds in domain B’s. A cross-version functor proves that ontology version 1’s structure embeds in version 2’s. Both are first-class theorems verified at test time.

The alternative — silently rewriting an ontology in place — has two failure modes pr4xis avoids:

1. Hidden breakage. Existing tests that passed against version 1 silently start using version 2, and any change that broke a previously-true claim is invisible until something downstream fails.
2. Lost provenance. Once the old version is gone, there is no way to ask “what changed and why” — the audit trail is the diff in git, not a categorical proof object.

With the functor pattern, both problems are solved by construction: the old ontology stays compilable, the new one stays compilable, and the functor between them either passes the laws check or fails it explicitly.

The patterns

Five common evolution operations, each expressed as a functor:

Add a concept

The new ontology has all the old concepts plus the new one. The functor Old → New is the inclusion functor — every old concept maps to itself, every old morphism maps to itself. The functor laws hold trivially. Existing tests against the old ontology continue to pass; new tests against the new ontology can use the new concept.

Refine a concept (add a quality, add an axiom)

The new ontology has the same concepts but with additional structure on one of them — a new Quality attached, a new structural axiom enforced. The functor Old → New is still inclusion, but downstream tests that depend on the new structure use the new ontology directly. Old tests are not affected unless they assumed the absence of the new structure.

Deprecate a concept

Add a #[deprecated] annotation to the old concept and create a New version without it. The functor Old → New cannot be a total inclusion — the deprecated concept has nowhere to go in the new ontology. Two valid handlings:

• Map to a placeholder. The deprecated concept maps to a Deprecated entity in the new ontology that exists only to hold its identity. Useful when downstream code still references it by name.
• Document the removal in the functor’s domain restriction. The functor is partial — it is defined only on the non-deprecated concepts. Tests that try to map the deprecated concept fail at compile or test time, surfacing the dependency.

Split a concept (gap closure via context)

The pattern that the gap detection result demonstrates concretely. A single concept in the old ontology turns out to encode two distinct things; the new ontology splits them. The mechanism is ContextDef::resolve — the old Kv becomes Kv_in_Constitutive_Context vs Kv_in_Therapeutic_Context, and a ContextDef resolves which one is meant in any given query. The functor from the old ontology to the new is no longer total — it requires a context to disambiguate. This is the only pattern in pr4xis where evolution requires changing the calling code, not just the ontology.

Merge two concepts

The opposite of split. Two concepts in the old ontology turn out to be the same thing; the new ontology merges them. The functor Old → New collapses the two old concepts onto one new concept. Provable because category theory allows non-injective functors as long as the laws still hold.

Why this matters

Most ontology systems treat a knowledge base as a single mutable artifact: edit in place, hope nothing downstream breaks, run tests, fix what surfaced. pr4xis cannot do that and stay true to its core promise (every claim is provable; nothing is guessed). If an ontology silently rewrote concepts in place, every downstream proof would be re-grounded against potentially-incompatible axioms with no record of what changed.

The functor pattern makes evolution explicit, machine-checkable, and reversible. Explicit because the functor must be written down. Machine-checkable because the functor laws must hold. Reversible because the old ontology is still there — you can always run a test against the previous version, or compose a chain of evolution functors and ask exactly what migrated where.

Where evolution gets triggered

Three common triggers in practice:

1. Gap detection surfaced a missing distinction. The Molecular ⊣ Bioelectric adjunction collapsing 85.2% of entities revealed that Kv was conflating two roles. Evolution closed the gap with a ContextDef split. See Gap detection in scientific ontologies.
2. A new source paper invalidates an old axiom. Research updates the consensus; the ontology needs to follow. The new ontology uses the new axiom; the functor either preserves the old structure (if the new axiom is a refinement) or is partial (if the old axiom is now disproven and downstream code must update).
3. Cross-domain composition reveals a name collision. Two ontologies built independently use the same name for different things. The fix is a functor that renames one to disambiguate, then the composition can proceed.

Where to look in the codebase

• crates/domains/src/natural/biomedical/molecular/ — the MolecularFunctionalContext and ContextDef::resolve that closed the Kv gap
• crates/pr4xis/src/category/validate/ — the check_functor_laws validator that every evolution functor must pass
• crates/pr4xis/src/ontology/reasoning/context.rs — the ContextDef trait that handles context-driven resolution

Related

• Concepts — what an ontology is, why categories, how functors work
• Architecture — the five-layer Rust stack and the engine that runs these ontologies
• Foundations — academic lineage including Spivak’s functorial data migration, which this pattern is modeled after
• Gap detection — the bioelectricity result that demonstrates evolution closing a real gap
• #46 — the issue that prompted this doc

• Document date: 2026-04-14

Domain Catalog

Note (2026-07-11): This page is in transition. The previous catalog enumerated ~21 domains using a science::math / games::chess / systems::* organization that no longer matches the codebase. The current workspace contains 182 ontologies under a different structure (formal/applied/social/natural/cognitive), and a hand-maintained catalog of every entry is not the right shape going forward. Instead, this page now points at the canonical source, the current organization, and the two pieces of in-flight work that will replace it: per-ontology READMEs (#57) and the source-of-truth report pipeline (#60).

Canonical source

Every ontology lives at exactly one path under crates/domains/src/. The full list is re-derivable by:

find crates/domains/src -name ontology.rs

Pipe it to | wc -l to count; today that returns 182 ontologies.

Every ontology directory contains an ontology.rs file with the pr4xis::ontology! invocation that declares its concepts, kinded morphisms, axioms, and metadata. To understand any specific ontology, read its ontology.rs directly. Per-ontology README.md and citings.md files are pending #57.

Current organization

crates/domains/src/
├── formal/                      formal sciences — math, information, calculator, meta
│   ├── math/                    linear algebra, geometry, probability, statistics, signal
│   │                            processing, control theory, rotation, temporal, quantity
│   ├── information/             communication, concurrency, dialogue, events, knowledge,
│   │                            measurement, provenance, schema, storage, systems, diagnostics
│   ├── calculator/              scientific calculator with exact rationals
│   └── meta/                    ontology diagnostics, gap analysis, archive,
│                                knowledge-graph, artifact-identity,
│                                well-behaved-lens, source-taxonomy
│
├── applied/                     applied engineering domains
│   ├── sensor_fusion/           Kalman filter, observation, state, time, frame, fusion
│   ├── navigation/              AHRS, GNSS, IMU, INS-GNSS, celestial, odometry
│   ├── perception/              occupancy grid, lidar-camera, radar-camera fusion
│   ├── tracking/                single-target, multi-target, radar tracking
│   ├── space/                   orbital mechanics, attitude determination
│   ├── underwater/              sonar, AUV control
│   ├── industrial/              process, structural engineering
│   ├── localization/            SLAM, terrain
│   ├── hardware/                elevator dispatch, traffic signal control
│   └── theming/                 base16 color theme validation, WCAG contrast
│
├── social/                      social and human-system domains
│   ├── games/                   chess, rubik, tetris, simon
│   ├── software/                HTTP state machine, XML, OWL, RDF, LMF
│   ├── judicial/                case lifecycle, motion workflow, evidence, burden of proof
│   ├── compliance/              escalation ladder
│   └── military/                electronic warfare, situation awareness
│
├── natural/                     natural sciences
│   ├── physics/                 kinematics, relativity, energy
│   ├── biomedical/              biology, molecular, bioelectricity, biochemistry,
│   │                            biophysics, mechanobiology, immunology, pharmacology,
│   │                            pathology, hematology, electrophysiology, regeneration,
│   │                            chemistry, acoustics
│   ├── hearing/                 acoustics, anatomy, audiology, neuroscience, psychoacoustics,
│   │                            transduction, vestibular, music perception, signal processing,
│   │                            speech, environmental, devices, pathology, bone conduction
│   ├── geodesy/                 coordinate systems, reference frames
│   ├── colors/                  RGB, WCAG contrast, color theory
│   ├── physics/                 mechanics, electromagnetism, energy
│   └── music/                   scales, chords, intervals
│
└── cognitive/                   cognitive and linguistic domains
    ├── linguistics/             english (WordNet), grammar, lambek pregroup, lexicon,
    │                            morphology, orthography, pragmatics, semantics, symbols
    └── cognition/               epistemics, metacognition, self-model

This tree is the schematic view; it is not exhaustive (some sub-modules are omitted for brevity). For the complete list of every ontology directory, run find crates/domains/src -name ontology.rs.

Cross-domain functors

Domains are not isolated. They compose through proven functors — structure-preserving maps whose laws are checked at test time. To count the functor implementations in the workspace, run:

grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/ | wc -l

The most distinctive use of the functor machinery is in the biomedical stack, where three categorical adjunctions (Molecular ⊣ Bioelectric, Biology ⊣ Bioelectric, Pharmacology ⊣ Molecular) automatically detect missing distinctions in the source ontologies. To see the live percentages of how much information is lost in each round-trip:

cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

For the explanation of what these numbers mean, see the README and Concepts.

Why this page is short

A domain catalog written by hand goes stale immediately. Every commit that adds, removes, or renames an ontology silently invalidates a hand-maintained list. The right shape for this page is automated generation from the codebase, plus per-ontology pages for depth. Both are in flight:

• #57 — every ontology directory gets a README.md (one paragraph: what it models, its scope, its functor connections, its status) and a citings.md (the ontology’s bibliography). The README is the abstract, citings.md is the bibliography.
• #59 — every per-ontology README also gets two mermaid diagrams: an internal structure view (concepts and relations) and an external connections view (functors and adjunctions to other ontologies). Auto-generated from Concept::variants() and the existing functor implementations.
• #60 — a CI-generated pr4xis-report.json that captures every numerical metric the codebase produces (test counts, ontology counts, functor counts, adjunction collapse percentages, per-ontology entity/relation counts) and publishes it to GitHub Pages so the README and this catalog can pull live numbers instead of hand-typing them.

When all three land, this page becomes either a redirect to a generated catalog or a thin wrapper around the live JSON.

Related

• README — the project entry point
• Architecture — the five-layer Rust stack
• Concepts — what ontologies are and how they compose
• Foundations — academic lineage

• Document date: 2026-04-14
• Verification: the ontology count and functor count above are re-derivable by the cited find and grep commands. The structural tree is hand-typed and may drift; the canonical source of truth is crates/domains/src/ itself.

Glossary

Terms used across the pr4xis docs, in plain English. For deeper coverage of any of these, see Concepts, Architecture, or Foundations.

Axiom

A statement that is taken as given, without needing to be proven from anything else. The starting point of a chain of reasoning. In pr4xis, every axiom is either grounded in a published source (a textbook, a paper, a standard) or is a structural rule of the substrate itself (no cycles in taxonomies, etc.). When pr4xis says a claim is provable, it means the claim can be derived from the axioms by logical and categorical operations.

Ontology

In pr4xis, an ontology is more than a list of facts. It is a category (in the formal mathematical sense) of concepts and the kinded morphisms between them (subsumption, parthood, causation, opposition, …), plus the axioms the structure must satisfy. Every domain in pr4xis — biology, chess, sensor fusion, traffic signals, judicial workflow — is an ontology in this stricter sense. Authored declaratively via the ontology! proc macro.

Category

A mathematical structure with objects, morphisms (directed maps between objects), composition (combining two morphisms into a third), and identity (a morphism that does nothing). Two laws govern composition: associativity (the order of grouping doesn’t matter) and identity (composing with identity changes nothing). pr4xis treats every domain as a category and verifies the laws at test time. See Concepts for the long version.

Morphism

A directed map from one object to another inside a category. In pr4xis, a morphism is an Arrow between two Concept values, carrying a Kind tag and per-instance provenance — for example, a Subsumption-kinded Arrow Dog → Mammal represents “dog is a mammal”.

Functor

A structure-preserving map between two categories. If F: A → B is a functor, then every object x in category A has a corresponding object F(x) in category B, and every morphism f: x → y in A has a corresponding morphism F(f): F(x) → F(y) in B. Two laws hold: identities are preserved, and composition is preserved. In pr4xis, functors are how two ontologies are proved to share structure — when the functor laws hold, the source ontology faithfully embeds in the target. The workspace has more than 95 functor implementations; run grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/ | wc -l for the live count.

Functor laws

The two conditions a functor must satisfy:

1. Identity preservation: F(id_x) = id_{F(x)} — the identity morphism in the source maps to the identity morphism in the target.
2. Composition preservation: F(g ∘ f) = F(g) ∘ F(f) — composing two morphisms before mapping gives the same result as mapping each then composing.

Each law is an Axiom whose verify() returns a typed Verdict (proof or counterexample); they live at crates/pr4xis/src/category/laws.rs as functor_law_axioms::<F>() / assert_functor_laws::<F>(), run by cargo test -p pr4xis category::laws. Every functor in pr4xis must pass.

Adjunction

A pair of functors F: A → B and G: B → A that are “optimal inverses” of each other in a precise categorical sense (the unit η: Id_A → G ∘ F and counit ε: F ∘ G → Id_B natural transformations satisfy the triangle identities). In pr4xis, adjunctions are the mechanism for gap detection: when you take an object in A, apply F to get its image in B, then apply G to come back, you should get the original object. If you don’t, the original ontology has a missing distinction the math just surfaced. The bioelectricity Kv discovery is the canonical example — see Gap detection.

Reasoning system

In pr4xis, a category becomes an ontology when one or more reasoning systems are layered on top of it, each interpreting the morphisms in a specific way:

• Taxonomy — interprets some morphisms as is-a, with axioms NoCycles and Antisymmetric
• Mereology — interprets some morphisms as part-of, with axiom WeakSupplementation
• Causation — interprets some morphisms as causes, with axiom NoSelfCausation
• Opposition — interprets some morphism pairs as opposes, with axioms Symmetric and Irreflexive
• Context — disambiguates entities by context (ContextDef::resolve)
• Analogy — Analogy<F> is a wrapper around a functor F, treating the functor as a proven analogy between two domains

Each reasoning system is a Rust trait that an ontology can implement.

Engine

The runtime layer of pr4xis. An Engine<A> carries a current Situation (immutable world state), a list of Preconditions (rules that must hold before any action), and a function that applies an Action to produce a new Situation. When you call engine.next(action), the engine checks every precondition; if all pass, the action is applied and a trace entry is recorded; if any fail, an EngineError::Violated is returned with the failing precondition named, and the engine is recoverable for rollback. Supports back(), forward(), and branching.

Situation

An immutable snapshot of the world at a single point in time. Every action produces a new situation; the old situation is preserved in the engine’s history stack. This is what enables undo, redo, and branching without mutation.

Action

A proposed change to the current situation. Actions are checked against the engine’s preconditions before they are applied. An action that violates a precondition is blocked, named, and recoverable — never silently approximated.

Precondition

A rule that must hold before an action can be applied. A precondition takes the current situation and the proposed action and returns either Satisfied (with a reason) or Violated (with the failing rule and a diagnostic). Both carry context, so traces are useful for debugging and auditing.

Trace

The full structured history of every action the engine has processed. Each trace entry records the precondition results, the resulting situation (or the violation), and the timing. Used for audit, replay, and the TracedPipeline writer monad in chat-style applications.

Quality

A property that inheres in an entity (DOLCE term). For example, in the colors ontology, an Rgb entity has a Luminance quality. Qualities are how pr4xis attaches measurable or comparable values to objects without making the objects themselves carry the values.

Substrate

A word the README uses for “the engineering layer that makes ontologies composable with mathematical proof”. Loosely: the parts of pr4xis that aren’t specific to any one domain — the categorical machinery, the engine, the reasoning systems, the validators. The opposite of “the domains” themselves.

DOLCE

A foundational ontology from Masolo et al. (2003) that classifies all of being into Endurants (physical objects, social objects, mental objects), Perdurants (events, processes), and Qualities. pr4xis uses DOLCE as the upper-layer classification that domain ontologies classify their concepts against.

WordNet

An open lexical database of English (~107K concepts, decades of curation). pr4xis ingests WordNet via its codegen::wordnet build-time generator and exposes it as the English ontology. The WASM browser demo at pr4xis.dev loads it at startup.

ontology!

A Rust proc macro at pr4xis::ontology (re-exported from pr4xis-derive) that takes a declarative ontology specification (name:, source:, concepts:, labels:, optional sugar clauses is_a: / has_a: / causes: / opposes: for the canonical kinds, optional free-form edges: for other kinded morphisms, optional inline axioms: block) and emits the full implementation: the Concept enum, the Category impl, the Arrow impl with kind tagging, an Ontology impl whose fn axioms() inherits structural axioms from the catalog, and a type-level fn meta() -> Provenance for trace attribution. The macro is the canonical way to author an ontology in pr4xis. Every file at crates/domains/src/**/ontology.rs is an instance.

Provenance

The type returned by every ontology’s type-level fn meta() (and by every Functor, Adjunction, and Axiom for that matter). Carries the name, description, and citation set by the ontology! macro from its name: + source: clauses, plus version metadata. Used by the engine to attribute trace entries to the ontologies that produced them. Defined at crates/pr4xis/src/ontology/meta.rs.

Categorical extensional mereology (CEM)

The classical formal theory of parts and wholes — Simons (1987), Stanford Encyclopedia of Philosophy on Mereology. In pr4xis, parthood is expressed as Parthood-kinded morphisms in an ontology’s Category — the structural-axioms catalog (structural_axioms_for::<C>()) attaches NoCyclesOnKind automatically (OBO-RO; Smith et al. 2005). The full CEM WeakSupplementation axiom (if a whole has a proper part, it has another disjoint part — Casati & Varzi 1999) is not in the catalog; ontologies that need it add it as a domain axiom in their Ontology::axioms() impl. Heim’s modernized syntrometric logic also grounds part/whole reasoning in CEM, which is one of the structural alignments cited in Foundations.

Kripke semantics

A formal semantics for modal logic in which truth depends on which “possible world” you are evaluating in. pr4xis does not use full Kripke semantics today, but the modernized syntrometric logic tradition (Heim 1980, formalized 2025) does, and pr4xis’s pattern of multiple ontologies viewing the same domain through different functors is the computational realization of an aspect-relative Kripke frame. See the foundations doc for the connection.

Property-based testing

A testing technique in which invariants are expressed as properties that must hold for ALL inputs, and a library generates random inputs to look for counterexamples. pr4xis uses proptest for property-based testing of category laws, axiom satisfaction, and domain invariants. See the Wikipedia article on property testing for the broader context.

Manifest (praxis.toml)

The declarative registry of external sources praxis knows about. Lives at the workspace root, one [sources.<name>] block per source, naming the version, the SourceTaxonomy type, and the authoritative URL. Read at startup; unknown types fail closed. See Register a Source.

Lock (praxis.lock)

The integrity layer next to praxis.toml. Pins the expected content digest for every registered source’s on-disk bytes under [hashes], in the tagged grammar <algorithm>:<64 lowercase hex> — blake3: for every praxis-emitted pin (BLAKE3 is the one emit algorithm), sha256: / bare hex loadable as SHA-256. The LockManifestAgreement axiom verifies manifest, lock, and local file all agree.

PdfBuildExtraction

The typed const a codegen module emits at build time for sources whose authoritative format is PDF (see crates/domains/src/applied/data_provisioning/build_extraction.rs). One of five variants — Extracted { text, bytes_hash } / NotOnDisk / ParseFailed / Encrypted / UnsupportedContentType. Downstream canonical_audit.rs modules pattern-match on the variant. Anchored against W3C PROV-O (Lebo et al. 2013) as a typed prov:Activity outcome; each variant cites either an ISO 32000-2 section or a Wilkinson FAIR principle. The PdfBuildExtractionTotality axiom enforces exhaustiveness.

Scope: PDF-format sources are case law (court opinions), administrative orders, and similar court-system publications. Statutes are NOT in this set — US statutes load via USLM XML from uscode.house.gov per 1 U.S.C. § 204, through the bytes ⇄ Statute composed lens (M4.λ.3.b), not through PdfBuildExtraction. See the Registered source entry’s content-type matrix for the canonical format per source category.

Registered source

A [sources.<name>] entry in praxis.toml plus its matching praxis.lock entry plus the on-disk artifact at the path derived from the source’s SourceTaxonomy type. The unit the engine reasons about; the unit the pr4xis update CLI fetches and verifies.

SourceTaxonomy

The ontology behind a registered source’s type field. Roots at Source and branches into several families — Lexicon (Language, DomainLexicon, LegalLexicon, SchemaVocabulary leaves), LegalCorpus (Statute / UsFederalStatute, UsCodeTitle, Regulation, ConstitutionalArticle, ProceduralRule, CaseLaw leaves), and schema/test families (SchemaSpec with leaves including OntologyVocabulary, plus TestSuite). The is_a chain drives the decoder family and the on-disk path convention; Adjoins edges connect families that interoperate at runtime. Hart 1961’s primary/secondary rule distinction attaches as a quality. The full leaf set is the concepts: block in crates/domains/src/formal/meta/source_taxonomy/ontology.rs.

Data provisioning

The engine subsystem at pr4xis_domains::applied::data_provisioning that reads praxis.toml and praxis.lock, exposes typed RegistryEntry values to the rest of the runtime, and enforces eight axioms over the registered set (LockManifestAgreement, RegistryUniquenessByNameVersion, IdentityClaimsUseLeaves, DecoderTotalityPerKind, …). Loaded once per process via OnceLock; new manifest entries are visible only after process restart. The pr4xis update CLI is the operator-side surface of the same subsystem.

.prx

The self-contained archive format praxis packs a loaded source into. praxis reads a .prx back in milliseconds — instead of re-parsing the original source — after checking its fingerprint and refusing anything that has been altered, and it can still rebuild the original bytes exactly. Today praxis archives its own OWL ontologies, its U.S. Code (USLM) text, and the English dictionary (WordNet) this way; the English and U.S. Code archives are compact — smaller than the source download — for the fast read-back. The format is one realisation of the Archive ontology; the realisation lives at crates/domains/src/social/software/markup/xml/owl/prx.rs (gated on feature = "prx").

Archive

Content-addressed Merkle-DAG storage for an archived source, declared as the OntologyArchiveStorage ontology (crates/domains/src/formal/meta/ontology_archive/) rather than described only in prose — its concepts (ContentAddressableNode, MerkleDag, MerkleRoot, BinaryEnvelope, CompressedForm, SourcePin, LoadGate, IntegrityClaim) and its guarantees are runnable axioms. Each node is named by the cryptographic hash of its bytes (Merkle 1987; Benet 2014 IPFS), so identical content yields the identical address and the store deduplicates. The emit/load round-trip is a well-behaved lens (Foster et al. 2007): rebuilding from the archive reproduces the source bytes exactly.

Graph slice / GraphSnapshot

A content-addressed graph-slice primitive (crates/domains/src/formal/meta/praxis_knowledge_graph/snapshot.rs): select a slice of the knowledge graph as the relational image of a RootSet under an EdgeKindFilter — computed through the category’s own morphisms_from over the transitive closure the ontology! macro materializes, not a re-derived traversal — and content-address it as a Merkle DAG. The result is a ReachableSubgraph. Edges of a filtered kind that leave the slice (from inside, to outside) are its UnboundReferences; a slice with none is closed. The slice rehydrates through the same fail-closed admit gate the .prx archive uses, reusing the same content-hash and codec primitives — no parallel hash or codec.

IntegrityClaim

A typed, verifiable claim binding a resource to its expected content hash (W3C Subresource Integrity 2016) — a first-class concept in the Archive ontology, not a bare string compare. The underlying content hash is multi-algorithm: the RawHash leaf of the ArtifactIdentity taxonomy (crates/domains/src/formal/meta/artifact_identity/) covers SHA-256, SHA-512, and BLAKE3 (the archive’s SourcePin records a BLAKE3 content address — praxis emits under one algorithm and verifies claims under any). A claim is discharged — never merely trusted — by the fail-closed load gate.

Fail-closed load gate

The LoadGate concept (and the LoadGateFailsClosed axiom) of the Archive ontology. It admits a node only by re-deriving the content address from the node’s own bytes and checking it equals the externally recorded pin; it never trusts an embedded self-asserted label. On a mismatch, an unverifiable claim, or an absent pin, nothing is installed. Grounded in Dolstra (2006) fixed-output derivations, W3C SRI (2016), and TUF (Samuel et al. 2010).

Codegen / async loading / mmap

Three different mechanisms pr4xis supports for delivering ontology data into the runtime, all proven equivalent as functors from the same OntologyBuilder source:

• Codegen (build-time): pre-compile declarative source into static Rust. Used by the WordNet ontology in the WASM demo.
• Async loading (runtime): load ontology data from a file or stream asynchronously. Used for ontologies that are too large to embed or that need hot reloading.
• Memory-mapped files (runtime, zero-copy): mmap a precomputed binary directly into memory.

The choice between them is operational, not semantic. See Architecture for the layer description.

• Document date: 2026-04-14
• Verification: every term that names a code element (ontology!, Engine, ContextDef, etc.) corresponds to actual code in crates/pr4xis/src/ or crates/domains/src/. Grep to verify.

pr4xis for Engineers

You are an engineer evaluating whether to put pr4xis in your stack. This page is for you.

What it is

pr4xis is a domain engine for systems that need to be correct, not just plausible. It is a different kind of AI — it derives its answers from formally proven axioms instead of statistical patterns — and it runs as a Rust workspace you embed directly in your code. There is no service, no GPU, no API key, no model weights. The engine carries the knowledge and runs it: the worked examples in crates/domains/src/ (the dialogue state engine, the HTTP and judicial-lifecycle state machines) execute their transitions against loaded axioms rather than merely checking something else. Running more of the workspace this way is the direction, not a finished claim.

Concretely:

• A state engine, demonstrated end to end. You define situations, actions, and preconditions; the engine validates a transition against its loaded ontologies and either applies it or names the exact rule that blocked it. The worked example is the dialogue engine the pr4xis chat binary drives, alongside the HTTP and judicial-lifecycle state machines under crates/domains/src/. No silent approximation, no probabilistic answer.
• An axiomatic reasoner. When pr4xis tells you that a fact in one domain implies a claim in another, the implication is a chain of categorical morphisms back to a published source. You can ask which axioms participated; you can reproduce the derivation deterministically.
• A composable knowledge substrate. pr4xis loads more than 160 ontologies today (biomedical, sensor fusion, navigation, perception, tracking, space, underwater, industrial, linguistics, formal mathematics, music, colors, judicial workflow), composed through cross-domain functors whose laws are checked at test time. To count either live, run find crates/domains/src -name ontology.rs | wc -l and grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/ | wc -l. More ontologies are still to be added — that’s the bigger opportunity, and the substrate exists precisely so the additions can be machine-checkable.

The contrast with statistical AI: where an LLM predicts the next token, pr4xis derives the next claim. Where an LLM hallucinates as a structural feature, pr4xis instead derives — every claim it makes traces to a proof over its loaded axioms, and where those axioms don’t reach, it abstains rather than guesses. Where an LLM is opaque, pr4xis names the failing axiom when something doesn’t hold. See the README for the side-by-side comparison.

What you get out of the box today

How it composes with what you already have

pr4xis is a Rust library, not a service. There is no daemon, no API key, no GPU requirement. You add pr4xis-domains (or just the parts of it you need) as a Cargo dependency and call the engine directly. The chat surface is a thin wrapper; the WASM demo is one binary that’s <1 MB plus the loaded ontology data.

The composition patterns:

1. As the runtime decision engine inside your service. Your code calls engine.next(action) whenever a state transition happens. The engine validates against preconditions and either returns the new state or returns a named violation. The engine is the decision; it doesn’t checkpoint someone else’s decision.
2. As a domain rules engine for state machines. HTTP connection state, judicial case lifecycle, traffic signal control, elevator dispatch — pr4xis already has these as worked examples. The pattern generalizes to anything where “what’s allowed next” depends on rich context.
3. Alongside an LLM, where the LLM produces text and pr4xis produces the answers that have to be right. This is not “pr4xis checks the LLM” — it’s “pr4xis is the part of the stack that knows things, and the LLM is the part that talks”. They are different functions, both first-class. Use each for what it’s good at.

What you should do first

1. Run the test suite locally:

   git clone https://github.com/i-am-logger/pr4xis
   cd pr4xis
   cargo test --workspace
   

2. Open one of the existing ontologies (crates/domains/src/social/judicial/ontology.rs is a good starter — lifecycle of a legal case modeled as a kinded relation graph). Notice that it’s a single pr4xis::ontology! block.
3. Run the WASM demo: pr4xis.dev. Try a few queries. File issues on the ones that break.
4. If your domain isn’t covered: build your own ontology from a paper.

What it is NOT

• Not a knowledge graph database. Knowledge graphs store facts; pr4xis proves theorems against axioms. The reasoning systems verify category laws, not just SPARQL queries.
• Not a theorem prover for pure math. Coq, Lean, and Agda do that, and they do it well. pr4xis is the engine for applied domain knowledge.
• Not a magic ontology generator. Humans still author ontologies, with assistive tooling planned. pr4xis runs them; it does not invent them.
• Not a complement to LLMs. It is the alternative AI for tasks where accuracy and verifiability matter. The composition with an LLM (point 3 above) is one valid pattern, not the project’s identity.

Where to go from here

• Architecture — how the five-layer stack works
• Concepts — categories, functors, adjunctions, in plain English
• Get started — install, run, write your first interaction
• Build an ontology from a paper — the contributor authoring guide
• Glossary — every term defined

• Document date: 2026-04-14

pr4xis for Researchers

You are a researcher — academic, industrial, or independent — evaluating whether pr4xis is intellectually credible and worth your time. This page is for you.

The novelty claim, briefly

pr4xis is, to our knowledge, the first executable, test-verified instance of a categorical substrate for composing scientific ontologies across many domains.

That is a careful sentence. Each clause matters:

• Executable. The substrate runs as a Rust workspace, not a paper or a Coq library. Every concept, every functor, every axiom corresponds to compilable code.
• Test-verified. Category laws and functor laws are checked at test time via cargo test --workspace — more than 7,000 tests in the workspace today. To count them, run grep -rn "#\[test\]" --include='*.rs' crates | wc -l.
• Categorical substrate. Domains are categories in the formal mathematical sense. Compositions between domains are functors with verified laws. Adjunctions detect missing distinctions.
• For composing scientific ontologies. The intent is not pure-math theorem proving (Coq/Lean/Agda do that). It is putting WordNet, BioPortal, the Gene Ontology, DOLCE, and the rest into a substrate where they can be combined with proof.
• Across many domains. More than 160 ontologies today covering biomedical, sensor fusion, navigation, linguistics, formal mathematics, music, colors, judicial workflow, and more (find crates/domains/src -name ontology.rs | wc -l).

The full novelty argument with comparisons to prior art lives in Novelty.

The intellectual lineage

pr4xis sits in a sixty-year tradition of distinction-calculus and compositional logic:

• G. Spencer-Brown, Laws of Form (1969) — the calculus of indication. Spencer-Brown starts with one instruction: “Draw a distinction.” From that single act, all of logic, Boolean algebra, and self-reference emerge. Spencer-Brown’s mark is the same gesture as a category-theoretic morphism: the act of distinguishing one object from another.

• Burkhard Heim, Syntrometrische Maximentelezentrik (mid-20th century, published posthumously) — a logical framework built from predicates, permutation operators, mereological composition, and goal-oriented “telecenters”. For most of its history, syntrometry was treated as Heim’s philosophical scaffolding for his unified field theory and was not engaged with on its own terms.

• A Modernized Syntrometric Logic (2025) — heim-theory.com — explicitly reformulates Heim’s syntrometric machinery using modern category theory, modal logic with Kripke semantics, classical extensional mereology, and natural transformations. This is the decisive recent work for the lineage claim.

The structural alignment between pr4xis and the modernized syntrometric logic is concrete in eight of nine mapping points (verified during the #51 first-pass research):

1. Syntrix as category of leveled structures, Synkolator as endofunctor ↔ pr4xis’s ontology-as-category + functors-as-morphisms-of-ontologies
2. Aspektrelativität via Kripke frames ↔ pr4xis’s multiple ontologies viewing the same domain via functorial alignment
3. Classical extensional mereology for Part(A,B) ↔ pr4xis’s Kind::Parthood-tagged morphisms (NoCyclesOnKind from the catalog; WeakSupplementation available as a domain axiom)
4. Reflexivity as natural transformation ↔ pr4xis’s Self-Model ontology describing its own structure
5. Korporator as structure-mapping functor ↔ pr4xis’s cross-domain functors
6. Hypersyntrix as category-of-categories ↔ pr4xis’s higher-order composition through repeated functor application
7. Predicates as primitives ↔ pr4xis’s Concept enums (Guarino 2009)
8. C/c permutation operators (sequence and orientation) ↔ pr4xis’s morphism composition under associativity

The one that does NOT map: adjunctions. Heim does not have adjoint functors; the gap-detection mechanism that pr4xis uses — F and G as paired functors with unit and counit, round-trip collapse as a missing-distinction signal — has no Heim counterpart. This is genuinely pr4xis’s contribution.

What pr4xis explicitly does not inherit: Heim’s twelve-dimensional spacetime, particle mass formulas, “Metronic Gitter”, or teleological cosmology. The structural overlap is real; the metaphysical extensions are not.

What’s verifiable today

What’s intentionally not yet claimed

• No claim of formal proof in Coq/Lean/Agda. pr4xis verifies its axioms via property-based testing and exhaustive enumeration of finite categories, not by interactive theorem proving. If you need a Coq mechanization of one of the proofs, that is open work.
• No claim that BioPortal, the Gene Ontology, etc., are integrated today. WordNet is integrated via codegen::wordnet. The biomedical stack consists of pr4xis-authored ontologies that are informed by the literature but not imported from BioPortal. Importing existing ontology corpora is the next layer of work.
• No claim of completeness in any single domain. The biology ontology has ~30 concepts; real biology has hundreds of thousands. The point is that the categorical substrate is the right shape for them, not that every concept has been authored yet.

Open research directions

The pr4xis project has several open questions where research collaboration would land:

1. Adjunction discovery. The biomedical adjunctions were authored by hand. The categorical question: given two categories with shared morphisms, is there an algorithm that finds candidate adjunctions automatically? This is a real open research problem.
2. Composition with existing OWL/RDF ontology corpora. Importing BioPortal, the Gene Ontology, OBO Foundry, and DOLCE as composable categories. The conceptual mapping (RDF triples → category morphisms, OWL axioms → category-theoretic axioms) is sketched but not implemented.
3. The relationship to Spivak’s ologs and functorial data migration — pr4xis’s evolution-via-functor model (see Evolution) is a specific instance of Spivak’s pattern, but the connection has not been formalized in writing.
4. Self-reference and reflexivity. The Self-Model ontology describes pr4xis’s own type system. The fixed-point semantics (the system observing itself) is a topic where second-order cybernetics, eigenform theory, and category theory all converge. Pr4xis has the executable substrate for this, but the theoretical write-up is not done.
5. LLM weight projection (#50) — projecting an external ontology onto LLM internals via a functor as a mechanistic interpretability framework. Speculative, but the substrate is the right shape for it.

Where to go from here

• Concepts — what an ontology is in pr4xis, why categories, how functors and adjunctions work
• Foundations — the full academic lineage with sources for every claim
• Novelty — the long-form novelty argument and the comparison to prior art
• Gap detection — the bioelectricity result in technical detail
• Paper outline — the draft architecture paper

• Document date: 2026-04-14

What’s Novel About pr4xis

This document makes the novelty argument carefully: what pr4xis claims to be the first to do, what is genuinely new versus standing on prior art, and how the project applies its own honesty principle to its lineage claims.

The short version: pr4xis is the first executable, test-verified, multi-domain instance of a categorical substrate for composing formally-grounded ontologies with proof. The substrate is novel as code; many of the structural ideas have a sixty-year intellectual history.

The novelty claim

pr4xis is, to our knowledge, the first executable, test-verified instance of a categorical substrate for composing scientific ontologies across many domains, with categorical adjunctions used to detect missing distinctions in the source ontologies automatically.

Each clause is calibrated to be defensible:

• “To our knowledge” is a hedge. We have not exhaustively surveyed every Coq/Agda/Lean library, every applied-category-theory project, or every formal ontology framework. If a prior project did the same thing, we would like to know. The hedge stays until we have done the literature survey, which is open work (see “Open verifications” below).
• “Executable” distinguishes pr4xis from formal frameworks that exist only as papers, theorems, or interactive proof scripts. pr4xis is a Rust workspace that compiles, runs, serves a WASM browser demo, and ships ontologies as executable artifacts.
• “Test-verified” means the structural laws (category laws, functor laws, axiom satisfaction) are checked at test time via cargo test --workspace. There are 4,855 such tests today.
• “Multi-domain” distinguishes pr4xis from frameworks that demonstrate the categorical substrate on a single domain (a database schema, a single biology taxonomy, etc.). pr4xis has 106 domain ontologies covering biomedical, sensor fusion, navigation, perception, tracking, space, underwater, industrial, linguistics, formal mathematics, music, colors, judicial, and more.
• “Adjunctions used for gap detection” is the most concretely novel claim. The bioelectricity Kv discovery (see Gap detection) is the first instance we know of where a categorical adjunction was used to automatically surface a missing distinction in a scientific ontology, leading to a real fix. The methodology is general — any pair of ontologies connected by an adjunction can be analyzed this way.

What is not original

The honest list of things pr4xis stands on:

• Category theory — Mac Lane (1971), Riehl (2016), Awodey (2010), and a sixty-year tradition. pr4xis is a consumer of category theory, not a contributor to its foundations.
• Applied category theory — Spivak’s ologs and functorial data migration (2010, 2012), Fong & Spivak’s Seven Sketches in Compositionality (2019), Coecke & Kissinger on categorical quantum mechanics (2017), the broader applied-CT community. pr4xis applies these patterns to scientific ontologies; it does not invent the patterns.
• Formal ontology — Guarino (1998), Gruber (1993), DOLCE (Masolo et al. 2003), BFO (Smith, ongoing). pr4xis adopts DOLCE as its upper layer and uses the existing formal-ontology vocabulary.
• Cybernetics and the Good Regulator Theorem — Conant & Ashby (1970), Ashby (1956), Wiener (1948), Bateson (1972), von Foerster (1981). The architectural justification (the engine must contain a model of the system) is Conant-Ashby; pr4xis is one specific way to satisfy the theorem.
• The DisCoCat tradition for compositional language — Coecke, Sadrzadeh & Clark (2010), Lambek pregroup grammar (1958, 1999). pr4xis’s linguistics pipeline is built on this.
• Distinction-calculus — Spencer-Brown’s Laws of Form (1969). The act of drawing a distinction is older than category theory and pr4xis is one descendent of that tradition.
• Syntrometric logic — Heim (1980, posthumously published), reformulated categorically in 2025. The lineage claim with respect to Heim is the most-prominent unverified assertion in the project. See “The Heim lineage — pending machine-verification” below for how we plan to convert it from research claim to test-checked theorem.

What is genuinely new

After subtracting the prior art, the things we believe pr4xis contributes — pending the literature survey that would let us drop the “to our knowledge” hedge:

1. Adjunction-based automatic gap detection in scientific ontologies. Categorical adjunctions are well-known in math and theoretical computer science; using them as a diagnostic on ontology pairs to surface missing distinctions is, as far as we know, original. The bioelectricity Kv result is the proof of concept. See Gap detection.

2. A multi-domain categorical substrate that compiles and runs. Spivak’s ologs are categorical knowledge representations but are presented mathematically rather than as a living codebase. Coq/Agda/Lean libraries for category theory exist but are oriented toward pure-math theorem proving, not applied domain reasoning across many fields. The combination — categorical substrate, multi-domain coverage, executable Rust, runtime engine, WASM browser surface — does not appear to exist in another project, but we have not done the exhaustive survey.

3. The ontology! proc macro pattern. A declarative way to specify an ontology that emits the Concept enum, the Category impl, the kinded Arrow impl (Subsumption / Parthood / Causation / Opposition / arbitrary user-defined kinds), the structural axioms inherited from the catalog (OBO-RO; Smith et al. 2005), and the Provenance metadata — all in a single block. The pattern is similar to Spivak’s olog notation but is concrete Rust code that the type system checks. We are not aware of an equivalent in another applied-CT framework.

4. Functor-based ontology evolution as a first-class concern. See Evolution. The pattern of “transform via functor, never rewrite” is implicit in Spivak’s functorial data migration but pr4xis applies it to ontological evolution explicitly and operationally — every evolution is a functor whose laws are checked at test time.

5. The explicit codegen / async / mmap functor equivalence. Three different mechanisms for delivering ontology data into the runtime, all proven equivalent as functors from the same source. This is a small-but-load-bearing piece of infrastructure that lets the same ontology run as a static binary, an asynchronously loaded resource, or a memory-mapped file without semantic drift.

The Heim lineage — machine-verified across eight functors

The most prominent lineage claim in the project is the structural alignment with the modernized syntrometric logic tradition (Heim 1980, reformulated categorically in 2025). Per the project’s core principle — every claim must be machine-checkable — this is operationalised as eight tested theorems (one primary lineage functor + seven cross-functors, including the historical-direction Distinction → Syntrometry embedding) spanning the substrate, meta-ontology layer, composition layer, cognitive layer, and modal/dialectical logic layers.

Verify

cargo test -p pr4xis-domains -- syntrometry

What the test proves

Heim’s 18 syntrometric primitives — distinction primitives (Predicate, Predikatrix, Dialektik, Koordination, Aspekt), structures (Syntrix, SyntrixLevel, Synkolator, Korporator), mereology (Part), teleological/hierarchical (Telecenter, Maxime, Transzendenzstufe, Metroplex), permutation operators (SequencePermutation C, OrientationPermutation c), multi-aspect (Aspektivsystem), self-observation (Reflexivity ρ) — are encoded as a pr4xis ontology at crates/domains/src/formal/meta/syntrometry/. A Functor: Syntrometry → Pr4xisSubstrate carries each Heim concept to its pr4xis-core counterpart. check_functor_laws verifies identity preservation + composition preservation exhaustively over every morphism. The structural alignment is no longer argued — it is proven.

Measured information-loss profile

The gap analysis on the primary lineage functor reports 4 intentional unit collapses out of 18 concepts (Dialektik, SequencePermutation, OrientationPermutation, Aspektivsystem) and 0% counit loss (the substrate is closed under the round-trip). The four collapses are honest: each of these concepts has a richer dedicated home — Dialektik → the Dialectics ontology, Aspektivsystem → the Kripke ontology, the permutations → endomorphism-class at the substrate level. Full precision is preserved by the corresponding cross-functors below.

Cross-functors to existing and new pr4xis ontologies

The primary lineage maps Heim into pr4xis’s categorical substrate; cross-functors preserve richer structure by routing into dedicated ontologies:

• Syntrometry → MetaOntology (ontology_diagnostics) — Heim’s categorical primitives match the meta-ontology vocabulary pr4xis uses to diagnose gaps across ontology pairs.
• Syntrometry → Staging (Futamura 1971) — Transzendenzstufen ↦ Futamura projection levels.
• Syntrometry → Algebra (Goguen / Zimmermann) — Korporator ↦ Mapping, Aspekt ↦ Product, Dialektik ↦ Coproduct, Telecenter ↦ Pushout. Heim’s composition operators align with the categorical primitives the pr4xis compose API uses at runtime.
• Syntrometry → Dialectics (Hegel, Aristotle, Marx, Adorno, Priest) — Heim’s Dialektik ↦ Hegel’s DialecticalMoment; opposition structure is carried by a dedicated literature-grounded ontology.
• Syntrometry → Kripke (Kripke 1959, 1963) — Aspekt ↦ KripkeFrame, Aspektivsystem ↦ AccessibilityRelation, Synkolator ↦ Necessity, Korporator ↦ Possibility, Reflexivity ↦ Reflexive (frame condition). Heim’s Aspektrelativität is structurally Kripke-style possible-worlds semantics.
• Distinction → Syntrometry (Spencer-Brown 1969 → Heim, historical direction) — kinded→kinded embedding; ReEntry ↦ Synkolator preserves the self-application edge structure.
• Syntrometry → C1 (Heim → Dehaene GWT) — Maxime ↦ Attention, Metroplex ↦ GlobalWorkspace. Heim anticipated the attention/workspace split Dehaene formalises 34 years later. The (Maxime, Aspekt, Selects) morphism lands on the declared (Attention, ConsciousAccess, Selects) in C1 — Heim’s “extremal of expedient ideas selects among candidate Aspekts” and Dehaene’s “attention selects which coalition accesses consciousness” are structurally the same morphism.

Each functor has check_functor_laws running against it as a test; the lineage is verified not just structurally but quantitatively (per-functor collapse profiles) and contextually (across the meta, composition, and cognitive layers of pr4xis).

What pr4xis explicitly does not inherit: Heim’s twelve-dimensional spacetime, particle mass formulas, Metronic Gitter, or teleological cosmology. The structural substrate is verified; the metaphysical extensions are not adopted.

Open verifications

For the novelty claim to lose its “to our knowledge” hedge, two more pieces of work are needed:

1. A literature survey for prior multi-domain categorical-ontology projects. Specifically: Coq/Agda/Lean libraries that implement category theory applied to multiple scientific domains; applied-CT frameworks that go beyond a single use case; ontology platforms (BioPortal, Cyc, etc.) that have flirted with categorical formalization. If any of them are doing what pr4xis is doing, we want to cite them — and either acknowledge the prior work or sharpen our novelty claim to the specific dimension where pr4xis is still first.

2. The Heim ontology and functor implementation (#62). Once the lineage is machine-verified, the “to our knowledge first executable instance of this tradition” claim can be defended without hedging.

Both are tracked. Neither is done.

How this document will evolve

Per the project’s own evolution model (see Evolution), this novelty document is itself subject to change — and the changes should be visible. Two specific updates are pending:

• When the literature survey lands: every “to our knowledge” hedge is either dropped (if no prior art is found) or replaced with a specific citation and a sharpened claim about what pr4xis still does that the prior project did not.
• When #62 lands: the Heim section moves from “pending machine-verification” to “verified by the following tests”, and the README’s lineage sentence loses its “to our knowledge” hedge for the Spencer-Brown / Heim half.

Related

• Foundations — academic lineage with sources for every claim
• Concepts — what an ontology is in pr4xis, why categories
• Gap detection — the bioelectricity result, the strongest single concrete demonstration of a novel methodology
• Paper outline — draft architecture paper
• #51 — the syntrometric logic first-pass research
• #62 — the Heim ontology implementation that will machine-verify the lineage

• Document date: 2026-04-14

pr4xis Architecture: Composable Domain Ontologies with Categorical Proof

Abstract

We present pr4xis architecture — a software architecture where domain knowledge lives in composable ontologies rather than in mechanical processing logic. Every domain is encoded as a category in the formal mathematical sense; cross-domain composition is achieved via category-theoretic functors that mathematically preserve behavioral properties; categorical adjunctions automatically detect missing distinctions in the source ontologies. The architecture is justified by the Good Regulator Theorem (Conant & Ashby, 1970): every effective controller must contain a model of its system. In pr4xis, the ontology IS the model. We demonstrate the architecture across 106 domains (physics, chess, natural language, traffic control, judicial proceedings, sensor fusion, biomedical reasoning, and more) with 4,855 machine-verified proofs and 61 proven cross-domain functors.

1. Introduction

The problem

Traditional software architectures embed domain knowledge in code. Domain-Driven Design puts the domain model in classes. Model-Driven Architecture generates code from UML models. Expert systems externalize rules but as flat if-then productions without compositional guarantees.

The claim

We propose that domain knowledge should live entirely in composable ontologies — formal descriptions of what exists and how things relate — and that the code should be a generic engine with no domain knowledge whatsoever. We call this pr4xis architecture.

The proof

The claim is not aspirational. We demonstrate it with a working system containing 106 domain ontologies, 61 proven functors between domains, and 4,855 machine-verified proofs. The same generic engine enforces chess rules, physics laws, grammatical constraints, and legal procedures.

2. Theoretical Foundations

2.1 Category Theory as the Composition Mechanism

• Objects and morphisms (Mac Lane 1971)
• Functors: structure-preserving maps between categories
• Natural transformations: transformations between functors
• Compact closed categories: pregroups for grammar (Lambek 1999)

2.2 The Good Regulator Theorem

Conant & Ashby (1970): every effective regulator must be (or contain) a model of the system it regulates. In pr4xis: the ontology IS the model. This is not a design choice — it is a mathematical requirement for effective control.

2.3 Requisite Variety

Ashby (1956): a controller must have at least as many states as the disturbances it regulates. The ontology must be as rich as the domain. An ontology that is too simple cannot regulate its domain effectively.

2.4 DOLCE Upper Ontology

Masolo et al. (2003): classification of being into Endurant (Physical, Social, Mental, Abstract), Perdurant (Event, Process), and Quality. Every domain ontology in pr4xis is classified by Being type via a verified functor.

3. Architecture

3.1 Five Layers

Logic     → Axioms, propositions, inference
Category  → Concept, Arrow, Category, Functor
Ontology  → Domain knowledge, reasoning patterns, DOLCE
Engine    → Situation, Action, Precondition, enforcement
Codegen   → Build-time ontology generation from data sources

3.2 The Engine as Control System

The Engine implements a closed-loop control pattern. We prove this with a functor from Control Systems to the Engine pattern:

3.3 Domain Knowledge in Ontologies, Not in Mechanical Logic

The Engine trait, Category trait, and Functor trait contain no domain-specific logic — no parser-with-special-cases, no rule-engine-with-hardcoded-strings, no if-statements branching on domain values. Domain knowledge lives in the ontologies (which are themselves Rust code, but Rust code that the type system checks as categorically valid). Adding a new domain (e.g., chess, traffic, English grammar) requires only:

1. Defining an ontology (Concept enum + Arrow impl + Category impl)
2. Defining actions and situations (Action + Situation traits)
3. Defining preconditions (Precondition trait)

No code paths change. The framework is invariant across domains.

4. Composition via Functors

4.1 Cross-Domain Proofs

Every functor is verified by check_functor_laws():

• Identity preservation: F(id_A) = id_{F(A)}
• Composition preservation: F(g∘f) = F(g)∘F(f)

Proven functors include:

• Traffic IS Systems (TrafficToSystems)
• Chess IS EventDriven (ChessToEvents)
• Chess IS Concurrent (ChessToConcurrency)
• EventDriven IS Concurrent (EventsToConcurrency)
• Systems IS Concurrent (SystemsToConcurrency)
• Dialogue IS Communication (DialogueToCommunication)
• Control IS Engine (ControlToEngine)
• pr4xis types IS DOLCE (OwnToDolce)

4.2 Composable Proof Chains

If A IS B (functor) and B IS C (functor), then A IS C (composition). The composed proof is automatic and correct by the functor composition theorem. This gives us:

Chess IS EventDriven IS Concurrent
Systems IS Concurrent IS EventDriven
Traffic IS Systems IS Concurrent

4.3 Ontology Evolution via Functor

When transforming ontologies, pr4xis creates the new ontology alongside the old and proves the mapping via functor. The functor guarantees structure preservation. This is implicit in Spivak’s functorial data migration (2010) but applied here to ontological evolution.

5. Natural Language as Ontological Composition

5.1 The Linguistics Pipeline

Text → Language::lexical_lookup → Pregroup algebra → Montague functor → Speech acts → Discourse

Every arrow is a functor. The tokenizer is language-agnostic (parameterized by &dyn Language). The pregroup grammar (Lambek 1999) is an algebraic ontology — parsing is group-like contraction. The Montague functor maps syntax to semantics. Speech acts (Searle 1976) classify what utterances DO. Discourse reference (Kamp 1981, Grosz/Joshi/Weinstein 1995) tracks entities across utterances.

5.2 Spelling Correction as Adjunction

The noisy channel model (Shannon 1948, applied by Kernighan/Church/Gale 1990) is an adjunction:

• F: Lang → Obs (the channel functor — words become misspellings)
• G: Obs → Lang (Bayesian right adjoint — correction)
• G∘F ≠ Id (information loss through channel)

5.3 No Hardcoded Word Knowledge

The system contains zero hardcoded English words. Function words are constructed during language initialization from OLiA categories. Content words come from WordNet. Verb transitivity comes from WordNet subcategorization frames. Pronoun classification (anaphoric vs interrogative) comes from OLiA’s PronounKind taxonomy. A Hebrew or Turkish implementation would use the same code with different ontology data.

6. Related Work

7. Evaluation

• 106 domain ontologies
• 61 proven cross-domain functors
• 4,855 machine-verified proofs
• Physics, chess, music, linguistics, traffic, law, logic puzzles
• Property-based testing with proptest
• Full WordNet English (107K concepts) loaded in <200ms
• All proofs execute in <5 seconds on a single core

8. Conclusion

pr4xis architecture demonstrates that a software system can keep all domain knowledge in composable ontologies — never in mechanical processing logic — while maintaining behavioral correctness across more than a hundred domains. The key enablers are:

1. Category theory as the composition mechanism (functors preserve structure)
2. The Good Regulator Theorem as architectural justification (the ontology must model the system)
3. DOLCE as the classification foundation (every domain has a type of being)
4. The Engine as a generic control loop (one pattern, all domains)

The name “pr4xis” is not marketing — it is a claim backed by 4,855 proofs (verifiable via cargo test --workspace).

References

See docs/understand/foundations.md for the full bibliography, including the recently added Spencer-Brown / Heim distinction-calculus lineage section.

• Document date: 2026-04-14
• Status: draft outline. Numerical claims are re-derivable from the codebase: 4,855 tests via cargo test --workspace, 106 ontologies via find crates/domains/src -name ontology.rs | wc -l, 61 functors via grep -rn "impl Functor" crates/domains/src/ crates/pr4xis/src/.

Gap Detection in Scientific Ontologies

One-paragraph result. A pr4xis adjunction automatically detected that the molecular biology ontology had collapsed two functionally distinct roles of voltage-gated potassium channels (Kv) into a single entity. Categorical math surfaced the gap; a ContextDef resolution disambiguated the two roles; the gap closed. 85.2% of molecular entities collapse in the Molecular ⊣ Bioelectric round-trip — every collapse is a missing distinction the math detected automatically. Reproduce in 5 seconds:

cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

This page is the casual-reader summary of a categorical methodology that is described in full as a draft research paper — see Adjunction Information Loss in Scientific Ontologies for the methods, the per-entity tables, the literature verification, and the testable predictions.

What gets verified

• Three biomedical adjunctions between Molecular ↔ Bioelectric, Pharmacology ↔ Molecular, Biology ↔ Bioelectric. Code at crates/domains/src/natural/biomedical/adjunctions.rs.
• Per-adjunction collapse percentages computed live by the gap-analysis runner. The output of test_full_chain_collapse_measurement is the source of truth.
• The Kv channel discovery — voltage-gated potassium channels serve two functionally distinct roles (constitutive homeostasis vs therapeutic target). The molecular ontology had collapsed them; the adjunction surfaced the gap; a ContextDef::resolve distinguishes (Kv, Constitutive) from (Kv, Therapeutic). Verified by cargo test -p pr4xis-domains test_kv_gap_is_resolved_by_context.

Why this matters in one sentence

The discovery was made by mathematics, not by domain experts — the categorical adjunction surfaced the conflation as a forced consequence of the round-trip, and the methodology generalizes to any pair of ontologies connected by an adjunction.

Read more

• Paper 02 — Adjunction Information Loss — the academic version: methods, results, discussion, references, with inline footnote verification next to every numerical claim.
• Concepts — what adjunctions are and why they detect gaps, in plain English.
• Foundations — academic lineage including the categorical machinery this result builds on.
• #60 — once the source-of-truth pipeline lands, the percentages on this page will pull from a deployed JSON instead of being hand-typed.

• Document date: 2026-04-14

Kinded Functor Failures — What Actually Goes Wrong

Issue: #98 — understand why cross-ontology functors keep failing check_functor_laws and decide whether the fix is a framework extension (lax functor / profunctor) or something more mundane.

The three cases we’ve actually hit

Over the last three sessions the workspace has accumulated three functor-law failures, each documented as a deferred follow-up in the respective ontology’s mod.rs:

The initial framing — “strict functors can’t do dense-to-kinded” — pattern-matches across all three and invites the conclusion that we need profunctors, lax functors, or some other categorical generalisation. On closer inspection each of the three has a different underlying cause, and none of them need a framework extension.

Case 1 — Consciousness → Metacognition: target coverage gap

This is the case #98’s issue body already diagnoses, citing Nelson & Narens (1990). The metacognition ontology simply lacks counterparts for three concepts the consciousness ontology carries:

• Attention (GWT spotlight)
• PhenomenalMonitoring (IIT cause-effect structure)
• BroadcastMessage (GWT broadcast)

With no target object for these, any functor has to map them to something, and under the current attempted mapping that forces object collisions or other unnatural assignments. The morphism mapping then becomes ill-typed or cannot preserve identities and composition consistently — not because functor laws demand object-injectivity (they don’t; many-to-one is fine in principle) but because the forced collisions leave no well-typed choice of morphism image.

Fix: enrich metacognition. This is a content problem, not a structural one. Once the three concepts land in metacognition, the functor should type-check.

Case 2 — Dependability → Diagnostics: directional mismatch (abductive inversion)

The original framing (“many-to-one collapse”) is wrong. Look at the two chains:

Dependability:   Fault  →  Error  →  Failure             (causal)
Diagnostics:     Symptom → Hypothesis → Diagnosis → FaultMode   (abductive / Reiter 1987)

Dependability goes cause-to-observation. Diagnostics goes observation-to-cause — it inverts the causal arrow because diagnosis is abduction. A functor F: Dependability → Diagnostics that tries to preserve direction has to send Fault → Error to an arrow F(Fault) → F(Error); but the only arrow between the natural candidates (FaultMode, Symptom) in Diagnostics runs Symptom → … → FaultMode, i.e. the reverse. There is no arrow in Diagnostics pointing the way the functor needs it to. The composition law failure is a symptom of that — not many-to-one collapse.

Fix (first attempt): the right morphism is F: Dependability^op → Diagnostics (or equivalently, a contravariant functor). The Op<C> wrapper was landed in #130 precisely for this case.

Second constraint, discovered empirically: landing Op<C> was necessary but not sufficient. Running the mapping through check_functor_laws surfaces a further structural mismatch:

• DependabilityCategory is dense — generated with no edges: block, so the Relation type has no kind field. Self-loops DepRel{A, A} are ambiguous; there is no distinction between the identity morphism and a morphism that happens to end at its start point after composition.
• DiagnosticCategory is kinded — Relation type carries kind: DiagnosticRelationKind which distinguishes Identity from Composed.

When f = Op(DepRel{A, B}) and g = Op(DepRel{B, A}) are composed in Op<Dep>, the result is an underlying self-loop DepRel{A, A}. Under the natural mapping this goes to DiagRel{F(A), F(A), Identity} — but F(g) ∘ F(f) in Diagnostics produces DiagRel{F(A), F(A), Composed}. Different kinds, composition law fails. This isn’t directional, and it isn’t the many-to-one case; it’s dense-source-vs-kinded-target identity-distinction incompatibility.

Options that would fix case 2:

1. Make Dependability kinded (e.g., give causes: / is_a: / opposes: edges real kind names). This loses some dense-category closure convenience but makes the target reachable by strict functors from either direction.
2. Sub-category restriction — define the functor only on the causal sub-category {Fault, Error, Failure, ServiceFailure, ErrorDetection, ErrorRecovery, ...} carrying kinded causal edges; the dense part of Dependability (that’s just carried by Concept variants, not by semantic morphisms) is irrelevant to the abductive structure.
3. Enrich Diagnostics to be dense — aligns with option (b) of case 3 below; loses kind information in Diagnostics.

All three are content decisions rather than framework extensions. Recommendation: option (2) once a sub-category construction lands. No framework piece available today can make the literal Op<DependabilityCategory> → DiagnosticCategory functor pass strict laws.

Case 3 — Resilience → Dependability: trivial-functor disguised as failure

Every Resilience pattern (CircuitBreaker, Retry, Supervisor, Microreboot, …) is a FaultTolerance means. Mapping all 38 resilience concepts to Dependability::FaultTolerance and every resilience morphism to id_{FaultTolerance} does satisfy the functor laws — it’s the trivial functor into the one-object subcategory {FaultTolerance, id}. The laws hold because every composite in Resilience maps to id ∘ id = id, which is well-defined.

Verified empirically:

cargo test -p pr4xis-domains -- resilience::dependability_functor
# test applied::resilience::dependability_functor::tests::trivial_functor_satisfies_laws ... ok

Code: crates/domains/src/applied/resilience/dependability_functor.rs. The ResilienceToFaultTolerance functor sends every Resilience object to FaultTolerance and every morphism to id_FaultTolerance, and check_functor_laws passes. The previous “laws failed” claim in the Dependability/Resilience mod.rs notes reflected an attempt to preserve non-trivial morphism structure without enriching the target — not a structural impossibility.

What fails in the repo’s current check is the expected non-trivial mapping where morphism kinds are preserved. A Resilience Retry --Schedules--> BackoffStrategy wants to map to a Dependability morphism carrying a compatible kind between whatever Retry and BackoffStrategy map to. Dependability’s category is dense (no edges: block; only Identity and Composed morphism kinds), so it cannot express kind-bearing morphisms like Schedules at all — regardless of whether FaultTolerance has taxonomic children (it does: ErrorDetection, ErrorRecovery, etc.). The mismatch is about missing typed-morphism presentation in the target, not about FaultTolerance itself lacking structure.

Fix: choose between two routes.

• (a) Accept the trivial functor and state explicitly that “Resilience factors through the subcategory {FaultTolerance}” — it’s honest and the functor laws pass. The category-theoretic content is “every resilience pattern lives under FaultTolerance,” which is the intended ontological claim.
• (b) Enrich Dependability’s means hierarchy with sub-kinds matching resilience families: StabilityMeans, BackoffMeans, SupervisionMeans, RecoveryMeans under FaultTolerance. The functor then has distinct targets and can preserve non-trivial structure.

Either is valid. (a) is less work and captures the right thing; (b) adds more information but risks duplicating the Resilience ontology’s own hierarchy. Default recommendation: (a), with a short doc comment explaining it’s the terminal functor onto the {FaultTolerance} subcategory.

What we DO NOT need

• Lax functors. Mac Lane’s lax functors weaken the composition law to a 2-cell (F(g∘f) ⇒ F(g)∘F(f) instead of =). None of the three failures above were “the composition law almost holds up to a canonical 2-cell”. They were either directional mismatch, target coverage, or expected triviality. Lax functors solve a different problem.
• Profunctors. Profunctors (C^op × D → Set) generalise relations, not mappings. None of the above was a multi-valued-relation case.
• Natural transformations. NTs connect two existing functors. We don’t have two competing functors; we have one failed one.

What we DO need

• Op<C> opposite-category construction — landed in #130 as pr4xis::category::Op. Necessary for any contravariant functor expressed as a covariant Functor impl. Not sufficient on its own for case 2: empirical testing surfaced the dense/kinded identity-distinction constraint described in the case-2 update above, so the Op<Dependability> → Diagnostics worked example is deferred pending one of the three content-decision fixes.
• TerminalFunctor<C, Object> helper — builds “map everything to a single target object and every morphism to its identity.” Case 3’s hand-rolled ResilienceToFaultTolerance would fold into this. Tracked as #131.
• No framework changes for case 1 — it’s purely about authoring more concepts in the metacognition ontology. Tracked as #132.

Loose ends and honest uncertainty

• Case 2’s follow-up is now a content decision, not a framework piece. The three options — make Dependability kinded, restrict to a causal sub-category, or densify Diagnostics — each have different trade-offs in representational richness vs. reasoning ergonomics. The choice is deferred.
• For case 3, the hand-written functor verification confirmed the laws pass. The open question there is purely ergonomic: the TerminalFunctor<...> helper (#131) would replace boilerplate, nothing more.
• “Kinded-to-kinded” across totally different kind alphabets (not examined above) is a separate question; none of our three cases are of that shape yet. If we hit one, revisit.

Recommendation

Close #98 as “diagnosed” with the following action items split out:

1. #130 — ✅ Op<C> landed, case-2 worked example deferred. A follow-up ticket picks one of the three content-decision fixes (likely sub-category restriction).
2. #131 — TerminalFunctor helper. ~1 hour, folds case 3’s hand-rolled functor into the helper.
3. #132 — enrich metacognition. Ontology work (Dehaene GWT, Tononi IIT, Nelson-Narens). Unblocks case 1’s functor.

The single-sentence summary: we thought we had three cases of the same problem; we actually had four problems across three cases, and none of them requires a lax / profunctor generalisation — just a dash of framework helpers plus a few content decisions.

• Document date: 2026-04-17
• Issue: #98
• Related: Paper 02 — Adjunction Information Loss, Paper 03 — Ontology Diagnostics

Pipeline Architecture — Literature Survey

Issue: #117 — PipelineStep was drawn ad-hoc as the chat pipeline evolved. The choice of 13 stages (Tokenize → Parse → Interpret → EntityLookup → TaxonomyTraversal → CommonAncestor → Metacognition → SpeechActClassification → ResponseFrameSelection → ContentDetermination → DocumentPlanning → Realization → EpistemicClassification) has no single literature anchor. This survey picks one.

The candidates

Why MAPE-K

The existing 13 steps map cleanly onto MAPE-K’s four-phase loop:

No step is orphaned. No MAPE-K phase is unused. The current pipeline IS a MAPE-K loop; we just hadn’t named it that.

Why the other candidates are secondary

• Reiter & Dale / KAMP cover only Execute (generation). Already-present; subsumed by MAPE-K’s Execute phase.
• BDI is the right architecture inside MAPE-K’s Plan phase (belief → desire → intention selection), not above it.
• Moggi’s monads are the right architecture for the computational structure of each step (Writer for tracing, State for context, etc.). Orthogonal composition axis; not the step-sequence structure.
• Marr’s three levels are the right abstraction axis for each phase (each step has a computational, algorithmic, and implementational description). Orthogonal layering, not a sequence.
• Good Regulator justifies why pr4xis needs a model at all — Conant-Ashby’s theorem. Already cited; doesn’t structure the pipeline.

The recommended encoding

One top-level MapeK ontology formalising:

• Six concepts — MapeKPhase, Monitor, Analyze, Plan, Execute, Knowledge
• Four transition edges — Monitor → Analyze, Analyze → Plan, Plan → Execute, Execute → Monitor
• Each phase Consults Knowledge
• Domain axioms: FourPhaseCycle (the four operational phases are the children of MapeKPhase), LoopIsClosed (the Execute → Monitor edge closes the loop), EveryPhaseConsultsKnowledge (MAPE-K is a knowledge-based loop)

Plus a cross-functor PipelineStep → MapeK that maps each existing step to its phase. That puts the existing 13 steps in a literature-grounded structural home without rewriting the steps themselves.

Part 1 refactor (meta-driven names) — no longer blocked

Per the issue, Part 1 (replace hardcoded ontology-name strings in trace_functors.rs with meta() lookups) was blocked on the architectural decision because refactoring into a structure we were about to replace would have been wasted work. With MAPE-K chosen as the primary, the refactor is now well-scoped: replace hardcoded strings with <OntologyStruct>::meta().name lookups — no step-structure change needed.

Open questions (still open)

1. Is the pipeline really linear? — MAPE-K says no, it’s a cycle with the Execute → Monitor edge closing the loop. Encoded.
2. Should PipelineStep be an enum at all, or a composable category of computational effects? — MAPE-K says both: the top-level is a 4-phase loop (enum), each phase’s internal composition is effectful (Moggi).
3. ContentDetermination / DocumentPlanning / Realization — three stages or Marr levels? — MAPE-K treats them as three sub-steps of Execute. Marr is available as an orthogonal axis on each of them if we want to add it later.
4. Metacognition — inside or above? — MAPE-K Monitor + Knowledge together do the job; Metacognition belongs in Monitor.
5. Symmetric parse/generate adjunction (#93) — orthogonal; lives at the Monitor/Execute boundary.

• Document date: 2026-04-17
• Issue: #117
• Related: #95 Response formation chain, #93 Parse ⊣ Generate adjunction

Draft Papers

Drafts on ontological structure, gap detection, and machine-checkable scientific knowledge representation. Every numerical claim in every paper is paired with a cargo test command that re-derives it from the live codebase — see the “Code & Verification” section at the end of each paper.

Reproducibility

Every paper’s numerical claims can be verified from the codebase by running:

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo test --workspace
cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

The first command runs the full test suite (4,855 tests as of the document date; re-counted on every run). The second prints the live per-adjunction collapse percentages cited in all three papers — including the 85.2% molecular-bioelectric round-trip loss and the Kv channel discovery.

For the per-claim test index, see the “Code & Verification” section at the bottom of each paper.

Status

• Paper 1 — draft. Awaits a literature-review pass and one scan for stale subset counts.
• Paper 2 — draft. Awaits the methodology generalization section to be fleshed out with at least one non-biomedical adjunction example.
• Paper 3 — draft. Awaits the threshold-validation section to be expanded once more adjunctions are measured (currently 3).

A fourth draft on the syntrometric logic lineage (the structural alignment with Heim’s syntrometry, formalized as a pr4xis ontology with a verified functor) is tracked in #62 — not yet drafted, will land in this directory once #62 lands.

Related

• Novelty argument — the careful prose about what is new vs prior art, with the same intellectual honesty applied to the lineage claims
• Gap detection — the same biomedical result, written for the README audience instead of the journal audience
• Foundations — academic lineage that grounds the broader project
• Concepts — the categorical machinery the papers build on, in plain English

Category-Theoretic Formalization of Bioelectric Morphogenesis

Subtitle

Provable Ontologies for Levin’s Bioelectric Framework via Functors, Adjunctions, and Machine-Verified Axioms

Abstract

Dr. Michael Levin’s bioelectric framework proposes that endogenous membrane potential (Vmem) patterns encode morphogenetic information, guiding tissue repair and regeneration through gap junction-mediated collective cell behavior. While experimentally validated across planaria, Xenopus, and cancer models, this framework has lacked a formal mathematical foundation. We present a category-theoretic formalization of Levin’s bioelectric framework, encoding 12 scientific domains¹ as formal ontologies with 839 machine-verified tests². We prove that the cross-domain relationships between molecular biology, bioelectricity, immunology, pharmacology, regeneration, and pathology are structure-preserving maps (functors) with verified composition laws³, and identify three adjunction pairs⁴ that capture the “zoom in / zoom out” relationship between biological scales. This formalization enables automated reasoning about therapeutic interventions, identifies previously unrecognized structural equivalences between domains, and provides a rigorous foundation for the emerging field of bioelectric medicine.

1. Introduction

1.1 The Bioelectric Framework

Levin’s body of work (Levin 2014; Chernet & Levin 2013; Levin 2021) has established that:

• Membrane potential (Vmem) acts as an instructive signal for pattern formation
• Gap junction networks propagate bioelectric information across cell collectives
• Depolarized Vmem correlates with proliferative/neoplastic states
• Restoring normal Vmem is sufficient to trigger morphological repair
• Every biological scale exhibits goal-directed competency (TAME framework)

These claims are supported by extensive experimental evidence but have not been formalized mathematically. Computational models exist (Pietak & Levin 2018; Cervera et al. 2020) but focus on simulation rather than formal verification of structural relationships.

1.2 Category Theory as a Foundation

Category theory provides the natural language for formalizing cross-domain structural relationships. A functor F: C -> D is a structure-preserving map between categories that maps objects to objects and morphisms to morphisms while preserving identity and composition. If such a functor exists and satisfies its laws, the relationship between C and D is not analogical but mathematically proven.

An adjunction F -| G captures the notion of “optimally inverse” functors: the unit and counit measure the information lost in the round-trip, making precise what it means for two domains to be “the same up to information loss.”

1.3 Contributions

1. Formal encoding of 12 scientific domains¹ as categories with taxonomy, mereology, causation, opposition, and quality structures
2. 21 functors³ proving structure-preserving maps between domains
3. 3 adjunctions⁴ capturing scale-bridging relationships
4. 839 machine-verified tests² proving all axioms, functor laws, and composition properties
5. Identification of structural equivalences invisible to informal reasoning

2. Methods

2.1 The Praxis Framework

We use the praxis ontology framework, which implements:

• Category: objects (concepts) + morphisms (kinded relationships) with identity and composition laws (Mac Lane 1971; Awodey 2010)
• Taxonomy (Kind::Subsumption): is-a hierarchies as directed acyclic graphs, with NoCyclesOnKind + AntisymmetricOnKind from the catalog
• Mereology (Kind::Parthood): part-whole relationships, with NoCyclesOnKind from the catalog
• Causation (Kind::Causation): cause-effect directed acyclic graphs, with AsymmetricOnKind + IrreflexiveOnKind from the catalog
• Opposition (Kind::Opposition): symmetric, irreflexive contrast pairs, with SymmetricOnKind + IrreflexiveOnKind from the catalog
• Quality: properties that inhere in concepts
• Axiom: a verify() predicate returning a typed Verdict plus a required citation() to published literature
• Ontology: bundles Category + Quality + Axioms with self-validation
• Functor: structure-preserving maps between categories
• Adjunction: optimally inverse functor pairs with unit and counit

All structures are implemented in Rust and verified by the type system and 839 automated tests² including property-based testing (proptest).

2.2 Domain Selection

Domains were selected based on their relevance to Levin’s bioelectric framework and grounded in published literature:

2.3 Axiom Design

Each axiom encodes a specific claim from published literature:

Axiom: Piezo1IsMechanosensitiveChannel
Source: Coste et al. 2010, Science (Nobel 2021)
Proof: ∃ a Subsumption-kinded morphism Piezo1 → Mechanosensitive
       AND ∃ a Subsumption-kinded morphism Piezo1 → IonChannel
       in BiomedicalCategory::morphisms()

Axioms are not structural trivia — they are falsifiable scientific claims that would FAIL if the ontological structure contradicted the literature.

3. Results

3.1 Domain Structure

12 domains¹ encode 275+ entities with 130+ axioms⁵. Each domain is a category with objects (entities) and morphisms (relationships). The morphism structure is verified by automated category law tests (identity, composition, associativity, closure)².

3.2 Cross-Domain Functors

21 functors³ prove structure-preserving maps between domains:

Key result: The functor MolecularToBioelectric maps molecular entities to their bioelectric roles (Piezo1 -> MechanicalStimulation, Cx43 -> GapJunctionModulation, Calcium -> Signal). This functor satisfies:

• Identity preservation: map(id_A) = id_{F(A)} for all molecular entities
• Composition preservation: map(g . f) = map(g) . map(f)

This is not an analogy — it is a mathematical proof that molecular biology HAS the structure of bioelectric signaling.

3.3 Adjunctions

Three adjunction pairs⁴ capture scale-bridging:

MolecularToBioelectric -| BioelectricToMolecular

The unit eta: A -> G(F(A)) maps a molecule to its round-trip form. For example, Piezo1 -> MechanicalStimulation -> Piezo1 (identity — no information loss for specific channels). But CalciumSignal -> Signal -> CalciumSignal (lossy: multiple signals share the Signal category).

The counit epsilon: F(G(B)) -> B maps a bioelectric concept to its round-trip. MechanicalStimulation -> Piezo1 -> MechanicalStimulation (identity). But Signal -> CalciumSignal -> Signal (lossy: Signal collapses to one canonical representative).

This adjunction precisely captures what is lost and preserved when “zooming” between molecular and bioelectric scales — the central question in Levin’s multi-scale framework.

3.4 Causal Chain Verification

12 causal graphs⁶ encode 100+ cause-effect relationships⁶. Functor composition tests³ verify that causal chains compose across domains:

pharmacology -> molecular -> bioelectricity: Ivermectin -> GlyR -> IonChannelModulation

This chain is verified end-to-end: for every pharmacological entity, the composed map through molecular to bioelectric is well-defined and preserves identity morphisms.

3.5 Novel Structural Findings

Cross-domain equivalences: MacrophageM1, MacrophageM2, and Fibroblast are proven identical across biology and immunology ontologies via functor identity mapping. TargetMorphology is proven identical across bioelectricity and regeneration. These equivalences were not assumed — they emerged from functor analysis.

Opposition structure: 26 opposition pairs⁷ across 8 domains encode scientific contrasts (Na+/K+, M1/M2, Healthy/Dysplastic). The opposition axioms (symmetric, irreflexive) are verified automatically², ensuring no entity opposes itself and all oppositions are bidirectional.

The TAME hierarchy as category: The 5-level TAME competency hierarchy (Molecular -> Cellular -> Tissue -> Organ -> Organism) is encoded as a taxonomy⁸ with verified DAG structure and transitive is-a relationships. Every bioelectric entity is assigned an operating level, and the axiom AllTAMELevelsRepresented proves that all 5 levels are populated.

4. Discussion

4.1 What Formalization Adds

Informal scientific reasoning allows ambiguity: “ion channels are involved in bioelectricity” is true but imprecise. Formal functorial reasoning says exactly HOW: Piezo1 maps to MechanicalStimulation (not to Signal, not to Intervention — specifically to MechanicalStimulation), and this mapping preserves the relational structure of both domains.

4.2 Predictive Power

The ontology identifies gaps: if a new ion channel is discovered in esophageal tissue, the functor immediately tells you its bioelectric role, its pharmacological targets (via composition), and its pathological implications (via the causal chain).

4.3 Limitations

• The discrete category structure (all pairs as morphisms) is mathematically convenient but does not distinguish “strong” from “weak” relationships
• Axioms verify qualitative structure, not quantitative dynamics
• The formalization captures Levin’s framework as published; it does not generate new experimental predictions (though it identifies structural gaps that suggest where experiments should focus)

4.4 Relation to Existing Work

Computational models of bioelectric patterning (Pietak & Levin 2018; Cervera et al. 2020; Manicka & Levin 2019) simulate dynamics numerically. Our approach is complementary: we formalize the STRUCTURE of the domain, not its dynamics. The two approaches could be combined — the ontology defines what entities and relationships exist, the simulation computes their behavior.

5. Conclusion

We present the first category-theoretic formalization of Levin’s bioelectric framework, proving with machine-verified tests that molecular biology, bioelectricity, immunology, pharmacology, regeneration, and pathology are connected by structure-preserving maps. Three adjunctions capture the multi-scale nature of biological competency. This formalization provides a rigorous foundation for bioelectric medicine and demonstrates that category theory is a practical tool for biological knowledge representation.

Code & Verification

All ontology source code, tests, and documentation are available at:

https://github.com/i-am-logger/pr4xis

Re-deriving every numerical claim in this paper

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo test --workspace
cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

The first command runs the full test suite (4,855 tests across the workspace as of the document date; cargo test --workspace re-counts on every run). The second prints the live per-adjunction collapse percentages cited throughout this paper — including the 85.2% molecular-bioelectric round-trip loss that triggered the Kv discovery.

Specific files

• crates/domains/src/natural/biomedical/ — the 14 biomedical domain ontologies (biology, molecular, bioelectricity, biochemistry, biophysics, mechanobiology, immunology, pharmacology, pathology, hematology, electrophysiology, regeneration, chemistry, acoustics)
• crates/domains/src/natural/biomedical/adjunctions.rs — the three adjunctions (MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction) with their unit and counit implementations and the test suite that verifies them
• crates/domains/src/formal/meta/gap_analysis.rs — the live computational analysis (analyze_molecular_bioelectric(), analyze_biology_bioelectric(), analyze_pharmacology_molecular(), test_full_chain_collapse_measurement)
• crates/domains/src/natural/biomedical/molecular/ontology.rs — MolecularEntity enum (Kv, Piezo1, Piezo2, etc.) and the MolecularFunctionalContext / ContextDef resolution that closed the Kv gap
• crates/domains/src/natural/biomedical/biology/bioelectricity_functor.rs — BiologyToBioelectric (left adjoint of the Biology-Bioelectric adjunction)
• crates/domains/src/natural/biomedical/molecular/bioelectricity_functor.rs — MolecularToBioelectric (left adjoint of the Molecular-Bioelectric adjunction)
• crates/domains/src/natural/biomedical/bioelectricity/molecular_functor.rs — BioelectricToMolecular (right adjoint)

Test-command index for the load-bearing claims

The numerical counts in the abstract and Section 3 (12 domains, 839 tests, 21 functors, 275 entities, 130 axioms, 26 opposition pairs, 12 causal graphs, 100+ cause-effect relationships) are subset counts specific to the bioelectric stack at the time the paper was drafted. They are approximate; current values may differ as the workspace evolves. The ground-truth values are always re-derivable from the codebase via find, grep, and the cargo test commands above.

References

(See docs/papers/references.md for complete bibliography — 70+ papers)

Verification Footnotes

Key references:

• Levin M (2014). Molecular bioelectrics in developmental biology. Mol Biol Cell.
• Chernet BT, Levin M (2013). Transmembrane voltage potential of tumor suppression. DMM.
• Coste B et al (2010). Piezo1 and Piezo2. Science. (Nobel Prize 2021)
• Fields C, Levin M (2022). Competency in navigating arbitrary spaces. Entropy.
• Kofman K, Levin M (2024). Bioelectric pharmacology of cancer.
• Weinheimer-Haus EM et al (2014). WBV improves wound healing. PLOS ONE.
• Lewis AH et al (2017). Repetitive mechanical stimuli and Piezo channels. Cell Reports.
• Strasser MK et al (2025). Barrett’s Esophagus to adenocarcinoma. Dev Cell. (Nolan lab)
• Fukada E, Yasuda I (1957). Piezoelectric effect of bone. J Phys Soc Japan.

1. Re-derive by find crates/domains/src/natural/biomedical -name ontology.rs | wc -l for the biomedical subset, or find crates/domains/src -name ontology.rs | wc -l for the workspace total. ↩ ↩2 ↩3

2. Re-derive by running cargo test --workspace. The “839” subset count is the bioelectric stack at drafting time; the workspace total grows as new ontologies are added. Both are computed live by the test runner. ↩ ↩2 ↩3 ↩4 ↩5

3. Re-derive by grep -rn "impl Functor" crates/domains/src/natural/biomedical/ | wc -l for the biomedical subset, or the same grep over crates/domains/src/ for the workspace total. Each functor implementation passes check_functor_laws() at test time. ↩ ↩2 ↩3 ↩4

4. The three adjunctions (MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction) live at crates/domains/src/natural/biomedical/adjunctions.rs. Their unit and counit implementations are verified by the test suite in the same file. Run cargo test -p pr4xis-domains adjunctions::tests. ↩ ↩2 ↩3

5. Each axiom is its own Axiom impl. Count via grep -rn "impl Axiom" crates/domains/src/natural/biomedical/ | wc -l. Each axiom is verified by a corresponding test. ↩

6. Causal graphs are encoded as Kind::Causation-tagged morphisms in each ontology’s Category::morphisms(), declared via the causes: sugar clause of the ontology! macro. Count via grep -rn "causes:" crates/domains/src/natural/biomedical/. ↩ ↩2

7. Opposition pairs are encoded as Kind::Opposition-tagged morphisms in each ontology’s Category::morphisms(), declared via the opposes: sugar clause of the ontology! macro. Count via grep -rn "opposes:" crates/domains/src/natural/biomedical/. ↩

8. The TAME hierarchy is encoded in the bioelectricity ontology at crates/domains/src/natural/biomedical/bioelectricity/ontology.rs. Run cargo test -p pr4xis-domains bioelectricity::tests to verify the taxonomy structure. ↩

DRAFT — Adjunctions as Gap Detectors in Scientific Ontologies

Subtitle

How Categorical Adjunctions Automatically Identify Missing Distinctions in Biological Knowledge Representation

Abstract

We present a methodology for automatically detecting missing distinctions in scientific ontologies using categorical adjunctions. Given two domain ontologies formalized as categories with structure-preserving maps (functors) between them, the adjunction’s unit and counit morphisms identify entities that COLLAPSE under the round-trip — revealing where the source ontology lacks a distinction that the target ontology requires. We demonstrate this methodology on 12 biological domains¹ formalized in the pr4xis category-theory framework, with 846 machine-verified tests². The adjunction between molecular biology and bioelectricity (Levin’s framework) automatically detects that ion channels serve dual functional roles (constitutive homeostasis vs therapeutic target)³ — a distinction documented in the literature but absent from the initial molecular ontology. We resolve the detected gap using context-dependent disambiguation (ContextDef)³, and show that the methodology generalizes: every adjunction in our system identifies at least one missing distinction⁴, and every detected distinction is independently verifiable in published literature. We propose adjunction-based gap detection as a general tool for ontology engineering in the sciences.

1. Introduction

1.1 The Ontology Completeness Problem

Scientific ontologies — formal representations of domain knowledge — are constructed by human experts who decide which entities and distinctions to include. This process is inherently incomplete: experts encode what they consider important, but may omit distinctions that only become visible when two domains are formally connected.

How would you know your ontology is missing something?

1.2 Adjunctions Detect Gaps

A categorical adjunction F -| G between categories C and D consists of:

• Left adjoint F: C -> D (“zoom out”)
• Right adjoint G: D -> C (“zoom in”)
• Unit eta: Id_C -> G.F (embed into round-trip)
• Counit epsilon: F.G -> Id_D (project from round-trip)

If eta_A = id_A for all A, the round-trip C -> D -> C preserves all information — no gap exists. But if eta_A != id_A for some A, then the round-trip CHANGES A — meaning C lacks a distinction that D makes and that G maps back differently.

The SET of entities where eta != id IS the gap. The specific morphism eta_A: A -> G(F(A)) tells you exactly what A collapses into.

1.3 Contribution

We show that:

1. Adjunctions between scientific domain ontologies automatically identify missing distinctions
2. Every detected gap corresponds to a real scientific distinction documented in published literature
3. The gaps can be resolved using context-dependent disambiguation
4. The methodology is general — it works across all domain pairs we tested

2. Methods

2.1 Domain Formalization

We formalize 12 scientific domains¹ as categories using the pr4xis framework: biology, molecular biology, bioelectricity (Levin’s framework), regeneration, pharmacology, immunology, electrophysiology, pathology, biophysics, biochemistry, chemistry, and hematology. Each domain is a category with objects (entities), morphisms (relationships), taxonomy (is-a), causation (cause-effect), and qualities (properties).

2.2 Functor Construction

21 structure-preserving maps (functors)⁵ connect the domains. Each functor maps every entity in the source domain to an entity in the target domain, preserving identity and composition. Functor laws are verified by automated tests⁵.

2.3 Adjunction Construction

Three adjunction pairs⁶ are constructed from opposing functor pairs:

2.4 Gap Detection

For each adjunction, compute:

• For every entity A in the source: does eta_A = id_A? If not: A is a GAP ENTITY — the source ontology is missing a distinction.
• For every entity B in the target: does epsilon_B = id_B? If not: B is a GAP ENTITY in the reverse direction.

2.5 Gap Resolution

Detected gaps are resolved using praxis’s ContextDef — context-dependent disambiguation that maps (entity, context_signal) -> resolved_interpretation. This does not add new entities to the ontology; it adds new DISTINCTIONS to existing entities.

3. Results

3.1 Molecular-Bioelectric Adjunction

Left functor F (MolecularToBioelectric):

Right functor G (BioelectricToMolecular):

Unit analysis (eta: A -> G(F(A))):

Unit gap entities⁴: Piezo2, TRPV4, Kv, Cx26, Calcium (5 of 27 = ~19%)

These gaps mean: the bioelectric domain cannot distinguish Piezo1 from Piezo2 from TRPV4 — they all look like “MechanicalStimulation.” The molecular distinctions are invisible at the bioelectric scale.

Counit analysis (epsilon: F(G(B)) -> B):

Counit gap entities: MembranePotential, VoltageGradient, TargetMorphology

Critical finding³: MembranePotential maps to Kv (the channel that sets it), but Kv maps BACK to IonChannelModulation (not MembranePotential). The round-trip RE-CLASSIFIES a passive signal as an active intervention.

This means: at the molecular level, there is NO distinction between “what sets Vmem” and “what you modulate to change Vmem.” They are the same channel in two functional contexts.

3.2 The Detected Gap

The counit collapse MembranePotential -> Kv -> IonChannelModulation reveals that the molecular ontology has a single entity (Kv) for what the bioelectric ontology considers two separate concepts (passive signal vs active intervention).

This is not an error in either ontology. It is a genuine scientific fact: Kv channels simultaneously maintain resting potential (constitutive role) and serve as drug targets (therapeutic role). The molecular ontology was CORRECT but INCOMPLETE — it lacked the functional-mode distinction.

3.3 Resolution via ContextDef

We resolve the gap using context-dependent disambiguation:

(Kv, Constitutive)  -> PassiveHomeostatic    (sets resting Vmem)
(Kv, Therapeutic)   -> TherapeuticTarget     (drug shifts Vmem)

(Piezo1, Constitutive)  -> MechanicalSensor  (senses environment)
(Piezo1, Therapeutic)   -> TherapeuticTarget  (vibration therapy)

(Cx43, Constitutive)  -> InterCellularChannel (existing GJ network)
(Cx43, Therapeutic)   -> TherapeuticTarget    (upregulate connectivity)

(Collagen, Constitutive) -> StructuralScaffold  (ECM)
(Collagen, Therapeutic)  -> MechanicalSensor    (piezoelectric effect)

Every resolution is independently supported by published literature:

• Kv as passive: textbook electrophysiology
• Kv as target: Kofman & Levin 2024
• Piezo1 as sensor: Coste et al. 2010 (Nobel 2021)
• Piezo1 as target: Lewis et al. 2017
• Cx43 constitutive: Inose et al. 2009
• Cx43 as target: Levin 2014
• Collagen as scaffold: standard histology
• Collagen as sensor: Fukada & Yasuda 1957

3.4 The Other Adjunctions

Pharmacology-Molecular adjunction: The counit reveals that molecular entities like Kv map to drugs (Minoxidil) that map back to a different bioelectric role than expected. Gap: the pharmacology ontology doesn’t distinguish between drugs that OPEN channels (agonists) and drugs that BLOCK channels (antagonists) at the molecular level — both map to the same molecular target.

Biology-Bioelectric adjunction: The counit reveals that CognitiveLightcone maps to Esophagus (organ-level competency) maps back to CognitiveLightcone (preserved). But MembranePotential maps to SquamousEpithelial (cell with Vmem) maps back to MembranePotential… or does it? The unit reveals that multiple cell types (SquamousEpithelial, ColumnarEpithelial, GobletCell) all map to MembranePotential — the bioelectric ontology cannot distinguish which cell type has which Vmem pattern. Gap: the bioelectric ontology needs cell-type-specific Vmem entities.

3.5 Generalization

Every adjunction we tested identified at least one gap⁴:

These are COMPUTED values from the codebase⁴, not estimates.

The pattern is consistent: adjunctions between domains at DIFFERENT SCALES always reveal information loss, and this loss always corresponds to a scientifically meaningful distinction.

4. Discussion

4.1 Adjunctions as a Gap Detection Methodology

We propose a general methodology:

1. Formalize two related domains as categories
2. Build functors in both directions
3. Construct the adjunction (unit + counit)
4. Compute eta and epsilon for all entities
5. Entities where eta != id or epsilon != id are GAPS
6. Resolve gaps using ContextDef or by enriching the ontology
7. Verify resolutions against published literature

This is mechanical — it can be automated. The adjunction does the discovery; the human does the literature verification.

4.2 Why This Works

Inter-scale information loss in biology is not random. It follows a pattern: entities at a finer scale (molecular) DIFFERENTIATE what entities at a coarser scale (bioelectric) CONFLATE. The adjunction unit measures exactly this conflation. The counit measures the reverse: coarse-scale distinctions that collapse at fine scale, revealing that the fine-scale ontology lacks a contextual distinction.

4.3 Relation to Existing Work

• Ontology alignment (Euzenat & Shvaiko 2013): focuses on MATCHING entities across ontologies. Our approach finds MISSING entities via round-trip analysis.
• Ontology debugging (Schlobach & Cornet 2003): finds logical inconsistencies. Our approach finds INCOMPLETENESS, not inconsistency.
• Category theory in biology (Rosen 1991, Baez & Stay 2011): theoretical foundations. Our contribution is a PRACTICAL methodology with machine-verified results.
• Levin’s multi-scale framework (Levin 2022 TAME): describes the multi-scale challenge qualitatively. Adjunctions make it quantitative.

4.4 Limitations

• The discrete category structure (all pairs as morphisms) means the functor mapping choices affect which gaps are detected. Different functor constructions might reveal different gaps.
• The methodology detects structural gaps but cannot determine their scientific significance without literature verification.
• ContextDef resolves gaps by adding distinctions to existing entities, not by adding new entities. Some gaps might require new entities instead.

4.5 Testable Predictions

1. Asymmetric reasoning reliability: If the unit loss (molecular->bioelectric) is higher than the counit loss, then bioelectric->molecular reasoning should be empirically more reliable than molecular->bioelectric reasoning. This is testable by comparing prediction accuracy in both directions across published experimental results.

2. Universal dual-role pattern: If every ion channel has constitutive and therapeutic modes, then every channel-targeting drug should have a measurable effect on resting Vmem (constitutive disruption) in addition to its therapeutic effect. This is testable pharmacologically.

3. Gap detection generalizability: Applying this methodology to other domain pairs (e.g., genomics-proteomics, ecology-evolution) should reveal analogous missing distinctions. This is testable by formalizing additional domain pairs.

5. Conclusion

We show that categorical adjunctions can automatically detect missing distinctions in scientific ontologies. The detected gaps are not artifacts of the formalization — they correspond to real scientific distinctions documented in published literature. The methodology is general, mechanical, and machine-verifiable. We propose it as a standard tool for ontology engineering in the sciences: build your ontology, construct adjunctions to related domains, and let the unit/counit tell you what you missed.

What Is Literature vs What Is Novel vs What Is Hypothesis

Established (literature):

• Kv channels set resting Vmem AND are drug targets (textbook + Kofman & Levin 2024)
• Piezo1 senses environment AND is therapeutic target (Coste 2010 + Lewis 2017)
• Cx43 is constitutive AND modulatable (Inose 2009 + Levin 2014)
• Multi-scale information loss exists in biology (Levin 2022 TAME)

Novel (our contribution):

• Adjunction unit/counit as automated gap detectors in ontologies
• ContextDef resolution of detected gaps
• Quantification of inter-scale information loss via gap entity ratios
• The specific methodology: formalize → functor → adjunction → detect → resolve → verify

Hypothesis (untested):

• Asymmetric reasoning reliability between scales
• Universal dual-role pattern for all ion channels
• Generalizability to non-biological domain pairs

Code & Verification

All source code, tests, and the live computational analysis are available at:

https://github.com/i-am-logger/pr4xis

Re-deriving the percentages in this paper

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

The output prints the live per-adjunction loss percentages from the actual functor implementations. Every percentage in the table in §3.5 (Generalization) — 85.2% molecular-bioelectric unit loss, 78.9% counit loss, 68.0% pharmacology-molecular unit, 70.4% counit, 82.6% biology-bioelectric unit, 78.9% counit — is computed live by this single command. They are not estimates; they will update automatically as the biomedical ontologies evolve.

The Kv discovery (§3.2 — the round-trip Kv → IonChannelModulation → GlyR collapse) is verified by:

cargo test -p pr4xis-domains test_kv_gap_is_resolved_by_context

This test demonstrates both the gap (Kv collapses on the round-trip) and the resolution (ContextDef::resolve distinguishes (Kv, Constitutive) from (Kv, Therapeutic)).

Key files

• crates/domains/src/natural/biomedical/adjunctions.rs — the three adjunction implementations (MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction) with unit and counit and the test suite
• crates/domains/src/natural/biomedical/molecular/ontology.rs — MolecularEntity enum, MolecularFunctionalContext, and the ContextDef resolution that closed the Kv gap
• crates/domains/src/natural/biomedical/molecular/bioelectricity_functor.rs — MolecularToBioelectric (left adjoint of adjunction 1)
• crates/domains/src/natural/biomedical/bioelectricity/molecular_functor.rs — BioelectricToMolecular (right adjoint)
• crates/domains/src/natural/biomedical/biology/bioelectricity_functor.rs — BiologyToBioelectric (left adjoint of adjunction 3)
• crates/domains/src/natural/biomedical/bioelectricity/biology_functor.rs — BioelectricToBiology (right adjoint)
• crates/domains/src/natural/biomedical/pharmacology/molecular_functor.rs — PharmacologyToMolecular (left adjoint of adjunction 2)
• crates/domains/src/natural/biomedical/molecular/pharmacology_functor.rs — MolecularToPharmacology (right adjoint)
• crates/domains/src/formal/meta/gap_analysis.rs — analyze_molecular_bioelectric(), analyze_pharmacology_molecular(), analyze_biology_bioelectric(), test_full_chain_collapse_measurement — the live computational analysis driving every number in this paper

The “846 machine-verified tests” count in §2 is the bioelectric subset at the time of drafting; the current workspace total is 4,855 tests across all domains, re-derivable via cargo test --workspace.

References

• Coste B et al (2010). Piezo1 and Piezo2. Science. Nobel 2021.
• Chernet BT, Levin M (2013). Vmem and tumor suppression. DMM.
• Levin M (2014). Molecular bioelectrics. Mol Biol Cell.
• Levin M (2022). TAME framework. PMID:35401131.
• Fields C, Levin M (2022). Competency in navigating spaces. Entropy.
• Kofman K, Levin M (2024). Bioelectric pharmacology. PMID:38971325.
• Lewis AH et al (2017). Repetitive stimuli and Piezo channels. Cell Reports.
• Inose T et al (2009). Cx26/Cx43 in esophagus. Ann Surg Oncol.
• Fukada E, Yasuda I (1957). Piezoelectric effect of bone. J Phys Soc Japan.
• Weinheimer-Haus EM et al (2014). WBV wound healing. PLOS ONE.
• Euzenat J, Shvaiko P (2013). Ontology Matching. Springer.
• Schlobach S, Cornet R (2003). Non-standard reasoning in description logics. IJCAI.
• Rosen R (1991). Life Itself. Columbia University Press.
• Baez JC, Stay M (2011). Physics, topology, logic and computation. New Structures for Physics.
• Mac Lane S (1971). Categories for the Working Mathematician. Springer.

Verification Footnotes

1. Re-derive by find crates/domains/src/natural/biomedical -name ontology.rs | wc -l for the biomedical subset, or find crates/domains/src -name ontology.rs | wc -l for the workspace total. ↩ ↩2

2. Re-derive by running cargo test --workspace. The “846” count is the bioelectric subset at drafting time; the workspace total is computed live on every run. ↩

3. The Kv channel gap detection and ContextDef resolution are verified by cargo test -p pr4xis-domains test_kv_gap_is_resolved_by_context. The test demonstrates both the gap (Kv collapses on the round-trip) and the resolution (ContextDef::resolve distinguishes (Kv, Constitutive) from (Kv, Therapeutic)). The context-dependent resolution lives in crates/domains/src/natural/biomedical/molecular/ontology.rs as MolecularFunctionalContext. ↩ ↩2 ↩3

4. Every collapse percentage in this paper is computed live by cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture. The output prints per-adjunction unit-loss and counit-loss percentages from the actual functor implementations. Numbers will update automatically as the biomedical ontologies evolve. ↩ ↩2 ↩3 ↩4 ↩5 ↩6 ↩7 ↩8 ↩9 ↩10

5. Re-derive by grep -rn "impl Functor" crates/domains/src/natural/biomedical/ | wc -l for the biomedical subset. Each functor implementation passes check_functor_laws() at test time. ↩ ↩2

6. The three adjunctions (MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction) live at crates/domains/src/natural/biomedical/adjunctions.rs. Their unit and counit implementations are verified by the test suite in the same file. Run cargo test -p pr4xis-domains adjunctions::tests. ↩

DRAFT — Ontology Diagnostics: Adjunction-Based Gap Detection in Scientific Knowledge Representation

Core Claim

Existing approaches to ontology quality focus on consistency (is it logically sound?) and alignment (do two ontologies match?). Neither addresses COMPLETENESS: is the ontology missing distinctions that it should have?

I present a formal meta-ontology — an ontology about ontology engineering — that formalizes the process of detecting and resolving missing distinctions using categorical adjunctions. The methodology is:

1. Formalize two related domains as categories
2. Build structure-preserving maps (functors) in both directions
3. Construct the adjunction (unit + counit morphisms)
4. Entities where unit != identity = MISSING DISTINCTIONS in the source
5. Resolve via ContextDef (non-destructive) or enrichment (destructive)
6. Verify resolutions against published literature
7. Measure improvement via loss ratio reduction

The meta-ontology itself is formalized as a pr4xis domain with 29 entities¹, 14 methodology steps¹, 13 axioms¹, and 894 machine-verified proofs².

What Exists in Literature vs What Is Novel

Exists:

• Meta-ontology (Van Inwagen 1998): philosophical study of what ontology IS. Asks “what do we mean by existence?” — DIFFERENT from our question.
• Upper ontologies (BFO, DOLCE, SUMO): top-level categories for all domains. Provide classification, not gap detection.
• Ontology alignment (Euzenat & Shvaiko 2013): matching entities across ontologies. Finds CORRESPONDENCES, not MISSING entities.
• Ontology debugging (Schlobach & Cornet 2003): finds logical INCONSISTENCIES. We find INCOMPLETENESS — a different problem.
• Ologs (Spivak & Kent 2012): categorical knowledge representation using functors. Maps between domains. Does NOT use adjunctions for gap detection.
• Category theory (Mac Lane 1971): adjunctions are standard mathematics.

Novel:

• Using adjunction unit/counit to DETECT missing ontological distinctions
• Quantifying inter-scale information loss via gap ratios
• ContextDef as non-destructive gap resolution (preserves functor validity)
• Loss threshold classification (Low/Moderate/High → different resolution types)
• The meta-ontology itself: formalizing the methodology as a praxis domain
• Empirical finding: every adjunction between biological domains at different scales has gaps, and every gap corresponds to a published distinction

The Meta-Ontology

Entities (29)

Methodology Pipeline (14 steps)

FormalizeDomains → ConstructFunctors → VerifyFunctorLaws → ConstructAdjunction
→ ComputeUnit + ComputeCounit → DetectGaps → ClassifyGaps + ComputeLossRatios
→ ProposeResolution → VerifyAgainstLiterature → ImplementResolution
→ RunMachineProofs → AssessImprovement

Key Qualities

IsAutoDetectable: Most gap types (UnitGap, CounitGap, InformationLoss, GranularityMismatch, CanonicalRepresentative) are automatically detectable by adjunction analysis. Only MissingDistinction requires human judgment to NAME the distinction — the adjunction tells you WHERE it is, the human tells you WHAT it is.

PreservesFunctorValidity: ContextResolution adds distinctions WITHOUT changing the category structure — existing functors remain valid. OntologyEnrichment adds new entities which may require updating all functors (breaking change).

SuggestedForLossLevel: Empirical classification from 3 adjunctions:

• <40% loss → GranularityRefinement (minor adjustment)
• 40-80% loss → ContextResolution (add functional modes)

• 80% loss → IntermediateDomain (domains too far apart)

Proven Axioms (13)

Empirical Validation

Computed from the codebase (not estimated)⁴:

The Molecular ⊣ Bioelectric loss of 85% triggered the IntermediateDomain recommendation. The biochemistry domain was already built as this intermediate — connecting molecular→biochemistry→bioelectricity should reduce the direct loss.

The Kv Discovery (Case Study)

The adjunction between molecular biology and bioelectricity detected that the potassium channel Kv COLLAPSES on the round-trip:

Kv → (MolecularToBioelectric) → IonChannelModulation
   → (BioelectricToMolecular) → GlyR

Kv goes in, GlyR comes out. The round-trip changed the identity.

What the adjunction detected: The bioelectric ontology treats MembranePotential (passive signal) and IonChannelModulation (active intervention) as separate concepts. But at the molecular level, BOTH are implemented by the same Kv channel. The molecular ontology was missing a distinction between constitutive and therapeutic functional modes.

How ContextDef resolved it:

(Kv, Constitutive)  → PassiveHomeostatic    — sets resting Vmem
(Kv, Therapeutic)   → TherapeuticTarget     — drug shifts Vmem

Literature verification: Kv as resting Vmem setter = textbook electrophysiology. Kv as drug target = Kofman & Levin 2024. Both roles are established. The adjunction didn’t discover new biology — it discovered a MISSING FORMALIZATION of known biology.

Discussion

Why This Matters

Most ontology engineering relies on human experts to decide which distinctions to include. This is inherently incomplete — experts model what they think is important, not what the STRUCTURE requires. Adjunctions provide an objective, automated criterion: if the round-trip changes an entity’s identity, the ontology is missing something.

Relation to Spivak’s Ologs

Spivak & Kent (2012) introduced ologs as categorical ontologies with functors for cross-domain mapping. Our contribution extends this: Spivak uses functors to CONNECT domains. I use adjunctions (paired functors) to DIAGNOSE domains. The gap detection methodology is a natural extension of the olog framework that Spivak did not explore.

Limitations

• The discrete category structure means functor mapping choices affect which gaps are detected. Different functors might reveal different gaps.
• The loss thresholds (40%/80%) are empirical from 3 adjunctions. More adjunctions needed to validate these thresholds.
• ContextDef resolves gaps but doesn’t reduce loss ratios. The loss reflects genuine abstraction, not an error.

Testable Predictions

1. Adding more adjunctions to the system should always reveal gaps (the methodology should generalize)
2. Intermediate domains should measurably reduce loss ratios
3. The loss thresholds should be stable across different scientific domains

Code & Verification

All source code, tests, and the live computational analysis are at:

https://github.com/i-am-logger/pr4xis

Re-deriving every numerical claim

git clone https://github.com/i-am-logger/pr4xis
cd pr4xis
cargo test --workspace
cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture

The first command runs the full workspace test suite. The second prints the live per-adjunction collapse percentages cited in this paper — including the 85.2% molecular-bioelectric round-trip loss that the meta-ontology classifies as “high loss → IntermediateDomain recommended”.

Key files

• The meta-ontology itself lives at crates/domains/src/formal/meta/ontology_diagnostics/ontology.rs — the pr4xis::ontology! block that encodes the 29 concepts, the 14-step methodology pipeline, and the 13 axioms about ontology engineering. The directory also contains collapse_patterns.rs (the loss-threshold classifications) and a README.md.
• The computational gap analysis is at crates/domains/src/formal/meta/gap_analysis.rs — the live functions (analyze_molecular_bioelectric(), analyze_pharmacology_molecular(), analyze_biology_bioelectric(), test_full_chain_collapse_measurement) that compute the collapse percentages from the actual functor implementations every test run.
• The three adjunctions themselves live at crates/domains/src/natural/biomedical/adjunctions.rs — MolecularBioelectricAdjunction, PharmacologyMolecularAdjunction, BiologyBioelectricAdjunction, each with unit and counit implementations and the test suite that verifies them.
• The Kv gap and its ContextDef resolution live at crates/domains/src/natural/biomedical/molecular/ontology.rs — the MolecularEntity enum, the MolecularFunctionalContext enum, and the ContextDef impl that disambiguates (Kv, Constitutive) from (Kv, Therapeutic).

Test-command index for the load-bearing claims

The “894 machine-verified tests” count in §1 is the meta-ontology subset at the time of drafting. The workspace total is 4,855 tests, re-derivable via cargo test --workspace. Both numbers update automatically with the codebase.

References

• Spivak DI, Kent RE (2012). Ologs: a categorical framework for knowledge representation. PLoS ONE.
• Spivak DI (2014). Category Theory for the Sciences. MIT Press.
• Mac Lane S (1971). Categories for the Working Mathematician. Springer.
• Euzenat J, Shvaiko P (2013). Ontology Matching. Springer.
• Schlobach S, Cornet R (2003). Non-standard reasoning in description logics. IJCAI.
• Van Inwagen P (1998). Meta-ontology. Erkenntnis.
• Rosen R (1991). Life Itself. Columbia University Press.
• Levin M (2014). Molecular bioelectrics in developmental biology. Mol Biol Cell.
• Kofman K, Levin M (2024). Bioelectric pharmacology of cancer.
• Coste B et al (2010). Piezo1 and Piezo2. Science. Nobel 2021.

Verification Footnotes

1. The meta-ontology lives at crates/domains/src/formal/meta/ontology_diagnostics/ontology.rs. The 29 concepts, 14 methodology steps, and 13 axioms are encoded in the pr4xis::ontology! block. Run cargo test -p pr4xis-domains formal::meta::ontology_diagnostics to verify the encoding compiles and the structural axioms hold. ↩ ↩2 ↩3

2. Re-derive by running cargo test --workspace. The “894” count is the meta-ontology subset at drafting time; the workspace total is computed live on every run. ↩

3. The 13 axioms about ontology engineering (including EveryAdjunctionHasGaps, PipelineIsComplete, ContextResolutionPreservesFunctors, etc.) are implemented as Rust Axiom impls in the meta-ontology directory. Each axiom has a corresponding test that verifies it holds against the actual three-adjunction analysis. Run cargo test -p pr4xis-domains formal::meta::ontology_diagnostics::tests. ↩

4. Every collapse percentage in this paper is computed live by cargo test -p pr4xis-domains test_full_chain_collapse_measurement -- --nocapture. The output prints per-adjunction unit-loss and counit-loss percentages from the actual functor implementations in crates/domains/src/natural/biomedical/adjunctions.rs. Numbers update automatically as the biomedical ontologies evolve. ↩ ↩2 ↩3 ↩4 ↩5 ↩6 ↩7

5. The Kv channel discovery — round-trip collapse and ContextDef resolution — is verified by cargo test -p pr4xis-domains test_kv_gap_is_resolved_by_context. The context resolution lives in crates/domains/src/natural/biomedical/molecular/ontology.rs as MolecularFunctionalContext. ↩

Overview

marp: true theme: default paginate: true backgroundColor: #0d1117 color: #c9d1d9 style: | section { font-family: -apple-system, BlinkMacSystemFont, ‘Segoe UI’, Helvetica, Arial, sans-serif; font-size: 28px; } h1 { color: #58a6ff; font-size: 1.6em; } h2 { color: #c9d1d9; font-size: 1.3em; } a { color: #58a6ff; } table { font-size: 0.85em; width: 100%; border-collapse: collapse; background: transparent; } th { color: #58a6ff; font-size: 0.9em; border-bottom: 2px solid #30363d; background: #161b22; padding: 0.5em 0.7em; } td { color: #e6edf3; padding: 0.5em 0.7em; border-bottom: 1px solid #21262d; background: #0d1117; } tr:nth-child(even) td { background: #161b22; } code { background: #161b22; color: #e6edf3; padding: 0.1em 0.4em; border-radius: 4px; } pre { background: #161b22 !important; border: 1px solid #30363d; border-radius: 6px; padding: 1em; } pre code { background: transparent !important; } strong { color: #f0f6fc; } em { color: #8b949e; } .pass { color: #3fb950; } .fail { color: #f85149; } .ignore { color: #d29922; } section::after

pr4xis

Axiomatic intelligence.

Doing the right thing — with proof.

“Every good regulator of a system must be a model of that system.” — Conant & Ashby (1970)

Logger

i-am-logger

What is pr4xis?

Aristotle named three kinds of knowing:

• episteme — knowing how things ARE (science)
• techne — knowing how to MAKE things (technology)
• praxis — the doing itself, done well

pr4xis is the doing.

Domain knowledge lives in composable ontologies. Not in mechanical processing logic. No parser-with-special-cases, no rules with hardcoded strings. Every transformation is a proven functor. Every claim traces to an axiom.

How it works

Define rules (Ontology) → Check rules (Engine) → Prove rules hold (Tests)
         ↑                                              |
         └──────────── feedback ────────────────────────┘

The ontology IS the model. The engine IS a control system. Conant-Ashby (1970) proven in code: Model → Ontology.

The Architecture

No domain logic in framework code. Adding chess, physics, or English changes nothing in the engine.

Domains compose via functors

If Chess IS EventDriven (functor) and EventDriven IS Concurrent (functor), then Chess IS Concurrent (composition). The proof is automatic.

Natural Language Pipeline

Text → Language::lexical_lookup → Pregroup types → Contract → Semantics → Response

• Language trait — language-agnostic. English, Hebrew, same code.
• Pregroup grammar — parsing as group algebra (Lambek 1999)
• Montague functor — syntax → semantics (proven)
• Zero hardcoded words — everything through the ontology

np · n^l · n · np^r · s → contract → s — “the dog runs” parsed by algebra.

Turing Test Benchmark

Questions from real competitions (Loebner Prize, Winograd Schema Challenge).

Every pending test = a research task. When the ontology is built, the test passes.

pr4xis vs LLMs

Contributions

pr4xis architecture — a synthesis built on a sixty-year intellectual lineage:

1. Domain knowledge in composable ontologies — every domain is a category in the formal sense (Guarino 1998 framing; Spivak ologs as prior art)
2. Functorial composition between behavioral ontologies — extending Spivak’s data-migration pattern from schemas to behavior
3. Conant-Ashby as architectural justification — the engine is a model because the theorem requires it
4. DOLCE as upper layer with category theory as the substrate — both used together
5. Composable proof chains — if A IS B and B IS C, then A IS C, by functor composition

Academic Foundation

50+ papers, all downloaded and cited:

• Category theory — Mac Lane, Awodey, Spivak (ologs)
• Control systems — Wiener, Ashby, Conant-Ashby, Powers
• Formal ontology — DOLCE, Guarino, Gangemi (ODPs)
• Linguistics — Lambek, Montague, Kamp (DRT), Steedman (CCG)
• Information — Shannon, Damerau, Brill & Moore
• Metacognition — von Foerster, Spencer-Brown

Full lineage: docs/understand/foundations.md

Live Demo

~107,000 WordNet concepts. Running in your browser right now. No server, no GPU, no API key.

What’s next

• More ontologies — each grammar gap and missing concept is a research task
• More functors — importing BioPortal, the Gene Ontology, OBO Foundry, DOLCE as composable categories
• Hebrew — a second language proves the architecture is language-agnostic
• Drafts in flight — three research papers on bioelectricity, gap detection, and ontology diagnostics; see docs/research/papers/

The name pr4xis is not marketing. It is a claim backed by cargo test --workspace.

Thank you

Logger

i-am-logger

github.com/i-am-logger/pr4xis

Axiomatic intelligence. Domain knowledge in composable ontologies. Every claim has a proof.

References

Primary academic sources for the ontologies in this repository.

Relationship to per-ontology citings.md files. Each ontology under crates/domains/src/ now has its own citings.md listing the sources it actually stands on (see issue #57). This file is the workspace-wide cross-reference: it collects the sources that appear in multiple per-ontology bibliographies and provides their full bibliographic entries in one place. When you add a citation to an ontology’s citings.md, check whether the full entry belongs here too — if another ontology already cites it, move the full entry here and replace the per-ontology form with a pointer.

Coverage gap. The sections below were written before the per-ontology rollout and cover only 14 domains (geometry, rotation, time, linear algebra, probability, kinematics, geodesy, sensor fusion, military standards, clock characterization, signal processing, statistics, control theory). The rollout produced ~100 per-ontology citings.md files covering the full formal/natural/applied/social/cognitive tree; many of the sources in those files are not yet represented here. Filling the gap is tracked under issue #57 as a follow-up sweep.

Geometry

• Hilbert, D. (1899). Grundlagen der Geometrie. Teubner, Leipzig. [The axiomatic foundation of Euclidean geometry — 20 axioms in 5 groups: incidence, order, congruence, parallelism, continuity.]
• Avigad, J., Dean, E., & Mumma, J. (2009). “A Formal System for Euclid’s Elements.” Review of Symbolic Logic, 2(4):700-768. PDF
• Coxeter, H.S.M. (1969). Introduction to Geometry (2nd ed.). Wiley.

Rotation (SO(3)) and Rigid Motion (SE(3))

• Shuster, M.D. (1993). “A Survey of Attitude Representations.” Journal of the Astronautical Sciences, 41(4):439-517. [Comprehensive comparison of rotation representations: quaternion, DCM, Euler, axis-angle, MRP.]
• Sola, J. (2017). “Quaternion kinematics for the error-state Kalman filter.” arXiv:1711.02508. [Quaternion conventions, composition, perturbation, for sensor fusion.]
• Murray, R.M., Li, Z., & Sastry, S.S. (1994). A Mathematical Introduction to Robotic Manipulation. CRC Press. [SE(3) Lie group, twists, wrenches, exponential coordinates.]
• Kumar, V. “Rigid Body Kinematics and the Lie group SE(3).” University of Pennsylvania MEAM 620 lecture notes. PDF
• Kim, J. “Lie Group Formulation of Articulated Rigid Body Dynamics.” CMU Technical Report. PDF

Time

• Allen, J.F. (1983). “Maintaining Knowledge about Temporal Intervals.” Communications of the ACM, 26(11):832-843. [The 13 interval relations — foundational temporal reasoning.]
• Grüninger, M. & Li, Z. (2017). “The Time Ontology of Allen’s Interval Algebra.” TIME 2017, LIPIcs Vol. 90. PDF
• W3C (2017). “Time Ontology in OWL.” W3C Recommendation. Specification
• Allan, D.W. (1966). “Statistics of Atomic Frequency Standards.” Proceedings of the IEEE, 54(2):221-230.
• Riley, W.J. (2008). Handbook of Frequency Stability Analysis. NIST Special Publication 1065. PDF
• IEEE Std 1139-2008. “Standard Definitions of Physical Quantities for Fundamental Frequency and Time Metrology — Random Instabilities.”

Time Systems

• IAU 2000 Resolution B1.9: Definition of Terrestrial Time (TT = TAI + 32.184 s).
• IAU 2006 Resolution B3: Barycentric Coordinate Time (TCB) and related scales.
• IS-GPS-200 (2022). “Interface Specification: Navstar GPS Space Segment / Navigation User Segment Interfaces.” US Space Force. [GPS time definition: GPS = TAI - 19 s.]
• ITU-R TF.460 (2002). “Standard-frequency and time-signal emissions.” [UTC definition with leap seconds.]
• Ashby, N. (2003). “Relativity in the Global Positioning System.” Living Reviews in Relativity, 6(1). PMC
• ESA Navipedia. “Transformations between Time Systems.” Reference

Linear Algebra

• Axler, S. (2024). Linear Algebra Done Right (4th ed.). Springer. [Vector space axioms, eigenvalues, spectral theorem.]
• Strang, G. (2023). Introduction to Linear Algebra (6th ed.). Wellesley-Cambridge Press. [Positive definite matrices, Cholesky, SVD.]
• Kahan, W. “Axioms for Fields and Vector Spaces.” UC Berkeley Math H110 notes. PDF
• Horn, R.A. & Johnson, C.R. (2013). Matrix Analysis (2nd ed.). Cambridge University Press. [Determinant properties, matrix inequalities, Schur complement.]

Probability and Estimation Theory

• Kolmogorov, A.N. (1933). Grundbegriffe der Wahrscheinlichkeitsrechnung. Springer, Berlin. [The axiomatic foundation of probability: 3 axioms.] Archive
• Tao, T. (2015). “275A, Notes 0: Foundations of probability theory.” Blog
• Mahalanobis, P.C. (1936). “On the generalized distance in statistics.” Proceedings of the National Institute of Sciences of India, 2(1):49-55.
• Fisher, R.A. (1925). “Theory of Statistical Estimation.” Mathematical Proceedings of the Cambridge Philosophical Society, 22(5):700-725. [Fisher information, Cramér-Rao bound.]

Kinematics

• Goldstein, H., Poole, C., & Safko, J. (2002). Classical Mechanics (3rd ed.). Addison-Wesley. [Lagrangian and Hamiltonian formulations, rigid body dynamics.]
• Shabana, A.A. (2020). Dynamics of Multibody Systems (5th ed.). Cambridge University Press. [Kinematics on manifolds, screw theory.]
• Bernstein, D.S., Goel, A., & Ansari, A. “Geometry, Kinematics, Statics, and Dynamics.” Cornell University. PDF

Geodesy

• Torge, W. & Müller, J. (2012). Geodesy (4th ed.). de Gruyter. [WGS84, ellipsoid, coordinate systems.]
• NIMA (2000). “Department of Defense World Geodetic System 1984.” Technical Report TR8350.2 (3rd ed.). [WGS84 specification: a = 6378137.0 m, f = 1/298.257223563.]
• Bowring, B.R. (1976). “Transformation from spatial to geographical coordinates.” Survey Review, 23(181):323-327. [Geodetic ↔ ECEF conversion algorithm.]

Sensor Fusion

• Kalman, R.E. (1960). “A New Approach to Linear Filtering and Prediction Problems.” Journal of Basic Engineering, 82(1):35-45. [The Kalman filter.]
• Bar-Shalom, Y., Li, X.R., & Kirubarajan, T. (2001). Estimation with Applications to Tracking and Navigation. Wiley. [Multi-target tracking, data association, JPDA, MHT.]
• Groves, P.D. (2013). Principles of GNSS, Inertial, and Multisensor Integrated Navigation Systems (2nd ed.). Artech House. [INS/GNSS integration, strapdown mechanization, lever arm, boresight.]
• Maybeck, P.S. (1979). Stochastic Models, Estimation, and Control (Vols. 1-3). Academic Press. [State space models, Kalman filter theory.]
• Thrun, S., Burgard, W., & Fox, D. (2005). Probabilistic Robotics. MIT Press. [SLAM, particle filters, occupancy grids.]

Military Standards

• US DoD JDL (1999). “Data Fusion Lexicon.” Joint Directors of Laboratories, Data Fusion Sub-Panel. [JDL fusion model: Levels 0-5.]
• STANAG 4586 (2012). “Standard Interfaces of UAV Control System for NATO UAV Interoperability.” NATO.
• MISB ST 0601 (2021). “UAS Datalink Local Set.” Motion Imagery Standards Board. [Sensor metadata for UAS platforms.]
• MIL-STD-1553B (1978). “Aircraft Internal Time Division Command/Response Multiplex Data Bus.” US DoD.

Clock Characterization

• IEEE Std 1139-2008. “Standard Definitions of Physical Quantities for Fundamental Frequency and Time Metrology.”
• ITU-R TF.538-4 (2017). “Measures for random instabilities in frequency and time.” Recommendation
• Rohde & Schwarz (2019). “Time Domain Oscillator Stability Measurements.” Application Note 1EF69. PDF

Signal Processing

• Shannon, C.E. (1949). “Communication in the Presence of Noise.” Proceedings of the IRE, 37(1):10-21.
• Nyquist, H. (1928). “Certain Topics in Telegraph Transmission Theory.” Transactions of the AIEE, 47(2):617-644.
• Oppenheim, A.V. & Willsky, A.S. (1997). Signals and Systems (2nd ed.). Prentice Hall.
• Peyré, G. (2019). Mathematical Foundations of Data Sciences. CNRS/DMA. PDF
• Byrne, C.L. Mathematics of Signal Processing: A First Course. UMass Lowell. PDF

Statistics

• Fisher, R.A. (1925). “Theory of Statistical Estimation.” Mathematical Proceedings of the Cambridge Philosophical Society, 22(5):700-725.
• Neyman, J. & Pearson, E.S. (1933). “On the Problem of the Most Efficient Tests of Statistical Hypotheses.” Philosophical Transactions A, 231:289-337.
• Student (Gosset, W.S.) (1908). “The Probable Error of a Mean.” Biometrika, 6(1):1-25.
• Cramér, H. (1946). Mathematical Methods of Statistics. Princeton University Press.
• Rao, C.R. (1945). “Information and the accuracy attainable in the estimation of statistical parameters.” Bulletin of the Calcutta Mathematical Society, 37:81-91.

Control Theory

• Åström, K.J. & Murray, R.M. (2008). Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press. PDF
• Ogata, K. (2010). Modern Control Engineering (5th ed.). Prentice Hall.
• Lyapunov, A.M. (1892). “The General Problem of the Stability of Motion.” Kharkov Mathematical Society.
• Ziegler, J.G. & Nichols, N.B. (1942). “Optimum Settings for Automatic Controllers.” Transactions of the ASME, 64:759-768.
• Doyle, J.C., Francis, B.A. & Tannenbaum, A.R. (1992). Feedback Control Theory. Macmillan.