Shared Source Observation Dependence

Abstract

Two copies of one fair Boolean source agree surely but are not independent.

Theorem 1.1 (Shared fair-source observations are not independent).

$$\begin{array}{c}P(X_p=X_q)=1\wedge \\ P(X_p=1)P(X_q=1)=\frac{1}{4}\wedge \\ P(X_p=1)P(X_q=1)\ne P(X_p=1\wedge X_q=1)\wedge \\ P(X_p=1\wedge X_q=1)=\frac{1}{2}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Information/SharedSourceObservationDependence.shared_source_observations_are_not_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source law assigns mass one half to each Boolean state. Both observation channels copy that same source state.

Their equality event therefore has probability one. Each one-event has probability one half, so the marginal product is one quarter.

The joint one-event is the single true source state and has probability one half. Its mismatch with the marginal product is the explicit failure of independence.

References

• Truth anchor: D5/S3/ConceptDynamics/Information/SharedSourceObservationDependence.shared_source_observations_are_not_independent
• Dependency: D5/S3/ConceptDynamics/Information/RefinementEntropyMonotonicity