Exact synthesis of small Boolean functions in three bases: an annotated atlas for n ≤ 5

A map of a corpus that is mostly published; where a fact is not in a public deposit, §7 says so. It contains no new result. For each fact it says where the fact is, what certifies it, and what remains open. The cross-base laws belong to the companion paper Base laws for the formula–circuit gap at four inputs: AIG, MIG and XAG compared class by class (doi:10.5281/zenodo.23913155), so this document stays an atlas: when it needs a law, it points to that paper. Scope: Boolean functions of n ≤ 5 variables, exact synthesis (proved minimum size, not a heuristic bound), in three bases. Out of scope: depth, unbounded fan-in, asymptotic families, multi-output functions, and anything without a checkable artifact.