Indexed Readout Monotonicity

Abstract

Enlarging a finite index set refines its dependent joint readout and shrinks its equality kernel.

Theorem 1.1 (Larger index sets refine joint readouts).

$$\begin{array}{r}\forall I,X:\mathrm{Type},\\ \forall O:I\to \mathrm{Type},\\ \forall q:\forall i:I,X\to O(i),\\ \forall J,K:\mathrm{Finset}\left(I\right),J\subseteq K\Rightarrow \mathrm{Refines}\left(q_J,q_K\right)\wedge \ker \left(q_K\right)\subseteq \ker \left(q_J\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementFactorization/IndexedReadoutMonotonicity.indexed_readout_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a dependent readout family q_i : X -> O_i and a finite index set J, the readout q_J records exactly the coordinates in J.

When J is contained in K, coordinate restriction from the K-output to the J-output is a forgetting map. This directly witnesses that q_K refines q_J.

Equality of the K-readouts can be evaluated at every coordinate coming from J. Hence every pair identified by q_K is also identified by q_J, giving the reverse kernel inclusion.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementFactorization/IndexedReadoutMonotonicity.indexed_readout_monotonicity
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion