# Variance in finite probability models: translation, scaling and the zero-variance characterization [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-variance/) 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-variance-01 · production-20261019-adopted-96 ## Goal and scope In a valid finite probability model, prove Var(X)≥0, Var(X+c)=Var(X), Var(kX)=k²Var(X), and Var(X)=0 ⇔ X takes one common value at every positive-weight outcome. Then with S={1,2,3,4}, w₁=1/2, w₂=1/4, w₃=1/4, w₄=0 and X=(1,3,−1,10), compute μ=1, Var(X)=2, Var(X+5)=2 and Var(−3X)=18, and use Z=(2,2,2,7) to show that a different value at a zero-weight outcome does not prevent zero variance. Stays inside the MKO: finite nonempty sample space, nonnegative normalized weights, a total real-valued function, the probability-distribution variance rather than a sample estimator, and a clear distinction between the positive-weight support and the whole sample space (a1, a2). All arithmetic is exact and rational. Linearity of expectation is cited from mko-expectation. Var(X+Y), covariance, standard deviation and the formula E[X²]−μ² are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - finite_sum_rules - square_nonneg - order_basics - distributive - power_laws - numeric_evaluation - G1 — General model: S is finite and nonempty, w_s≥0 for all s with Σ_{s∈S} w_s=1; X:S→ℝ is total; μ=E[X]=Σ w_s X(s); c and k are reals. - G2 — Instance: S={1,2,3,4}, w₁=1/2, w₂=1/4, w₃=1/4, w₄=0. - G3 — X(1)=1, X(2)=3, X(3)=−1, X(4)=10; Z(1)=Z(2)=Z(3)=2, Z(4)=7. - \mu=E[X] — the expectation of X - \mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2 — the variance of X - \mathrm{supp}=\{s\in S\mid w_s>0\} — the positive-weight support - c,k — translation amount and scaling factor (reals) - t_s — the s-th term of the variance sum ## Rules and sources - 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. - square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0. - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - 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. - 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. - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - add_zero · prerequisite — Additive identity: u+0=u. - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - 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. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0. - case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility. - exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x). - contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_variance_def · cited — Put μ=E[X]. In a valid finite probability model, define V(X)=Var(X)=Σ_s w_s(X(s)−μ)²≥0. Translation leaves variance unchanged and Var(kX)=k²Var(X). Variance is zero exactly when X has one common value at every positive-weight outcome. · mko-variance - mko_expectation_lin · 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). On the same probability model, E[aX+b]=aE[X]+b and E[X+Y]=E[X]+E[Y] without assuming independence of X and Y; a constant c has expectation c. · mko-expectation - support_def · prerequisite — Positive-weight support: supp={s∈S ∣ w_s>0}. Since w_s≥0, s∉supp means exactly w_s=0. - L_shift · lemma — In the model of G1, for every real c: Var(X+c)=Var(X). - L_scale · lemma — In the model of G1, for every real k: Var(kX)=k²Var(X). - L_nonneg_sum_zero · lemma — If finitely many reals t_s are all ≥0 and Σ_s t_s=0, then every t_s=0. - L_var_zero · lemma — In the model of G1: Var(X)=0 ⇔ X(s)=μ for every s∈supp. - L_const_support · lemma — In the model of G1: Var(X)=0 ⇔ there is a real c with X(s)=c for every s∈supp. ## Main derivation S01 · impliesBefore w=(\tfrac12,\tfrac14,\tfrac14,0) After w_s\ge0,\ \sum_s w_s=1,\ \mathrm{supp}=\{1,2,3\} Conditions: none Rule: numeric_evaluation · Uses: G2, support_def Leaf basis: numeric_evaluation + support_def Validate the model first: the four weights are nonnegative and 1/2+1/4+1/4+0=1, so they are valid. The positive-weight support is {1,2,3}; outcome 4 belongs to the sample space S but has weight 0 and is not in the support. MKO assumption a2 asks for these two sets to be kept apart. S02 · equivalentBefore \mu=E[X] After \tfrac12\cdot1+\tfrac14\cdot3+\tfrac14\cdot(-1)+0\cdot10=1 Conditions: none Rule: mko_expectation_lin · Uses: S01, G3, mko_expectation_lin Leaf basis: mko_expectation_lin + numeric_evaluation By the definition of expectation: 1/2+3/4−1/4+0=1. The value 10 at outcome 4 is multiplied by weight 0 and contributes 0. S03 · equivalentBefore X(s)-\mu\ \ (s=1,2,3,4) After 0,\ 2,\ -2,\ 9 Conditions: none Rule: numeric_evaluation · Uses: S02, G3 Leaf basis: numeric_evaluation Compute the deviations pointwise: 1−1=0, 3−1=2, −1−1=−2, 10−1=9. The deviation is defined at every outcome, including the zero-weight outcome 4. S04 · equivalentBefore \mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2 After \tfrac12\cdot0^2+\tfrac14\cdot2^2+\tfrac14\cdot(-2)^2+0\cdot9^2=2 Conditions: none Rule: mko_variance_def · Uses: S03, S01, mko_variance_def Leaf basis: mko_variance_def + power_laws + numeric_evaluation Substitute into the definition: 0+1+1+0=2. The zero-weight outcome 4 has a large deviation 9, but multiplied by weight 0 it contributes 0. S05 · impliesBefore w_s\ge0,\ (X(s)-\mu)^2\ge0 After \mathrm{Var}(X)\ge0 Conditions: none Rule: square_nonneg · Uses: G1, mko_variance_def Leaf basis: square_nonneg + order_basics + mul_zero + finite_sum_rules General property. Each term t_s=w_s(X(s)−μ)²: the square is nonnegative; if w_s=0 then t_s=0; if w_s>0, multiplying 0≤(X(s)−μ)² by the positive w_s keeps the order, so t_s≥0. A finite sum of nonnegative numbers is nonnegative, so Var(X)≥0. S06 · equivalentBefore \mathrm{Var}(X+c) After \mathrm{Var}(X) Conditions: none Rule: L_shift · Uses: G1, mko_variance_def Leaf basis: mko_expectation_lin + eq_replace By Lemma L_shift, translation does not change variance. The proof is in S06.1 and S06.2: the mean also shifts by c, so the deviations are unchanged. S07 · equivalentBefore \mathrm{Var}(kX) After k^2\,\mathrm{Var}(X) Conditions: none Rule: L_scale · Uses: G1, mko_variance_def Leaf basis: mko_expectation_lin + power_laws + finite_sum_rules By Lemma L_scale, scaling by k multiplies the variance by k². The proof is in S07.1 to S07.3 and holds for every real k, including k=0 and negative k. S08 · impliesBefore \mathrm{Var}(X+5),\ X+5=(6,8,4,15) After \mathrm{Var}(X+5)=\mathrm{Var}(X)=2 Conditions: none Rule: L_shift · Uses: S06, S04, G3 Leaf basis: mko_variance_def + numeric_evaluation By S06 (c=5), Var(X+5)=2. Direct check: X+5 has values 6, 8, 4, 15, mean 1/2·6+1/4·8+1/4·4+0·15=6=μ+5, deviations 0, 2, −2, 9 as before, so the variance is still 2. S09 · impliesBefore \mathrm{Var}(-3X),\ -3X=(-3,-9,3,-30) After \mathrm{Var}(-3X)=(-3)^2\cdot2=18 Conditions: none Rule: L_scale · Uses: S07, S04, G3 Leaf basis: mko_variance_def + numeric_evaluation By S07 (k=−3), Var(−3X)=9·2=18. Direct check: −3X has values −3, −9, 3, −30, mean −3=−3μ, deviations 0, −6, 6, −27, and variance 1/4·36+1/4·36+0·729=18. A negative factor does not make the variance negative. S10 · impliesBefore t_s\ge0,\ \sum_s t_s=0 After t_s=0\ \ \forall s Conditions: none Rule: L_nonneg_sum_zero · Uses: finite_sum_rules, order_basics Leaf basis: order_basics + finite_sum_rules + contradiction Prepare Lemma L_nonneg_sum_zero for the zero-variance characterization: if a finite sum of nonnegative numbers is zero, every term is zero. The proof is in S10.1 and S10.2. S11 · equivalentBefore \mathrm{Var}(X)=0 After X(s)=\mu\ \ \forall s\in\mathrm{supp} Conditions: none Rule: L_var_zero · Uses: G1, mko_variance_def, support_def Leaf basis: L_nonneg_sum_zero + zero_product + square_nonneg + case_analysis By Lemma L_var_zero, zero variance means exactly that X equals the mean at every positive-weight outcome. The condition involves only the support; values at zero-weight outcomes are unrestricted. The proof is in S11.1 (⇒) and S11.2 (⇐). S12 · equivalentBefore \mathrm{Var}(X)=0 After \exists c\ \forall s\in\mathrm{supp}:\ X(s)=c Conditions: none Rule: L_const_support · Uses: S11 Leaf basis: L_var_zero + exists_intro + finite_sum_rules Rewrite S11 in the MKO's words: zero variance means exactly that X takes one common value at all positive-weight outcomes. This is Lemma L_const_support, proved in S12.1 and S12.2. S13 · impliesBefore Z=2\ \text{on}\ \mathrm{supp}=\{1,2,3\},\ Z(4)=7 After \mathrm{Var}(Z)=0 Conditions: none Rule: L_const_support · Uses: S12, S01, G3 Leaf basis: L_const_support + numeric_evaluation Z equals 2 throughout the support {1,2,3}, so by S12 Var(Z)=0, even though Z is not constant on all of S (Z(4)=7). Direct check: μ_Z=2·(1/2+1/4+1/4)+7·0=2 and Var(Z)=0+0+0+0·25=0. S14 · impliesBefore X(1)=1\neq3=X(2),\ 1,2\in\mathrm{supp} After \mathrm{Var}(X)\neq0 Conditions: none Rule: contrapositive · Uses: S12, S01, G3, S04 Leaf basis: contrapositive + L_const_support X takes the different values 1 and 3 at two outcomes of the support, so it has no common value there; by the contrapositive of the ⇒ direction of S12, Var(X)≠0. This agrees with Var(X)=2>0 from S04. S15 · impliesBefore \text{S04 to S14} After \mathrm{Var}\ge0,\ \mathrm{Var}(X+c)=\mathrm{Var}(X),\ \mathrm{Var}(kX)=k^2\mathrm{Var}(X),\ \mathrm{Var}=0\iff\text{const on supp} Conditions: none Rule: and_intro_elim · Uses: S04, S05, S06, S07, S08, S09, S12, S13 Leaf basis: and_intro_elim Summary: the four general properties are proved; in the instance μ=1, Var(X)=2, Var(X+5)=2, Var(−3X)=18, and Var(Z)=0 although Z differs at a zero-weight outcome. ## Substeps and lemmas S06.1 · equivalentBefore E[X+c] After \mu+c Conditions: none Rule: mko_expectation_lin · Uses: G1, mko_expectation_lin Leaf basis: mko_expectation_lin By linearity of expectation (a=1, b=c): E[X+c]=E[X]+c=μ+c. This needs the weights to sum to 1. S06.2 · equivalentBefore \sum_s w_s\bigl((X(s)+c)-(\mu+c)\bigr)^2 After \sum_s w_s(X(s)-\mu)^2 Conditions: none Rule: eq_replace · Uses: S06.1, eq_replace Leaf basis: eq_replace + add_assoc + add_comm + add_inverse + add_zero For each s: (X(s)+c)−(μ+c)=X(s)−μ (associativity, commutativity and inverses for addition). Each term is replaced by an equal term, so the sum is unchanged. S06.1 and S06.2 together prove Lemma L_shift. S07.1 · equivalentBefore E[kX] After k\mu Conditions: none Rule: mko_expectation_lin · Uses: G1, mko_expectation_lin Leaf basis: mko_expectation_lin By linearity of expectation (a=k, b=0): E[kX]=kμ. S07.2 · equivalentBefore (kX(s)-k\mu)^2 After k^2(X(s)-\mu)^2 Conditions: none Rule: power_laws · Uses: S07.1, distributive, power_laws Leaf basis: distributive + power_laws + mul_comm First factor out k by distributivity: kX(s)−kμ=k(X(s)−μ); then use (ab)²=a²b². The deviation is multiplied by k, and squaring brings out k², so a negative sign disappears. S07.3 · equivalentBefore \sum_s w_s\,k^2(X(s)-\mu)^2 After k^2\sum_s w_s(X(s)-\mu)^2=k^2\,\mathrm{Var}(X) Conditions: none Rule: finite_sum_rules · Uses: S07.2, finite_sum_rules Leaf basis: finite_sum_rules + def_unfold The constant k² factors out of the finite sum, and what remains is Var(X) by definition. S07.1 to S07.3 together prove Lemma L_scale. For k=0 this gives Var(0)=0, consistent with the variance of a constant variable. S10.1 · impliesBefore t_r>0\ \text{for some}\ r After \sum_s t_s=t_r+\sum_{s\neq r}t_s\ge t_r>0 Conditions: t_s\ge0 Rule: order_basics · Uses: finite_sum_rules, order_basics Leaf basis: finite_sum_rules + order_basics Assume for the moment that some term t_r>0. Split the sum into t_r plus the remaining terms; the remaining terms are nonnegative, so is their sum, and the total is ≥t_r>0. S10.2 · impliesBefore \sum_s t_s>0\ \text{and}\ \sum_s t_s=0 After \neg\exists r:\ t_r>0,\ \text{so}\ t_s=0 Conditions: none Rule: contradiction · Uses: S10.1, contradiction Leaf basis: contradiction + order_basics The conclusion of S10.1 contradicts the hypothesis Σ t_s=0, so no t_r>0. Each t_s is ≥0 and not >0, so by trichotomy t_s=0. S10.1 and S10.2 together prove Lemma L_nonneg_sum_zero. S11.1 · impliesBefore \mathrm{Var}(X)=0,\ s\in\mathrm{supp} After X(s)=\mu Conditions: w_s>0 Rule: L_nonneg_sum_zero · Uses: S05, S10, zero_product, square_nonneg Leaf basis: L_nonneg_sum_zero + zero_product + square_nonneg (⇒) By S05 each term t_s=w_s(X(s)−μ)²≥0, and their sum Var(X)=0, so by L_nonneg_sum_zero every t_s=0. For s∈supp, w_s>0 so w_s≠0, and the zero-product property gives (X(s)−μ)²=0; since a square is zero exactly when its base is zero, X(s)=μ. S11.2 · impliesBefore X(s)=\mu\ \ \forall s\in\mathrm{supp} After \mathrm{Var}(X)=\sum_s 0=0 Conditions: none Rule: case_analysis · Uses: G1, support_def, case_analysis Leaf basis: case_analysis + support_def + mul_zero + finite_sum_rules (⇐) Each s is either in the support or not. In the support: X(s)−μ=0 and t_s=w_s·0=0. Outside: w_s=0 and t_s=0·(X(s)−μ)²=0. Every term is 0, so the sum is 0. S11.1 and S11.2 together prove Lemma L_var_zero. S12.1 · impliesBefore \mathrm{Var}(X)=0 After X(s)=\mu\ \ \forall s\in\mathrm{supp}\ \Rightarrow\ c=\mu Conditions: none Rule: L_var_zero · Uses: S11, exists_intro Leaf basis: L_var_zero + exists_intro (⇒) By the ⇒ direction of L_var_zero, X equals μ throughout the support; taking c=μ gives the common value. S12.2 · impliesBefore X(s)=c\ \ \forall s\in\mathrm{supp} After \mu=\sum_{s\in\mathrm{supp}}w_s c+\sum_{s\notin\mathrm{supp}}0\cdot X(s)=c,\ \text{so}\ \mathrm{Var}(X)=0 Conditions: none Rule: L_var_zero · Uses: S11, G1, support_def Leaf basis: L_var_zero + finite_sum_rules + support_def + mul_zero (⇐) Split the sum for μ into the parts inside and outside the support: outside, every weight is 0 and contributes 0, which also makes the weights inside sum to 1; so μ=c·1=c. Then X(s)=c=μ for every s∈supp, and the ⇐ direction of L_var_zero gives Var(X)=0. S12.1 and S12.2 together prove Lemma L_const_support. ## Reverse audits - S15 · sufficient_goal_reduction · S04, S05, S06, S07, S08, S09, S12, S13, and_intro_elim — Goal G is the proofs and computations in the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction. - S14 · premise_audit · S12, contrapositive — Two different values inside the support suffice to rule out a common value; the conclusion only says nonzero, and the value comes from S04. - S13 · premise_audit · S12, S01 — Only the ⇐ direction of S12 and the identification of the support are used; the direct computation is a cross-check. - S12.2 · premise_audit · L_var_zero, finite_sum_rules, support_def, mul_zero — The key point is that μ is determined by the values on the support alone; values outside (such as Z(4)=7) are multiplied by 0 and vanish. - S12.1 · premise_audit · L_var_zero, exists_intro — Existential introduction needs only the witness c=μ. - S12 · inverse_equivalence · L_const_support — Both directions are proved in the sub-steps. - S11.2 · premise_audit · case_analysis, support_def, mul_zero — The two cases exhaust S (support_def guarantees w_s=0 outside the support). - S11.1 · premise_audit · S05, L_nonneg_sum_zero, zero_product, square_nonneg — For outcomes with w_s=0, t_s=0 gives no information about X(s), so the conclusion holds only on the support. - S11 · inverse_equivalence · L_var_zero — The two directions are proved in the sub-steps, so this is an equivalence. - S10.2 · premise_audit · contradiction, order_basics — Proof by contradiction discharges the temporary assumption of S10.1; trichotomy turns '≥0 and not >0' into '=0'. - S10.1 · premise_audit · finite_sum_rules, order_basics — Only the nonnegativity of the other terms and order-preservation under addition are used; this is reasoning under a temporary assumption, discharged in S10.2. - S10 · premise_audit · L_nonneg_sum_zero — It needs every term nonnegative; with negative terms allowed, for example 1+(−1)=0, the conclusion fails. - S09 · premise_audit · S07, S04 — The conclusion comes from the lemma; the direct computation is only a cross-check. - S08 · premise_audit · S06, S04 — The conclusion comes from the lemma; the direct computation is only a cross-check. - S07.3 · inverse_equivalence · finite_sum_rules, def_unfold — Factoring out a constant and folding back the definition are equations and hold both ways. - S07.2 · inverse_equivalence · distributive, power_laws — Both are identities valid for all reals, so the step holds both ways. - S07.1 · inverse_equivalence · mko_expectation_lin — Linearity is an equation and can be used either way. - S07 · inverse_equivalence · L_scale — Both sides are the same number (by the lemma) and can replace each other. - S06.2 · inverse_equivalence · eq_replace, add_inverse, add_comm — Term-by-term replacement of equals; it holds both ways. - S06.1 · inverse_equivalence · mko_expectation_lin — Linearity is an equation and can be used either way. - S06 · inverse_equivalence · L_shift — Both sides are the same number (by the lemma) and can replace each other. - S05 · premise_audit · square_nonneg, order_basics, finite_sum_rules — It needs nonnegative weights; with a negative weight the conclusion could fail. This is one-way and does not claim Var(X)>0. - S04 · inverse_equivalence · mko_variance_def, numeric_evaluation — Unfolding the definition and exact arithmetic; both sides have the same value. - S03 · inverse_equivalence · numeric_evaluation — Integer subtraction, checkable backwards (deviation plus μ returns the value). - S02 · inverse_equivalence · mko_expectation_lin, numeric_evaluation — Unfolding the definition plus exact arithmetic; both sides have the same value. - S01 · premise_audit · G2, support_def, numeric_evaluation — Exact arithmetic and reading a definition; independently recomputable. ## Error controls and negative controls Zero variance constrains only positive-weight outcomesOne misconception identified in the MKO is requiring a zero-variance variable to agree at zero-probability outcomes as well. Z is not constant on S (Z(4)=7), but w₄=0 and Var(Z)=0 (S13). The correct characterization of zero variance is constancy on the support (S12). Distribution variance is not the sample varianceThe other misconception is to mix in the sample variance. Treating 1, 3, −1, 10 as four data points with denominator n−1=3 gives 275/12, not this model's Var(X)=2. Variance here is weighted by the probabilities and uses no n−1 denominator; the standard deviation √2 is a different quantity not treated here. The factor is squared, and a shift is not added to the varianceVar(−3X)=(−3)²·2=18, not −3·2=−6 nor 3·2=6; Var(X+5)=2, not 2+5=7. The reasons are the square in S07.2 and the unchanged deviations in S06.2. - Z(4)=7≠2, so Var(Z)>0 → reject — w₄=0, so the term of outcome 4 is 0·25=0; Z is constantly 2 on the support and Var(Z)=0. - Var(−3X)=−3Var(X)=−6 → reject — Variance is nonnegative; the correct value is (−3)²·2=18. - Var(X+5)=Var(X)+5=7 → reject — The shift also adds 5 to the mean, the deviations are unchanged, and Var(X+5)=2. - The variance of X is the sample variance 275/12 of 1, 3, −1, 10 → reject — This model's variance is weighted by (1/2,1/4,1/4,0) and equals 2; a sample estimator is a different thing. ## Result and limitations In every valid finite model Var(X)≥0, Var(X+c)=Var(X) and Var(kX)=k²Var(X), and Var(X)=0 exactly when X takes one common value throughout the positive-weight support. Instance: μ=1, Var(X)=2, Var(X+5)=2, Var(−3X)=18; Z=(2,2,2,7) is constantly 2 on the support {1,2,3}, so Var(Z)=0 and Z(4)=7 does not matter. - Var(X+Y), covariance and standard deviation are outside this guide; the formula E[X²]−μ² is not used either. - Linearity of expectation is cited from mko-expectation; its proof belongs to that MKO's guide and is not repeated here. ## Verification and source binding 15 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: ce0f84e07a301a2959c247b101c66b419e062d8b1325ebf04f27a9c4914677a1 - original source SHA-256: ce0f84e07a301a2959c247b101c66b419e062d8b1325ebf04f27a9c4914677a1 - 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-variance-01.json)