 Representation invariant

A representation invariant $I(r)$ specifies which concrete storage states $r$ are valid at the API boundary. Construction must establish it, and each completed operation must preserve it. Internal steps may temporarily violate it only while that state is inaccessible to observers; callbacks or concurrent access would require further reasoning.^[ref]

The short proof pattern is mathematical induction on the number of completed calls: the initial state satisfies $I$; every permitted transition from an $I$-state ends in an $I$-state; hence every state observable through the API satisfies $I$. An unrestricted external write falls outside this argument.