Minimum Installed Readout

Abstract

The attained minimum effective installed alphabet for arbitrary finite configuration families.

Theorem 1.1 (Sink labels plus an actual minimum enabled-event hitting set).

$$\begin{gathered} \forall E:\mathrm{Type},[\mathrm{Fintype}\left(E\right)][\mathrm{DecidableEq}\left(E\right)],F:\mathrm{Finset}\left(\mathrm{Finset}\left(E\right)\right),\mathrm{Nonempty}\left(F\right)⟹ \\ \exists H:\mathrm{Finset}\left(E\right),\mathrm{Hits}\left(F,H\right)\wedge |H|=\mathrm{hittingNumber}\left(F\right)\wedge \forall K:\mathrm{Finset}\left(E\right),\mathrm{Hits}\left(F,K\right)⟹\mathrm{hittingNumber}\left(F\right)\le |K|\wedge \forall Q:\mathrm{Type},r:\mathrm{State}\left(F\right)\to Q,\exists p:\mathrm{History}\left(E,Q\right)\to \mathrm{Decision}\left(F\right),\mathrm{Acquires}\left(r,p\right)⟹|\mathrm{sinks}\left(F\right)|+\mathrm{hittingNumber}\left(F\right)\le \mathrm{effectiveSize}\left(r\right)\wedge \exists r:\mathrm{State}\left(F\right)\to \mathrm{Sum}\left(\mathrm{State}\left(F\right),E\right),\mathrm{FiniteAcquirable}\left(r\right)\wedge \mathrm{effectiveSize}\left(r\right)=|\mathrm{sinks}\left(F\right)|+\mathrm{hittingNumber}\left(F\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

For the finite insertion model, sinks F contains the operational sinks. Hits F H means that H contains an enabled event for every nonsink. The number tau is the least cardinality of a hitting set, defined by minimization over natural numbers. The full event set hits every nonempty enabled set, so this minimum exists. The theorem includes both a minimizing set and its universal minimality property.

effectiveSize r is the cardinality of the actual image of r on F, regardless of its symbol carrier. For an arbitrary successful history policy, each sink has a private symbol. Every other effective fiber has a common enabled event, including singleton nonsinks. Choosing one event per such fiber produces a hitting set whose size is no larger than the number of those fibers. This proves the lower bound for unrestricted history policies.

For attainment, choose a minimum hitting set H and, at each nonsink C, choose one event in H enabled at C. Give a sink its own left label C and a nonsink the right label of its selected event. The two label families are disjoint. Each right-label fiber has a common enabled event, and every sink label is private. The finite acquisition criterion constructs the actual finite-table policy and proves the addition bound. Its effective image has at most card T plus card H symbols; the lower bound forces equality.

The family may be disconnected and need not contain the empty configuration or any root. The empty event type, a singleton family, and an all-sink family are included. If every state is a sink, the empty hitting set has minimum size zero and the readout directly identifies each state. Only the number of effective installed symbols is minimized. Same-run recovery of an earlier state, source transport and physical implementation require their own interfaces.

References

• Truth anchor: D5/S3/ConceptDynamics/Agency/MinimumInstalledReadout.installed_readout_optimum
• Dependency: D5/S3/ConceptDynamics/Agency/FiniteConfigurationAcquisition