Epistemic Calculi
A Categorical Formalization of Epistemic Uncertainty Frameworks
Formal Verification Certificate
All 90+ theorems machine-checked by the Lean 4 kernel with zero sorry gaps. Includes corrections to the original paper.
Epistemic Calculi • Lean 4 + Mathlib • Apoth3osis Labs
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.
Overview
Aambø's framework unifies probability theory, possibility theory, certainty factors, and Dempster–Shafer theory under a single categorical spine: a non-trivial unital symmetric monoidal posetal category. Eight axiom classes (E1–E8) systematically generate the landscape of existing and novel uncertainty calculi.
Our formalization in 26 Lean 4 modules with 90+ sorry-free theorems discovered and corrected three issues in the original paper:
- Theorem 3.6 gap: composition coherence for odds-form Bayesian updating required an additional naturality condition not stated in the paper.
- CF residuation: fragile instance resolution in the closed certainty-factor calculus needed explicit universe annotations to avoid Lean 4 diamond inheritance.
- Bridge coverage: categorical bridge tests between probability and possibility instances were missing from the original framework.
Key Results
Epistemic Calculus Typeclass
Core categorical structure capturing the common spine of all uncertainty frameworks as a non-trivial unital symmetric monoidal posetal category.
8 Axiom Classes (E1–E8)
Optimistic, Complete, ConservativeFusion, Closed, StronglyConservative, Idempotent, Fallible, and Cancellative — each proved to generate specific calculi.
V-Enriched Bayesian Updating
Bayesian conditioning formalized as a V-enriched functor with corrected composition coherence for odds-form updating.
Landscape Instances
Probability, possibility, certainty factors, and Dempster-Shafer all instantiated as specific axiom-class combinations.
Artifacts & Links
MENTAT Contribution Records
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerCategorical Framework for Epistemic Uncertainty
Contributor
Torgeir Aambø
Norwegian Defence Research Establishment (FFI)
Core insight: epistemic uncertainty frameworks (probability, possibility, certainty factors, Dempster-Shafer) share a common categorical spine — a non-trivial unital symmetric monoidal posetal category. Axiom classes (E1–E8) systematically generate the landscape of existing and novel calculi through lattice-theoretic extension.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerBayesian Updating as V-Enriched Functor
Contributor
Torgeir Aambø
Norwegian Defence Research Establishment (FFI)
The theory layer recasts Bayesian conditioning as a V-enriched functor between epistemic calculi. Odds-form updating, certainty-factor residuation, and Dempster-Shafer combination emerge as instances of a single categorical pattern.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization with Paper Corrections
Contributor
Apoth3osis Labs
R&D Division
Machine-checked formalization in 26 modules with 90+ sorry-free theorems. Discovered and corrected a composition coherence gap in the original paper's Theorem 3.6 (odds-form Bayesian updating), fixed fragile instance resolution in closed CF residuation, and added missing categorical bridge test coverage.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026