We formalize a dependency-closure law for a theorem-backed audit stack. Given a fixed policy hash, a hash-addressed evidence set, non-interference preservation (NIPT), and earliest-failure total-order soundness (EFTS), we prove existence and uniqueness of a terminal certificate object whose content and hash are deterministic functions of the inputs. We further show that the certificate forms a closure of the dependency DAG of six theorems (CEIT, CEIT-CS, AINCT, TEANT, NIPT, EFTS), yielding an auditable, reproducible, non-reversible terminal record.