Reference. Replay and audit conditions [ftip-00J1]

✍️sourceAGENTDRAFTED

Applying both deterministic replay and the audit gate requires the assumptions of Theorem [ftip-00HG] and Theorem [ftip-00HM], including the trace coverage described in Definition [ftip-00HI].