Specify the Version Gate business algorithm

[k-barseghyan]

What changed

• rewrote docs/business-rules.md as the normative, implementation-neutral concurrency specification
• defined the per-resource abstract state, fixed safety invariants, linearization boundary, bootstrap state, immutable policy, and permanent snapshot model
• specified operation-ID replay, renewable leases, atomic expiry, fencing assumptions, stale-base rejection, uncertain-write recovery, and retryable snapshot attempts
• added readable Mermaid yes/no trees for retry handling, write admission, live-read admission, snapshot admission, and stored snapshot retrieval
• defined deterministic race and rejection precedence and explicitly excluded fairness guarantees, retention, dynamic policy, and implementation concerns

Why

The previous document mixed target rules with implementation planning and left several safety-relevant cases undefined. This revision is intended to be the human-readable basis for a corresponding TLA+ model.

Important decisions made explicit

• an uncertain or expired write quarantines the resource until verified recovery
• pre-existing data enters through the normal first fenced write; there is no special initialization shortcut
• snapshot policy is immutable, retention is excluded, and snapshots are permanent
• snapshot support DISABLED disables both generation and retrieval
• immutable stored snapshot retrieval remains available during recovery and reports recovery state
• the algorithm guarantees non-overlap of valid sessions; physical non-overlap additionally requires participant-side session and fencing enforcement

Validation

• only docs/business-rules.md changed
• the committed branch content exactly matches the reviewed draft
• GitHub-flavored Markdown renders successfully through Pandoc
• the prose, tables, race ordering, and Mermaid branches received independent consistency and TLA+-readiness passes

No implementation code was inspected or changed.