The Minimal Runtime Axiom

Runtime Is Proof of Ignorance: A Type-Theoretic and Category-Theoretic Formalization of the Compile-Time/Runtime Boundary

Matthew Long, The YonedaAI Collaboration, YonedaAI Research Collective

The Axiom

A decision d reaches runtime if and only if no static witness can be constructed for it:

R(P) = D(P) \ C(P)

where C(P) = { d in D(P) | there exists a static witness w_d = (tau, pi, sigma) }

• tau -- a type encoding the invariant
• pi -- a proof term (inhabitation of tau)
• sigma -- a staging certificate that pi is constructible before execution

The Three Corollaries

1. Runtime Irreducibility: A decision is legitimately runtime iff it depends on omega-data (user input, I/O, time, nondeterminism). Everything else is a failure of static reasoning.

2. The Duality: |R(P)| is proportional to the epistemic deficit of the type system. More expressive types yield smaller runtime sets.

3. The Yoneda Correspondence: Runtime type inspection is isomorphic to failure of the Yoneda embedding.

The Principle

Every non-omega decision at runtime is a theorem waiting to be proven.

Paper

• PDF
• LaTeX Source
• Peer Review

Project Structure

minimal-runtime-axiom/
  papers/
    latex/    -- LaTeX source
    pdf/      -- Compiled PDF
  reviews/    -- Peer review
  docs/       -- Website
  src/        -- Source code / examples

License

Copyright 2026 YonedaAI Research Collective.