# A complete model with two parameter values and four sample points

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

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



## Goal and scope

Validate every parameter law and distinguish likelihood from posterior.

A complete finite table; no posterior or optimality inference.





## 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.


- θ — fixed unknown parameter





## Rules and sources


- mko_definition · cited — Validate the finite parameter set and every nonnegative normalized row of the complete law table. In L(theta;x)=P_theta(x), likelihood varies theta while the observation x is fixed. It is not a posterior; without a prior no Bayes update is performed. One observation does not establish identifiability. · mko-parametric-statistical-model
- 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

\Theta=\{1/4,3/4\},\quad\Omega=\{00,01,10,11\}

After

P_\theta:\Omega\to[0,1]\quad(\theta\in\Theta)

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Fix the common carrier without deleting samples as theta changes.



S02 · impliesBefore

P_{1/4}=(9,3,3,1)/16

After

(9+3+3+1)/16=1

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

All four entries of the first row are nonnegative and normalized.



S03 · impliesBefore

P_{3/4}=(1,3,3,9)/16

After

(1+3+3+9)/16=1

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Validate the second row explicitly rather than skipping it by appearance.



S04 · impliesBefore

x=01\text{ fixed}

After

L(1/4;01)=3/16,\quad L(3/4;01)=3/16

Conditions: none

Rule: mko_definition · Uses: G1, S03, mko_definition

Leaf basis: mko_definition

After fixing the observation, theta is the likelihood's argument.



S05 · impliesBefore

\sum_{\theta\in\Theta}L(\theta;01)

After

3/16+3/16=3/8\ne1

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Likelihood values across parameters need not normalize to a probability law.



S06 · impliesBefore

x=00

After

L(1/4;00)=9/16>1/16=L(3/4;00)

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Another observation gives different likelihoods for the two parameters.



S07 · impliesBefore

P_{1/4}(00)=9/16\ne1/16=P_{3/4}(00)

After

P_{1/4}\ne P_{3/4}

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The model laws are distinct, witnessed by an explicit sample event.



S08 · impliesBefore

\theta\mapsto P_\theta\text{ with both rows normalized}

After

\{P_\theta:\theta\in\Theta\}\text{ is a finite parametric model}

Conditions: none

Rule: mko_definition · Uses: G1, S07, mko_definition

Leaf basis: mko_definition

The common carrier and every parameter law qualify the finite model.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, mko_definition — No prior was supplied, so no Bayes update is performed.
- S07 · premise_audit · G1, S06, work — This comparison uses the complete laws, not one observed 01.
- S06 · premise_audit · G1, S05, work — A larger likelihood is not a computed parameter probability.
- S05 · premise_audit · G1, S04, work — The sum3/8 explicitly refutes treating likelihood itself as a posterior.
- S04 · premise_audit · G1, S03, mko_definition — Do not interchange the roles of x and theta.
- S03 · premise_audit · G1, S02, work — These two rows exhaust the parameter set.
- S02 · premise_audit · G1, S01, work — The weight9 is not itself probability 9.
- S01 · premise_audit · G1, work — Both rows require four entries.





## Error controls and negative controls

RowwiseCheck both complete denominator 16 rows separately.

Fixed observationFix x before traversing every theta for the likelihood table.


- The posterior at 01 is(3/16,3/16). → reject — Its sum is 3/8, not 1, and no prior is supplied.
- Each theta may silently use a different carrier. → reject — This model requires the same four-sample carrier.
- One01 proves the laws identical. → reject — Their00 probabilities differ:9/16 versus1/16.





## Result and limitations

The rows define a valid finite parametric model; both L(theta;01) values are 3/16, not a posterior.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: d00df7b6f9cdd89591f628108246c88f499ea10b7d1142e3b840f769915b49dc
- original source SHA-256: fcaef8fae4f87c9c47807672f655dbe899166728be3799d64ec5e07d2e5c74f2
- 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-parametric-statistical-model-01.json)