Six Birds Verified VII: Formation and Explanation

Abstract

A theory has to be formed, explained and run. Each step invites a shortcut: counting generators as if they counted roles, treating “why” as one status, and treating a running program as the object it runs. For finite systems this paper replaces each shortcut by exact mathematics. Formation is a generation calculus in which records are produced from seeds and admitted providers by finite rules. On three finite instances with 10, 16 and 121 records, the least number of providers that generate every record is 0, 1 and 2, while all six role meanings of Six Birds Theory remain separately representable. Explanation is a typed receipt whose ingredients are defined independently. A constructed normalizer returns a receipt exactly when the submitted evidence packet is valid, and that receipt meets the requested grade exactly when the packet supports every requested obligation. Realization induces a finite system on a quotient, stores it as tables and runs it; when every gate holds, the run agrees with the original on every word and formula. Two systems on four states with the same public behavior at every horizon are not conjugate, so a public theory does not determine its dynamics. Most results are formalized in Lean 4, and the formalization section lists the exceptions.