1. The written form. The written form consists of machine-readable symbols, each with a type and a signature.

• In this deck a type labels a symbol in the written form, whereas a kind sorts the objects in the domain.

2. The domain of meaning. The objects we model, such as state spaces, probability laws, value functions and operators, are sorted into kinds with relations between them.

3. The map Υ (upsilon). Explicit interpretation rules specify how typed expressions denote objects of the matching kind.

Excludes. The ontology excludes three misreadings. A missing annotation may not be read as the absence of a function, under the open-world assumption, which treats an absent statement as unknown rather than false. A NOT qualifier, which records that a gene lacks a function, may not be read as an inconclusive result. A term may not be read by its name rather than by its definition and relations, since a label must be unique and a definition must always denote the same referents (principles 12 and 19 of the OBO Foundry, the body that sets the rules for biomedical ontologies).

For economics. A model's object is named by a term with a definition and relations, not by a variable name. The role tags !ctrl and !vlu and the law line of a stage file play that part, as the sboTerm of the Systems Biology Ontology does for a rate law in SBML, the exchange format for biochemical models.

Excludes. The ontology excludes a model confused with the system it models and a model variable confused with the physical quantity it stands for. The relation models joins a model to its system, while correspondsToQuantity pairs a variable with a quantity, as a declared domain excludes the deck's function on the wrong space (slide 55).

For economics. OntoCAPE is the nearest case to Project A because it is an ontology of models themselves. Model variables, equation systems and solution strategies are kinds in its modules (its sub-ontologies), so that a process model and its solver are distinct typed objects, as Υ and Ρ keep a model apart from its numerical method.

Excludes. The ontology excludes a quantity name read as any of several kinds, since a SWEET class fixes the kind by its definition and by its place among realms (SWEET's divisions of the Earth system), quantities and phenomena. The Climate and Forecast (CF) standard names, published as SKOS concepts (the W3C's format for agreed lists of terms) on the NERC vocabulary server, each linked to its canonical unit, settle the same question for a variable such as temp in a netCDF data file (a format for climate data). In the deck's terms this is the question of the shock law (slide 30) and of timing stated in words (slide 31).

For economics. The comparison paper of the special issue that Project A proposes needs a vocabulary of this kind: which object each team reports, a value or a marginal value function, on which state and under which timing, as in the comparison projects that den Haan, Judd and Juillard (2010, 2011) introduced.

Excludes. The ontology excludes an issuer read as the obligor (the party that owes the payments) of a bond and a notional amount read as a principal, since each is a defined class or property (OWL's word for a relation). The 2023 revision of the Swaps ontology separated the nominal from the notional amount, which its change note says "were confused". In the deck's terms these are a function on the wrong space (slide 55) and the shock law (slide 30).

For economics. FIBO is finance's own ontology, with the Bureau of Economic Analysis, the Bureau of Labor Statistics, the CFTC and the Office of Financial Research among its contributors. The 2026 rule under the Financial Data Transparency Act records it among the standards that commenters proposed. Project A's ontology names the objects of a model as FIBO names the parties and terms of a contract.

Excludes. The language excludes any reading of the axioms other than the one fixed by the Direct Semantics, OWL's official rule for what its statements mean, under which "the correct answer to any such question is predetermined by the formal semantics", whatever reasoner computes it (Primer §2). It also does not read a missing statement as false, and it does not assume that two names denote two individuals.

For economics. This is the three-part definition in full: classes, properties and individuals as typed symbols, an interpretation as the domain, and a map whose consistency (that the axioms do not contradict one another) and entailments (what follows from them) a reasoner decides. A stage file's Υ plays the part of the Direct Semantics, and the elaborator the part of the reasoner.

Autoformalization. The AI translates the paper into the written form, which the checker accepts or refuses (Wu et al. 2022, where the checker decided syntactic correctness and people judged faithfulness; AlphaProof, Hubert et al. 2026, which learned by reinforcement with Lean's kernel, the core program that checks each proof step, as the verifier).

Refuse and repair. The checker's refusal, with its rule named, is the AI's next prompt, as the error message of a proof assistant (a program that checks proofs) is in Baldur, a proof-repair system (First et al. 2023). The elaborator's rules shock-reintroduced and field-perch are messages of this kind.

Constrained generation. The AI's output is restricted, as the AI produces each word of its output, to the grammar of the written form, so that only its meaning remains to be checked (Poesia et al. 2022; Geng et al. 2023).

Compute, then answer. From the accepted file the ontology's programs compute Υ's object and Ρ's numbers (or, for a proof, the kernel checks it), so that the AI's answer to the user is built from that output rather than from its own guess.

Round trip. A second program writes the accepted object back into prose for a judge, a program or a second AI, to compare with the paper (Li et al. 2024), or regenerates the object for comparison with the original (Allamanis et al. 2024). Matsya, the project's assistant service, runs the first loop with the elaborator and two judges and the second with its comparator.

1. Objects and rounding. We use finite FP32 (IEEE 754 single-precision) values $x,y,z$. For the calculations below, $\operatorname{RN}_{32}$ rounds a real number to nearest FP32, with ties to even.

2. Interpretation Υ. Fused multiply-add rounds once; separate multiplication and addition round twice.

$$\begin{array}{ccc} \text{written form} & \xrightarrow{\quad\Upsilon\quad} & \text{domain of meaning} \\[0.5em] \mathtt{fma}(x,y,z) & \longmapsto & \operatorname{RN}_{32}(xy+z) \\[0.45em] \mathtt{add}(\mathtt{mul}(x,y),z) & \longmapsto & \operatorname{RN}_{32}\!\left(\operatorname{RN}_{32}(xy)+z\right) \end{array}$$

3. NVIDIA's example. Set $a=1+2^{-23}$ and $b=-(1+2^{-22})$.

$$\begin{aligned} \operatorname{RN}_{32}(a^2+b)&=\color{#1f476b}{2^{-46}} &&\text{(fused multiply-add)},\\[0.5em] \operatorname{RN}_{32}\!\left(\operatorname{RN}_{32}(a^2)+b\right)&=\color{#c41230}{0} &&\text{(multiply, then add)}. \end{aligned}$$