docs: Update and clarify invariants

[johnsaigle]

• Make Pause invariant more explicit in terms of what pausing should limit
• Make it clear that the transceiver count should never go back to 0 after initial deployment
• Add information about registering vs enabling transceivers, why transceivers can't be deleted, and how it relates to business logic

[nvsriram]

We can maybe add a Maximum Threshold Requirement invariant as well since the threshold is always (after initial deployment):

1 <= threshold <= num_enabled_transceivers

[nvsriram]

LGTM!