14. Proof fields, closure, and executable certificates

A reasoning archive contains more than its final proofs. It may retain alternative derivations, conjectures, unsuccessful proposals, and observations that later become obsolete. A checker must know which of those records it is permitted to use. Otherwise an archive that is useful for discovery can become an unsound source of premises.