Theorem. Audit-before-commit safety gate [ftip-00HM]
✍️source

    A commit decision is admissible only if every required check in an Definition [ftip-00HL] record is pass, the audited digest equals the proposed record digest, and the decision is \(commit\).

    Proof. 

      Admissibility is defined as the conjunction of these three recorded conditions; failure of any conjunct yields hold or reject.