# One data function under two parameter laws

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

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-statistical-estimator-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Validate a total estimator and its parameterwise expectations.

Expectations here do not automatically establish estimator quality.





## 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 — On a finite parameter model with one common sample space, the statistic table depends only on the observation. Expectations can be computed under each parameter law, but no unbiasedness, consistency, sufficiency, identifiability or posterior claim follows here. Full sampling distributions are a later object. · mko-statistical-estimator
- work · prerequisite — Finite laws have nonnegative probabilities summing to one; a statistic depends only on data, and expectation sums all weighted outcomes.





## Main derivation

S01 · impliesBefore

\Omega=\{00,01,10,11\}

After

U=(0,1/4,1/4,1/2)

Conditions: none

Rule: work · Uses: G1, G2, work

Leaf basis: work

Every outcome has exactly one value, giving a total function.



S02 · impliesBefore

U(x)=(x_1+x_2)/4

After

U\text{ does not depend on }\theta

Conditions: none

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

Leaf basis: work

The rule reads only the observed bits, not the unknown parameter.



S03 · impliesBefore

x=01

After

u_{\rm obs}=U(01)=1/4

Conditions: none

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

Leaf basis: work

The estimate is the function's value at this observation.



S04 · impliesBefore

E_{1/4}[U]=0(9/16)+(1/4)(3/16)+(1/4)(3/16)+(1/2)(1/16)

After

E_{1/4}[U]=1/8

Conditions: none

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

Leaf basis: work

Weight all outcomes under the first law, retaining both middle outcomes.



S05 · impliesBefore

E_{3/4}[U]=0(1/16)+(1/4)(3/16)+(1/4)(3/16)+(1/2)(9/16)

After

E_{3/4}[U]=3/8

Conditions: none

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

Leaf basis: work

The second law assigns9/16 to 11, rather than reusing the first row.



S06 · impliesBefore

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

After

\theta\mapsto E_\theta[U]\text{ is a parameterwise table}

Conditions: none

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

Leaf basis: work

Distributional properties of the same function may vary with theta.



S07 · impliesBefore

V_\theta(x)=\theta

After

V_\theta\text{ is not a usable unknown-parameter estimator rule}

Conditions: none

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

Leaf basis: work

Changing the constant rule with unknown theta does not define a data-executable estimator.



S08 · impliesBefore

U:\Omega\to\mathbb Q\text{ total and parameter-independent}

After

U\text{ qualifies as an estimator for this model}

Conditions: none

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

Leaf basis: work

The functional qualification is complete; bias, variance and sufficiency need separate audits.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, G2, S07, work — The two expectation values are not inflated into consistency or posterior claims.
- S07 · premise_audit · G1, G2, S06, work — Each fixed Vtheta is a function, but not the one common data function required here.
- S06 · premise_audit · G1, G2, S05, work — The law changes, not the estimator definition.
- S05 · premise_audit · G1, G2, S04, work — Do not mix weights from different theta laws.
- S04 · premise_audit · G1, G2, S03, work — 01 and 10 share a value but each contributes mass.
- S03 · premise_audit · G1, G2, S02, work — The value 1/4 is not the entire four-entry function U.
- S02 · premise_audit · G1, G2, S01, work — Both theta values use the same U table.
- S01 · premise_audit · G1, G2, work — Neither11 nor any single-valuedness check is omitted.





## Error controls and negative controls

Total tableAssign every outcome even when values coincide.

Parameter and dataKeep one U and two Ptheta laws; do not silently change U.


- U may be total without a value at 11. → reject — Totality requires a value for every carrier outcome.
- Set U(x)=theta to estimate unknown theta from data. → reject — The unknown parameter cannot be an input to the data rule.
- The observed 1/4 equals E_(1/4)U. → reject — The complete expectation is 1/8.





## Result and limitations

U is one total estimator; at 01 the estimate is 1/4, while its two law expectations are 1/8 and 3/8.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 7d2a71efe1386b0a4e2ae04a859c98e82bdbfb5e2aa1303f1a80575333c06239
- original source SHA-256: 17561f6cd64c683c14d172706c4eb1d4846352d8213e1cf1b580c63cbb581dce
- 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-statistical-estimator-01.json)