# Extracted text

Source: Zenodo record 23987671, rikishi-1.1.0-paper.pdf.
Source PDF SHA-256: 0c4ced81075d3f4c6a5fae772b5497882dddc3fbae17fedce21e8b37336ada27
Extraction: pypdf 6.21.4, all 54 pages in order.

## Page 1

Rikishi
Reproducible operation and analysis of the Suggested Upper Merged Ontology
Daniel Ari Friedman
Active Inference Institute
ORCID: 0000-0001-6232-9096
DOI: 10.5281/zenodo.23987670
Software methods manuscript v1.1.0 (2026-11-06)


## Page 2

From ontology commitments to finite mathematics
A source formula, a mathematical law, and a calculation answer different questions. The shared witness makes
their relationship inspectable.
Graphical abstract 1 of 3

## Page 3

Shared finite witnesses and exact posterior inference
The same prior, observation kernel, candidate distribution, and observed outcome enter every evidence lane. Exact
arithmetic identifies what the calculation should return.
Graphical abstract 2 of 3

## Page 4

Evidence for models representations calculations and results
Evidence attaches to specific claims about specific artifacts. Shared identifiers connect the lanes without replacing
their separate proof and measurement obligations.
Graphical abstract 3 of 3

## Page 5

Contents
Abstract 6
1 SUMO foundations and scholarship 6
1.1 A reader’s map: ontology, mathematics and execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2 SUMO as an axiomatized upper ontology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.3 Vocabulary, sentences and interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Modeling commitments and source interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.5 Read a source expression from the outside in . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.6 SUO-KIF and reasoning translations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.7 Incomplete descriptions and logical consequence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.8 Sigma engineering and lexical mappings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.9 Competency questions, reengineering, and benchmarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.10 Active Inference alignment as direct precedent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2 Operator architecture and evidence 12
2.1 Provenance and thin orchestration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2 Quantification and interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3 Corpus and native reasoning observations 13
3.1 Source-derived measurements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.2 Direct taxonomy structure and source navigation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.3 Worked inspection of the pinned SUMO theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.3.1 Categories and relation signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.3.2 Probability and modal context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.3.3 Thin orchestration and separate proof controls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.4 Source-bound inference laboratory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.4.1 Questions, theories, and interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.4.2 Declared source selection and supported fragment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.4.3 Worked consequence families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.4.4 Adversarial controls and native evidence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.4.5 Reproduction and evidence transfer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.5 Restricted proofs and native diagnostics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
4 A finite variational example 24
4.1 Logarithmic evaluation and numerical support . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5 Connections to formalization 27
5.1 What connects SUMO to FEP_Formal? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5.2 Finite elaboration and semantic scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5.3 From proposed alignment to a tested interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5.4 Executed finite interpretation and controls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5.5 Shared finite witnesses across representations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5.5.1 Four referents and the claims attached to them . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5.5.2 Exact examples that distinguish a model from its posterior . . . . . . . . . . . . . . . . . . . . . . . . . 33
5.5.3 A source-bound derivation and its counterexamples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5.5.4 Evidence roles as a research interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
5.5.5 A connection atlas with distinct tests at each arrow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
5.6 Changing representations without confusing the evidence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.6.1 A smaller divergence need not mean better inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.6.2 State aggregation and observation degradation are different experiments . . . . . . . . . . . . . . . . . . 42
5.7 Posterior identity, observation evidence and model comparison . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
5.8 Sequential inference, simulation and prediction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
5.8.1 Mixed histories expose the observation model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5.8.2 Model checking has several different meanings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5.9 What an ontology expression would have to preserve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
6 Reproducibility and contribution 50
6.1 Publication from declared authorities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
6.2 Operator workflow and limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4

## Page 6

6.3 Licensing and attribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5

## Page 7

Abstract
The Suggested Upper Merged Ontology (SUMO) supplies general categories, relations and axioms for knowledge
representation. Its source language, Standard Upper Ontology Knowledge Interchange Format (SUO-KIF), and
its reasoning environment, Sigma Knowledge Engineering Environment (KEE), have different roles. Rikishi is a
source-bound workbench for inspecting those commitments, submitting selected reasoning problems, and retaining
their inputs and evidence. This paper asks how that infrastructure can make a scientific modeling connection
inspectable. Prior Active Inference–SUMO alignment provides a direct precedent ( Douglass et al. , 2024).
One shared finite witness connects selected ontology expressions to probability models, numerical evaluation, pinned
FEP_Formal Lean statements and synthetic observation histories. The ontology lane investigates declared model,
representation, calculation and result roles. The mathematical lane supplies finite normalization, conditioning and
information identities under stated hypotheses. The computational lane checks numerical outputs and generates
trajectories from an explicit persistent-state model. Stable identifiers and common inputs join these lanes without
treating their claims as interchangeable.
Worked source formulas, direction-sensitive queries, numerical references and formal controls make the connections
testable. Exact conditioning is separated from simulated frequencies, and variational inference from action selection
and empirical model assessment. The resulting interface supports reproducible inspection of particular examples;
it does not establish full-SUMO consistency, a general SUMO-to-Lean interpretation, verification of all Python
execution, or biological validity of the Free Energy Principle (FEP).
The manuscript’s concept digital object identifier (DOI), covering all versions, is 10.5281/zenodo.23987670. The
version 1.1.0 manuscript is identified by 10.5281/zenodo.23987671 and its Zenodo version record . The separately
archived software version 1.1.0 is identified by 10.5281/zenodo.23987623.
1 SUMO foundations and scholarship
The research question is how an ontology operator can make a proposed scientific alignment inspectable and exe-
cutable without conflating its different objects. A source formula states an ontological commitment; a mathematical
law specifies a finite probability model; a program evaluates that model; and a proof concerns a proposition under
hypotheses. The alignment precedent supplies candidate senses ( Douglass et al. , 2024), while SUMO translation
work shows that the target logic and its treatment of types are substantive parts of an interpretation ( Pease, 2023;
Brown et al. , 2023). Rikishi connects these objects through explicit inputs and evidence, rather than treating a
shared label as a semantic correspondence.
1.1 A reader’s map: ontology, mathematics and execution
An upper ontology provides reusable commitments about kinds of entities and their relations. SUMO can help
two applications state whether they mean an individual, a class, a process, a representation or a result, and which
axioms constrain those choices. Its value is both organizational and inferential: compatible definitions support
integration, while axioms can support queries whose answers require more than finding a matching word ( Niles
and Pease , 2001; Pease and Schulz , 2014). The precise consequence still depends on the selected theory and its
interpretation.
The components used here have different jobs:
Component What it supplies Question it addresses here
SUMO General classes, relations, signatures
and axioms
What is the proposed referent, and
which consequences follow from the
selected commitments?
SUO-KIF The language of the source
expressions
What exactly is asserted, with
which quantifiers, argument roles
and contexts?
6

## Page 8

Component What it supplies Question it addresses here
Sigma KEE Ontology browsing, management,
translation and prover integration
How is a configured theory operated
and submitted to a reasoning
system?
FEP_Formal Pinned Lean definitions and
mathematical statements
Which finite laws and identities
hold under the stated hypotheses?
Rikishi’s evaluators and simulator Numerical calculations and
synthetic trajectories from declared
inputs
What does this implementation
return or generate for this
particular model?
Rikishi’s evidence records Source, input, command, output
and role bindings
Which observation supports which
claim about which artifact?
SUMO is therefore not interchangeable with its source language, a theorem prover, or a simulator. Likewise, a
vocabulary correspondence is a proposal about meaning; a numerical equality, a checked Lean term and a synthetic
trajectory supply different tests of that proposal. The running connection is a shared finite witness : one explicitly
specified probability model is represented in each lane, with stable identifiers and a separate obligation at every
connection. The ontology foundations below establish the source side; sec. 5.1 follows one witness through the
mathematical and computational sides.
1.2 SUMO as an axiomatized upper ontology
The Suggested Upper Merged Ontology (SUMO) supplies general categories, relations, and axioms intended to sup-
port more specialized theories. Its original proposal addressed the Institute of Electrical and Electronics Engineers
(IEEE) Standard Upper Ontology working group and sought a common foundation for knowledge representation
and integration. The construction method distinguished a syntactic merge, converting selected prior representations
into SUO-KIF, from a semantic merge, reconciling their conceptual commitments. A merged upper structure based
on Sowa’s and Russell and Norvig’s ontologies organized additional content, including temporal and mereotopolog-
ical theories. Integration could require inserting intermediate categories, rejecting unsuitable content, recognizing
equivalent axioms, or revising partially overlapping theories. This was an explicit modeling and reconciliation
process; its consistency goal is not a proof about every subsequent SUMO revision ( Niles and Pease , 2001).
The distribution preserves a layered organization. Merge.kif contains the upper ontology; the Mid-Level Ontology
(MILO), distributed as Mid-level-ontology.kif , bridges abstract categories and domain detail. Domain files
extend this vocabulary for particular subject areas. Natural-language formatting and lexical resources add another
operational layer. Consequently, the indexed source corpus, a configured reasoning profile, and an all-domain load
must be identified separately. Loading additional files changes the theory under investigation. Rikishi’s source lock,
file manifest, and runtime profile make that selection inspectable ( OntologyPortal, n.d.c).
1.3 Vocabulary, sentences and interpretations
An upper ontology offers a reusable account of what kinds of things a domain model talks about. SUMO makes
that account explicit through named categories, relations, function symbols and axioms. A physical execution,
a proposition that specifies a model, a number used in a calculation and an agent involved in an execution can
therefore receive different descriptions even when an application handles them in one software object. Choosing the
description is a modeling commitment: it determines which inherited constraints and consequences apply ( Niles
and Pease , 2001; OntologyPortal, n.d.c).
Three levels help a reader follow the notation. A symbol names something in the vocabulary. A sentence uses
symbols and logical operators to make an assertion. An interpretation supplies a domain and meanings for those
symbols; it is a model of a selected theory when it satisfies that theory’s sentences. Counting symbols describes a
source inventory. Following an asserted taxonomy edge describes a syntactic projection. Establishing a consequence
requires the selected axioms and their interpretation. These activities answer different questions even when their
displays contain the same names.
7

## Page 9

The distinctive combination is a broad shared vocabulary with expressive, axiomatized relationships. For example,
the existing source classifications of ProbabilityFn describe a function entity, while an occurrence of that function
inside a term denotes a value under an interpretation. Likewise, agent names a relation that can itself be classified
and given a signature; using it as the head of an assertion relates a process to a participant. Capitalization and
English resemblance are useful reading cues, but the surrounding formulas supply the classifications. A lexical
match to “agent” cannot decide whether the intended referent is that relation or an entity belonging to an agent
class ( OntologyPortal, n.d.c).
For a scientific extension this changes the first question from “which label looks similar?” to “what entity or
relationship does the proposed expression commit us to?” The next questions concern its argument roles, conditions
of application and expected consequences. A source file can contain both logical axioms and documentation or
presentation assertions. Documentation explains an intended reading, while logical constraints must be located in
active formulas; commented-out historical text does not add an axiom to the selected theory.
1.4 Modeling commitments and source interpretation
SUMO distinguishes membership from specialization. An instance assertion places an entity in a class, whereas
subclass relates classes through inclusion of their instances; multiple classification is permitted. Relations
themselves have classifications and signatures. domain constrains an argument to instances of a class, while
domainSubclass constrains it to subclasses. Function result restrictions likewise distinguish range from
rangeSubclass. Disjointness constrains shared membership and can therefore interact with inherited relation
classifications. These distinctions affect admissible substitutions and generated typing conditions, not merely the
arrangement of labels in a hierarchy ( OntologyPortal, n.d.c; Pease, 2009).
The upstream formalization guidance combines taxonomic placement, documentation, lexical presentation, and
axioms describing the relevant properties of a concept ( OntologyPortal, n.d.a). A proposed research term therefore
needs more than a plausible name or a nearby superclass. Its intended referents, argument roles, constraints, and
inferential consequences require explicit justification. Rikishi’s graph is a declared projection for navigation: binary
assertions do not stand in for the complete quantified theory. A predicate occurrence within a negation, conditional,
or contextual formula cannot be interpreted as an unconditional edge merely because the same symbols appear.
The modeling guidance is explicit: “Add axioms that describe the relevant properties of the concept” ( Ontology-
Portal, n.d.a). A superclass and an English description support discovery; the property axioms determine which
consequences an intended interpretation must admit. SUMO’s use of classes and relations as arguments makes
those commitments visible in the source itself.
Axiom 1 (Source membership propagation). Write 𝐼(𝑥, 𝐶) for instance and 𝑆(𝐶, 𝐷) for subclass. The
pinned source includes the following rule, expressed here with explicit quantifiers:
∀𝐶, 𝐷, 𝑥 (𝑆(𝐶, 𝐷) ∧ 𝐼(𝑥, 𝐶)) ⇒ 𝐼(𝑥, 𝐷). (1)
This is a rendering of a source axiom, not a new theorem establishing the semantics of the whole ontology. Multiple
membership and specialization remain different relations ( OntologyPortal, n.d.c).
The signature theory contains further axioms. For example, the source requires comparable class restrictions
when domain assigns different classes to the same relation position. Its range and rangeSubclass rules conclude
membership and subclass inclusion respectively. Replacing either with an undifferentiated “type” arrow would
erase a consequence that matters to an actual query ( OntologyPortal, n.d.c). Axiom 1 therefore illustrates one
inferential commitment rather than licensing a generic graph interpretation of all typing.
A symbol inventory must also be distinguished from a population of individuals. The index counts eligible tokens
in formulas; it does not decide that every token is an ordinary object, a class, or a relation in one mutually exclusive
syntactic category. In the pinned source, ProbabilityFn is an instance of UnaryFunction, and UnaryFunction is
a subclass of Function. Membership propagation classifies the function entity; it does not turn ProbabilityFn
into a subclass. Similarly, the lowercase agent relation and the AutonomousAgent class play different argument
roles despite their related English names ( OntologyPortal, n.d.c).
8

## Page 10

This use of class and relation entities inside other assertions is metamodeling. A relation can have a classification,
argument restrictions, and instances of its use, with different formulas governing each aspect. A source-level constant
used to talk about a relation must not silently become an unrestricted predicate variable in the target logic. The
declared laboratory below keeps object symbols and fixed predicate symbols in separate target namespaces and
records any finite predicate specialization explicitly. Its representational choice is a bounded encoding decision, not
a theorem that all source metamodeling is preserved.
1.5 Read a source expression from the outside in
SUO-KIF uses parenthesized prefix notation: the first item identifies an operator, predicate or function and the
following items are its arguments. The outer operator determines the role of everything inside it. A predicate
application forms a formula, which serves as a closed sentence once variable scope is fixed; a function application
forms a term used inside a formula. Parentheses therefore mark logical structure, rather than simply grouping
words in a taxonomy ( Pease, 2009).
Source feature Reading task Consequence for an operator
An instance or subclass assertion Determine whether the assertion
concerns membership or inclusion
between classes.
Preserve the relation label and
argument order.
A domain or domainSubclass
assertion
Determine whether an argument is
constrained by membership in a
class or by subclass inclusion.
Keep the argument position and the
kind of restriction.
A function term Identify the denoted value and the
applicable result restrictions.
Naming a function does not execute
a numerical algorithm.
An implication or biconditional Read the entire antecedent and
consequent, including their scope.
A nested occurrence does not
become an unconditional fact.
forall and exists Locate each variable’s binding and
the order of quantifiers.
A witness that may depend on each
object differs from one common
witness.
A formula used as an argument Identify its temporal, epistemic or
other context.
An embedded sentence cannot be
detached and asserted without
justification.
Ordinary variables are written with a question mark; row variables denote argument sequences. A variable in
predicate position calls for an interpretation of relations, rather than merely replacing an object name. These
features account for much of the distance between readable source and fixed-arity first-order prover input. The
source manual also distinguishes the outer interpretation of free assertion variables from that of free query variables;
explicit quantifiers make a worked example’s intended scope portable between those uses ( Pease, 2009).
An argument signature has two connected roles. It expresses an intended logical restriction, and tools may use that
restriction for checking, preprocessing or adding type guards. The operational policy must be identified separately.
For example, the agent signature discussed below puts the process in one argument position and the participant
in another. A term search can display that restriction. A type checker can inspect an application against it. A
translated query can include generated guards. None of these operations is specified merely by drawing an arrow
between the two argument names ( OntologyPortal, n.d.c; Pease, 2023).
1.6 SUO-KIF and reasoning translations
SUO-KIF provides authoring constructs that require care when mapped to an automated prover’s language. Its
manual discusses predicate-position variables, row variables, variable arity, and embedded formulas, including the
difference between higher-order interpretation and quotation as data. Bounded macro expansion is an implementa-
tion choice with a different reach from unbounded sequence-variable interpretation ( Pease, 2009). Benzmüller and
9

## Page 11

Pease examine temporal, epistemic, and doxastic contexts and show why a classical treatment of embedded proposi-
tions can produce unintended consequences. Their proposed modal embedding makes the contextual interpretation
explicit ( Benzmüller and Pease , 2012).
First-order translation is thus a substantive dependency. Pease describes predicate-variable instantiation, row-
variable expansion, variable-arity specialization, and inferred type restrictions in the path to prover input. The
typed first-order extension gives numerical expressions access to built-in arithmetic, but disjoint target sorts do
not directly reproduce SUMO’s multiple inheritance; much of the ontology’s type structure remains axiomatic.
The paper explicitly identifies loss of strictly higher-order content in first-order translations ( Pease, 2023). Brown,
Pease, and Urban instead interpret the SUMO-K fragment in higher-order set theory, handling sequence arguments,
relation quantification, class formation, and selected arithmetic. Their interactive proofs and derived automated
theorem proving (ATP) problems concern that interpretation. The fragment excludes temporal, modal, and proba-
bilistic operations, so it does not establish a universal translation of SUMO ( Brown et al., 2023). Rikishi accordingly
retains source formulas and submitted problem bytes as separate evidence objects.
Scope also depends on the use of a sentence. The manual gives free variables in assertions an outer universal
interpretation, while free query variables receive an existential interpretation. Its practical advice is: “To be
certain of the usage in all contexts, use explicit quantifiers” ( Pease, 2009, p. 11). Quantifier order distinguishes a
witness that may vary with each object from a single witness shared by all objects. Predicate-position variables
and argument sequences require their own interpretation. The actual subrelation rule applies the same argument
sequence to both relations and retains predicate guards; partition is explicitly classified as a variable-arity relation.
Neither construction is an unrestricted binary edge ( OntologyPortal, n.d.c).
The translation paper states that “all the strictly higher-order content in SUMO is lost in translation to first-order”
(Pease, 2023, sec. 1). The alternative SUMO-K treatment states its boundary equally clearly: “Elements of SUMO
not included in SUMO-K are temporal, modal and probabilistic operations” ( Brown et al. , 2023, sec. 2). These are
limits on different constructions, rather than contradictory assessments of a single interchangeable target theory.
A proof in a selected target must identify that target and its translation policy.
The alternatives address different research problems:
Approach
Construction and mathematical
target Consequence for comparison
Sigma’s first-order translations Predicate specialization, row
expansion and inferred guards
prepare first-order prover input;
typed translation additionally
interprets numerical expressions in
target arithmetic ( Pease, 2023).
A result depends on that
preprocessing and target theory.
SUMO-K A defined fragment receives a
higher-order set-theoretic
interpretation, with interactive
proofs and extracted automated
problems ( Brown et al. , 2023).
Its semantic account concerns that
fragment; probabilistic operations
are excluded.
Adimen-SUMO Reengineering translates and revises
studied upper and middle levels for
first-order reasoning ( Álvez et al. ,
2012).
Its repaired axiom set is a distinct
ontology variant.
Rikishi’s selected kernels Complete pinned formulas and
separately identified local
assumptions are compiled into the
declared function-free fragment in
sec. 3.4.2.
Controlled consequences concern
the submitted kernel; vocabulary,
arithmetic, and proof transport
require additional interpretations.
This comparison explains the design choice to retain both source and target problems. Reusing a prover does not
10

## Page 12

make these constructions interchangeable; changing the axiom set or interpretation changes the question being
answered.
1.7 Incomplete descriptions and logical consequence
A theory describes the interpretations it permits. A statement follows from that theory when every permitted
interpretation satisfies it. If a source inventory contains no matching assertion, an asserted-edge query can report
that absence; it has not thereby established the statement’s negation. The same distinction applies when a bounded
prover finds no proof. The statement may require other axioms, a different search, or an interpretation in which
it is independent of the selected commitments. Explicit negation and operational failure have different meanings
(Pease, 2009).
For classical reasoning, adding axioms retains existing consequences but can reduce the permitted interpretations,
potentially to none. Consistency controls therefore matter when an extension or a translated background is loaded.
If a background is inconsistent, classical entailment alone cannot supply the intended contrast between a positive
and a negative competency question. Rikishi tests backgrounds and selected premise removals separately and
retains an inconclusive query outcome when its native search times out.
The symbol inventory also supplies no automatic argument that all possible entities have been named, or that
different names denote different entities. Any domain-closure or distinctness assumptions belong in the identified
axioms or target-language policy. The laboratory’s explicit function-free fragment, object and predicate namespaces,
and absence of an implicit unique-names rule make that choice inspectable. This is why an ontology search result,
a finite countermodel and an empirical observation cannot share an undifferentiated “true/false” label.
1.8 Sigma engineering and lexical mappings
Sigma integrates ontology browsing, natural-language paraphrase, lexical resources, static checks, translation, and
theorem-prover interaction. The Sigma Knowledge Engineering Environment (KEE) system description explains the
engineering value of retaining and indexing a relatively stable background theory across queries, and of linking proof
steps back to premises. It also documents the practical evolution of prover integration ( Pease and Schulz , 2014).
Such architecture motivates recording the translator, generated caches, selected constituents, prover invocation,
and result together. A historical system description cannot certify that a particular installed pair of tools accepts
the same command grammar or produces the intended semantics.
WordNet provides a lexical route into SUMO. The original mapping work distinguishes equivalence of meaning,
subsumption, and instantiation. Its =, +, and @ markers record different alignments between a synset and an
ontology concept ( Niles and Pease , 2003). The distributed headers additionally document complementary mapping
relations, and the README explains that mappings may target MILO and domain terms as well as the upper
ontology (OntologyPortal, n.d.d). These are sense-specific mapping assertions. They do not identify every spelling
or synonym with an ontology entity, and a subsumption mapping does not assert synonymy. Lexical alignment can
guide term discovery and test generation while still requiring examination of the chosen sense, mapping relation,
and formal axioms.
1.9 Competency questions, reengineering, and benchmarks
Adimen-SUMO provides an instructive comparison because it is an ATP-oriented reengineering of studied SUMO
upper and middle levels. Its developers translate, debug, repair, and augment axiomatization to obtain a usable
first-order theory. The resulting ontology must be identified as a derived artifact. Its treatment of second-order
constructions through finite reflection does not establish unrestricted second-order equivalence, and the original
paper leaves a proof of consistency outside its scope ( Álvez et al., 2012). Rikishi operates the pinned OntologyPortal
distribution and Sigma path; it does not silently substitute Adimen-SUMO or inherit its validation results.
Competency-question testing turns intended capabilities into explicit conjectures and expected outcomes. Work
on Adimen-SUMO combines manually designed questions with tests generated from lexical mappings and semantic
patterns, then uses ATP feedback to improve the ontology. A crucial distinction is between a demonstrated
consequence and an unknown result after bounded search ( Álvez et al. , 2015). The associated ATP benchmark
11

## Page 13

also includes negated questions: solving an expected falsity-test may reveal an unwanted consequence rather than
successful ontology behavior ( Álvez et al. , 2017). White-box testing adds tests derived from axiom structure
to expose redundancies and other defects. Its correction iterations support specific improvements, not complete
correctness or satisfiability certification ( Álvez et al. , 2019). Benchmark conclusions therefore require the ontology
variant, test construction, expected polarity, prover configuration, and resource limits. Published benchmark
performance is not evidence that Rikishi has executed the same campaign.
1.10 Active Inference alignment as direct precedent
Douglass and collaborators’ Aligning Active Inference Ontology to SUMO explicitly proposes aligning Active Infer-
ence topics with SUMO ( Douglass et al. , 2024). The preprint and accompanying spreadsheet provide scaffolding for
later rigorous mapping. They distinguish conceptual topics from linguistic terms, discuss broad and narrow senses,
and organize candidate SUMO locations, more general categories, argument domains, and proposed relationships.
An asterisk marks terms proposed for addition rather than existing SUMO identifiers. Rikishi therefore builds on
an established alignment agenda; its contribution is a reproducible environment for investigating proposals and
recording the scope of their evidence.
The alignment tables expose questions that an operator must preserve. The Agent entry discusses the lower-
case SUMO agent relation and its argument types. That case role relates a process to an autonomous agent;
matching the English word does not make the relation a class of inference systems. The Generative Model entry
proposes placement beneath Process, whereas Rikishi’s illustrative SUO-KIF represents its finite model beneath
Proposition. These are different modeling choices requiring an account of the represented object, its description,
and the process that uses it. SUMO places Process under Physical and Proposition under Abstract, making
the distinction a formal category commitment ( OntologyPortal, n.d.c). Neither placement is validated here. The
preprint itself questions a proposed placement of abstract inference beneath learning because of the temporal dis-
tinction ( Douglass et al. , 2024). Its tables should therefore be read as reviewable proposals, not imported as an
already validated axiom set.
SUMO’s own signatures constrain the next step. In the pinned source, agent has process and autonomous-agent
argument domains, while ProbabilityFn is a unary function on formulas with a real-valued range ( OntologyPortal,
n.d.c). The latter does not by itself supply the finite carrier, probability mass vector, or normalization used in
sec. 4. A semantic alignment must specify how such mathematical objects are represented and which axioms
connect them. Source lookup, lexical resemblance, successful parsing, and proof of a separate numerical identity
each answer different questions.
2 Operator architecture and evidence
2.1 Provenance and thin orchestration
Rikishi operates the OntologyPortal distribution rather than a replacement demonstration ontology. Its name refers
to a sumo wrestler and distinguishes the operator from SUMO itself. Importable methods own indexing, numerical
calculation, native reasoning, and rendering. The command-line interface (CLI), dashboard, and Model Context
Protocol (MCP) entrypoints adapt those methods to their transports.
A source lock identifies upstream Git objects and the runtime. The index retains formulas, files, and line locations
alongside a narrower directed navigation projection. A source audit compares current SUO-KIF bytes with the
indexed manifest. Term lookup and interactive graphs preserve the distinction between asserted relations and the
quantified theory described in sec. 1. Predicate selection, truncation, assertion multiplicity, and distinct triples are
explicit observations.
Native execution preserves submitted Thousands of Problems for Theorem Provers (TPTP) problems, transitive
includes, executable identity, command grammar, stdout, stderr, and hashes. Proof-bearing results require trusted
invocation expectations. Unsupported syntax, ambiguous paths, extra problem inputs, stale captures, and mis-
matched receipts reject. Frozen replay uses retained inputs after originals change or move. These controls establish
custody of an invocation, not translation correctness.
12

## Page 14

Definition 1 (Restricted asserted-edge projection). Let 𝒯 be the parsed top-level source expressions and 𝑁
the indexer’s eligible symbol tokens, excluding numbers, variables and reserved logical syntax. The distinct edge
set is
𝐸(𝒯) = {(𝑎, 𝑟, 𝑏) ∣ (𝑟 𝑎 𝑏) ∈ 𝒯, 𝑟, 𝑎, 𝑏 are atomic , 𝑎, 𝑏 ∈ 𝑁 }. (2)
The stored assertion population retains repetitions; this set removes identical triples. Nested expressions are not
recursively asserted as edges. A relation filter restricts this population before the requested output limit is applied.
Definition 1 describes Rikishi’s index, not a model theory for SUMO. A ternary domain assertion, a partition
with several arguments, and a modal formula can all matter to the ontology while falling outside this projection.
Conversely, a recorded edge is a syntactic observation; its presence does not independently prove an intended
semantic interpretation.
2.2 Quantification and interfaces
The dashboard and MCP tools expose source inspection, bounded graphs, finite calculations, and operator methods.
Quantities describe a selected population and indexing policy; they do not estimate truth, independent facts,
completeness, or empirical validity. The cover abstract therefore separates SUMO source, operator evidence, and
the finite probabilistic example.
A failed parser, translator, or prover remains a failed observation. The standardized result ontology named for
Sutcliffe, Zimmer and Schulz (SZS) separates semantic outcomes from unsuccessful search ( TPTP, n.d.). Exhausted
search does not prove non-entailment, and contradictory premises cannot validate their intended model.
3 Corpus and native reasoning observations
3.1 Source-derived measurements
The indexed source revision is efcd059f8feebfe3488a09f575f88d4d009b1e5c. Its checked export reports:
Structural observation Exported value
Indexed Knowledge Interchange Format (KIF) files 144
Parsed top-level formulas 212845
Distinct indexed symbols 34885
Asserted binary edges, including multiplicity 71701
Parse errors 0
These values are injected from the corpus export. Nested files belong to the index population, whereas a configured
Sigma profile selects its own constituents. An all-domain load is another theory and another experiment.
The distribution in fig. 1 is heterogeneous. Geographical and language-related files contribute many formulas;
revision and selection policy change the population. Redundancy and development proposals can contribute to
counts, which do not measure independent meanings.
File concentration uses each file’s share of parsed formulas. The Herfindahl sum of squared shares summarizes
the population, not ontology quality. The graph denominator in fig. 2 includes every indexed symbol, including
zero-degree terms. The analytics export defines denominators and distinguishes assertion multiplicity from distinct
triples.
3.2 Direct taxonomy structure and source navigation
SUMO’s class hierarchy and relation hierarchy are different source graphs. For each selected relation 𝑟, an indexed
top-level atomic statement (𝑟 𝑠 𝑡) supplies the directed pair (𝑠, 𝑡), oriented from child to parent. The projection
13

## Page 15

Figure 1: Largest indexed Suggested Upper Merged Ontology (SUMO) files, with exact formula counts and full-
population shares. Source structure does not measure logical importance or proof coverage.
14

## Page 16

Figure 2: Suggested Upper Merged Ontology (SUMO) formula-head composition with an exact remainder, and
direct-edge degree distribution including zero-degree symbols. Deduplication concerns identical predicate-subject-
target triples; graph absence is absence from this restricted projection.
15

## Page 17

deduplicates those pairs. Its node population consists of their endpoints. Variables and assertions nested inside
implications or quantifiers remain in their complete source formulas rather than becoming unconditional graph
edges. The same read-only methods power the corpus dashboard, command-line inspection and MCP tools.
Let 𝐸𝑟 denote the selected directed pairs and 𝑉𝑟 their endpoints. The structural summaries use
ℛ𝑟 = {𝑣 ∈ 𝑉 𝑟 ∶ deg+𝑟 (𝑣) = 0},
ℳ𝑟 = {𝑣 ∈ 𝑉 𝑟 ∶ deg+𝑟 (𝑣) > 1},
𝒞𝑟 = {𝑆 ∈ SCC(𝑉𝑟, 𝐸𝑟) ∶ |𝑆| > 1 ∨ ∃𝑣 ∈ 𝑆 (𝑣, 𝑣) ∈ 𝐸 𝑟}.
(3)
Here out-degree counts distinct direct parents. Roots, multiple inheritance and strongly connected components in
eq. 3 describe this restricted source graph. A directed cycle is an inspection target; its presence does not establish
inconsistency, and its absence does not establish consistency. SUMO constraints and quantified axioms extend
beyond this projection ( OntologyPortal, n.d.c; Pease, 2023).
The following values are recomputed from the complete retained Merge.kif bytes, using the same index and
taxonomy analysis methods as the dashboard. They are file-specific populations and therefore differ from whole-
corpus totals.
Relation Assertions Distinct edges Endpoint nodes Roots Multiple parents
subclass 840 840 711 1 110
subrelation 100 100 124 29 4
The white corpus workbench separates complete population totals from filtered and paginated rows. Selecting a file
or formula head opens complete SUO-KIF formulas with original file, line and source Secure Hash Algorithm 256-bit
(SHA-256) fingerprint. A breadth-first traversal returns a deterministic shortest child-to-parent path and the source
formula for every step. Reaching a depth or visit budget is reported separately from exhausting reachable nodes.
These source paths support inspection, while ATP entailment remains a separate operation. The exact-input report
accompanying fig. 3 retains assertion multiplicity separately from distinct graph edges.
3.3 Worked inspection of the pinned SUMO theory
The demonstration method audits the current index against source bytes, freezes the complete Merge.kif, and
selects formulas structurally through the existing parser. The retained source path is .rikishi/upstream/sumo/M
erge.kif at revision efcd059f8feebfe3488a09f575f88d4d009b1e5c. Its computed SHA-256 is 2e4c3d6b8392a4
cb6fbeccb6eb7441e11d6b45592082333285c951fd7c7d3e14. The file contains 5520 parsed top-level formulas and
2275 binary edge assertions under Definition 1. The worked cases cite 12 distinct source formulas; reused formulas
count once. These are file-specific populations rather than the full-corpus totals above.
The following blocks are injected from the checked source, preserving their logical context. SUMO excerpts acknowl-
edge the Institute of Electrical and Electronics Engineers, Inc. (IEEE), copyright 2004, as source and copyright
owner, under the distribution’s copying and attribution terms ( OntologyPortal, n.d.c). Formula locations, excerpt
hashes and the full source bytes are retained in the demonstration report. Changing an excerpt, its line range or a
derived observation causes portable replay to reject it.
3.3.1 Categories and relation signatures
fig. 4 provides a map for the worked source blocks below.
The selected taxonomic commitments are:
(partition Entity Physical Abstract)
(subclass Physical Entity)
(subclass Abstract Entity)
16

## Page 18

Figure 3: Suggested Upper Merged Ontology (SUMO) subclass and subrelation graph populations in complete
retained Merge.kif, with endpoint counts and structural diagnostics. Source provenance uses the Secure Hash
Algorithm 256-bit (SHA-256) fingerprint. The figure and table are replayed from source; cycle counts carry no
logical-consistency conclusion.
17

## Page 19

Figure 4: Suggested Upper Merged Ontology (SUMO) source commitments: subclass structure, relation and
function signatures, and a complete modal example. Arrow and role labels distinguish specialization, membership
and argument constraints. Secure Hash Algorithm 256-bit (SHA-256) provenance binds the frozen source. The
diagram is not a full inference or translation result.
18

## Page 20

(subclass Process Physical)
(subclass Proposition Abstract)
This is more specific than a general-purpose label hierarchy. Process belongs on the physical branch; Proposition
belongs on the abstract branch. Under the partition’s decomposition axioms, the branches exclude a common
instance. For 𝑃 = Physical and 𝐴 = Abstract, the relevant condition is
¬∃𝑥 (𝐼(𝑥, 𝑃 ) ∧ 𝐼(𝑥, 𝐴)). (4)
This is an explanatory consequence of the stated partition semantics, not an ATP result produced by the source-
inspection method. A class placed below incompatible categories may be forced to be empty; a contradiction
additionally needs a commitment supplying a common instance. Likewise, a model’s mathematical content, the
file that describes it and the process that executes it require distinct referents. The competing generative-model
placements in sec. 1.10 cannot be reconciled by matching their English names.
The membership/specialization distinction is directly inspectable:
(subclass Process Physical)
(instance agent CaseRole)
(instance ProbabilityFn UnaryFunction)
agent here is an instance of a relation class, whereas Process is a subclass of a category. Its argument order is
also a substantive commitment:
(domain agent 1 Process)
(domain agent 2 AutonomousAgent)
The first role is a process and the second an autonomous agent. A posterior vector or an abstract model description
does not supply those referents merely because an implementation is called an agent. A proposed extension must
say what performs the process, what that process is, and how the source role applies. These source signatures are
not a claim that every installed translator enforces their intended consequences in the same way.
3.3.2 Probability and modal context
The probability vocabulary has its own representational commitments:
(instance ProbabilityFn UnaryFunction)
(domain ProbabilityFn 1 Formula)
(range ProbabilityFn RealNumber)
Formula is a source class beneath Sentence. Its instances must not silently be identified with Proposition, a
Python list or a probability tensor. ProbabilityFn’s unary signature and real-valued range do not exhaust its
probabilistic axiomatization or automatically supply the finite model below.
Remark 1 (An interpretation obligation). For a proposed finite interpretation, let 𝑒 ∶ 𝑆 → ℱ represent latent
alternatives by event formulas. An intended correspondence would require
𝑝(𝑠) = ProbabilityFn(𝑒(𝑠)), 𝑝(𝑠) ≥ 0, ∑
𝑠∈𝑆
𝑝(𝑠) = 1. (5)
This stipulates obligations for a proposed representation. It derives neither normalization nor event exclusiv-
ity/exhaustiveness from the unary signature. Formula identity, conditioning, support and the target arithmetic
still need definitions and preservation arguments.
Conditioning illustrates why argument roles must be read from source. The complete signature assertions at
Merge.kif:3348–3352 are:
19

## Page 21

(instance conditionalProbability ProbabilityRelation)
(instance conditionalProbability TernaryPredicate)
(domain conditionalProbability 1 Formula)
(domain conditionalProbability 2 Formula)
(domain conditionalProbability 3 RealNumber)
The accompanying documentation at lines 3354–3362 interprets (conditionalProbability A B r) as the proba-
bility of B given A being r. An event encoding of ℓ(𝑠) = 𝑝(𝑜 ∣ 𝑠) must therefore put the state condition first and the
observation second. This is a proposed interpretation of two formulas, not an equality between the source predicate
and a Python array ( OntologyPortal, n.d.b, lines 3348–3362).
Arithmetic also needs an explicit interpretation. Two complete signature selections from Merge.kif:5880–5885
and 6139–6142 are:
(instance DivisionFn BinaryFunction)
(instance DivisionFn PartialValuedRelation)
(domain DivisionFn 1 RealNumber)
(domain DivisionFn 2 RealNumber)
(range DivisionFn RealNumber)
(instance LogFn BinaryFunction)
(domain LogFn 1 RealNumber)
(domain LogFn 2 PositiveInteger)
(range LogFn RealNumber)
The division documentation explicitly leaves a zero denominator undefined (lines 5887–5894). The logarithm
documentation assigns its second argument the base (lines 6144–6148). Thus this binary, integer-base signature
cannot simply be substituted for Lean’s unary natural logarithm in a quantity measured in nats. The declared
first-order laboratory has an even narrower boundary: its numeral symbols are uninterpreted constants. Neither
those constants nor a function’s name execute real arithmetic. The finite numerical and Lean layers below supply
their own stated arithmetic semantics ( OntologyPortal, n.d.b, lines 5880–5894, 6139–6148; Pease, 2023; Active
Inference Institute , n.d.a).
A complete contextual formula supplies a contrasting source example:
(=>
(instance ?AGENT AutonomousAgent)
(modalAttribute
(exists (?PROC)
(and
(instance ?PROC Process)
(agent ?PROC ?AGENT)))
Possibility))
The existential statement appears inside modalAttribute and is conditioned on the antecedent. It is not an
assertion of an observed process-agent event. The structural demonstration preserves the full formula and records
that it is not a ground binary edge. No modal theorem is inferred by stripping away those operators ( OntologyPortal,
n.d.c; Benzmüller and Pease , 2012).
3.3.3 Thin orchestration and separate proof controls
From the repository root, the orchestration script can retain a fresh report and optionally run the existing restricted
taxonomy method:
uv run python scripts/demonstrate_sumo.py \
--output output/demonstrations/source-report.json \
--proof-directory output/demonstrations/taxonomy
20

## Page 22

The destinations must be fresh. The script selects paths and delegates to importable methods; it does not implement
another parser, ontology engine or prover. The default report makes no ATP invocation. Its portable verifier
hashes and reparses the frozen bytes, rederives the selections and observations, and checks exact agreement. That
establishes internal agreement of the retained snapshot. The acquisition/source-audit record supplies the binding
to the Git revision; a self-contained digest alone cannot authenticate a claimed revision.
The optional operation separately submits the selected hierarchy’s direct subclass assertions plus transitivity. It
checks Process beneath Entity and contrasts Process beneath Abstract, retaining exact problems and native
outcomes. A countermodel to the latter applies to that restricted projection, which omits the partition’s full
axiomatization; it is not a countermodel of the complete SUMO theory. This separation keeps the successful source
inspection, restricted proof and native Sigma diagnostic in sec. 3.5 from acquiring each other’s claims.
3.4 Source-bound inference laboratory
3.4.1 Questions, theories, and interpretations
The inference laboratory turns selected pinned source formulas into explicit first-order logic (FOL) problems. It
complements the source demonstrations by asking which consequences actually follow under a declared encoding,
then testing the dependencies that make those consequences possible. It is separate from the finite alignment study
in sec. 5.4 and from Sigma’s configured full-profile translation. A theorem in one of these settings does not silently
transfer to another.
Let 𝑇 denote the submitted premises and 𝑞 the conjecture. Satisfiability of 𝑇 means that some interpretation
satisfies every premise. Entailment, 𝑇 ⊧ 𝑞 , means that every model of 𝑇 satisfies 𝑞. Classical refutation tests the
latter through the unsatisfiability of 𝑇 ∪ {¬𝑞} . The prover’s problem therefore needs both the selected background
and the exact conjecture; an isolated query string is insufficient to identify the inference experiment.
Non-entailment is also a positive logical finding when a countermodel is supplied. A model satisfying 𝑇 ∪ {¬𝑞}
establishes 𝑇 ⊭ 𝑞 . It does not establish 𝑇 ⊧ ¬𝑞 : another model may satisfy both 𝑇 and 𝑞. This distinction supports
an open-world reading of incompletely specified knowledge. An absent source assertion or graph path does not
automatically become a negative fact. A bounded search that produces no proof establishes neither a countermodel
nor entailment of the negation.
Background satisfiability must be considered independently. If 𝑇 is inconsistent, it has no models and classically
entails every conjecture. The implication “all models of 𝑇 satisfy 𝑞” then holds vacuously. Consequently, a successful
refutation can be diagnostically correct while providing no useful validation of the intended ontology model. The
laboratory submits a conjecture-free background control alongside each positive obligation. This does not certify
consistency of the full source distribution; it tests the premises actually used in that case.
3.4.2 Declared source selection and supported fragment
The packaged study identifies the complete pinned Merge.kif file, its revision and content fingerprint, selected
formula start lines, explicit local assumptions, queries, and one registered removal choice per scenario. Source
extraction requires the expected full-file identity before recovering complete formulas. Reused source formulas
remain source claims; generated problems and teaching assumptions remain separate objects.
The target fragment is function-free and first-order. It admits fixed-arity predicates, object constants, individual
variables, explicit quantifiers, Boolean connectives, implication, biconditional, and equality. Free assertion vari-
ables are universally closed. Where a selected source schema uses a predicate variable, the study records a finite
substitution to a fixed predicate before compilation. This is one declared schema instance, not unrestricted quantifi-
cation over relations. Function applications, unrestricted row-variable expansion, modal interpretation, and general
higher-order translation are outside this laboratory. Numerals are uninterpreted object constants. No arithmetic,
unique-names rule, or closed-world completion is added implicitly.
These choices matter to interpreting the worked problems. A synthetic witness such as StudyHuman names an
assumed teaching entity, not an entity discovered in the source. Its membership assumption must appear in the
retained background. A countermodel after that assumption is removed demonstrates underdetermination in the
21

## Page 23

reduced kernel; it does not assert that humans are absent from the intended source interpretation. Likewise, a class
constant and a predicate used to express a relation occupy distinct syntactic roles in the target language.
3.4.3 W orked consequence families
The taxonomy scenarios use actual source class links with selected source rules. For example, the human-taxonomy
case asks for the declared Human-to-Animal consequence, while its negative query reverses the direction. A corre-
sponding membership scenario assumes a teaching witness is a Human and asks whether it inherits Animal mem-
bership. These are different obligations: a class inclusion statement and an instance classification. Removing
the registered class link or witness assumption tests the appropriate dependency, rather than merely changing an
expected output label.
Mereological scenarios exercise properPart, part, and piece rules. The forward proper-part consequence, the
exclusion of reverse parthood, and the converse condition are separate source obligations. Family-relation scenarios
exercise the source argument order: mother and father relate a child to a parent, so copying an English subject–
object intuition can reverse the query. Separate attribute consequences concern the relevant parent argument.
These examples show why a generic unlabeled edge cannot stand in for the full formula.
Existential scenarios test whether selected source rules require some witness without requiring a particular named
object. The containment case asks for a hole and appropriate filling relation; the organism case asks for a parent;
the physical-object case asks for location and time witnesses. The negative queries can ask for a specific otherwise
unconstrained name. Existence of some witness does not identify that witness with an arbitrary constant. The
generated target must retain this quantifier distinction.
Domain-inheritance scenarios derive selected argument metadata for daughter and son from their source subrela-
tion and parent-domain premises. A separate classification scenario concerns the subclass relation entity itself.
Specialized relation-schema cases exercise declared transitivity instances. Disjointness cases derive explicit negative
membership consequences when the required disjointness rule, source classification, and witness assumption are
present. Those are proofs of a negation under stated premises, unlike a mere failure to prove positive membership
(OntologyPortal, n.d.c).
3.4.4 Adversarial controls and native evidence
Each scenario generates related problems with different roles. The background control contains premises without a
conjecture. The positive problem retains the declared conjecture. The negative-query problem asks a deliberately
unsupported consequence, which need not be the logical negation of the positive query. The premise-removal variant
omits the registered source selection or local assumption. Finally, the explicit refutation control adds the negated
positive query as an axiom, creating a conjecture-free satisfiability obligation. These roles prevent conflating an
inconsistent background with the intended refutation of a conjecture’s negation.
Expected outcomes are part of the study design; observed outcomes come only from native execution and valid
capture. A desired Theorem cannot stand in for a timeout, missing executable, failed process, or invalid receipt. A
removal countermodel demonstrates necessity relative to that selected comparison. It does not establish uniqueness
of a proof, global premise minimality, or complete independence of all source axioms. The result vocabulary follows
the standardized SZS result ontology ( TPTP, n.d.).
The runner submits generated problem bytes to E, Vampire, or both, retaining per-case problem and capture
identities. Comparison first requires the same source selection and problem bytes. A theorem from one prover and
a timeout from the other records a search difference, not contradictory model-theoretic answers. A theorem and a
countermodel claim for identical inputs require investigation of the native commands, status parsing, tool identities,
and proof or model evidence. Agreement supplies bounded implementation corroboration; it proves neither general
prover correctness nor preservation of the ontology’s intended semantics.
The retained laboratory report supplies 49 scenarios and 490 native case executions. The following summary is
derived from that report, including its control categories and observed outcomes:
22

## Page 24

Source category Scenarios E matched Vampire matched
class disjointness 4 20 20
domain and relation types 5 25 25
existential consequences 5 25 25
family relations 5 25 25
identity constraints 1 5 5
instance inheritance 6 30 30
mereology 6 30 30
source individual inheritance 3 15 15
spatial relations 3 15 15
specialized relation schemas 3 15 15
subclass chains 8 40 40
3.4.5 Reproduction and evidence transfer
The catalog command exposes design without launching a prover. A native run requires a fresh repository-local
destination and a declared per-case budget:
uv run --locked --no-sync rikishi inference-catalog
uv run --locked --no-sync rikishi inference-run \
output/inference --prover both --timeout 10
Preserve the complete directory rather than copying only the summary. The report binds selected source formulas,
study identity, generated problems, native captures, implementation and tool identities, expected polarities, and
observed statuses. Portable verification requires the separately retained report digest:
uv run --locked --no-sync rikishi inference-verify \
output/inference/inference-report.json \
--sha256 "$REPORT_SHA256"
Here REPORT_SHA256 is the independently retained expected content fingerprint. An outer fingerprint identifies the
bytes selected by its authority; computing a fresh fingerprint from an untrusted bundle does not authenticate its
history. Portable replay rederives the supported problems and validates retained evidence without launching the
native prover. Native repetition is a new execution. Neither operation independently checks every native proof
inference, which remains a separate proof-assurance objective ( Reger, 2017).
The dashboard’s proof laboratory and read-only agent tools expose the same catalog and report-verification methods.
Source inspection, evidence replay, and new proof execution remain distinct operations. A claim transferred to
a research note must therefore retain its theory, conjecture, encoding, controls, native execution, and verification
boundary, rather than carrying only a successful status label.
3.5 Restricted proofs and native diagnostics
The taxonomy-proof operation projects direct subclass assertions from Merge.kif, adds explicit transitivity, and
submits a conjecture to E. Its result concerns that restricted obligation. It neither translates arbitrary SUO-KIF
nor imports every domain axiom. Source assertions, projected problem, command, process status, and output
remain separate artifacts.
The native Sigma path supplies a diagnostic case. Saved negative-control evidence identifies a contradiction in
translated cached premises independently of the conjecture. The retained subset is unsatisfiable, while each single-
premise deletion is satisfiable. This establishes inclusion-minimality for that saved subset, not uniqueness or
minimum cardinality over the complete background.
The localized path combines a source assertion classifying path as total, a generated cache assertion classifying it as
partial, and disjointness conditions. The isolated experiment constructs a fresh knowledge base (KB), ingests source-
only KIF, and calls KBcache.buildCaches() with no prepopulated maps. Both its declared minimal fragment and
23

## Page 25

complete pinned Merge.kif input produce the additional partial classification while retaining the direct total one.
Removing the parent’s partial classification or the subrelation edge removes the generated classification. Adding
a synthetic superclass link to InheritableRelation changes the cache’s positive membership observation while
leaving the generated classification present. These controls concern generated classification, not the intended truth
of an inheritance rule.
The fresh experiment retains its versioned selections, raw Java warnings, commands, observations and pre/post
source, Java archive (JAR) and toolchain bindings under the manuscript’s research artifacts. It reconstructs the
complete Merge file, not the complete multi-file core profile. Intended inheritance semantics, a source-to-target
argument, and acceptance of a corrected full profile remain open. Inconsistency of the original ontology is not
established.
Positive native statuses remain diagnostic in that context. Rikishi’s invocation adapter now selects Sigma’s existing
custom Vampire execution route with a fixed supported option set, preserving upstream preprocessing, translation
and assembled background bytes. Invocation-local profile copies retain the configured source and serialized-cache
inputs with pre/post hashes. The executable, query, profile, adapter and exact submitted TPTP remain bound
to the result. Tiny real Sigma profiles exercise a theorem and a countermodel; a full-core query that exhausts its
budget remains inconclusive. Refutation of an extracted conjecture-free translated subset is a separate observation.
These outcomes do not establish consistency of the configured profile or validity of a SUMO interpretation.
Historical contradiction context is checked separately from the query outcome. After strict capture verification,
Rikishi compares the complete ordered TPTP statement sequence against its registered background under pinned
executable, Sigma-class, lock and profile-configuration identities. Sigma’s regenerated source comments contain
invocation-local profile paths, so identical statements can have different raw file hashes. The existing structural
parser omits only standalone comments and layout; statement text, names, roles, order and any annotations
remain part of the fingerprint. The exact submitted bytes and raw hashes remain in each capture. Missing or
changed statements, changed bindings, or an invalid capture leave context unknown. This recognizes the registered
translated background; it supplies no equivalence procedure for arbitrary theories and does not change the query’s
status or scientific scope.
Readable proof output, premise extraction and independent proof-step checking are distinct engineering goals
(Reger, 2017). Rikishi structurally extracts complete named input premises and requires native same-family replay
of an exported subset; it does not independently check every inference in the prover’s proof calculus. Local
observations remain distinct from the published campaigns in sec. 1.9.
For the translated object 𝑡 and total/partial classes 𝑇 , 𝑈, the retained core has the following schematic form:
disjoint(𝑇 , 𝑈 ), 𝐼(𝑡, 𝑇 ), 𝐼(𝑡, 𝑈 ),
∀𝐶, 𝐷 ( disjoint(𝐶, 𝐷) ⇒ ¬∃𝑥 [𝐼(𝑥, 𝐶) ∧ 𝐼(𝑥, 𝐷)]) . (6)
The saved TPTP premises own the exact replay bytes; this display explains the refutation’s structure. It contains
no conjecture. The source inheritance rule guards propagated relation classifications with InheritableRelation,
while the fresh diagnostic observes generated classifications for explicitly retained inputs. That distinction localizes
a question for engineering review without establishing intended inheritance semantics ( OntologyPortal, n.d.c).
4 A finite variational example
The example implements the negative evidence lower bound (ELBO) identity used in variational inference ( Blei
et al. , 2017, sec. 2.2). Friston, Kilner and Harrison connect a variational objective to perception, learning and
action by relating an encoded density to a system that exchanges with its environment ( Friston et al. , 2006, secs.
3–5). That modeling step supplies the FEP motivation; the identity alone does not identify an executing system
with an organism ( Friston, 2010). The alignment precedent likewise groups several free-energy senses ( Douglass
et al., 2024). Here the modeled object is a finite variational objective, with natural-log units and a fixed observation.
Its Kullback-Leibler (KL) decompositions specify the reference law explicitly.
24

## Page 26

Definition 2 (Finite generative model). Let 𝑆 be a finite latent carrier, 𝑝(𝑠) a normalized prior, and ℓ(𝑠) =
𝑝(𝑜 ∣ 𝑠) the selected observation’s likelihood. Require positive evidence. Define the joint, evidence, and exact
posterior by
𝑝(𝑠, 𝑜) = 𝑝(𝑠)ℓ(𝑠), 𝑍 = 𝑝(𝑜) = ∑
𝑠∈𝑆
𝑝(𝑠)ℓ(𝑠), 𝑝(𝑠 ∣ 𝑜) = 𝑝(𝑠, 𝑜)𝑍 . (7)
The configured example has 2 latent states . Its parameters and derived quantities are injected from the packaged
model and calculation:
Quantity Configured or computed value
Prior 𝑝 (0.500000, 0.500000)
Observation likelihood ℓ (0.800000, 0.200000)
Candidate 𝑞 (0.500000, 0.500000)
Joint mass 𝑝(𝑠, 𝑜) (0.400000, 0.100000)
Evidence 𝑍 0.500000
Exact posterior 𝑝(𝑠 ∣ 𝑜) (0.800000, 0.200000)
Definition 3 (Supported finite variational objective). For normalized 𝑞, require 𝑞(𝑠) > 0 only where 𝑝(𝑠, 𝑜) >
0. Define
𝐹 (𝑞) = ∑
𝑠∈𝑆∶ 𝑞(𝑠)>0
𝑞(𝑠) log 𝑞(𝑠)𝑝(𝑠, 𝑜) . (8)
Proposition 1 (Finite free-energy decomposition). On the domain of Definition 2 , Definition 3 ,
𝐹 (𝑞) = 𝐷 KL(𝑞‖𝑝(⋅ ∣ 𝑜)) − log 𝑝(𝑜). (9)
Substitution of 𝑝(𝑠, 𝑜) = 𝑝(𝑠 ∣ 𝑜)𝑝(𝑜) into eq. 8, with normalization of 𝑞, gives eq. 9. This elementary identity
concerns the stated finite model and support assumptions.
The same objective has a prior-relative decomposition. Write 𝐻(𝑞) = − ∑ 𝑠 𝑞(𝑠) log 𝑞(𝑠), with zero-mass terms
interpreted as zero. Then
𝐹 (𝑞) = −𝐻(𝑞) − 𝔼 𝑞[log 𝑝(𝑠, 𝑜)]
𝐹 (𝑞) = 𝐷 KL(𝑞‖𝑝) − 𝔼 𝑞[log ℓ(𝑠)]
𝐹 (𝑞) = 𝐷 KL(𝑞‖𝑝(⋅ ∣ 𝑜)) − log 𝑍.
(10)
These are decompositions of the same supported finite sum ( Blei et al. , 2017, eqs. 12–14; Friston et al. , 2006,
sec. 5). Logarithmic expectations are restricted to states with positive 𝑞, as in Definition 3. The prior-relative term
measures departure from prior belief; the posterior-relative term is the gap above surprise. Calling both simply “the
KL term” would confuse their references. Nonnegativity gives 𝐹 (𝑞) ≥ − log 𝑍, with equality at the exact posterior.
For an approximate family 𝒬, equality is available only if that posterior belongs to the family. This example can
enumerate its exact posterior, so it exposes the bound without benchmarking an approximate inference algorithm
(Blei et al. , 2017, secs. 2.1–2.2).
Natural logarithms give nats. At the configured candidate, direct evaluation gives 0.916291, surprise 0.693147,
and posterior KL 0.223144. The floating-point decomposition residual is 8.326673e-17. At the exact poste-
rior, the computed objective is 0.693147 and posterior divergence 0.000000. Display values use the publication
configuration; JavaScript Object Notation (JSON) retains the computed floating-point values.
25

## Page 27

Figure 5: Finite inference from one model authority. Model and belief bars distinguish prior, likelihood, posterior
and candidate. The objective panel marks the candidate and analytical posterior at 0.800000; the dashed line is
surprise. The decomposition compares the surprise bound and posterior divergence in nats.
26

## Page 28

The curve in fig. 5 and the cover abstract use the same authority as the parameter table and eq. 7. No plotting
literal fixes the posterior location. Changing valid parameters changes the numerical result, prose, and marker
through the same calculation.
Nonfinite, negative, nonnormalized, mismatched, and unsupported inputs reject. Zero candidate probability con-
tributes zero. Positive candidate mass at zero joint mass would give an infinite extended-real objective; this finite
JSON interface reports a domain error. Real negative controls exercise those failures.
4.1 Logarithmic evaluation and numerical support
The numerical kernel now accepts logarithmic prior and likelihood inputs. For the supported states 𝑇 , write
𝑎𝑠 = log 𝑝(𝑠) and 𝑏𝑠 = log ℓ(𝑠). A shifted normalization can be expressed as
𝑏∗ = max𝑠∈𝑇 𝑏𝑠, 𝑟 𝑠 = 𝑎 𝑠 + (𝑏𝑠 − 𝑏∗), 𝑟 ∗ = max𝑠∈𝑇 𝑟𝑠,
𝐿 = log ∑
𝑠∈𝑇
exp(𝑟𝑠 − 𝑟∗),
log 𝑍 = 𝑏 ∗ + 𝑟∗ + 𝐿, log 𝑝(𝑠 ∣ 𝑜) = 𝑟 𝑠 − 𝑟∗ − 𝐿.
(11)
Shifted weights supply the rounded posterior, while log posterior values retain support when a positive linear
projection underflows. This follows established shifted-normalization practice; finite-precision error still requires
controls (Blanchard et al. , 2019). The objective and posterior KL are evaluated separately from the same supported
log inputs, and their decomposition residual is retained.
In the log interface, an input null denotes exact zero mass. An output null evidence denotes positive evidence below
the linear floating-point range; null log-posterior entries instead denote exact zero support. Rounded positive atoms
are explicitly identified when their linear projections underflow. Impossible evidence and positive candidate mass
on exact zero support reject. The linear facade preserves arithmetic evidence/posterior projections and directs
callers to the log interface when the evidence itself cannot be represented. No epsilon replaces a zero-support event.
The explicit JSON-model command provides a thin entrypoint:
uv run rikishi fep-evaluate \
examples/fep-log-model.json --logarithmic
This numerical extension expands the executable input range while retaining the same finite objective and support
contract.
5 Connections to formalization
5.1 What connects SUMO to FEP_Formal?
FEP_Formal is a formalization project; the Free Energy Principle is the broader scientific and mathematical
research programme that motivates it. This paper uses two pinned finite modules and named instantiations, rather
than treating the repository’s name as evidence that every FEP claim has been formalized. The useful connection
is concrete: a probability law and observation kernel become typed mathematical objects, while selected SUMO
expressions describe their model, representation, calculation and result roles ( Active Inference Institute , n.d.b,n;
OntologyPortal, n.d.b).
Consider the registered uniform-prior witness. In state order (false, true) , its prior is (1/2, 1/2) and the like-
lihood of observation true is (1/4, 3/4). The state labels name the two finite alternatives; they do not assert
the truth values of an arbitrary SUMO sentence. One observation leads to the following connected but distinct
questions:
27

## Page 29

Lane Question about the same witness Specific answer or obligation
Ontology What does the named Lean
expression represent?
The selected representation rules
connect its declared
language-relative role to a
represents consequence; they do
not calculate a posterior.
Mathematics What follows from the finite law
and kernel?
Joint masses (1/8, 3/8) give
evidence 1/2 and posterior
(1/4, 3/4); Lean checks the stated
instances under their hypotheses.
Numerical execution Did the evaluator compute that
case correctly?
Bound inputs, exact/reference
comparisons and residuals check the
returned values, separately from the
Lean proof.
Simulation What observations does the
specified process generate?
Sampling the persistent state and
its kernel produces synthetic
histories to compare with exact
probabilities.
Scientific interpretation Does the model describe a target
system?
Measurement semantics and
suitable observations must be
supplied in an additional study.
The exact arithmetic, complete source rules and controlled queries are developed in sec. 5.5; the temporal assump-
tions are made explicit in sec. 5.8. These connections permit inspection and criticism of a common case. They
supply neither an automatic SUMO-to-Lean translator nor a transfer of correctness from a representation label to
a program.
5.2 Finite elaboration and semantic scope
The inspected fep_formal revision is 9a0694f16b8e89b66b2f7f8cc7426c650dd2c4de (Active Inference Institute ,
n.d.a). Source inspection and compilation are distinct observations. The retained finite elaboration records:
Formalization observation Receipt-derived value
Compiler version 4.35.0
Pinned finite source modules 2
Inspected declaration axiom reports 3
Compiled dependency artifacts fingerprinted 57968
Lean distinguishes elaboration and proof construction from the kernel’s checking of the resulting terms; its extensible
automation does not itself identify the mathematical meaning of an imported domain model ( de Moura and Ullrich ,
2021, secs. 2, 5). Here “formalized” refers to named declarations with explicit types and hypotheses. The execution
claim is narrower still: the receipt identifies which pinned modules were elaborated and which declarations had
their axioms inspected. Compiler, source, dependency revisions, imported artifacts, outputs, and commands are
recorded. Complete compiled-library fingerprints are compared before and after elaboration as a conservative
superset of transitive imports. Admitted proofs and unapproved axioms reject. Existing Mathlib artifacts are
inputs; this is not a fresh dependency build or certification of the complete formalization catalogue.
The pinned FiniteLaw carrier contains a real-valued mass function, a proof of nonnegativity at every atom and a
proof that the finite sum is one. A FiniteKernel supplies a normalized output law for each input. Its posterior
_mul_predictive theorem reconstructs joint mass from posterior and positive evidence. These are mathematical
real-valued objects, whereas the Python evaluator uses finite-precision numbers. The mathematical connection
28

## Page 30

must identify both the carriers and the numerical representation ( Active Inference Institute , n.d.b, lines 28–32,
153–156, 263–281).
For candidate 𝑎 and reference 𝑏 on that finite carrier, the information module defines
𝐻𝐿(𝑎) = ∑
𝑠
negMulLog(𝑎𝑠),
𝐶𝐿(𝑎, 𝑏) = − ∑
𝑠
𝑎𝑠 log 𝑏𝑠,
𝐷𝐿(𝑎, 𝑏) = ∑
𝑠
𝑏𝑠 klFun(𝑎𝑠/𝑏𝑠).
(12)
These are the definitions entropy, crossEntropy and finiteKL, not an informal replacement of the last definition
by a logarithmic ratio ( Active Inference Institute , n.d.a, lines 24–34). The named theorem finiteKL_eq_cro
ssEntropy_sub_entropy assumes 𝑏𝑠 > 0 for every state. Its pointwise helper contributes a correction 𝑏𝑠 − 𝑎𝑠;
normalization cancels the sum of those corrections, yielding 𝐷𝐿(𝑎, 𝑏) = 𝐶 𝐿(𝑎, 𝑏)−𝐻 𝐿(𝑎) (Active Inference Institute,
n.d.a, lines 135–154). On that domain, setting 𝑎 = 𝑞 and 𝑏 = 𝑝(⋅ ∣ 𝑜) connects the pinned KL theorem to the
posterior-relative term in eq. 9.
Zero reference mass reveals why the hypothesis matters. For the disjoint Boolean point masses, the pinned decla-
rations state 𝐶𝐿(𝛿true, 𝛿false) = 0 and 𝐷𝐿(𝛿true, 𝛿false) = 1 , using totalized real operations ( Active Inference Institute ,
n.d.a, lines 56–72). Rikishi rejects the corresponding positive candidate mass on zero joint support. These source-
level witnesses distinguish definitions; they are not new numerical observations in this study. Requiring strictly
positive posterior mass for the shared witnesses below meets the pinned logarithmic theorem’s full-reference-support
condition, which is stronger than the numerical evaluator’s candidate-support condition.
Proposed vocabulary mappings identify probability, functions, real-valued quantities, reasoning, processes, and
agents as candidate SUMO connections. SUMO’s distinctions between instance, subclass, relation signature, and
function range make these obligations substantive sec. 1.4. The author-created FEP ontology extension remains
separate from upstream and from the prior alignment tables in sec. 1.10. It neither enforces normalization nor
transports a Lean proof.
5.3 From proposed alignment to a tested interpretation
A reproducible extension should preserve the original topic and sense, the versioned alignment row, the proposed
mapping relation, and the defining SUMO axioms. A superclass candidate, an individual classification, a subrelation,
and a merely related concept impose different logical commitments. Their direction and argument types must be
checked before generating axioms. Historical table entries must also be rechecked against the selected source
revision.
Formalization maturity is assessed here per claim and per artifact. The following ledger distinguishes the evidence
already produced by the methods from the additional obligation needed to enlarge a conclusion:
Claim and evidence object Warranted conclusion Additional obligation
A pinned, complete source formula
and its locator
Identity and context of the
inspected commitment sec. 3.3.
An interpretation and a submitted
problem to assess a consequence.
A selected kernel, explicit
assumptions and native controls
Observed entailment or
counter-satisfiability for that
submitted problem sec. 3.4.
A preservation argument to transfer
the conclusion to a richer source
semantics.
Supported numerical inputs, an
independent reference and residuals
Agreement of the implemented
finite calculation on the measured
inputs sec. 4.
An error argument or further tests
for a wider numerical domain.
Pinned Lean declarations,
elaboration and inspected axioms
Checking of the named finite
mathematical obligations against
recorded imports sec. 5.2.
An interpretation connecting other
representations to those definitions.
29

## Page 31

Claim and evidence object Warranted conclusion Additional obligation
One witness authority shared across
Lean, numerical and SUMO
artifacts
The matched finite study in sec. 5.5,
with each layer’s obligations
reported separately.
A general translation and proof of
preservation to transport arbitrary
statements.
A proposed biological interpretation A hypothesis motivated by the FEP
literature ( Friston et al. , 2006;
Friston, 2010).
Observations, estimation and model
criticism for the claimed empirical
system.
Competency questions should include intended consequences and unwanted ones, following the testing distinctions
in sec. 1.9. A syntactically valid mapping that admits an unintended consequence remains a modeling problem.
The finite alignment campaign and isolated elaboration are separate experiments; the shared-witness study below
supplies a common input binding.
5.4 Executed finite interpretation and controls
The packaged study authority db59ce4fca12295242ba0dc046156dac587e0fe6e0f6e75c9162034507427526 fixes
the selected workbook rows, source formulas, sense decisions, resource limits, expected polarities and numerical
tolerances before execution. It retains 12 source rows from the precedent ( Douglass et al. , 2024). The local content
sense places the model beneath Proposition; a separate execution is beneath Process. The ordered relation abst
ractCounterpart(model, execution) uses its selected abstract-first, physical-second domain commitments. This
makes the content/execution distinction explicit rather than treating every use of “model” as the same ontological
sense.
The finite FOL interpretation has a nonempty untyped carrier, class constants, binary instance and subclass,
selected subclass edges, instance inheritance, subclass transitivity, Physical/Abstract exclusion and the selected ar-
gument types of abstractCounterpart. It omits general SUO-KIF translation, partition exhaustiveness, universal
Entity membership and Sigma cache construction. No unique-name assumption is added: disjoint inhabited types
themselves force the two local individuals to differ. An empty class may be beneath disjoint branches without an
inhabitant; the inhabited control tests the additional commitment.
Competency/control Expected E Vampire
background Satisfiable Satisfiable Satisfiable
model-abstract Theorem Theorem Theorem
execution-physical Theorem Theorem Theorem
model-physical CounterSatisfiable CounterSatisfiable CounterSatisfiable
execution-abstract CounterSatisfiable CounterSatisfiable CounterSatisfiable
model-process CounterSatisfiable CounterSatisfiable CounterSatisfiable
execution-proposition CounterSatisfiable CounterSatisfiable CounterSatisfiable
model-not-physical Theorem Theorem Theorem
execution-not-abstract Theorem Theorem Theorem
alias Unsatisfiable Unsatisfiable Unsatisfiable
empty-double-class Satisfiable Satisfiable Satisfiable
inhabited-double-class Unsatisfiable Unsatisfiable Unsatisfiable
E matched 12 of 12 declared outcomes; Vampire matched 12 on identical problem hashes. The 24 retained invo-
cations agree on 12 cases. A satisfiable background is required before campaign completion. Timeout, unknown
and mismatched outcomes would prevent that condition. Agreement is a comparison of statuses for these frozen
problems, not a proof of general solver correctness or full-SUMO consistency.
Separately, the numerical design generated 36 models in dimensions 2, 3, 8, evaluated across prior, uniform, in-
dependently computed posterior and posterior-mode candidates. All 144 of 144 rows passed. The independent
reference uses 80-digit Decimal arithmetic on the exact supplied binary-float log inputs. The following maxima
30

## Page 32

are absolute errors; permutation reverses the state order, and rescaling checks the declared likelihood shift and
posterior invariance.
States Rows Reference Permutation Rescaling
2 48 2.919848e-16 0.000000e+00 5.551115e-16
3 48 4.489543e-16 0.000000e+00 3.330669e-16
8 48 1.039747e-15 0.000000e+00 4.440892e-16
The ordinary tolerance is 1e-12 and the extreme-case tolerance is 1e-10. The run passed 4 of 4 boundary cases and
rejected 8 of 8 invalid inputs. Structural zeros and positive masses below linear floating-point range remain distinct.
Arithmetic and posterior update are checked numerically; they are not axiomatized by these FOL problems. fig. 6
shows all logical polarities and numerical error-to-tolerance ratios. Its offline research explorer retains individual
rows and complete source provenance.
research-run delegates native execution to the same capture methods as direct prover operation. research-verify
rederives the retained source selections, problems, numerical matrix and status interpretation without a live source
index. Saved replay checks internal consistency; a separately trusted outer hash is needed to detect coherent
replacement of a whole evidence bundle. Neither replay nor cross-family agreement supplies a Lean interpretation,
preservation theorem or empirical validation.
5.5 Shared finite witnesses across representations
The bridge study addresses a concrete gap in running a numerical example beside an unrelated ontology query:
all layers must identify the same finite case. Its authority fixes Boolean state and observation carriers, strictly
positive rational prior and candidate laws, a complete normalized observation kernel, the observation true, and
stable identifiers for the model, its representation, calculation and result roles. The likelihood in Definition 2 is the
selected column of that kernel; row normalization concerns observations conditional on each state, not a sum down
the selected column ( Active Inference Institute , n.d.b, lines 153–156, 237–243).
The completed campaign instantiates the registered method below. The population and outcomes are injected
from its verified bridge report: 3 shared witnesses, 15 SUMO scenarios, 150 native executions and 51 Lean
declarations audited (definitions included) . A native execution may be a satisfiability or countermodel control
rather than a theorem result; the declaration inventory also includes entity names, laws and kernel definitions.
Witness
Posterior (false,
true) Free energy / nats
Floating divergence /
nats Native matched/total
uniform-prior (1/4, 3/4) 0.836988 0.143841 50/50
biased-prior (1/4, 3/4) 0.789041 0.383576 50/50
exact-candidate (6/7, 1/7) 0.538997 -1.665335e-16 50/50
The numerical columns are floating-point measurements. Scientific notation preserves nonzero round-off residuals at
the exact candidate rather than displaying them as signed zero; they do not contradict the real-valued nonnegativity
theorem.
5.5.1 F our referents and the claims attached to them
A shared witness is a common case, not a claim that its artifacts are one object. The mathematical model specifies
a probability law. A Lean expression represents that model in a language. A calculation is an identified activity
using declared inputs. A result is a record produced by that activity. Keeping these referents separate allows a
reader to ask a more useful question than whether two vocabularies share a label: which assertion about which
object is supported by which evidence?
31

## Page 33

Figure 6: Finite first-order logic (FOL) controls, with no full Suggested Upper Merged Ontology (SUMO) con-
sistency claim. Solver keys: E = E theorem prover; V = Vampire. Logical panels show declared polarities and
observed outcomes. Numerical panels compare independent-reference, permutation and rescaling errors with their
tolerances; exact zeros remain zero. Complete inputs accompany the offline explorer.
32

## Page 34

Role
Concrete uniform-prior
referent Checkable claim
Evidence that does not
replace it
Model BridgeUniformPriorMode
l, the declared finite
probability specification
The registered prior and
every observation-kernel
row normalize; the
selected evidence is
positive.
Classification as
Proposition or Abstract
does not prove
normalization.
Representation BridgeUniformPriorLea
n, the authored Lean
expression
The retained program
elaborates the intended
finite laws and the named
theorem instances.
SUMO represents does
not certify the
expression’s denotation or
the correctness of a
compiler.
Calculation BridgeUniformPriorCalc
ulation, the identified
evaluation
The retained invocation
consumes the matching
finite inputs and its
numerical values meet the
declared reference
comparison.
A local Calculating
classification does not
establish that an arbitrary
computer execution is a
psychological process.
Result BridgeUniformPriorResu
lt, the named numerical
record
Its exact posterior and
measured objective agree
with the specified witness.
A result role does not
make a false number true,
and an existential result
need not be this named
record.
These are authored referents in the experiment. Calling the first role a mathematical model does not assert an
untested SUMO MathematicalModel classification. The local bridge rule assigns it Proposition; the pinned (su
bclass Proposition Abstract) assertion and membership propagation support the narrower tested conclusion.
Likewise, the three retained state-space instances are mathematical examples, not observations of an organism.
Their value is that the proposed interpretation can be examined in full, including the premises that would have to
change for a different scientific use.
The diagram in fig. 7 makes these evidence lanes explicit. Its shared identifier is an index into obligations; it is not
an arrow that automatically transports truth between logical systems.
5.5.2 Exact examples that distinguish a model from its posterior
The graphical abstracts on physical pages 2–4 provide a visual introduction; the following table exposes their exact
inputs. Every ordered pair uses state order (false, true) . Values are derived from the retained rational witness
records, rather than rounded from a plotted curve.
The compact row labels correspond to the retained identifiers: Uniform = uniform-prior; Biased = biased-prior;
Exact = exact-candidate.
Witness Prior p
Likelihood
K(s,true) Joint pK Evidence Z Posterior Candidate q
Uniform (1/2, 1/2) (1/4, 3/4) (1/8, 3/8) 1/2 (1/4, 3/4) (1/2, 1/2)
Biased (1/3, 2/3) (1/2, 3/4) (1/6, 1/2) 2/3 (1/4, 3/4) (2/3, 1/3)
Exact (3/4, 1/4) (2/3, 1/3) (1/2, 1/12) 7/12 (6/7, 1/7) (6/7, 1/7)
For the uniform-prior witness, multiplication gives joint masses (1/8, 3/8). Their sum is 𝑍 = 1/2 ; dividing each
mass by 𝑍 gives posterior (1/4, 3/4). The complete observation kernel is 𝐾(𝑠, false) = 1 − 𝐾(𝑠, true) together with
the displayed true column. Thus each row sums to one, while the selected likelihood column is not required to sum
to one. This distinction separates an observation law from a distribution over hidden states.
33

## Page 35

Figure 7: Shared finite witnesses and the evidence attached to their mathematical model, representation, calculation
and result roles. Solver keys: E = E theorem prover; V = Vampire. Connections identify common inputs and
identifiers; each layer retains its own proof or measurement obligation.
34

## Page 36

Bayes’ rule also exposes what changes between witnesses. With positive entries, posterior odds factor into prior
odds and a likelihood ratio:
𝑝(𝑆 = true ∣ 𝑂 = true)
𝑝(𝑆 = false ∣ 𝑂 = true) = 𝑝(𝑆 = true)𝑝(𝑆 = false) 𝐾(true, true)𝐾(false, true) . (13)
In the uniform-prior case the two factors are 1 and 3. In the biased-prior case they are 2 and 3/2. Both give posterior
odds 3, yet the joint masses and evidences differ. Equal posteriors therefore do not identify equal generative models
or equal surprise. The biased example has 𝑍 = 2/3 rather than 1/2, and its candidate (2/3, 1/3) is farther from
the common posterior than the uniform candidate in the measured divergence. Each statement is a comparison of
the declared finite cases, not an ontology entailment about probability arithmetic.
The exact-candidate witness supplies a complementary test: joint masses (1/2, 1/12) give 𝑍 = 7/12 and posterior
(6/7, 1/7), already equal to the candidate. Over the reals, its posterior divergence is zero and free energy equals
surprise. The retained tiny floating residual is reported rather than relabelled a negative real divergence. This
example tests the equality case of the finite identity, while the other two expose the gap from a nonoptimal candidate.
Together they distinguish a correct formula, a concrete theorem instance, a numerical evaluation and its precision
boundary ( Active Inference Institute , n.d.a; Blei et al. , 2017; Blanchard et al. , 2019).
For each witness, the compiled Lean source constructs FiniteLaw and FiniteKernel values and proves nor-
malization, positive-evidence and pointwise exact-posterior obligations. It applies posterior_mul_predictiv
e, finiteKL_nonneg, finiteKL_self and the full-support finiteKL_eq_crossEntropy_sub_entropy theorem
at the pinned definitions ( Active Inference Institute , n.d.b, lines 263–281; Active Inference Institute , n.d.a, lines
43–54, 146–154). The numerical branch consumes the same rational model through its declared floating-point rep-
resentation and compares the objective and decomposition with a Decimal reference. Kernel checking establishes
the stated real-valued identities; numerical agreement concerns the declared finite-precision inputs and tolerance.
The retained commands and declaration-axiom audits cover the concrete module and paired well-formed control
environments. Invalid normalization, a wrong posterior and an admitted proof are rejected by the registered
diagnostic-specific controls; a timeout or unrelated import failure cannot satisfy those controls. The driver does
not prove the complete Python evaluator correct.
The SUMO branch makes representation commitments explicit. Two complete source rules at Merge.kif:5572–
5574 and 5589–5592 are:
(=>
(representsForAgent ?REP ?ENTITY ?AGENT)
(represents ?REP ?ENTITY))
(=>
(representsInLanguage ?REP ?ENTITY ?LANGUAGE)
(exists (?AGENT)
(representsForAgent ?REP ?ENTITY ?AGENT)))
They support representation consequences under the selected local assumptions ( OntologyPortal, n.d.b, lines 5545–
5592). Their conclusion concerns what stands for what; represents does not state equality of mathematical
denotations, a normalization identity, or preservation of a Lean theorem. The source Calculating subclass assertion
at line 15484 and membership rule at lines 146–150 separately support a classification question. Assigning a
synthetic calculation that type is an explicit modeling assumption; the prover does not infer intentional psychological
activity from running a numerical function ( OntologyPortal, n.d.b, lines 146–150, 15484–15490).
5.5.3 A source-bound derivation and its counterexamples
The representation case can be followed without treating the plot as evidence of logical entailment. Its local premise
is
(representsInLanguage BridgeUniformPriorLean
BridgeUniformPriorModel BridgeLeanLanguage)
35

## Page 37

Figure 8: Finite free-energy measurements for the shared witnesses, derived from the bridge report’s numerical
comparisons. The decomposition separates surprise from posterior divergence; agreement and residuals concern the
declared numerical inputs and reference.
36

## Page 38

The second source rule above produces an agent-relative representation for some agent. Applying the first rule to
that witness gives
(represents BridgeUniformPriorLean BridgeUniformPriorModel)
The shared spelling of BridgeUniformPriorAgent elsewhere in the study does not identify the existential agent with
that constant. The first-order query only needs existence. Nor do these premises establish the reverse representation,
that the representation is its referent, or that all formulas in its language have the same meaning. The registered
unsupported query reverses the arguments; its countermodel control is a concrete test of this missing converse.
Removing the relevant source rule tests dependence on the derivation, rather than merely checking whether the
target sentence appears somewhere in the file.
The calculation chain is equally specific. Under the local Calculating premise, the retained source subclass chain
through IntentionalPsychologicalProcess and IntentionalProcess reaches Process. The positive query asks
for this inherited membership; the unsupported query asks for Abstract. The three selected subclass premises are
at Merge.kif:15484, 13421, and 13390, in derivation order. The full source also links IntentionalPsycholog
icalProcess to PsychologicalProcess at line 13423; that separate axiom is not selected in this kernel and is
not credited to this executed derivation. These separately submitted backgrounds are not combined into a single
full SUMO theory. The type vocabulary brings intentional and psychological commitments that would require
additional justification before reusing this interpretation for an actual software agent or biological system. The
method makes that scientific modeling choice visible instead of hiding it behind the word “calculation” .
The named-result scenario starts from an additional local rule that assigns the witness model to Proposition, the
calculation to Calculating, and the named record to its result role. It combines the source assertion
(disjointRelation result instrument)
with a locally authored binary instance of the source disjoint-relation schema. The intended query excludes the same
record’s being an instrument of that calculation. The schema at Merge.kif:489–495 contains a row variable; the
strict compiler does not translate that general schema, so the binary instance is identified as a study assumption
(OntologyPortal, n.d.b, lines 489–495, 3264). This tests a declared role distinction, not the correctness of the
record’s numerical contents.
Source-required result production asks a different question. The complete source rule is:
(=>
(instance ?DEVELOP ContentDevelopment)
(exists (?OBJ)
(and
(instance ?OBJ ContentBearingObject)
(result ?DEVELOP ?OBJ))))
Under the declared ContentDevelopment assumption, it requires some content-bearing result ( OntologyPortal,
n.d.b, lines 16326–16331). It does not identify that existential object with the study’s named numerical record.
The study tests existence and named-result identification separately, with unsupported-query and removed-premise
controls. Reusing a stable calculation identifier across scenarios binds their subject without combining their sepa-
rately declared backgrounds or adding a unique-name assumption.
Every scenario has a conjecture-free satisfiable-background requirement, a positive query, an unsupported query, a
registered premise removal and an explicit refutation control for each selected prover. The observed statuses and
denominators come from the report, following the result distinctions in sec. 3.4.4.
The canonical packet is output/bridge/bridge-report.json . Read-only inspection exposes the catalog, report
and individual case evidence; executing a campaign is a separate operator action. Portable verification requires
an independently supplied outer report fingerprint. The offline bridge explorer presents the same report-derived
inputs and case evidence without starting a prover.
The shared study connects these representations through matched inputs, checked finite theorem instantiations
and source-bound representation controls. Its completed report records which obligations were met and retains the
37

## Page 39

Figure 9: Native bridge controls grouped by their declared problem roles and observed statuses. Satisfiable back-
grounds, theorem queries, countermodel controls and explicit refutations have separate meanings; counts are derived
from retained executions.
38

## Page 40

generated sources, exact native problems, commands, diagnostics and numerical references. Its SUMO theory still
contains no probability arithmetic or interpretation equating LogFn with natural logarithms. These experiments
do not compose into a general SUMO-to-Lean preservation theorem; their distinct claims are the rows of the ledger
in sec. 5.3.
5.5.4 Evidence roles as a research interface
The connection suggests a practical unit of scientific integration: a claim with a typed subject, an explicit inter-
pretation, and the evidence needed to challenge it. A future probability vocabulary bridge would need a map
from finite events to the propositions accepted by ProbabilityFn, together with normalization, conditioning and
arithmetic compatibility. Its real-valued range alone supplies none of those laws. A logarithm bridge would also
need to relate SUMO’s binary positive-integer-base operation to Lean’s unary natural logarithm on its declared
domain. Reusing the same identifier is the beginning of such work, not its preservation proof.
This emphasis connects the study to two complementary traditions. The World Wide Web Consortium’s provenance
ontology distinguishes entities, activities and agents, with qualified usage and generation able to record roles and
other attributes ( Lebo et al. , 2013). It offers a useful design comparison for attaching the input model, executed
calculation and generated record to one case. A PROV assertion describes provenance; it is not an independent
proof that a computation returned the right value. No equivalence between PROV and the SUMO case roles is
asserted here.
Ologs provide a second comparison: typed arrows and commuting paths express constraints that an interpretation
must satisfy ( Spivak and Kent , 2012). For this bridge, the relevant future question is whether following “source
expression to finite semantics to result” agrees with an independently defined route through a target representation.
The present study checks named endpoints and obligations, but has not constructed such a functor or proved a
commuting semantic interpretation. The diagram is an agenda for that theorem, not a picture of a theorem already
established.
Next experiment Concrete example
Required evidence before claiming
success
Representation adequacy An event encoding for the two
Boolean states and the observed
outcome.
An injective event interpretation
where needed, the intended
proposition semantics, and positive
and collision controls.
Operation preservation Conditioning the uniform-prior
model through both SUMO-oriented
and Lean-oriented representations.
A stated map for multiplication,
summation, division and
conditioning, plus a proof that the
two routes agree on the declared
domain.
Result provenance A posterior record with a model
identifier, evaluator version and
numerical reference.
Exact input/output custody,
declared precision, comparison
controls and an explicit distinction
between generation and value
correctness.
Intervention sensitivity Swap the likelihoods while
preserving the prior and separately
change the candidate.
Newly registered witnesses,
predicted posterior/energy changes,
independent arithmetic and fresh
native/proof evidence before
reporting outcomes.
Scientific application A separately justified observation
model for a real agent.
Measurement semantics, empirical
design and model criticism in
addition to the logical and
numerical obligations above.
39

## Page 41

These experiments turn an ambitious alignment into falsifiable work. A wrong representation direction, a nonnor-
malizing kernel, a mismatched result record and an unsupported named existential each fail for a different reason.
The current campaign already separates those kinds of obligation; extending its scientific reach requires retaining
that separation while adding the missing interpretations and evidence.
5.5.5 A connection atlas with distinct tests at each arrow
The most useful connection is a path that can be challenged at intermediate steps. For the uniform witness, the
representation is BridgeUniformPriorLean , the model is BridgeUniformPriorModel , and the calculation and
result have their own identifiers. The following atlas places the actual expressions beside the mathematical work
they do, rather than using an undifferentiated “verified” label.
Connection
Actual expression or
object
Consequence or
calculation
Control that distinguishes
the claim
Source language to
representation role
representsInLanguage(B
ridgeUniformPriorLean,
BridgeUniformPriorMode
l, BridgeLeanLanguage)
plus the two complete
selected SUMO rules
Some representing agent
exists, and the expression
represents this model.
Reversing the
representation query or
removing the required rule
must not preserve
entailment; the existential
does not name an agent.
Finite specification to a
Lean value
UniformPrior.prior, Uni
formPrior.kernel, and
their
FiniteLaw/FiniteKernel
obligations
The prior and each
conditional observation
row normalize.
The retained
wrong-normalization
program must fail for its
designated obligation,
rather than for an
unrelated import error.
Conditioning to a concrete
theorem instance
UniformPrior.posterior
_reconstruction, using p
osterior_mul_predictiv
e
For each state, posterior
mass times positive
evidence equals prior mass
times selected likelihood:
false, 14 × 12 = 18 ; true,3
4 × 12 = 38 .
The retained
wrong-posterior program
is rejected; dropping the
positive-evidence
hypothesis changes the
problem.
Real-valued objective to
evaluated numbers
The full-support finite KL
decomposition and the
registered numerical
evaluator
Joint masses, evidence,
free energy, divergence
and signed residual are
compared with the
independent Decimal
route.
A result-role statement
with a changed numerical
tuple is still a role
statement, but fails the
arithmetic comparison.
Result record to a later
prediction
Posterior-weighted use of
the same kernel, with
persistent state and
conditional independence
made explicit
A second true observation
has probability 5/8 for the
uniform model and 11/16
for the biased model.
Redrawing the state
instead gives their initial
marginal probabilities 1/2
and 2/3; these are
different experiments.
The source-to-language arrow merits particular care. Verified compilation provides a useful methodological compar-
ison: Leroy relates source and target states through a simulation invariant and matches transitions and observable
effects, including initial and final states ( Leroy, 2009, §4.3). A future translation of the finite event language would
likewise need a stated relation between interpretations and proofs that relevant operations respect it. Our endpoint
comparisons and selected theorem instances do not constitute such a general semantic-preservation result. They
expose tractable obligations for attempting one.
There is also an arithmetic boundary inside the apparent numerical arrow. Exact rational joint masses, a real
logarithmic identity and a finite-precision returned value are three different objects. Harrison’s verified floating-
40

## Page 42

point examples supplement exact reasoning with explicit rounding bounds, and separate function-approximation
error from evaluation error ( Harrison, 2006, §4.2 and the trigonometric-function discussion). Here the reference
comparisons test the actual retained inputs; no theorem bounds every execution of the Python evaluator. This is
why the tiny signed residual at the exact candidate remains visible alongside the real equality case.
5.6 Changing representations without confusing the evidence
The shared cases support a further executable experiment: change the finite representation while keeping explicit
track of the information it discards. This derived analysis uses the same rational inputs, but does not add cases to
the historical SUMO campaign or declarations to its Lean receipt. Its exact masses, 100-digit Decimal logarithms
and source report digest are exported in witness-research.json . Exact arithmetic establishes the displayed
rational equalities; numerical residuals and their declared tolerances remain separate.
Let 𝑇𝑠𝑎 be a nonnegative, row-stochastic channel from fine states 𝑠 to reported states 𝑎. With joint mass 𝑗𝑠 =
𝑝𝑠𝐾(𝑠, true), define
𝑝′𝑎 = ∑
𝑠
𝑝𝑠𝑇𝑠𝑎, 𝑗 ′𝑎 = ∑
𝑠
𝑗𝑠𝑇𝑠𝑎, 𝐾 ′(𝑎, true) = 𝑗 ′𝑎/𝑝′𝑎. (14)
The last expression is defined on positive coarse prior support, which all outputs of the four channels used here
satisfy. It is a prior-weighted induced observation model, not an unweighted average of likelihood entries. Because
the channel rows sum to one, ∑𝑎 𝑗′𝑎 = 𝑍 and the coarse posterior is 𝑟′ = 𝑟𝑇 . Thus conditioning the induced model
agrees exactly with pushing the original posterior forward. The candidate must pass through the same channel,
𝑞′ = 𝑞𝑇 , for the information comparison below.
This calculation connects concretely to the pinned FEP_Formal application programming interface (API). Its Fini
teKernel.comp later earlier multiplies and sums kernel masses, supplies nonnegativity and row-normalization
proofs, and predictive_comp identifies the two routes through sequential prediction ( Active Inference Institute ,
n.d.b, lines 190–209, 246–254). These source declarations motivate the typed comparison; this new Python exper-
iment does not claim that the retained Lean execution proved its channel contraction or its induced conditioning
construction. Markov-kernel scholarship provides a broader language for composition and conditioning while re-
taining their different types ( Fritz, 2020).
For the uniform case, the noisy state channel has rows (3/4, 1/4) and (1/4, 3/4). It gives 𝑝′ = (1/2, 1/2) , 𝑗′ =
(3/16, 5/16), 𝐾′(⋅, true) = (3/8, 5/8) and 𝑟′ = (3/8, 5/8) , with unchanged 𝑍 = 1/2 . For the singleton erasure
channel the coarse likelihood is simply 𝑍. Its three values are therefore 1/2, 2/3 and 7/12. Unweighted averaging
would instead give 1/2, 5/8 and 1/2: the uniform case alone would conceal that error, while the other two cases
expose it.
5.6.1 A smaller divergence need not mean better inference
For a common stochastic channel, the classical data-processing inequality states 𝐷(𝑞𝑇 ‖𝑟𝑇 ) ≤ 𝐷(𝑞‖𝑟) (van Erven
and Harremoës , 2014, Theorem 9, order one). In the finite supported setting, the log-sum inequality applied at
each output to 𝑞𝑠𝑇𝑠𝑎 and 𝑟𝑠𝑇𝑠𝑎 yields this bound. Summing the right-hand terms uses ∑𝑎 𝑇𝑠𝑎 = 1 . Terms with
zero candidate mass contribute zero; positive candidate mass outside reference support requires an explicit support
treatment. The new evaluator rejects that unsupported finite-log calculation rather than emitting an infinite value
as a JSON number.
Witness State channel
Candidate
after Posterior after KL before / nats KL after / nats
Uniform identity (1/2, 1/2) (1/4, 3/4) 0.143841 0.143841
Uniform swap-labels (1/2, 1/2) (3/4, 1/4) 0.143841 0.143841
Uniform noisy-quarter (1/2, 1/2) (3/8, 5/8) 0.143841 0.032269
Uniform erase-state (1) (1) 0.143841 0.000000
Biased identity (2/3, 1/3) (1/4, 3/4) 0.383576 0.383576
41

## Page 43

Witness State channel
Candidate
after Posterior after KL before / nats KL after / nats
Biased swap-labels (1/3, 2/3) (3/4, 1/4) 0.383576 0.383576
Biased noisy-quarter (7/12, 5/12) (3/8, 5/8) 0.383576 0.088792
Biased erase-state (1) (1) 0.383576 0.000000
Exact identity (6/7, 1/7) (6/7, 1/7) 0.000000 0.000000
Exact swap-labels (1/7, 6/7) (1/7, 6/7) 0.000000 0.000000
Exact noisy-quarter (19/28, 9/28) (19/28, 9/28) 0.000000 0.000000
Exact erase-state (1) (1) 0.000000 0.000000
Uniform, Biased and Exact refer to the registered witness identifiers already defined above. Identity and state-label
permutation preserve divergence; the noisy channel reduces the first two gaps; singleton erasure makes all coarse
candidate/posterior pairs equal. In particular, the uniform case falls from approximately 0.143841 to 0.032269
nats under noise, and to zero under erasure. Its original candidate has not been repaired. The exact-candidate
case remains equal without needing loss. This distinguishes optimization of the original inference problem from
loss of the ability to tell two answers apart. With evidence unchanged, the induced coarse objective is 𝐹 ′(𝑞𝑇 ) =
− log 𝑍 + 𝐷(𝑞𝑇 ‖𝑟𝑇 ); it belongs to a changed state description.
5.6.2 State aggregation and observation degradation are different experiments
The previous channel changes what hidden state is reported. A channel on the observation instead changes the
event being conditioned on. Suppose the Boolean observation is flipped with probability 𝑒 = 1/4 . The likelihood
of the newly observed true output is 𝑒 + (1 − 2𝑒)𝐾(𝑠, true). Exact conditioning now gives the uniform posterior
(3/8, 5/8) at evidence 1/2; the biased posterior (2/7, 5/7) at evidence 7/12; and the exact-candidate model’s
posterior (21/26, 5/26) at evidence 13/24. The last model’s old candidate (6/7, 1/7) is no longer its posterior.
This changes a hypothesis, not the truth of its earlier equality instance. Completely erasing observations would
recover the hidden-state prior; completely erasing hidden-state identity gives a singleton posterior. The domains
and codomains of the arrows explain why those answers differ.
5.7 Posterior identity, observation evidence and model comparison
There is another controlled way to preserve a posterior. Multiply only the selected likelihood column by 𝑐 > 0
while keeping it in [0, 1], and complete each Boolean observation row with 1 − 𝑐𝐾(𝑠, true). Then
𝑍𝑐 = 𝑐𝑍, 𝑟 𝑐 = 𝑟, 𝐹 𝑐(𝑞) = 𝐹 (𝑞) − log 𝑐. (15)
For 𝑐 = 1/2 all three current models remain valid and their exact posteriors remain unchanged. This is a changed
observation kernel, not multiplication of every entry of a normalized row by the same constant. Posterior KL stays
the same for the same candidate; surprise and absolute free energy rise by log 2. Consequently a posterior record
alone cannot identify its evidence, its complete generative model or its absolute variational objective.
Witness Original evidence Scaled evidence
Unchanged
posterior Surprise increase / nats
Uniform 1/2 1/4 (1/4, 3/4) 0.693147
Biased 2/3 1/3 (1/4, 3/4) 0.693147
Exact 7/12 7/24 (6/7, 1/7) 0.693147
Model comparison introduces a different random variable, 𝑀 . Treating the uniform and biased toy models as
alternatives for the same observation, with equal prior model probabilities, gives Bayes factor 𝑍biased/𝑍uniform = 4/3
and posterior model probability 𝑃 (𝑀 = biased ∣ true) = 4/7 . These are ratios of declared marginal observation
42

## Page 44

Figure 10: Changing a finite state representation can hide candidate error. Identity, label swap, shared noisy
channel and singleton erasure are applied to both candidate and posterior. Kullback-Leibler (KL) divergence uses
natural-log nats; a smaller coarse divergence is not improved inference on the original state space. Exact inputs
and numerical tolerances accompany the source-bound data export.
43

## Page 45

Figure 11: Identical posteriors can accompany different observation evidence. Scaling the selected likelihood column
by 1/2 and completing the other Boolean outcome preserves each posterior while increasing surprise and free energy
by log 2 for a fixed candidate. Model, representation, calculation and result provenance remain distinct obligations.
The transformed models are derived finite experiments, not new native ontology or Lean proof results.
44

## Page 46

probabilities, not posterior-state divergences; unequal prior model odds would multiply the factor ( Kass and Raftery,
1995). No empirical evidence-strength label is attached to this synthetic comparison.
Equal state posteriors also need not imply equal predictions. If a second observation uses the same hidden state
and the same kernel, with observations conditionally independent given that state and model, its true probability
is ∑𝑠 𝑟𝑠𝐾(𝑠, true). The three exact values are 5/8, 11/16 and 13/21. The first two differ despite their common
current state posterior. Redrawing a new hidden state would define another model and another prediction. The
added assumption is stated here and in the method contract; it is not silently attributed to the original native
campaign.
5.8 Sequential inference, simulation and prediction
The next experiment makes the additional temporal assumptions executable. One latent Boolean state is drawn
once and retained within each trajectory; the observation kernel is unchanged, and observations are conditionally
independent given that state and model. We condition on a prefix of 𝑛 true observations. With ℓ𝑠 = 𝐾(𝑠, true), its
exact probability is 𝑍𝑛 = ∑ 𝑠 𝑝𝑠ℓ𝑛𝑠 , its state posterior is 𝑟𝑛(𝑠) = 𝑝 𝑠ℓ𝑛𝑠 /𝑍𝑛, and the next true-observation probability
is 𝑎𝑛 = ∑ 𝑠 𝑟𝑛(𝑠)ℓ𝑠 = 𝑍 𝑛+1/𝑍𝑛. At 𝑛 = 0 , 𝑍0 = 1 and 𝑟0 = 𝑝 . These quantities are computed for every 𝑛 from
zero through twelve using rational arithmetic. An independent iterative route updates the preceding posterior and
multiplies the successive predictive probabilities; it must agree exactly with the direct products.
Witness Z2
Posterior (false,
true) P(next true)
Simulated prefix count
/ trials
uniform-prior 5/16 (1/10, 9/10) 7/10 20645 / 65536
biased-prior 11/24 (2/11, 9/11) 31/44 30123 / 65536
exact-candidate 13/36 (12/13, 1/13) 25/39 23749 / 65536
The first observation makes the uniform and biased posteriors identical, (1/4, 3/4), but their second updates
separate them. At 𝑛 = 2 the uniform posterior is (1/10, 9/10) with 𝑍2 = 5/16 , whereas the biased posterior is
(2/11, 9/11) with 𝑍2 = 11/24 . For the third model it is (12/13, 1/13) with 𝑍2 = 13/36 . A candidate that was
exact after one observation is therefore not automatically exact after a new observation. The kernels, not just the
current posterior vectors, determine these trajectories. The equations also identify the persistence assumption as
testable: independently redrawing the state before every observation would instead give prefix probability 𝑍𝑛1 . For
the uniform model at 𝑛 = 2 that would be 1/4, rather than the persistent-state value 5/16.
The forward simulation provides a separate, deliberately less exact view. For each model it generates 65,536
trajectories with a recorded fixed seed, samples the state once per trajectory, then samples the 12 observations
from that state’s kernel. At each prefix it retains the integer number of surviving all-true trajectories and how
many have latent state false. Dividing those counts gives an empirical prefix probability and, when the survivor
count is positive, an empirical posterior. The exported witness-dynamics.json retains the counts, generator
identity and exact rational answers. The plotted simulation marks are observations of this synthetic generator, not
extra Lean declarations, new ontology outcomes, confidence bounds or biological data. Rare long prefixes have
fewer surviving trajectories, so a deterministic and internally consistent simulation record still does not replace
exact conditioning.
The direction of this procedure matters. Forward generation starts with a specified model and produces synthetic
observations. Conditioning starts with a specified observation history and computes a distribution over its possible
hidden causes. The simulator implements the former, then uses surviving histories to estimate quantities that the
exact calculation obtains by the latter. It is not a Markov chain Monte Carlo sampler of an unknown posterior.
Generating replications from a posterior and checking them against actual data would be a further model-assessment
step ( Gelman et al. , 2020, §§2.4, 4.1, 6.1). Here the observations are generated by the very model being examined,
so agreement with exact conditioning checks implementation and assumptions rather than empirical fit.
Nor does the changing posterior imply that the simulated hidden state moves: the state remains fixed within a
trajectory. Discrete active-inference models add action-dependent transitions, policy evaluation and action selection;
45

## Page 47

their expected-free-energy objective concerns prospective courses of action ( Da Costa et al. , 2020, arXiv v2, §§3,
6–7). Those components are not implemented by the present fixed-state simulation. Its role is to make a tractable
inference ingredient, and the evidence attached to it, inspectable before claiming a larger agent model.
The model-comparison path is different again. With equal prior probabilities on the uniform and biased models,
their probability after an all-true prefix is obtained by normalizing their two 𝑍𝑛 values. The biased-model probability
changes from 4/7 after one observation to 22/37 after two. For a fixed model, the chain identity log 𝑍𝑛 = ∑
𝑛−1
𝑡=0 log 𝑎𝑡
expresses the sequence probability as a sum of conditional log scores. Thus the difference of those cumulative scores
is a log Bayes factor. This compares probabilities of an observation history; it is not the KL divergence between a
variational candidate and a state posterior. Gneiting and Raftery explain logarithmic scoring and its connection to
Bayes factors, including the distinction between forecasts specified before assessment and models fitted using the
scored data ( Gneiting and Raftery , 2007, §§4, 7.1). Here the cases are fixed synthetic models, not a model-selection
claim about measured organisms.
5.8.1 Mixed histories expose the observation model
An all-true prefix is only one possible observation history. The complete kernel also assigns probabilities to false
outcomes. For an ordered history 𝑦1∶𝑛, define the unnormalized state mass 𝑗𝑛(𝑠) = 𝑝 𝑠 ∏
𝑛
𝑡=1 𝐾(𝑠, 𝑦𝑡), its evidence
𝑍𝑛 = ∑ 𝑠 𝑗𝑛(𝑠), and posterior 𝑟𝑛(𝑠) = 𝑗 𝑛(𝑠)/𝑍𝑛 when 𝑍𝑛 > 0. The next-observation law is 𝑎𝑛(𝑦) = ∑ 𝑠 𝑟𝑛(𝑠)𝐾(𝑠, 𝑦).
Sequential Bayes updates and the direct joint products must agree exactly at every prefix, including the empty one.
An impossible history is rejected rather than assigned a fabricated posterior.
Witness P(TTF)
P(false state given
TTF)
P(next true given
TTF)
Redrawn-state
P(TTF)
uniform-prior 3/32 1/4 5/8 1/8
biased-prior 13/96 4/13 35/52 4/27
exact-candidate 7/54 6/7 13/21 245/1728
The atlas enumerates all eight length-three histories for all three models. Within a fixed persistent-state model,
histories with the same counts of true and false outcomes have equal evidence and final posterior: multiplication of
the same likelihood factors commutes. Their intermediate posteriors need not coincide. This is an exchangeability
property of the declared model, not a claim that time order can be ignored in arbitrary dynamical systems.
Model uncertainty adds another normalization. With declared model probabilities 𝜋𝑚, the weight after the history
is 𝑤𝑚 = 𝜋 𝑚𝑍𝑚,𝑛/ ∑𝑘 𝜋𝑘𝑍𝑘,𝑛, and the model-averaged next law is ∑𝑚 𝑤𝑚𝑎𝑚,𝑛(𝑦). This denominator differs from
a state posterior’s denominator. A model that makes the history impossible receives zero weight; if every positive-
prior model makes it impossible, the comparison is undefined and rejects. The default atlas compares only uniform
and biased models with equal prior weights; the third model is displayed separately, not silently added to that
comparison. Independently redrawing the hidden state gives ∏𝑡 ∑𝑠 𝑝𝑠𝐾(𝑠, 𝑦𝑡) instead of the persistent-state joint
sum, providing a concrete model-assumption counterexample for the same symbols.
5.8.2 Model checking has several different meanings
A well-formed kernel, a successful theorem instance, a reproduced simulation and a good empirical forecast answer
different questions. Predictive calibration concerns the relation between forecasts and realized outcomes; sharpness
concerns concentration of the forecasts themselves ( Gneiting et al. , 2007, p. 243). Neither normalization nor an
increasingly concentrated posterior establishes calibration. Similarly, computational science distinguishes adjusting
parameters against selected data from assessing predictive capability for a specified application ( Trucano et al. ,
2006, §1). The latter requires empirical commitments that the three toy models do not supply.
The distinction matters for selecting diagnostics. Gneiting, Balabdaoui and Raftery’s probability-integral-transform
characterization assumes continuous, strictly increasing forecast distributions and stated dependence conditions;
their examples show why a visually uniform histogram alone is not a universal certificate of forecast quality ( Gneiting
et al., 2007, §§2.1, 2.4, 3.1). Our Boolean examples do not satisfy that continuous-outcome setup. Evaluating them
46

## Page 48

Figure 12: Sequential inference links exact mathematics to a seeded forward simulation. Each trajectory holds its
hidden state fixed; observations are conditionally independent given that state and model. Exact posterior and
next-observation paths are distinguished from empirical prefix counts, and the uniform/biased model comparison
uses cumulative observation evidence. All values are derived from the same three registered witnesses; no new
native SUMO or Lean proof result is claimed.
47

## Page 49

Figure 13: All eight mixed Boolean observation histories connect complete kernels to exact joint probabilities, state
posteriors, next-observation laws and two-model posterior weights. Every fraction is generated from the registered
witnesses; identical-count histories expose the fixed-state exchangeability assumption. Model E is not included in
the uniform/biased comparison. The source JSON also retains the distinct redrawn-state probabilities; these are
derived mathematical examples, not additional Lean declarations, ontology outcomes or empirical observations.
48

## Page 50

empirically would instead require an appropriate binary-event protocol and observations kept separate from model
fitting. No such empirical assessment is supplied by the exact atlas or seeded trajectories.
Question Evidence available here
Additional evidence needed for a
scientific application
Does the expression select the
intended referent?
Pinned source formulas, local
premises and direction-sensitive
native controls.
A justified interpretation of
measured events and model entities.
Is the finite update mathematically
well formed?
Rational normalization and
conditioning; the retained concrete
Lean obligations.
Formalization of any new state,
observation or temporal
assumptions.
Does this implementation compute
the declared example?
Direct/iterative exact agreement,
retained simulation counts and
independent numerical comparisons.
Error bounds for broader arithmetic
regimes and implementation-level
assurance as required.
Does the forecast predict
observations well?
Declared synthetic predictive
probabilities, with no empirical
success claim.
Outcomes withheld from fitting,
suitable proper scores, calibration
diagnostics and uncertainty
analysis.
Does the model explain the target
system?
An explicit, inspectable example of
the inferential architecture.
Domain-specific measurement
semantics, comparison models,
model-discrepancy analysis and
empirical validation.
The research opportunity is to make these obligations composable at the level of a particular claim. A SUMO
expression can identify an event or a calculation; a Lean value can state its finite semantics; exact algebra can expose
an invariant; simulation can reveal consequences of a specified generative process; and subsequent observations can
challenge its predictions. A useful connection records which of those steps has evidence and which still needs it.
5.9 What an ontology expression would have to preserve
The SUMO distinction remains substantive. In the pinned source, ProbabilityFn is a unary function with domain
Formula and range RealNumber (OntologyPortal, n.d.b, lines 3334–3338). A finite state’s mass is not automatically
an application of that function. A proposed bridge must first assign each finite event a proposition, specify its
probability semantics, and preserve the operations needed by the intended claim. The current uninterpreted mass
labels in the selected first-order kernels do not do that.
A two-state collision demonstrates the missing obligation. Let 𝐴 = { false} and 𝐵 = { true}, and map both states
to a single coarse state. Direct images of 𝐴 and 𝐵 are the same nonempty event, so their intersection is nonempty
although the image of 𝐴∩𝐵 is empty. This map preserves total mass but not the intersection structure of fine events.
Inverse images preserve Boolean event operations in the other direction, but cannot recover every fine distinction
from a coarse event. Thus a represents assertion and matching posterior values do not establish faithfulness of
an event interpretation.
This obstruction is now executable in a separate, deliberately small event interface. FiniteStateMap validates
explicit finite carriers, total state assignments and event membership; it computes exact direct images, inverse
images and probability pushforwards. Bijective relabeling and many-to-one coarsening therefore have different,
testable operation-preservation behavior. The companion Lean source states inverse-image preservation of union,
intersection and complement, together with the concrete Boolean-to-unit intersection failure. These four statements
are separate from the retained bridge declaration population. They concern event operations, not the semantics of
arbitrary SUMO sentences, verified Python execution or the empirical interpretation of a hidden state.
A precise future restricted goal would pair a sentence translation 𝜏 with a target-model interpretation 𝑅 and require
compatibility of satisfaction, 𝑀 ′ ⊧ 𝜏 (𝜑) exactly when 𝑅(𝑀 ′) ⊧ 𝜑 . Institution theory makes that compatibility
central to change of notation ( Goguen and Burstall , 1992). Here it is a proposed contract for a deliberately small
49

## Page 51

event language, not an institution morphism between complete SUMO and Lean. The direction of the model map,
admissible sentences, support assumptions and operation-preservation proofs would all need to be supplied.
Finally, evidence about a result is itself represented and generated. An evaluator may produce a posterior entity;
a separate checking activity uses that entity, the exact input and an independent reference to produce a checking
receipt. PROV-DM bundles support descriptions of provenance, while PROV constraints check consistent histories
rather than numerical truth ( Moreau and Missier , 2013; Cheney et al. , 2013). Replacing the uniform result by
(1/3, 2/3) can leave an otherwise identical role graph well formed, yet fail the exact arithmetic check. Conversely,
a correct tuple without a bound execution record does not establish that a claimed activity occurred. PROV
responsibility, SUMO’s existential representing agent, and an empirical cognitive agent therefore remain different
commitments. These distinctions make the shared-witness interface useful for scientific model criticism without
making a new biological claim.
6 Reproducibility and contribution
6.1 Publication from declared authorities
The scientific body is authored once. A checked context injects corpus measurements, model values, version, source
revisions, compiler information, and author metadata from their authorities. Bibliography keys resolve through
native citation processing. Template filters generate section, formalism, equation, and figure labels. References
such as Definition 2 , Proposition 1 , eq. 9, and fig. 5 are generated labels, not manually assigned numbers.
Actual docxology/template combined Portable Document Format (PDF) and Hypertext Markup Language (HTML)
adapters and the native Word (.docx) adapter render the editions from a verified Git archive. PDF uses its
configured image cover and author block; HTML and Word receive a source-derived frontmatter projection. All
editions share the body, bibliography, substitutions, and labels. The unnumbered cover image does not advance
body-figure numbering.
A receipt binds source inputs, staged projections, graphical data, imported renderer modules, and final hashes.
Preflight rejects unresolved substitutions, missing citations, invalid labels, and conflicting measurements. Output
checks inspect actual references, author metadata, equations, and image bytes. These controls establish artifact
integrity, not scientific validity or perfect typography.
6.2 Operator workflow and limits
1. Prepare the declared Python environment and external storage bindings.
2. Acquire the pinned SUMO sources and runtime, then record identities.
3. Index and audit source bytes; regenerate measurements and graphics.
4. Retain queries, exact prover inputs, diagnostics, and outputs together.
5. Run finite numerical and formal checks with their explicit scope.
6. Render the manuscript and inspect every PDF page and native edition.
Upstream issues and pull requests require a minimal independently reproduced finding and a precise claim. Un-
known search status is not falsity. An unexpected consequence can expose an intended-model problem even when
the prover succeeds. Private research remains private unless deliberately released.
The claim ledger in sec. 5.3 specifies the remaining mathematical, semantic and empirical obligations. Public
hosting additionally requires a separately evaluated deployment.
6.3 Licensing and attribution
Copyright © 2026 Daniel Ari Friedman. Original manuscript text and figures are licensed under Creative Commons
Attribution 4.0 International (CC BY 4.0) . Software, figure-generating code and original code/Lean listings remain
MIT licensed. Quoted or reproduced third-party material retains its own attribution and terms; this grant covers
only the author’s original contributions.
50

## Page 52

References
Active Inference Institute. Finite information theory: pinned lean source. fep_formal, revision
9a0694f16b8e89b66b2f7f8cc7426c650dd2c4de, n.d.a. URL https://github.com/ActiveInferenceInstitute/fe
p_formal/blob/9a0694f16b8e89b66b2f7f8cc7426c650dd2c4de/lean/FepSketches/finite_information.lean .
Source reference. Rikishi separately records isolated Lean elaboration of the pinned finite-probability and finite-
information modules and declaration-axiom inspection; no full-repository certification or SUMO equivalence is
established.
Active Inference Institute. Finite probability laws and kernels: pinned Lean source. fep_formal, revision
9a0694f16b8e89b66b2f7f8cc7426c650dd2c4de, n.d.b. URL https://github.com/ActiveInferenceInstitute/fe
p_formal/blob/9a0694f16b8e89b66b2f7f8cc7426c650dd2c4de/lean/FepSketches/finite_probability.lean . Source
reference for FiniteLaw, FiniteKernel, predictive, posterior, and posterior_mul_predictive; native execution is
separately recorded by Rikishi.
Javier Álvez, Paqui Lucio, and German Rigau. Adimen-SUMO: Reengineering an ontology for first-order reasoning.
International Journal on Semantic Web and Information Systems , 8(4):80–116, 2012. doi: 10.4018/jswis.201210
0105. URL https://adimen.ehu.eus/~rigau/publications/ijswis12-alr.pdf.
Javier Álvez, Paqui Lucio, and German Rigau. Improving the competency of first-order ontologies. In Proceedings
of the 8th International Conference on Knowledge Capture , pages 15:1–15:8. ACM, 2015. doi: 10.1145/2815833.
2815841. URL https://adimen.ehu.eus/web/files/AdimenSUMO/k-cap2015.alrA.pdf.
Javier Álvez, Paqui Lucio, and German Rigau. Evaluating automated theorem provers using Adimen-SUMO. In
Vampire 2016. Proceedings of the 3rd Vampire Workshop , volume 44 of EPiC Series in Computing , pages 74–82.
EasyChair, 2017. doi: 10.29007/hplh. URL https://easychair.org/publications/paper/4LFw.
Javier Álvez, Montserrat Hermo, Paqui Lucio, and German Rigau. Automatic white-box testing of first-order
logic ontologies. Journal of Logic and Computation , 29(5):723–751, 2019. doi: 10.1093/logcom/exz001. URL
https://arxiv.org/html/1705.10219v3.
Christoph Benzmüller and Adam Pease. Higher-order aspects and context in SUMO. Journal of Web Semantics , 12–
13:104–117, 2012. doi: 10.1016/j.websem.2011.11.008. URL https://christoph-benzmueller.de/papers/J27.pdf.
Pierre Blanchard, Desmond J. Higham, and Nicholas J. Higham. Accurate computation of the log-sum-exp and
softmax functions, 2019. URL https://arxiv.org/abs/1909.03469v1 . Version 1, September 8, 2019; shifted
normalization and floating-point error analysis.
David M. Blei, Alp Kucukelbir, and Jon D. McAuliffe. Variational inference: A review for statisticians. Journal
of the American Statistical Association , 112(518):859–877, 2017. doi: 10.1080/01621459.2017.1285773. URL
https://www.cs.columbia.edu/~blei/papers/BleiKucukelbirMcAuliffe2017.pdf.
Chad E. Brown, Adam Pease, and Josef Urban. Translating SUMO-K to higher-order set theory. In Frontiers of
Combining Systems , volume 14279 of Lecture Notes in Computer Science , pages 255–274. Springer, 2023. doi:
10.1007/978-3-031-43369-6_14. URL https://link.springer.com/chapter/10.1007/978-3-031-43369-6_14 .
James Cheney, Paolo Missier, and Luc Moreau. Constraints of the PROV data model. W3c recommendation,
World Wide Web Consortium, 2013. URL https://www.w3.org/TR/2013/REC-prov-constraints-20130430/ .
Lancelot Da Costa, Thomas Parr, Noor Sajid, Sebastijan Veselic, Victorita Neacsu, and Karl Friston. Active
inference on discrete state-spaces: A synthesis. Journal of Mathematical Psychology , 99:102447, 2020. doi:
10.1016/j.jmp.2020.102447. URL https://arxiv.org/abs/2001.07203v2. Preprint reading: arXiv:2001.07203v2.
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer
and Geoff Sutcliffe, editors, Automated Deduction – CADE 28 , volume 12699 of Lecture Notes in Computer
Science, pages 625–635. Springer, 2021. doi: 10.1007/978-3-030-79876-5_37. URL https://link.springer.com/ch
apter/10.1007/978-3-030-79876-5_37 .
51

## Page 53

David S. Douglass, Adam Pease, Daniel Ari Friedman, Jessica Angeli Balbuena, Rhea Chokhalingam, Ana Mag-
dalena Hurtado, Maria Luiza Iennaco, V. Bleu Knight, Scott Ryan Maybell, Ali Rahmjoo, Paulo Duare Andrade
Sayeg, Jakub Smékal, Dean Tickles, and Alex Vyatkin. Aligning active inference ontology to SUMO. Zenodo
preprint, June 2024. URL https://zenodo.org/records/11463326 . Preprint, version v2, June 3, 2024; includes
the accompanying alignment workbook.
Karl Friston. The free-energy principle: a unified brain theory? Nature Reviews Neuroscience , 11:127–138, 2010.
doi: 10.1038/nrn2787. URL https://doi.org/10.1038/nrn2787.
Karl Friston, James Kilner, and Lee Harrison. A free energy principle for the brain. Journal of Physiology-Paris ,
100(1–3):70–87, 2006. doi: 10.1016/j.jphysparis.2006.10.001. URL https://www.fil.ion.ucl.ac.uk/~karl/A%20fr
ee%20energy%20principle%20for%20the%20brain.pdf.
Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics.
Advances in Mathematics , 370:107239, 2020. doi: 10.1016/j.aim.2020.107239. URL https://arxiv.org/abs/1908
.07021v8.
Andrew Gelman, Aki Vehtari, Daniel Simpson, Charles C. Margossian, Bob Carpenter, Yuling Yao, Lauren Kennedy,
Jonah Gabry, Paul-Christian Bürkner, and Martin Modrák. Bayesian workflow, 2020. URL https://arxiv.org/
abs/2011.01808v1. Version 1.
Tilmann Gneiting and Adrian E. Raftery. Strictly proper scoring rules, prediction, and estimation. Journal
of the American Statistical Association , 102(477):359–378, 2007. doi: 10.1198/016214506000001437. URL
https://sites.stat.washington.edu/people/raftery/Research/PDF/Gneiting2007jasa.pdf.
Tilmann Gneiting, Fadoua Balabdaoui, and Adrian E. Raftery. Probabilistic forecasts, calibration and sharpness.
Journal of the Royal Statistical Society: Series B , 69(2):243–268, 2007. doi: 10.1111/j.1467-9868.2007.00587.x.
URL https://academic.oup.com/jrsssb/article/69/2/243/7109375.
Joseph A. Goguen and Rod M. Burstall. Institutions: Abstract model theory for specification and programming.
Journal of the ACM , 39(1):95–146, 1992. doi: 10.1145/147508.147524. URL https://courses.grainger.illinois.ed
u/cs522/sp2016/InstitutionsAbstractModelTheory.pdf.
John Harrison. Floating-point verification using theorem proving. In Marco Bernardo and Alessandro Cimatti,
editors, Formal Methods for Hardware Verification , volume 3965 of Lecture Notes in Computer Science , pages
211–242. Springer, 2006. doi: 10.1007/11757283_8. URL https://www.cl.cam.ac.uk/~jrh13/papers/sfm.pdf.
Robert E. Kass and Adrian E. Raftery. Bayes factors. Journal of the American Statistical Association , 90(430):
773–795, 1995. doi: 10.1080/01621459.1995.10476572. URL https://www.stat.cmu.edu/~kass/papers/bayesfact
ors.pdf.
Timothy Lebo, Satya Sahoo, and Deborah McGuinness. PROV-O: The PROV ontology. W3c recommendation,
World Wide Web Consortium, 2013. URL https://www.w3.org/TR/2013/REC-prov-o-20130430/ . Editors;
Recommendation of 30 April 2013.
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM , 52(7):107–115, 2009. doi:
10.1145/1538788.1538814. URL https://xavierleroy.org/publi/compcert-CACM.pdf.
Luc Moreau and Paolo Missier. PROV-DM: The PROV data model. W3c recommendation, World Wide Web
Consortium, 2013. URL https://www.w3.org/TR/2013/REC-prov-dm-20130430/ .
Ian Niles and Adam Pease. Towards a standard upper ontology. In Proceedings of the International Conference
on Formal Ontology in Information Systems , pages 2–9. ACM, 2001. doi: 10.1145/505168.505170. URL
https://adampease.com/FOIS.pdf.
Ian Niles and Adam Pease. Linking lexicons and ontologies: Mapping WordNet to the Suggested Upper Merged
Ontology. In Proceedings of the International Conference on Information and Knowledge Engineering , volume 2,
pages 412–416. CSREA Press, 2003. URL https://adampease.com/Niles-IKE.pdf.
OntologyPortal. SUO-KIF: Formalizing terms, n.d.a. URL https://github.com/ontologyportal/sumo/wiki/SUO%
E2%80%90KIF-Formalizing-Terms.
52

## Page 54

OntologyPortal. Suggested Upper Merged Ontology: pinned Merge.kif source, n.d.b. URL h t
t p s : / / g i t h u b . c o m / o n t o l o g y p o r t a l / s u m o / b l o b / e f c d 0 5 9 f 8 f e e b f e 3 4 8 8 a 0 9 f 5 7 5 f 8 8 d 4 d
0 0 9 b 1 e 5 c / M e r g e . k if. Revision efcd059f8feebfe3488a09f575f88d4d009b1e5c; complete file SHA-256
2e4c3d6b8392a4cb6fbeccb6eb7441e11d6b45592082333285c951fd7c7d3e14; selected formula locators are given
with the claims.
OntologyPortal. Suggested Upper Merged Ontology: Source distribution, n.d.c. URL https://github.com/ontolog
yportal/sumo. The evaluated revision and file identities are recorded in Rikishi’s source lock and source manifest.
OntologyPortal. SUMO–WordNet mapping files and format documentation, n.d.d. URL https://github.com/ont
ologyportal/sumo/tree/master/WordNetMappings . Mapping relations are documented in the file headers; the
inspected revision is recorded in Rikishi’s source lock.
Adam Pease. Standard Upper Ontology Knowledge Interchange Format . Articulate Software, June 2009. URL
https://github.com/ontologyportal/sigmakee/blob/master/suo-kif.pdf . Manual dated June 18, 2009; the
inspected copy is bound to the Sigma revision in Rikishi’s source lock.
Adam Pease. Converting the Suggested Upper Merged Ontology to typed first-order form, 2023. URL https:
//arxiv.org/abs/2303.04148.
Adam Pease and Stephan Schulz. Knowledge engineering for large ontologies with Sigma KEE 3.0. In Automated
Reasoning, volume 8562 of Lecture Notes in Computer Science , pages 519–525. Springer, 2014. doi: 10.1007/978-
3-319-08587-6_40. URL https://adampease.com/pe_sch_sigma.pdf.
Giles Reger. Better proof output for Vampire. In Vampire 2016. Proceedings of the 3rd Vampire Workshop ,
volume 44 of EPiC Series in Computing , pages 46–60. EasyChair, 2017. doi: 10.29007/5dmz. URL https:
//easychair.org/publications/paper/1DlL.
David I. Spivak and Robert E. Kent. Ologs: A categorical framework for knowledge representation. PLOS ONE ,
7(1):e24274, 2012. doi: 10.1371/journal.pone.0024274. URL https://journals.plos.org/plosone/article?id=10.13
71/journal.pone.0024274.
TPTP. The SZS ontologies, n.d. URL https://szs.tptp.org/.
Timothy G. Trucano, Laura P. Swiler, Takeru Igusa, William L. Oberkampf, and Martin Pilch. Calibration,
validation, and sensitivity analysis: What’s what. Reliability Engineering and System Safety , 91(10–11):1331–
1357, 2006. doi: 10.1016/j.ress.2005.11.031. URL https://www.sciencedirect.com/science/article/pii/S0951832
005002437.
Tim van Erven and Peter Harremoës. Rényi divergence and Kullback–Leibler divergence. IEEE Transactions on
Information Theory , 60(7):3797–3820, 2014. doi: 10.1109/TIT.2014.2320500. URL https://arxiv.org/abs/1206
.2459v2.
53