As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars whose metatheory is mechanized in Lean 4: a dependent type theory (EigenTT) separating confluent conversion from ontology subsumption and keeping proof irrelevance axiomatic so distinct warrants remain inspectable; proof-calculus institutions acting as strongly typed integration boundaries; and a content-addressed immutable storage layer. Epistemic status (declared/observed/derived/verified) forms a bounded lattice over a justification logic enforced at commit. Cross-system comorphisms carry explicit axiom policies (Adopt, Discharge, Relativize), transport witnesses at commit, and materialize outputs into the graph, while EigenQL provides a Grothendieck query view across all hosted logics and shared on-chain IRs collapse multi-system translations to identity. Pairing empirical justification logic with an in-process Lean 4 term checker, an end-to-end recomputation of a published Nature study from pinned data discharges all 52 derived conclusions and surfaces four machine-checked discrepancies in the original study.
Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established. A persistent knowledge store, by contrast, must retain that record: who established a claim, by which derivation or external tool, and under which assumptions. This volume presents the theory of Eigenius---a store of typed knowledge over constructive institutions---and develops its metatheory from that requirement. The kernel theory is a dependent type theory with cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type. Proof irrelevance is an axiom with an explicit witness rather than a conversion rule, so proofs of a proposition are provably equal yet remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system---confluent, injective on type formers, and decidable by a type-free test---while a separate subsumption judgment covers universe cumulativity, codomain-covariant function types, and declared class inclusions. We prove consistency via a set-theoretic model; develop a justification logic over the kernel's propositions to track evidence and support; organize environments as an institution so that store extensions are signature morphisms and external verdicts enter via comorphisms; formulate a typed knowledge-graph theory with records, classes, and refinements; and prove the correctness of conversion, normalization by evaluation, and bidirectional type checking relative to termination. A Lean 4 formalization accompanies the volume.