Preserve transcript-dependent invariants of probabilistic automata #222

The invariant in ProbStep.belief_simulation depends on inputs. Relating retained randomness to public outputs needs an invariant of the full transcript.

Add a standalone law in RandomSystems/System/ProbAutomaton.lean:
s ∈ (step.belief D μ h).support → inv h s,
assuming inv [] on the initial support and preservation by every supported outcome of each query admitted by D.

Reuse the existing belief, transition and distribution-support laws. Keep arbitrary domains and hidden state types; require no simulation kernel or query bound beyond the domain.

Acceptance:

• Prove the law for invariants that read replies.
• Test a retained-state/output relation and the zero belief after a rejected query, with unrestricted hidden state.
• Reuse it for an actual transcript-to-retained-state correspondence.
• Pass focused/full builds, standard linters and the axiom audit.

Related: #31 extracted recording-automaton facts; #221 provides state-map equality. Neither supplies this transcript-dependent invariant law.