Certificates

Each check in a decision record names the mathematical result it relies on, so an auditor can see what is proven and what is a practical stand-in. This module holds those references as constants (one CatalogRef per result, with a number in the companion math catalog, a title, whether a machine-checked proof covers it, and a note). You rarely import it; you read its values inside channels[].catalog on a record.

Public here: nothing at top level. The REF_* constants and trust_for are stable to read. What the trust levels mean: Trust levels and honest limits; where each result stands: Where each result stands.

certificates

Catalog pins used by the runtime.

Only claims that this library actually implements or enforces are listed. LEAN means the Comparator statement in lean/docs covers the check. PAPER means the manuscript states it and the runtime treats it as policy. OPERATIONAL means a calibrated stand-in with an explicit constant.