Source Contribution Decomposition

Abstract

Source contributions have unique ordered decompositions exactly when disjoint.

Theorem 1.1 (Unique source decomposition is equivalent to disjointness).

$$\begin{array}{r}\forall R,Y:\mathrm{Type},\\ [\mathrm{Ring}(R)],[\mathrm{AddCommGroup}(Y)],[\mathrm{Module}(R,Y)],\\ \forall S_O,S_E:\mathrm{Submodule}(R,Y),\\ (\forall y:Y,y\in \sup (S_O,S_E)\Rightarrow \exists !d:S_O\times S_E,d_1+d_2=y)⟺\mathrm{Disjoint}(S_O,S_E).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/SourceContributionDecomposition.source_contribution_unique_decomposition_iff_disjoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let the observer and external sources be submodules of the same module. Every element of their sum has an ordered decomposition into one observer contribution and one external contribution.

Such decompositions are unique exactly when the two source submodules are disjoint. Equivalently, the addition map from their product into the ambient module is injective.

References

• Truth anchor: D5/S3/Observer/Linear/SourceContributionDecomposition.source_contribution_unique_decomposition_iff_disjoint