Finite Extraction of a Faithful Observer Family

Abstract

A faithful observer family on a finite state carrier contains a faithful finite subfamily.

Theorem 1.1 (Full joint faithfulness is witnessed by finitely many coordinates).

$$\begin{array}{r}\forall X,I:\mathrm{Type},O:I\to \mathrm{Type},\\ [\mathrm{Finite}(X)],q:\forall i:I,X\to O(i),\\ \mathrm{Injective}(\mathrm{jointReadout}(q))⟹\\ \exists J:\mathrm{Finset}(I),\mathrm{Injective}(\mathrm{jointReadout}(i:\{i:I\mid i\in J\}\mapsto q(i))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Faithfulness/FiniteFaithfulSubfamilyExtraction.finite_faithful_subfamily_extraction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The full observer is the canonical dependent joint readout of the coordinate family. Its injectivity means every distinct pair of states is separated by at least one coordinate.

There are only finitely many distinct state pairs. A finite-subcover argument selects finitely many separating coordinates, and their restricted dependent joint readout remains injective.

References

• Truth anchor: D5/S3/ConceptDynamics/Faithfulness/FiniteFaithfulSubfamilyExtraction.finite_faithful_subfamily_extraction
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion