Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Var⁡(X)=E[X2]−E[X]2 and Cov⁡(X,Y)=E[XY]−E[X]E[Y]

Statement

For finite real random variables X,Y, Var⁡(X)=E[X2]−E[X]2, Cov⁡(X,Y)=E[XY]−E[X]E[Y]. Variance is nonnegative, and every constant random variable has variance zero. Zero variance forces equality to the mean on every positive-weight outcome, but not necessarily on zero-weight outcomes.

Facts & Assumptions

Given: Real random variables X,Y on a finite probability space.

[L1]

Expectation is linear for every finite family, without independence (Expectation is linear for every finite family of random variables, without any independence hypothesis).

[L2]

Variance and covariance are expectations of the displayed centred square and product (Variance, standard deviation, and covariance on a finite probability space).

Proof

technique · direct
1.1

Expand (X−E[X])2=X2−2E[X]X+E[X]2 and apply linearity to obtain Var⁡(X)=E[X2]−E[X]2.

L1L2algebra
1.2

Expanding (X−E[X])(Y−E[Y]) and applying linearity gives the covariance identity.

L1L2algebra
1.3

The centred square is pointwise nonnegative, so variance is nonnegative; if X is constant it vanishes identically. If the variance is zero, every positive-weight centred-square summand is zero, while a zero-weight outcome is unrestricted.

L2algebra
2.1

Steps 1.1, 1.2, and 1.3 give all claims.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 33 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources