# Covariance: symmetry, the affine rule, and why zero covariance does not imply independence

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-covariance/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-covariance-01 · production-20261019-adopted-96



## Goal and scope

On one exact finite joint law: (1) prove Cov(Y,X)=Cov(X,Y); (2) prove Cov(aX+b,cY+d)=ac·Cov(X,Y); (3) prove that independence of X and Y gives Cov(X,Y)=0, so a nonzero covariance refutes independence; (4) for the joint law with X uniform on −1, 0, 1 and Y=X², compute E[X], E[Y], E[XY] and Cov(X,Y)=0, and prove that X and Y are not independent.

Stays inside the MKO: every expectation is computed from one exact finite joint law (assumption a1); nonzero covariance can refute independence, while zero covariance cannot in general prove it (assumption a2). Correlation coefficients, conditional expectation and infinite sample spaces are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- distributive
- finite_sum_rules
- mul_comm
- numeric_evaluation
- marginal_def
- finite_sum_regroup


- G1 — (S,p) is a finite joint law: S consists of distinct integer pairs, each p(s)≥0 is an exact rational and Σ_{s∈S} p(s)=1. X and Y are the coordinates: at s=(x,y), X=x and Y=y. Every expectation is E[g]=Σ_{s∈S} p(s)g(s) with this one (S,p).
- G2 — a, b, c, d are real constants.
- G3 — Example: S={(−1,1),(0,0),(1,1)}, each pair with mass 1/3.


- (S,p) — finite joint law: distinct integer pairs with exact masses
- E[g] — expectation on the same joint law, Σ_{s∈S} p(s)g(s)
- \operatorname{Cov}(X,Y) — covariance E[XY]−E[X]E[Y]
- a,\ b,\ c,\ d — real coefficients of the affine maps
- S_X,\ S_Y — the sets of first and of second coordinates occurring in S
- p_X,\ p_Y — marginal masses of X and Y





## Rules and sources


- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- add_zero · prerequisite — Additive identity: u+0=u.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- mko_cov_def · cited — For X,Y on the same finite joint law, Cov(X,Y)=E[XY]−E[X]E[Y]. Covariance is symmetric in the two variables, and affine transformations satisfy Cov(aX+b,cY+d)=ac Cov(X,Y). · mko-covariance
- mko_expectation_def · cited — For nonempty finite S, normalized nonnegative weights w_s, and a real random variable X, define E[X]=Σ_(s∈S)w_s X(s). · mko-expectation
- mko_joint_def · cited — A two-dimensional finite joint distribution lists distinct pairs (x,y) and nonnegative exact masses summing exactly to 1. Marginals, rectangle events and single-pair masses all aggregate from that same joint law. · mko-finite-joint-distribution
- mko_indep_def · cited — Finite-valued X,Y are independent if every pair (x,y) satisfies P(X=x,Y=y)=P(X=x)P(Y=y). · mko-random-variable-independence
- marginal_def · prerequisite — Marginals: p_X(x)=P(X=x)=Σ_{y:(x,y)∈S} p(x,y) and p_Y(y)=P(Y=y)=Σ_{x:(x,y)∈S} p(x,y); P(X=x,Y=y) is p(x,y) when (x,y)∈S and 0 otherwise.
- finite_sum_regroup · prerequisite — Regrouping a finite sum: if a finite set is split into pairwise disjoint pieces (each element in exactly one), the sum over the whole set equals the total of the sums over the pieces; adding terms equal to 0 does not change a finite sum.
- L_lin_exp · lemma — On one finite joint law, for real functions U_1 to U_m of (X,Y) and reals c_1 to c_m: E[Σ_{k=1}^{m} c_k U_k]=Σ_{k=1}^{m} c_k E[U_k]; a constant c has expectation c.
- L_indep_prod · lemma — If X and Y are independent on a finite joint law, then E[XY]=E[X]E[Y].





## Main derivation

S01 · definitionBefore

X,\ Y\ \text{on one law}\ (S,p)

After

\operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y],\quad E[g]=\sum_{s\in S}p(s)\,g(s)

Conditions: \text{all expectations use the same }(S,p)

Rule: mko_cov_def · Uses: G1, mko_expectation_def

Leaf basis: mko_cov_def + mko_expectation_def + def_unfold

Define covariance by the MKO: compute E[X], E[Y] and E[XY], then subtract. All three expectations use the one joint law of G1, with sample space S and weights p (p is nonnegative and sums exactly to 1, the normalized weights the definition of expectation requires).



S02 · equivalentBefore

\operatorname{Cov}(Y,X)=E[YX]-E[Y]E[X]

After

\operatorname{Cov}(Y,X)=E[XY]-E[X]E[Y]=\operatorname{Cov}(X,Y)

Conditions: none

Rule: mul_comm · Uses: S01

Leaf basis: mul_comm + eq_replace + def_unfold

At every s∈S, Y(s)X(s)=X(s)Y(s) (real multiplication commutes), so YX and XY are the same function with the same expectation; E[Y]E[X]=E[X]E[Y] is also commutativity. So swapping the two variables does not change the covariance.



S03 · theorem_applicationBefore

E\Big[\sum_{k=1}^{m}c_kU_k\Big]

After

\sum_{k=1}^{m}c_k\,E[U_k],\quad E[c]=c

Conditions: U_k\ \text{functions of}\ (X,Y)\ \text{on the same}\ (S,p)

Rule: L_lin_exp · Uses: S01, G1

Leaf basis: L_lin_exp

Computing covariance needs linearity of expectation. Lemma L_lin_exp is proved in S03.1 and S03.2; it needs only that every U_k lives on the same (S,p), and no independence.



S04 · theorem_applicationBefore

E[aX+b],\ E[cY+d]

After

E[aX+b]=a\,E[X]+b,\quad E[cY+d]=c\,E[Y]+d

Conditions: none

Rule: L_lin_exp · Uses: S03, G2

Leaf basis: L_lin_exp

Take m=2, U_1=X, U_2=1 (the constant function), c_1=a and c_2=b: E[aX+b]=aE[X]+bE[1]=aE[X]+b. The same with c and d for Y.



S05 · equivalentBefore

(aX+b)(cY+d)

After

ac\,XY+ad\,X+bc\,Y+bd

Conditions: none

Rule: distributive · Uses: G2, distributive

Leaf basis: distributive + mul_comm + mul_assoc

Expand the product pointwise at every s∈S: (aX(s)+b)(cY(s)+d)=acX(s)Y(s)+adX(s)+bcY(s)+bd. This is distributivity and commutativity of real numbers, valid for every s, so the two functions are equal (N1 checks this degree-four multilinear identity on a grid).



S06 · theorem_applicationBefore

E[(aX+b)(cY+d)]

After

ac\,E[XY]+ad\,E[X]+bc\,E[Y]+bd

Conditions: none

Rule: L_lin_exp · Uses: S03, S05

Leaf basis: L_lin_exp + eq_replace

Substitute the expansion of S05 into the expectation and apply the lemma (m=4, with U equal to XY, X, Y, 1 and coefficients ac, ad, bc, bd). Here E[XY] must be computed on the same joint law and must not be assumed to equal E[X]E[Y] merely from the marginals.



S07 · equivalentBefore

E[aX+b]\,E[cY+d]=(a\,E[X]+b)(c\,E[Y]+d)

After

ac\,E[X]E[Y]+ad\,E[X]+bc\,E[Y]+bd

Conditions: none

Rule: distributive · Uses: S04

Leaf basis: distributive + mul_comm + mul_assoc

Expand the product of the two reals aE[X]+b and cE[Y]+d by distributivity, with the same pattern as S05.



S08 · equivalentBefore

\operatorname{Cov}(aX+b,cY+d)=E[(aX+b)(cY+d)]-E[aX+b]\,E[cY+d]

After

\operatorname{Cov}(aX+b,cY+d)=ac\,(E[XY]-E[X]E[Y])=ac\operatorname{Cov}(X,Y)

Conditions: none

Rule: eq_replace · Uses: S01, S06, S07

Leaf basis: eq_replace + add_inverse + distributive + add_comm

Substitute S06 and S07 into the definition and subtract: the terms adE[X], bcE[Y] and bd cancel, leaving acE[XY]−acE[X]E[Y]=ac(E[XY]−E[X]E[Y])=ac·Cov(X,Y). The constants b and d disappear and the coefficients a and c multiply, signs included. N2 checks this algebraic identity.



S09 · impliesBefore

S=\{(-1,1),(0,0),(1,1)\},\ p\equiv\tfrac13

After

\text{a finite joint law with}\ Y=X^2\ \text{on}\ S

Conditions: none

Rule: mko_joint_def · Uses: G3, mko_joint_def

Leaf basis: mko_joint_def + cartesian_product_def + numeric_evaluation

The first coordinates −1, 0, 1 are distinct, so the pairs are distinct; each mass 1/3>0; the total is 3·(1/3)=1. So it is a finite joint law. In each pair the second coordinate is the square of the first, (−1)²=1, 0²=0, 1²=1, so Y=X² on this law.



S10 · equivalentBefore

E[X]=\tfrac13(-1)+\tfrac13(0)+\tfrac13(1)

After

E[X]=0

Conditions: none

Rule: numeric_evaluation · Uses: S01, S09

Leaf basis: numeric_evaluation + frac_rules

By definition E[X]=Σ p(s)X(s); the X values of the three pairs are −1, 0, 1, each times 1/3, adding to 0.



S11 · equivalentBefore

E[Y]=\tfrac13(1)+\tfrac13(0)+\tfrac13(1)

After

E[Y]=\tfrac23

Conditions: none

Rule: numeric_evaluation · Uses: S01, S09

Leaf basis: numeric_evaluation + frac_rules

The Y values of the three pairs are 1, 0, 1, with weighted sum 2/3.



S12 · equivalentBefore

E[XY]=\tfrac13(-1)(1)+\tfrac13(0)(0)+\tfrac13(1)(1)

After

E[XY]=0

Conditions: none

Rule: numeric_evaluation · Uses: S01, S09

Leaf basis: numeric_evaluation + frac_rules

XY takes the values −1, 0, 1 on the three pairs (it equals X³), with weighted sum 0. E[XY] is computed pair by pair on the same joint law, not as E[X]E[Y].



S13 · equivalentBefore

\operatorname{Cov}(X,Y)=E[XY]-E[X]E[Y]

After

\operatorname{Cov}(X,Y)=0-0\cdot\tfrac23=0

Conditions: none

Rule: eq_replace · Uses: S01, S10, S11, S12

Leaf basis: eq_replace + numeric_evaluation

Substitute the three values of S10 to S12: 0−0·(2/3)=0. The covariance of this example is zero.



S14 · impliesBefore

X,\ Y\ \text{independent on}\ (S,p)

After

E[XY]=E[X]E[Y],\ \operatorname{Cov}(X,Y)=0

Conditions: P(X=x,Y=y)=p_X(x)p_Y(y)\ \text{for all}\ (x,y)\in S_X\times S_Y

Rule: L_indep_prod · Uses: S01, G1

Leaf basis: L_indep_prod + eq_replace + add_inverse

Lemma L_indep_prod (proved in S14.1 to S14.3) gives E[XY]=E[X]E[Y], and S01 then gives Cov(X,Y)=0. This is the basis of the first half of MKO assumption a2.



S15 · equivalentBefore

X,Y\ \text{independent}\Rightarrow\operatorname{Cov}(X,Y)=0

After

\operatorname{Cov}(X,Y)\neq 0\Rightarrow X,Y\ \text{not independent}

Conditions: none

Rule: contrapositive · Uses: S14

Leaf basis: contrapositive

Take the contrapositive of S14: computing a nonzero covariance refutes independence. This is the first half of MKO assumption a2.



S16 · impliesBefore

P(X=0,Y=1)\ \text{vs}\ P(X=0)\,P(Y=1)

After

0\neq\tfrac13\cdot\tfrac23=\tfrac29

Conditions: none

Rule: mko_indep_def · Uses: S09, marginal_def, mko_indep_def

Leaf basis: mko_indep_def + marginal_def + numeric_evaluation

(0,1)∉S, so P(X=0,Y=1)=0. P(X=0)=p(0,0)=1/3 and P(Y=1)=p(−1,1)+p(1,1)=2/3, with product 2/9≠0. Independence requires equality at every pair; it fails at this pair, so X and Y are not independent.



S17 · impliesBefore

\operatorname{Cov}(X,Y)=0\ \text{and}\ X,Y\ \text{dependent}

After

\operatorname{Cov}(X,Y)=0\not\Rightarrow X,Y\ \text{independent}

Conditions: none

Rule: exists_intro · Uses: S13, S16, S14

Leaf basis: exists_intro + quantifier_negation

On one joint law, Cov(X,Y)=0 (S13) while X and Y are not independent (S16). So the universal claim 'on every finite joint law, zero covariance gives independence' is false; the converse of S14 fails. This is the second half of MKO assumption a2.







## Substeps and lemmas

S03.1 · equivalentBefore

\sum_{s\in S}p(s)\sum_{k=1}^{m}c_kU_k(s)

After

\sum_{k=1}^{m}c_k\sum_{s\in S}p(s)\,U_k(s)=\sum_{k=1}^{m}c_k\,E[U_k]

Conditions: S\ \text{finite}

Rule: finite_sum_rules · Uses: G1, distributive, finite_sum_rules

Leaf basis: distributive + finite_sum_rules + mul_comm + mul_assoc

Distribute p(s) into the inner sum to get a double finite sum; the order of finite summation may be exchanged (repeated use of Σ(a_i+b_i)=Σa_i+Σb_i), and the constant c_k comes out (Σ c·a_i=c·Σa_i). Each Σ_s p(s)U_k(s) is E[U_k] by definition. All sums are finite, so there is no convergence issue.



S03.2 · equivalentBefore

E[c]=\sum_{s\in S}p(s)\,c

After

E[c]=c\sum_{s\in S}p(s)=c

Conditions: \sum_{s\in S}p(s)=1

Rule: finite_sum_rules · Uses: G1, finite_sum_rules

Leaf basis: finite_sum_rules + mul_one + mul_comm

The expectation of the constant function c: pulling out c leaves Σ_s p(s), which is exactly 1 by G1, so E[c]=c. If the masses only approximately summed to 1, this step would fail. S03.1 and S03.2 together prove Lemma L_lin_exp.



S14.1 · equivalentBefore

E[XY]=\sum_{(x,y)\in S}xy\,p(x,y)

After

E[XY]=\sum_{x\in S_X}\sum_{y\in S_Y}xy\,P(X=x,Y=y)

Conditions: S\subseteq S_X\times S_Y

Rule: finite_sum_regroup · Uses: G1, marginal_def, finite_sum_regroup

Leaf basis: finite_sum_regroup + mul_zero + add_zero

S_X and S_Y are the first and second coordinates occurring in S, so S⊆S_X×S_Y. On S, P(X=x,Y=y)=p(x,y); at grid points of S_X×S_Y outside S, P(X=x,Y=y)=0 and those terms are 0. Adding zero terms and regrouping by first coordinate leaves the finite sum unchanged.



S14.2 · impliesBefore

\sum_{x\in S_X}\sum_{y\in S_Y}xy\,P(X=x,Y=y)

After

\sum_{x\in S_X}\sum_{y\in S_Y}x\,p_X(x)\,y\,p_Y(y)

Conditions: X,\ Y\ \text{independent}

Rule: mko_indep_def · Uses: S14.1, mko_indep_def

Leaf basis: mko_indep_def + eq_replace + mul_comm

Under the independence hypothesis every grid point (x,y), including points outside S, satisfies P(X=x,Y=y)=p_X(x)p_Y(y); substitute term by term and reorder the factors by commutativity.



S14.3 · equivalentBefore

\sum_{x\in S_X}\sum_{y\in S_Y}x\,p_X(x)\,y\,p_Y(y)

After

\Big(\sum_{x}x\,p_X(x)\Big)\Big(\sum_{y}y\,p_Y(y)\Big)=E[X]\,E[Y]

Conditions: none

Rule: distributive · Uses: S14.2, distributive, finite_sum_rules, finite_sum_regroup

Leaf basis: distributive + finite_sum_rules + finite_sum_regroup + mul_comm

In the inner sum over y the factor x p_X(x) is constant and comes out, giving x p_X(x)·Σ_y y p_Y(y); the outer sum then pulls out the constant Σ_y y p_Y(y), giving a product of two sums. Finally Σ_x x p_X(x)=Σ_x Σ_y x p(x,y)=Σ_{s∈S} X(s)p(s)=E[X] by regrouping by first coordinate, and likewise for E[Y]. S14.1 to S14.3 together prove Lemma L_indep_prod.







## Reverse audits


- S17 · sufficient_goal_reduction · S13, S16, exists_intro — Goal G: zero covariance does not in general prove independence. Sufficient condition H: some finite joint law has zero covariance but is not independent; H⇒G because one counterexample refutes a universal claim. H is proved forwards in S09 to S16.
- S16 · premise_audit · S09, marginal_def, mko_indep_def — Refutation needs only one pair where equality fails; the support list must be complete to know that the mass of (0,1) is 0.
- S15 · inverse_equivalence · contrapositive — A statement and its contrapositive are logically equivalent, so the step is two-way; this is different from the converse, which is not proved.
- S14.3 · inverse_equivalence · distributive, finite_sum_rules, finite_sum_regroup — Pulling out constants and regrouping finite sums are rewrites of equal values and can be reversed. This sub-step does not use L_indep_prod.
- S14.2 · premise_audit · S14.1, mko_indep_def — This step depends on the independence hypothesis holding for every pair; holding for some pairs is not enough. Without independence the substitution cannot be made. This sub-step does not use L_indep_prod.
- S14.1 · inverse_equivalence · finite_sum_regroup, marginal_def — Deleting the zero terms returns the original sum, so it holds both ways. This sub-step does not use L_indep_prod.
- S14 · premise_audit · S01, L_indep_prod — Only 'independent ⇒ zero covariance' is proved; the converse 'zero covariance ⇒ independent' is not claimed, and S16 and S17 show it is false in general.
- S13 · inverse_equivalence · S10, S11, S12, eq_replace — Substituting equals can be reversed; both sides are the same number.
- S12 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
- S11 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
- S10 · inverse_equivalence · numeric_evaluation — Exact rational evaluation; both sides are the same number.
- S09 · premise_audit · G3, mko_joint_def — The three requirements and Y=X² were checked on each of the three pairs; no converse is claimed.
- S08 · inverse_equivalence · S06, S07, distributive, add_inverse — Every move replaces equals or adds and removes the same term, so it can be reversed; both sides are the same real number.
- S07 · inverse_equivalence · distributive, mul_comm — Expanding and factoring reals are inverse rewrites, so it holds both ways.
- S06 · premise_audit · S03, S05, L_lin_exp — It needs the pointwise identity of S05 (equal functions have equal expectations) and the lemma; linearity needs no independence.
- S05 · inverse_equivalence · distributive, mul_comm — Factoring is the reverse of expanding; the two expressions agree at every s, so the step holds both ways.
- S04 · premise_audit · S03, G2, L_lin_exp — It needs only the lemma and that a, b, c, d are constants; aX+b and cY+d both live on the same (S,p).
- S03.2 · inverse_equivalence · finite_sum_rules, mul_one — Pulling out a constant and multiplying by 1 can both be reversed; the condition used is Σp=1. This sub-step does not use L_lin_exp.
- S03.1 · inverse_equivalence · distributive, finite_sum_rules — Distributivity and rearranging finite sums are rewrites of equal values and can be reversed step by step. This sub-step does not use L_lin_exp.
- S03 · premise_audit · G1, L_lin_exp — The lemma's hypotheses are one finite joint law and weights summing to 1, both supplied by G1.
- S02 · inverse_equivalence · mul_comm, eq_replace — The two sides differ only in the order of multiplication; the same rewrite read backwards returns the original, so it holds both ways.
- S01 · premise_audit · G1, mko_cov_def, mko_expectation_def — This step only states the definition and derives no new fact; it requires the three expectations to come from the same (S,p).





## Error controls and negative controls

Zero covariance is not independenceThe common mistake named by the MKO is to declare independence on seeing Cov=0. In this guide Y=X² is completely determined by X, yet Cov(X,Y)=0 (S13); the single pair (0,1) refutes independence (S16). S14 gives only the direction 'independent ⇒ Cov=0'.

All expectations must come from one joint lawTake L1: (0,0) and (1,1) with 1/2 each; and L2: (0,0), (0,1), (1,0), (1,1) with 1/4 each. Both have marginals P(X=1)=P(Y=1)=1/2, but Cov=1/2−1/4=1/4 on L1 and Cov=1/4−1/4=0 on L2. So covariance is fixed by the joint law, not by the marginals; mixing E[XY] from L2 with E[X], E[Y] from L1 gives a number unrelated to L1.

The affine rule: constants vanish, coefficients multiplyIn S08, b and d vanish completely and a, c appear as the product ac with the sign kept. For example Cov(2X+1,−3Y+5)=−6·Cov(X,Y), not 6·Cov(X,Y) and not −6·Cov(X,Y)+5. N10 and N11 check this on the example with U=2X+1 and V=−3X+5: the direct computation agrees with 2·(−3)·Cov(X,X)=−4.


- In the example Cov(X,Y)=0, so X and Y are independent → reject — P(X=0,Y=1)=0 but P(X=0)P(Y=1)=2/9.
- Cov(2X+1,−3Y+5)=6·Cov(X,Y)+5 → reject — By S08 it equals 2·(−3)·Cov(X,Y)=−6·Cov(X,Y); the constants 1 and 5 do not appear.
- Knowing the two marginal tables of X and Y suffices to compute Cov(X,Y) → reject — L1 and L2 have the same marginals but covariances 1/4 and 0.
- It is possible that X and Y are independent while Cov(X,Y)=1/5 → reject — S14: on a finite joint law, independence implies Cov(X,Y)=0.





## Result and limitations

On one finite joint law, Cov(Y,X)=Cov(X,Y) and Cov(aX+b,cY+d)=ac·Cov(X,Y); independence implies Cov=0, so a nonzero covariance refutes independence. For the law with X uniform on −1, 0, 1 and Y=X², E[X]=0, E[Y]=2/3, E[XY]=0 and Cov(X,Y)=0, but P(X=0,Y=1)=0≠2/9=P(X=0)P(Y=1), so X and Y are dependent: zero covariance does not imply independence.


- Regrouping of finite sums (finite_sum_regroup) and marginal_def are premises of this guide; they are not derived here from more basic axioms.
- N10 and N11 cross-check S08 only on the example law with U=2X+1 and V=−3X+5 and cannot replace the general proof of S08; N12 and N13 are the numbers of L1 and L2 in the error controls.





## Verification and source binding

13 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 66770666a1625742c7623b7027ec9998c2e93b136060117940329d5723701fbc
- original source SHA-256: 66770666a1625742c7623b7027ec9998c2e93b136060117940329d5723701fbc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-covariance-01.json)