# A sufficiency certificate from every fibre conditional law [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-sufficient-statistic/) 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-finite-sufficient-statistic-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Audit invariance across theta on every positive-mass fibre, retaining undefined null conditions. No factorization theorem or estimator-quality inference. ## Givens and symbols - work - G1 — Theta={0,1}, Omega={a,b,c,d,z}; P0=(1/8,3/8,1/4,1/4,0), P1=(1/16,3/16,3/8,3/8,0). S(a)=S(b)=0, S(c)=S(d)=1, S(z)=2. - S — total statistic - t — fibre label ## Rules and sources - mko_definition · cited — A statistic is a total map on the full sample carrier and its fibers form a partition. For every (theta,t) first compute P_theta(T=t). Define and calculate the exact fiber conditional law only on a positive-mass cell, then compare all valid theta laws at each t. Leave zero-mass conditions undefined, encoded as null in these outputs. Separate explicit nonsufficiency witnesses, the identity statistic and the constant-statistic boundary. No factorization theorem or estimator-quality conclusion is introduced. · mko-finite-sufficient-statistic - work · prerequisite — Finite sufficiency: on each fibre compare full conditional laws only where conditioning has positive mass, requiring theta invariance; null quotients remain undefined. ## Main derivation S01 · impliesBefore P_0,P_1 After 1/8+3/8+1/4+1/4=1,\quad1/16+3/16+3/8+3/8=1 Conditions: none Rule: work · Uses: G1, work Leaf basis: work Both complete laws are normalized and nonnegative. S02 · impliesBefore S^{-1}(0),S^{-1}(1),S^{-1}(2) After \{a,b\},\{c,d\},\{z\} Conditions: none Rule: work · Uses: G1, S01, work Leaf basis: work S is total and its three nonempty fibres form a complete partition. S03 · impliesBefore P_\theta(S=t),\quad t=(0,1,2) After P_0^S=(1/2,1/2,0),\quad P_1^S=(1/4,3/4,0) Conditions: none Rule: work · Uses: G1, S02, work Leaf basis: work Compute every fibre mass before deciding where conditioning is defined. S04 · impliesBefore t=0:\quad P_0(a\mid S=0)=\frac{1/8}{1/2},\quad P_1(a\mid S=0)=\frac{1/16}{1/4} After P_0(\cdot\mid S=0)=P_1(\cdot\mid S=0)=(1/4,3/4,0,0,0) Conditions: none Rule: work · Uses: G1, S03, work Leaf basis: work The conditional masses of a,b agree across theta; the other three outcomes have mass zero. S05 · impliesBefore t=1:\quad\frac{1/4}{1/2}=\frac{3/8}{3/4}=1/2 After P_0(\cdot\mid S=1)=P_1(\cdot\mid S=1)=(0,0,1/2,1/2,0) Conditions: none Rule: work · Uses: G1, S04, work Leaf basis: work The second positive-mass fibre also has a fully invariant conditional law. S06 · impliesBefore P_0(S=2)=P_1(S=2)=0 After P_\theta(\cdot\mid S=2)\text{ undefined for both }\theta Conditions: none Rule: work · Uses: G1, S05, work Leaf basis: work Do not invent a0/0 distribution; this fibre has no valid theta conditions to compare. S07 · impliesBefore \text{all positive fibre conditionals invariant across valid }\theta After S\text{ is sufficient for this finite model} Conditions: none Rule: work · Uses: G1, S06, work Leaf basis: work Both parameters and all three fibres are exhausted, giving sufficiency by the finite conditional-law definition. S08 · impliesBefore R(x)\equiv0 After P_0(a\mid R=0)=1/8\ne1/16=P_1(a\mid R=0) Conditions: none Rule: work · Uses: G1, S07, work Leaf basis: work The constant statistic R has the single fibre Omega, with probability 1 under each theta. The conditional distribution of the sample outcome given R=0 is P_theta itself and varies with theta, so R is not sufficient for this finite model. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07, work — The identity statistic instead has point-mass conditionals on valid fibres and is sufficient; the boundaries differ. - S07 · premise_audit · G1, S06, work — No factorization theorem replaced the table audit. - S06 · premise_audit · G1, S05, work — Undefined is not a zero-vector probability law. - S05 · premise_audit · G1, S04, work — Both theta denominators on this cell are positive. - S04 · premise_audit · G1, S03, work — List the full five-point conditional law, not only a. - S03 · premise_audit · G1, S02, work — Sufficiency does not require the marginal law of S to be invariant. - S02 · premise_audit · G1, S01, work — Do not omit null fibre{z}. - S01 · premise_audit · G1, work — z has zero mass in both laws but remains in the carrier. ## Error controls and negative controls Mass firstCompute each(theta,t) fibre mass before division. Complete conditionalsList all five sample probabilities on each valid cell. - Sufficiency requires an invariant law of S. → reject — S is sufficient here although P0(S=0)=1/2 and P1(S=0)=1/4. - Use(0,0,0,0,0) as the law at S=2. → reject — It sums to 0 and conditioning has zero denominator, so it is undefined. - Constant R is sufficient here. → reject — Its conditional probability of a varies as1/8 or1/16. ## Result and limitations S is sufficient and constant R is not; null-fibre conditional laws remain undefined. ## Verification and source binding 3 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 7b86518f187ccbc75abb75a795f774026b2bfa13c74cea0f969179bcaa062304 - original source SHA-256: 99f4f978f27d4111a01876f24ceb88ab0e95d184de6346874988ea73556fac8f - 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-finite-sufficient-statistic-01.json)