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

A coarse-grained description drops distinctions and hopes to keep what matters. This paper gives an exact calculus, for finite systems, of what coarse-graining loses, what it gains, and whether it can be done in stages. Part I shows that coarsening can gain a law while losing distinctions. A coarser description can carry an exact autonomous dynamics that a finer one lacks. The smallest example has four states, and its minimum witnesses fall into exactly nine isomorphism classes. On explicit quotients of binary algebras, no function of the number of predicates lost determines the number of equations gained. Part II compares thirty-two directed pairs of notions of “sameness”, from kernel equality and congruence to lumpability, bisimulation, predictive equivalence and tolerance. Each implication is proved, or refuted by a countermodel of minimal size together with the hypothesis that repairs it, when one exists. Part III compares coarse-graining in one step with coarse-graining through an intermediate layer. The difference has an exact closed form. It is at most the error of reconstructing the middle layer times how strongly the later dynamics separates states that the middle layer identifies, with sharp constant one. It vanishes for every input exactly when that separation is zero, and for towers of many layers the local bounds add. All results are finite and exact, with Lean 4 formalizations for all three parts.