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

If the execution map is deterministic in all coordinates fixed by Definition [ftip-00HF], then equal input, revision, environment, and seed records produce equal finite traces, as proved in Theorem [ftip-00HG].

Theorem. Equal execution inputs give equal replay traces [ftip-00IJ]
✍️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]
✍️source

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

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

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

Definition. A replay contract [ftip-00HF]

Theorem. Deterministic replay reproduces a recorded trace [ftip-00HG]

Proof.