Minimum Rollback Alphabet

Abstract

Exact finite rollback logs need as many labels as the largest process fiber.

Theorem 1.1 (The largest process fiber is the minimum rollback alphabet).

$$\begin{gathered} \forall X,Y:\mathrm{Type},[\mathrm{Finite}X][\mathrm{Fintype}Y],U:X\to Y, \\ {m}_U=\underset{y\in Y}{\max }\Vert \{x:X\mid U(x)=y\}\Vert , \\ (\forall M:\mathrm{Type},[\mathrm{Finite}M],L:X\to M, \\ \mathrm{Injective}(x\mapsto (U(x),L(x)))\Rightarrow m_U\le \Vert M\Vert )\wedge \\ \exists L:X\to \mathrm{Fin}(m_U),\mathrm{Injective}(x\mapsto (U(x),L(x))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/History/Coding/MinimumRollbackAlphabet.minimum_rollback_alphabet (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite state types X and Y and a process U from X to Y, the number mU is computed as the maximum cardinality of an actual fiber of U. Every log whose paired process-log record is injective has an alphabet of cardinality at least mU.

Conversely, each fiber is enumerated independently and embedded into the common type Fin mU. Equal process outputs then place two states in the same fiber, while equal labels force equality inside that enumeration, so the paired record is injective.

Pinned Mathlib supplies Nat.card_le_card_of_injective, Finite.equivFin, Fin.castLEEmb, Finset.le_sup, and Finset.sup_le. Repository and pinned-Mathlib searches found no declaration packaging the complete lower bound and attaining construction.

References

• Truth anchor: D5/S0/History/Coding/MinimumRollbackAlphabet.minimum_rollback_alphabet