Theorem. Conditions for an admissible commit decision [ftip-00IL]
✍️source

Under the typed audit record of Definition [ftip-00HL], a commit is admissible exactly when all required checks pass, the digest matches, and the recorded decision is \(commit\), as proved in Theorem [ftip-00HM].

Theorem. Conditions for an admissible commit decision [ftip-00IL]
✍️source

Finite probability and execution results [ftip-00I2]

Convention. Domains of the finite results [ftip-00I5]

Theorem. Independent discovery probability [ftip-00I7]

Theorem. Discovery budget for a failure threshold [ftip-00I8]

Theorem. Support under finite exponential tilting [ftip-00I9]

Theorem. Uniform proxy error and objective regret [ftip-00IA]

Theorem. Utility under a change of evaluation law [ftip-00IB]

Theorem. Response classes under feedback refinement [ftip-00IC]

Theorem. Equal execution inputs give equal replay traces [ftip-00IJ]

Theorem. Observational equivalence under a common update kernel [ftip-00IK]

Theorem. Conditions for an admissible commit decision [ftip-00IL]
✍️source

Theorem. Admission of a finite audit plan [ftip-00IM]

Definition. An audit-before-commit record [ftip-00HL]

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

Proof.