Six Birds Foundations VIII: A Typed Calculus of Coarse-Graining

In plain words

A coarse description drops some distinctions and hopes to keep what matters. Thermodynamics drops the positions of molecules. A Markov model of a protein drops most of its shapes. A verification tool replaces a program by a much smaller abstraction. This paper gives an exact calculus, for finite systems, for three questions that come up whenever two such layers are compared. What does coarsening lose? What can it gain? And does coarsening in two steps agree with coarsening in one?

Part one shows that forgetting can create a law. A finer view may have no exact rule for what it sees next, while a coarser view of the same system does. Four states is the smallest case where this happens, and the smallest examples fall into exactly nine types. On an explicit family of algebra quotients, what is lost does not predict what is gained. Part two settles thirty two directed comparisons between notions of sameness, from congruence and lumpability to bisimulation, predictive equivalence and tolerance. Each false implication gets a countermodel of minimal size and, when one exists, the hypothesis that repairs it.

Part three compares a direct coarse graining with one that passes through a middle layer. Their difference has an exact formula. It is at most the error of rebuilding the middle layer times how strongly the later dynamics separates states that the middle layer lumps together, and the constant one is sharp. For tall towers the local bounds simply add. All three parts are formalized in Lean 4.

What it shows

• Coarsening can create an exact law; four states is the minimum, with nine types of smallest example.
• An atlas of thirty two comparisons between notions of sameness, each proved or refuted by a minimal countermodel.
• A sharp product bound on the gap between staged and direct coarse graining, adding up along towers.
• The usual audits of a layer do not determine that gap.

What it does not claim

Everything is finite and exact; nothing continuous, approximate or about infinite histories is claimed. Many individual facts are classical, and the contribution is sharpness rather than new phenomena. It does not prove the separate gain inequality posed in Foundations I.

Cite

Tsiokos, I. (2026). Six Birds Foundations VIII: A Typed Calculus of Coarse-Graining. Zenodo. https://doi.org/10.5281/zenodo.23097905