The project has no sorry, but selected operator-algebraic, perturbative, and
externally quoted results are represented by documented Lean axioms. This page
states the policy and trust-boundary categories; it is not a generated or
complete declaration register.
The JSON catalogue remains incomplete and non-authoritative until #5228. Until then, complete current declaration-level axiom occurrences, status, and capstone decisions remain in the interim legacy catalogue pages.