Papers · Foundations
Six Birds Foundations III: A Finite Audited Interaction Calculus for SBT
A finite bookkeeping system for how the six roles act on each other, with every claim audited.
In plain words
Foundations I and II gave the six birds: descent, representability, route mismatch, refinement, packaging and audit. They did not give one framework that records how the six act on each other. This paper builds one. It is a finite typed calculus. Each interaction is written as a directed cell, one role acting on another, judged under a named instrument. Each cell gets a status from a fixed list, such as action, blocked or absent. Recorded defects keep a claim from being accepted. Every claim carries a register of what it does not say.
The mathematics inside the theorems is standard, and the paper says so plainly: descent through a finite quotient, idempotent saturation, the duality between cycles and cochains. What is new is the calculus, its scope discipline and its countermodels. One headline result: there is no total algebra on the six symbols, because a cell's status is not fixed by which two roles it pairs. Another: an instrument cannot certify its own complete soundness. A finite stack of instruments can be audited from one level up, but the top level is never final.
Twelve small countermodels each block one specific overclaim, such as packaging without closure, holonomy without drive, or the same pair of roles with different statuses. Four model families, finite stochastic PICA, audited Cantor shells, abstract interpretation and graph cohomology, each realize a declared part of the calculus and nothing more. A Lean 4 track, with a strict validator, checks that the numbered definitions and claims have matching Lean declarations.
What it shows
- No total six symbol algebra: a cell's status does not factor through its pair of roles.
- Same level self audit fails, while a finite rotating audit can check every level below it.
- Twelve finite countermodels, each blocking one named overclaim.
- Four scoped model realizations and a Lean 4 coverage audit.
What it does not claim
It does not prove a universal exact six theorem, a universal six symbol algebra, a unique decomposition, or any empirical realization. The underlying mathematics is standard and not claimed as new, and the model realizations are scoped rather than theorem grade.
Cite
Tsiokos, I. (2026). Six Birds Foundations III: A Finite Audited Interaction Calculus for SBT. Zenodo. https://doi.org/10.5281/zenodo.23096391