Minimum Safe Observation Alphabet

Abstract

Safe-compatible partitions determine the exact minimum safe observation alphabet.

Theorem 1.1 (Safe partitions and deterministic safe observers have the same minimum size).

$$\begin{gathered} \forall X,A\in \mathrm{Type}, \\ Legal:X\to \mathrm{Set}\left(A\right),ch{i}_{safe}\in \mathbb{N}, \\ \mathrm{IsLeast}\left(\{k\in \mathbb{N}\mid \mathrm{SafeCompatiblePartition}\left(Legal,k\right)\},ch{i}_{safe}\right)⟺\mathrm{IsLeast}\left(\{k\in \mathbb{N}\mid \mathrm{SupportsDeterministicSafePolicy}\left(Legal,k\right)\},ch{i}_{safe}\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Agency/MinimumSafeObservationAlphabet.minimum_safe_observation_alphabet (✓ std3). ∎

Source. Repository-derived.

Commentary.

A safe-compatible partition is represented by a surjective readout into Fin k. Surjectivity ensures that all k observation values occur, and each effective fiber must admit one action legal at every state in that fiber.

The repository’s deterministic safe-policy existence theorem identifies this fiber condition with a policy on the effective observation values, for each fixed k.

Transporting that equivalence through IsLeast proves both required halves: the minimum partition size is attained by a safe observer, and every safe observer uses at least that many realized values.

References

• Truth anchor: D5/S3/ConceptDynamics/Agency/MinimumSafeObservationAlphabet.minimum_safe_observation_alphabet
• Dependency: D5/S3/ConceptDynamics/Agency/DeterministicSafePolicyExistence