Why Mathematics Even Works

Many objects that mathematics uses to solve a problem do not belong to the setting in which the problem is posed: imaginary numbers are not real, infinitesimals are not real numbers, roots of an irreducible polynomial need not lie in the base field, and a cohomology class is not a function on vertices. Yet the calculations end with answers in the original setting. We make this pattern precise. A lower problem fixes what its own candidates can try and which answers it accepts; a promoted layer supplies a hidden structure with no lower counterpart and a selected expression that returns an accepted answer under explicit checks. We bundle these data into a Strict Audited Utility certificate and prove that it licenses the returned answer but not the hidden structure as a lower object, and that concluding usefulness also requires the judging instrument’s permission. For root problems, non-descent is forced: if a lower operation F has no k-th root among the lower operations, and a promoted operation G, observed through a surjective map q, satisfies q ∘ Gkm = F ∘ q, then G has no lower counterpart through q; examples show that the hypotheses are needed. In an accepted computation modelled as a finite dependency graph, hidden content on which the answer depends must cross back to the lower layer at a checked boundary, and the rest can be replayed from lower data under explicit conditions; but an audit can make a hidden step essential even though the step descends, so essential use alone does not force non-descent. Complex numbers, dual numbers, Galois roots, and graph cohomology are worked out exactly, including the four-phase model of a hidden square root of reversal, polynomial first jets, the field ℚ(√2) with trace 0, norm −2 and orbit polynomial t2 − 2, and the triangle datum (1, 0, 0); they carry four distinct labels in a declared grammar of return constructors, and a shared shape transfers obligations, not evidence. The headline results are verified in Lean 4; source, Lean code, and reproducibility scripts are at https://github.com/ioannist/six-birds-math-usefulness. Version 2 replaces the general trace-necessity, normal-form, canonical-minimality, and six-role statements of version 1 by the results above, records the stronger statements as open problems with counterexamples to their unrestricted forms, and corrects several definitions; Appendix F of the paper lists the changes.