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

    If the execution map is deterministic in the coordinates fixed by Definition [ftip-00HF], replaying the same inputs, revision, environment, and seed produces the same event trace.

    Proof. 

      Induct over the finite event sequence. Equal initial coordinates give equal first events; determinism and equal prefixes give the next event.