Indexed Common-Source Upper Bound

Abstract

An indexed family of messages cannot jointly distinguish more than its common source readout.

Theorem 1.1 (The joint message readout remains below its common source).

$$\begin{array}{r}\forall I,X,B:\mathrm{Type},M:I\to \mathrm{Type},\\ m:\forall i:I,X\to M_i,s:X\to B,\\ (\forall i:I,\mathrm{Refines}\left(m\left(i\right),s\right))\Rightarrow \mathrm{Refines}\left(\mathrm{jointReadout}\left(m\right),s\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Communication/IndexedCommonSourceUpperBound.indexed_common_source_upper_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each component premise supplies a factor from the common source value to that message value. The proof selects those factors and bundles their outputs into the canonical dependent joint readout.

Evaluating the assembled factor at a state reduces componentwise to the given message factorization, so the entire message family remains a postprocessing of the same source.

References

• Truth anchor: D5/S3/ConceptDynamics/Communication/IndexedCommonSourceUpperBound.indexed_common_source_upper_bound
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion