Minimum Complete Observers as Set Cover

Abstract

Minimum-cost complete finite observer families are exactly minimum-cost set covers.

Theorem 1.1 (The minimum complete observer problem is weighted set cover).

$$\begin{array}{r}\forall n:\mathbb{N},I:\mathrm{Type}(),O:I\to \mathrm{Type}(),\\ c:I\to \mathbb{R},q:\forall i:I,\mathrm{Fin}(n)\to O(i),\\ J:\mathrm{Finset}(I),\\ X:=\mathrm{Fin}(n),U_X:=\{\{x,y\}\mid x,y\in \mathrm{Fin}(n),x\ne y\},\\ \forall i\in I,D_i:=\{\{x,y\}\in U_X\mid q(i)(x)\ne q(i)(y)\},\forall J\in \mathrm{Finset}(I),C(J):=\sum _{i\in J}c(i),\\ (\mathrm{Injective}(\mathrm{jointReadout}(\mathrm{restrict}(q,J)))\wedge (\forall K:\mathrm{Finset}(I),\mathrm{Injective}(\mathrm{jointReadout}(\mathrm{restrict}(q,K)))\Rightarrow C(J)\le C(K)))⟺\\ (U_X=\mathrm{Union}(i\in J,D_i)\wedge (\forall K:\mathrm{Finset}(I),U_X=\mathrm{Union}(i\in K,D_i)\Rightarrow C(J)\le C(K))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ExperimentDesign/MinimumCompleteObserverSetCover.minimum_complete_observer_is_set_cover (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite state carrier is X = Fin n. Its unordered-pair universe contains exactly distinct state pairs, and the detector set for observer i contains the pairs on which its readout differs.

For each finite observer selection J, C(J) is the sum of the supplied real candidate costs. No positivity assumption is added: the theorem compares the same objective over two extensionally equal feasible families.

The imported finite experiment cover criterion identifies joint-readout injectivity with coverage of the full distinct-pair universe. It therefore transports both feasibility of J and its cost comparison against every feasible candidate K.

References

• Truth anchor: D5/S3/ConceptDynamics/ExperimentDesign/MinimumCompleteObserverSetCover.minimum_complete_observer_is_set_cover
• Dependency: D5/S3/ConceptDynamics/Experiment/FiniteExperimentCoverCriterion