[MarcIlunga]

The probabilistic-automaton and program-attachment proofs repeated the recording invariant's support argument, and replyLaw named both an automaton step and a program invocation. Both proofs now reuse recording_reachable directly and share recording_init_reachable. The program's law explicitly names its memoryless inside replies; its definition and the public attachment statements keep their existing mathematical meaning.

Previous declaration	Replacement
Program.replyLaw	Program.memorylessReplyLaw
Program.replyLaw_inl	Program.memorylessReplyLaw_inl
Program.replyLaw_succ_inr	Program.memorylessReplyLaw_succ_inr

All repository consumers and documentation links are updated. The recursive reply law and the recording invariant are explained beside their definitions/proofs. Claude reviewed the comments with only file-reading/editing tools, with no shell, Git, external tools or hooks. The coordinator checked the resulting diff.

Validation: focused builds through PRG length extension and the systems axiom checks, standard Mathlib lint on every changed Lean file, the affected-module axiom audit, source checks and git diff --check. Classical openings in the ideal-system definitions were narrowed to their definitions to satisfy the standard linter.

Fixes #31.