A2 is withdrawn as a premise

Agent-decided. Freshness of opened obligations was claimed to make transfer chains terminate. It does not; the interval does. A hand-built cycle violating freshness in every representable way satisfies the corrected theorem. A2 is retained as fresh_by_construction, a check on the encoding, and named in no theorem.