Why Mathematics Even Works

Many of the objects mathematics uses to solve problems do not live in the layer where the problem is posed. Imaginary numbers are not real, infinitesimals are not real scalars, roots of irreducible polynomials need not lie in the base field, and cohomology classes are not vertex potentials. We study this pattern by separating a lower layer, where a problem and its accepted answers are stated, from a promoted layer, where additional objects may be available. We define theory layers, promotion bridges, audited descending expressions, and the Strict Audited Utility (SAU) certificate, and we show that the certificate is extracted from strict useful traces rather than stipulated. The main results are an essential boundary necessity theorem, which forces a hidden non-descending support and an audited lower-layer boundary expression; a boundary normal form; a partial converse closing the circle from trace to validated certificate to accepted lower-layer answer; a soundness theorem specifying what an accepted certificate licenses; a classification of primitive boundary heads; four canonical witnesses — imaginary numbers, dual numbers, Galois roots, and graph cohomology — each instantiating a distinct minimal or universal profile; and a transfer theorem showing that a validated profile is portable under matching audit hypotheses while not identifying objects across domains. Together these results show that, in finite typed audited promoted-use traces, strict mathematical usefulness forces hidden non-descent paired with audited boundary descent. The scope is intentionally narrow. We do not claim that all mathematics is useful, that every promoted extension is useful, that hidden promoted objects belong to the lower layer, or novelty for the classical constructions themselves. A companion Lean development supplies substantive proofs for selected direct, computational, and definitional fragments and records the remaining theorems as proof-carrying traceability records.