# Same-law second and centered moment cross-checks

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-estimator-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-estimator-variance-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Compute variance at all theta values and verify centered definitions.

Variance measures random spread, not correctness of estimation.





## Givens and symbols


- work


- G1 — Theta={1/4,3/4}, Omega={00,01,10,11}; P_(1/4)=(9,3,3,1)/16 and P_(3/4)=(1,3,3,9)/16.
- G2 — U(x)=(x1+x2)/4 has total table(0,1/4,1/4,1/2) in Omega order, with target g(theta)=theta.


- θ — fixed unknown parameter
- U — one total statistic





## Rules and sources


- mko_definition · cited — Keep sampling law, positive-mass support and mean at the same theta. Check Var_theta(T)=E_theta[(T−E_theta[T])^2]=E_theta[T^2]−(E_theta[T])^2 exactly. Zero variance means almost-sure constancy under that law, not equality with theta or unbiasedness. · mko-estimator-variance
- work · prerequisite — Finite laws have nonnegative probabilities summing to one; a statistic depends only on data, and expectation sums all weighted outcomes. Var(U)=E[(U-EU)^2]=E[U²]-(EU)².





## Main derivation

S01 · impliesBefore

P_{1/4}^U=(9,6,1)/16,\quad P_{3/4}^U=(1,6,9)/16

After

E_{1/4}U=1/8,\quad E_{3/4}U=3/8

Conditions: none

Rule: work · Uses: G1, G2, work

Leaf basis: work

Fix each center from its complete sampling law.



S02 · impliesBefore

E_{1/4}U^2=(1/16)(6/16)+(1/4)(1/16)

After

E_{1/4}U^2=5/128

Conditions: none

Rule: work · Uses: G1, G2, S01, work

Leaf basis: work

Square U values, not probabilities.



S03 · impliesBefore

\operatorname{Var}_{1/4}U=E_{1/4}U^2-(E_{1/4}U)^2

After

5/128-(1/8)^2=3/128

Conditions: none

Rule: work · Uses: G1, G2, S02, work

Leaf basis: work

Subtract the square of the mean from the same theta law.



S04 · impliesBefore

E_{1/4}(U-1/8)^2

After

(9/16)(1/8)^2+(6/16)(1/8)^2+(1/16)(3/8)^2=3/128

Conditions: none

Rule: work · Uses: G1, G2, S03, work

Leaf basis: work

Independently verify the first variance using all three centered-square terms.



S05 · impliesBefore

E_{3/4}U^2=(1/16)(6/16)+(1/4)(9/16)

After

E_{3/4}U^2=21/128

Conditions: none

Rule: work · Uses: G1, G2, S04, work

Leaf basis: work

Use the last mass 9/16 for the second law.



S06 · impliesBefore

\operatorname{Var}_{3/4}U=21/128-(3/8)^2

After

\operatorname{Var}_{3/4}U=3/128

Conditions: none

Rule: work · Uses: G1, G2, S05, work

Leaf basis: work

The second variance happens to equal the first despite a different mean.



S07 · impliesBefore

E_{3/4}(U-3/8)^2

After

(1/16)(3/8)^2+(6/16)(1/8)^2+(9/16)(1/8)^2=3/128

Conditions: none

Rule: work · Uses: G1, G2, S06, work

Leaf basis: work

Cross-check again with second-law centered squares.



S08 · impliesBefore

V(x)\equiv0,\quad\theta\in\{1/4,3/4\}

After

\operatorname{Var}_\theta(V)=0,\quad E_\theta[V]\ne\theta

Conditions: none

Rule: work · Uses: G1, G2, S07, work

Leaf basis: work

A constant estimator explicitly witnesses zero variance with nonzero bias.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, G2, S07, work — Zero variance only gives a.s. constancy under that law.
- S07 · premise_audit · G1, G2, S06, work — Every summand is nonnegative, so a negative variance signals error.
- S06 · premise_audit · G1, G2, S05, work — Equal variance does not imply equal sampling laws.
- S05 · premise_audit · G1, G2, S04, work — Do not import first-law weights.
- S04 · premise_audit · G1, G2, S03, work — The zero support value does not have zero centered deviation.
- S03 · premise_audit · G1, G2, S02, work — Do not subtract(3/8) squared here.
- S02 · premise_audit · G1, G2, S01, work — The squared middle value is 1/16.
- S01 · premise_audit · G1, G2, work — One U may have different centers under different laws.





## Error controls and negative controls

Same-law centerPair theta=1/4 with 1/8 and theta=3/4 with 3/8.

Two formulasIndependently compare centered sums and raw-moment subtraction at 3/128.


- Use the second mean 3/8 for the first variance. → reject — The first law has mean 1/8; centers must match laws.
- Zero variance implies unbiasedness. → reject — V identically0 has zero variance but is biased for theta>0.
- Equal variances imply equal laws. → reject — The U=0 masses differ:9/16 and 1/16.





## Result and limitations

Both theta variances are 3/128, verified by centered and raw second moments.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 2ad002b889b15f44b5c24941287a4fa911adb4a34398f427dbc154661eb2827b
- original source SHA-256: f2bbc9ab007672ceca721f29145874a8a606c1b10236341756c3630da64cd582
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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