To Become a Stone with Six Birds: A Physics is A Theory

Physics routinely replaces a detailed description with a coarser one — density matrices with probabilities, kinetic distributions with fluid moments, resolved fields with filtered fields, heterogeneous ensembles with averages — and then treats the coarse description as a theory in its own right. This paper describes each such step with one template from the Six Birds emergence calculus: a lens that records what is kept, a completion that rebuilds a fine state from it, and the fine-level dynamics. Up to three checks then become possible: whether packaging (lens followed by completion) is idempotent, whether a distinguishability audit such as relative entropy is non-increasing under coarse-graining, and whether packaging commutes with the dynamics (route mismatch). The checks are applied, wherever they are defined, in four settings: Quantum dephasing. Dephasing is an exact projection; for partial dephasing the coherence defect is exactly λ(1−λ) times the trace distance to the dephased state, and the route mismatch with unitary evolution scales exactly linearly in λ. A regression suite checks the quantum data-processing inequality. Kinetic theory to fluids. For a three-velocity BGK model the maximum-entropy local equilibrium is given in closed form (including |u| = 1), so the closure is idempotent to machine precision. A proposition, also proved in Lean, shows that under exact macroscopic dynamics evolve-then-package is idempotent precisely when that dynamics is, so its defect records macroscopic evolution rather than closure error. Three controlled failure modes show what a small defect can and cannot reveal. Filtering and large-eddy simulation. For viscous Burgers flow, filtering the right-hand side differs from evaluating it on the filtered field by minus the derivative of half the subgrid stress; a conservative pseudo-spectral scheme reproduces this identity to round-off, and a heat-flow control separates a nonzero stress from a dynamics that feels it. Averaging and backreaction. For y′ = y², Jensen’s inequality fixes the sign of the averaging gap, and an exact scaled-Beta moment completion gives a closure that is idempotent by construction yet fails to commute with the flow. Exact statements rest on short proofs, a Lean 4 / mathlib library whose audited declarations use only the standard axioms, and closed-form completions. Numerical statements come from deterministic scripts with null controls, direct audits of each completion, and regression tests; every figure and table is regenerated from the accompanying repository. The paper derives no continuum theories; its contribution is a common, checkable vocabulary for comparing closures across physics. Version 3 follows a full mathematical review of the paper, the Lean library, and the code, and a rewrite for readability; Appendix C of the paper lists the changes.