# Finite discrete probability distribution: validating a PMF, event probability, expectation and pushforward

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-discrete-probability-distribution/)

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-discrete-probability-distribution-01 · production-20261019-adopted-96



## Goal and scope

A random variable X takes the values −1, 0, 1, 2 with masses p(−1)=1/6, p(0)=1/3, p(1)=1/4, p(2)=1/4. (1) First check that p is a valid PMF; (2) find P(X≥1); (3) find E[X]; (4) find the pushforward distribution of Y=X², prove it is again a PMF, find E[Y] and cross-check it against Σx²p(x); (5) decide that two candidates q and r are not PMFs: every mass of q lies between 0 and 1 but the total is not 1, while r sums to 1 but has a negative mass.

Treats only mathematical distributions with a finite range of distinct values and exact rational masses (MKO assumption a1); no claim is made that the distribution comes from a sample estimate, a data fit or a real population (MKO assumption a2). The two lemmas on pushforwards and regrouped sums are proved for any finite range; the other computations concern the given numbers only. Joint distributions and Markov chains are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- frac_rules
- finite_sum_rules
- prob_axioms
- numeric_evaluation


- G1 — The range of X is R_X={−1,0,1,2}, four distinct values; p(−1)=1/6, p(0)=1/3, p(1)=1/4, p(2)=1/4, all exact rationals.
- G2 — g(x)=x² and Y=g(X).
- G3 — Two candidates on the same range: q(−1)=1/2, q(0)=1/3, q(1)=1/4, q(2)=0; r(−1)=1/2, r(0)=2/3, r(1)=−1/6, r(2)=0.
- G4 — These distributions are given mathematical distributions, not estimated or fitted from observed data (MKO assumption a2).


- R_X=\{-1,0,1,2\} — the finite range of X
- p(x) — the probability mass function of X
- P(X\in A) — the probability of the event A
- E[X] — the expectation of X
- g(x)=x^2,\ Y=g(X) — the map used for the pushforward and the new random variable
- p_Y(y) — the pushforward mass of Y





## Rules and sources


- frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
- finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
- prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- mko_pmf_def · cited — The probability mass function p of a finite discrete random variable assigns a nonnegative probability to each element of its finite value range, and all masses sum to 1. Event probabilities add the corresponding masses; expectation is the mass-weighted sum of values. · mko-finite-discrete-probability-distribution
- event_sum · prerequisite — For a subset A of the range, P(X∈A)=Σ_{x∈A} p(x); values outside A are not added.
- expectation_def · prerequisite — Expectation on a finite range: E[X]=Σ_{x∈R_X} x·p(x).
- pushforward_def · prerequisite — For a function g, Y=g(X) has range R_Y=g(R_X) and pushforward mass p_Y(y)=Σ_{x∈R_X, g(x)=y} p(x): the original masses mapped to the same new value are added.
- sum_over_partition · prerequisite — If a finite set S is the union of pairwise disjoint subsets S_y (y∈Y), then Σ_{x∈S} a_x=Σ_{y∈Y} Σ_{x∈S_y} a_x (associativity and commutativity of finite sums).
- L_pushforward_total · lemma — If p is a PMF on the finite range R_X and g is a function on R_X, then the pushforward mass p_Y is a PMF on R_Y=g(R_X).
- L_regroup · lemma — In the setting of L_pushforward_total, Σ_{y∈R_Y} y·p_Y(y)=Σ_{x∈R_X} g(x)·p(x).





## Main derivation

S01 · definitionBefore

p:R_X\to\mathbb{Q}

After

p\ \text{is a PMF}\iff \forall x\in R_X:\ p(x)\ge 0\ \land\ \sum_{x\in R_X}p(x)=1

Conditions: none

Rule: mko_pmf_def · Uses: mko_pmf_def, G1

Leaf basis: mko_pmf_def + prob_axioms

By the MKO a PMF must meet two conditions: every mass is nonnegative and all masses sum to exactly 1. The MKO's first paragraph requires checking this first; if it fails, the function may not be used as a distribution for event probabilities or expectation.



S02 · impliesBefore

R_X=\{-1,0,1,2\}

After

|R_X|=4,\ \text{values distinct}

Conditions: none

Rule: finite_counting_basics · Uses: G1

Leaf basis: finite_counting_basics

The four values −1, 0, 1, 2 are pairwise distinct, the range is finite, and each value has exactly one mass. This is what MKO assumption a1 requires: if a value appeared twice, its mass could be counted twice in the total.



S03 · impliesBefore

p(-1)=\tfrac16,\ p(0)=\tfrac13,\ p(1)=\tfrac14,\ p(2)=\tfrac14

After

\forall x\in R_X:\ p(x)\ge 0

Conditions: none

Rule: order_basics · Uses: G1

Leaf basis: order_basics + frac_rules

Each of the four masses is a positive numerator over a positive denominator, hence greater than 0 and in particular nonnegative. All four values are checked.



S04 · equivalentBefore

\sum_{x\in R_X}p(x)=\tfrac16+\tfrac13+\tfrac14+\tfrac14

After

1

Conditions: none

Rule: frac_rules · Uses: G1, S02

Leaf basis: frac_rules + finite_sum_rules + numeric_evaluation

Since the values are distinct (S02), the total adds each of the four masses exactly once. Bring them to the denominator 12 and add, as in sub-steps S04.1 and S04.2.



S05 · impliesBefore

p\ge 0,\ \sum p=1

After

p\ \text{is a PMF on } R_X

Conditions: none

Rule: mko_pmf_def · Uses: S01, S03, S04

Leaf basis: mko_pmf_def + and_intro_elim

S03 gives nonnegativity and S04 gives total exactly 1, so by the PMF conditions in S01, p is a PMF, and only now may event probabilities and expectations be computed.



S06 · equivalentBefore

A=\{x\in R_X\mid x\ge 1\}

After

A=\{1,2\}

Conditions: none

Rule: set_builder · Uses: G1

Leaf basis: set_builder + order_basics

Test each value of the range for x≥1: −1 no, 0 no, 1 yes (equality holds), 2 yes. So the event X≥1 corresponds to A={1,2}.



S07 · equivalentBefore

P(X\ge 1)=\sum_{x\in A}p(x)

After

\tfrac14+\tfrac14=\tfrac12

Conditions: none

Rule: event_sum · Uses: S05, S06, event_sum

Leaf basis: event_sum + frac_rules + numeric_evaluation

An event's probability is the sum of the masses of the values it contains (MKO paragraph 2): p(1)+p(2)=1/4+1/4=1/2; the values −1 and 0 outside the event are not added.



S08 · impliesBefore

P(X\in R_X\setminus A)=\tfrac16+\tfrac13

After

\tfrac12,\quad P(A)+P(R_X\setminus A)=1

Conditions: none

Rule: event_sum · Uses: S05, S06, S07, event_sum

Leaf basis: event_sum + prob_axioms + numeric_evaluation

Check: the complementary event {−1,0} has probability 1/6+1/3=1/2; the two add up to 1, in line with P(Aᶜ)=1−P(A) from the probability axioms.



S09 · equivalentBefore

E[X]=\sum_{x\in R_X}x\,p(x)

After

\tfrac{7}{12}

Conditions: none

Rule: expectation_def · Uses: S05, expectation_def

Leaf basis: expectation_def + frac_rules + numeric_evaluation

The expectation is the mass-weighted sum of the values (MKO). The terms are formed in S09.1 and added in S09.2.



S10 · impliesBefore

g(-1)=1,\ g(0)=0,\ g(1)=1,\ g(2)=4

After

R_Y=\{0,1,4\};\ g^{-1}(0)=\{0\},\ g^{-1}(1)=\{-1,1\},\ g^{-1}(4)=\{2\}

Conditions: none

Rule: image_preimage_def · Uses: G1, G2, pushforward_def

Leaf basis: image_preimage_def + function_def + numeric_evaluation

Compute g(x)=x² value by value: (−1)²=1, 0²=0, 1²=1, 2²=4. The new range is the image {0,1,4}; the preimage of each new value is the set of old values mapped to it. Both −1 and 1 map to 1.



S11 · equivalentBefore

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)

After

p_Y(0)=\tfrac13,\ p_Y(1)=\tfrac16+\tfrac14=\tfrac{5}{12},\ p_Y(4)=\tfrac14

Conditions: none

Rule: pushforward_def · Uses: S10, G1, pushforward_def

Leaf basis: pushforward_def + frac_rules + numeric_evaluation

By the pushforward definition, add the original masses mapped to the same new value (MKO paragraph 3): p_Y(1)=p(−1)+p(1)=2/12+3/12=5/12; the other two preimages have one element each.



S12 · theorem_applicationBefore

p_Y\ \text{on } R_Y=\{0,1,4\}

After

p_Y\ \text{is a PMF};\ \tfrac13+\tfrac{5}{12}+\tfrac14=1

Conditions: none

Rule: L_pushforward_total · Uses: S05, S11

Leaf basis: L_pushforward_total + numeric_evaluation

By Lemma L_pushforward_total (proved in S12.1 and S12.2 for any finite range), p being a PMF makes p_Y a PMF. Direct check: 4/12+5/12+3/12=12/12=1, consistent with the lemma.



S13 · equivalentBefore

E[Y]=\sum_{y\in R_Y}y\,p_Y(y)

After

0\cdot\tfrac13+1\cdot\tfrac{5}{12}+4\cdot\tfrac14=\tfrac{17}{12}

Conditions: none

Rule: expectation_def · Uses: S11, S12, expectation_def

Leaf basis: expectation_def + frac_rules + numeric_evaluation

p_Y is a PMF (S12), so its expectation may be computed: 0+5/12+1=5/12+12/12=17/12.



S14 · equivalentBefore

\sum_{y\in R_Y}y\,p_Y(y)

After

\sum_{x\in R_X}x^2p(x)=\tfrac16+0+\tfrac14+1=\tfrac{17}{12}

Conditions: none

Rule: L_regroup · Uses: S12, S13

Leaf basis: L_regroup + frac_rules + numeric_evaluation

Cross-check: by Lemma L_regroup (proved in S14.1), the expectation of Y can also be computed directly on the range of X: Σx²p(x)=1·(1/6)+0·(1/3)+1·(1/4)+4·(1/4)=2/12+0+3/12+12/12=17/12, the same as S13.



S15 · impliesBefore

\sum_{x}q(x)=\tfrac12+\tfrac13+\tfrac14+0

After

\tfrac{13}{12}\neq 1;\ q\ \text{is not a PMF}

Conditions: none

Rule: mko_pmf_def · Uses: G3, S01

Leaf basis: mko_pmf_def + frac_rules + numeric_evaluation

Every mass of q lies between 0 and 1, but the total is 6/12+4/12+3/12+0=13/12≠1, which fails the PMF conditions, so q is not a PMF and may not be used for event probabilities or an expectation.



S16 · impliesBefore

r(1)=-\tfrac16,\ \sum_x r(x)=1

After

r\ \text{is not a PMF}

Conditions: none

Rule: mko_pmf_def · Uses: G3, S01

Leaf basis: mko_pmf_def + order_basics + numeric_evaluation

r sums to 3/6+4/6−1/6+0=6/6=1, but r(1)=−1/6<0 violates nonnegativity, so r is not a PMF. The two PMF conditions are independent and both are required.







## Substeps and lemmas

S04.1 · equivalentBefore

\tfrac16+\tfrac13+\tfrac14+\tfrac14

After

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{3}{12}

Conditions: 2,4,3\neq 0

Rule: frac_rules · Uses: frac_rules

Leaf basis: frac_rules

Multiplying numerator and denominator by the same nonzero integer does not change a fraction: 1/6=2/12 (by 2), 1/3=4/12 (by 4), 1/4=3/12 (by 3).



S04.2 · equivalentBefore

\tfrac{2}{12}+\tfrac{4}{12}+\tfrac{3}{12}+\tfrac{3}{12}

After

\tfrac{12}{12}=1

Conditions: 12\neq 0

Rule: frac_rules · Uses: S04.1, frac_rules

Leaf basis: frac_rules + numeric_evaluation

Fractions with a common denominator add by their numerators: 2+4+3+3=12, giving 12/12=1. The total is exactly 1, not approximately 1.



S09.1 · equivalentBefore

\sum_{x\in R_X}x\,p(x)

After

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

Conditions: none

Rule: finite_sum_rules · Uses: G1, expectation_def

Leaf basis: finite_sum_rules

Expand the finite sum over the four values of the range, each value multiplied by its own mass. The term for the value 0 is 0 but still belongs to the sum.



S09.2 · equivalentBefore

(-1)\cdot\tfrac16+0\cdot\tfrac13+1\cdot\tfrac14+2\cdot\tfrac14

After

-\tfrac{2}{12}+0+\tfrac{3}{12}+\tfrac{6}{12}=\tfrac{7}{12}

Conditions: none

Rule: frac_rules · Uses: S09.1, frac_rules

Leaf basis: frac_rules + neg_mul + mul_zero + numeric_evaluation

The terms are −1/6=−2/12, 0, 1/4=3/12 and 2/4=6/12; adding numerators, −2+0+3+6=7, gives 7/12. An expectation need not be a value in the range.



S12.1 · impliesBefore

p(x)\ge 0\ \forall x

After

p_Y(y)=\sum_{x\in g^{-1}(y)}p(x)\ge 0

Conditions: none

Rule: order_basics · Uses: pushforward_def, order_basics

Leaf basis: order_basics + finite_sum_rules

For any y∈R_Y, p_Y(y) is a sum of nonnegative numbers, and a sum of nonnegative numbers is nonnegative (order is compatible with addition, applied term by term). This proves nonnegativity of the pushforward masses.



S12.2 · equivalentBefore

\sum_{y\in R_Y}p_Y(y)=\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}p(x)

After

\sum_{x\in R_X}p(x)=1

Conditions: none

Rule: sum_over_partition · Uses: S12.1, pushforward_def, sum_over_partition

Leaf basis: sum_over_partition + function_def + prob_axioms

Since g is a function, each x∈R_X lies in exactly one preimage g⁻¹(g(x)): the preimages are pairwise disjoint with union R_X. By summing over a partition, the double sum equals the sum over R_X, which is 1 because p is a PMF. S12.1 and S12.2 together prove Lemma L_pushforward_total.



S14.1 · equivalentBefore

\sum_{y\in R_Y}y\sum_{x\in g^{-1}(y)}p(x)

After

\sum_{y\in R_Y}\sum_{x\in g^{-1}(y)}g(x)p(x)=\sum_{x\in R_X}g(x)p(x)

Conditions: none

Rule: sum_over_partition · Uses: pushforward_def, sum_over_partition, distributive

Leaf basis: distributive + eq_replace + sum_over_partition + finite_sum_rules

After substituting the definition of p_Y(y), distribute y into the inner sum; every x in the inner sum satisfies g(x)=y, so y may be replaced by g(x); finally summing over the partition merges the double sum into a sum over R_X. S14.1 proves Lemma L_regroup.







## Reverse audits


- S16 · sufficient_goal_reduction · G3, mko_pmf_def, order_basics — Goal G: r is not a PMF. Sufficient condition H: some mass is negative; H⇒G by the definition. H is read off G3 (N13); G is never used as a premise.
- S15 · sufficient_goal_reduction · G3, mko_pmf_def, numeric_evaluation — Goal G: q is not a PMF. Sufficient condition H: the total is not 1; H⇒G by the definition. H comes from exact summation (N10, N11); G is never used as a premise.
- S14.1 · inverse_equivalence · distributive, eq_replace, sum_over_partition — Distributivity, replacement of equals and summing over a partition are all equations; undoing them in order restores the original.
- S14 · inverse_equivalence · L_regroup, numeric_evaluation — The lemma is an equation and holds both ways; the two independent computations give the same 17/12 (N8, N9).
- S13 · inverse_equivalence · expectation_def, frac_rules, numeric_evaluation — Exact evaluation (N8); both sides are the same number.
- S12.2 · inverse_equivalence · sum_over_partition, function_def — Summing over a partition is an equation and holds both ways; the key condition, each x in exactly one block, holds because g is a function.
- S12.1 · premise_audit · pushforward_def, order_basics — Only nonnegativity of p is used; neither p_Y(y)>0 nor any converse is claimed.
- S12 · premise_audit · S05, L_pushforward_total — The lemma needs p to be a PMF (S05) and g to be a function (G2); the numeric check N7 is a consistency check and does not replace the lemma.
- S11 · inverse_equivalence · pushforward_def, frac_rules, numeric_evaluation — Each p_Y(y) is an exact evaluation of its defining sum (N6), so the step is two-way.
- S10 · premise_audit · image_preimage_def, G2 — The three preimages are pairwise disjoint with union R_X, the partition property used in S12.2; g is not injective, so values of Y cannot be matched one-to-one with values of X.
- S09.2 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational arithmetic, independently recomputable.
- S09.1 · inverse_equivalence · finite_sum_rules — Expanding a finite sum and folding it back are inverse moves.
- S09 · inverse_equivalence · expectation_def, numeric_evaluation — Exact evaluation (N5); both sides are the same number.
- S08 · premise_audit · S07, event_sum, prob_axioms — This is a consistency check, not a new inference; it confirms that S07 neither missed nor double-counted a mass.
- S07 · inverse_equivalence · event_sum, frac_rules, numeric_evaluation — Exact evaluation; both sides are the same number (N3). The prerequisite is S05, which confirmed that p is a PMF.
- S06 · inverse_equivalence · set_builder — Membership in set-builder notation is two-way, and all four values were tested.
- S05 · sufficient_goal_reduction · S03, S04, mko_pmf_def — Goal G: p is a PMF. Sufficient condition H: nonnegative with total 1; H⇒G by the definition. H is proved forwards in S03 and S04; G is never used as a premise.
- S04.2 · inverse_equivalence · frac_rules, numeric_evaluation — Integer addition and the fraction rule are equations, independently recomputable (N2).
- S04.1 · inverse_equivalence · frac_rules — Reducing the fractions is the backward move, given the multipliers are nonzero.
- S04 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational evaluation; both sides are the same number (N1), so the step is two-way.
- S03 · premise_audit · G1, order_basics — Nonnegativity is only one of the PMF conditions; it does not give total 1.
- S02 · premise_audit · G1, finite_counting_basics — Only the shape of the range is checked; nothing is said about the sizes of the masses.
- S01 · premise_audit · mko_pmf_def, prob_axioms — This step only states the PMF conditions and derives no new fact; the two conditions match the axioms of nonnegativity and total probability 1.





## Error controls and negative controls

Masses between 0 and 1 do not make the total 1The MKO names the mistake of ignoring the total because every mass lies between 0 and 1. Every mass of q lies in [0,1], yet the total is 13/12; r sums to 1 yet has a negative mass. Both conditions must be checked, adding exact fractions rather than decimal approximations.

A theoretical PMF is not a data fitAnother mistake identified in the MKO is passing off a theoretical PMF as the result of a data fit. The masses 1/6, 1/3, 1/4, 1/4 here are a given mathematical distribution (G4) with no observed data; saying 'exactly 2 of 12 trials gave −1' or 'this distribution was estimated from a sample' goes beyond anything this guide supports. The pushforward is likewise an exact mathematical transformation.

A pushforward merges masses with the same imageBoth −1 and 1 map to 1, so p_Y(1)=1/6+1/4=5/12. Taking only p(1)=1/4, or listing the value 1 twice, breaks the total of 1 or the distinctness of values. Also E[X²]=17/12 differs from (E[X])²=49/144: the expectation of a square is in general not the square of the expectation.


- Every mass of q lies between 0 and 1, so q is a PMF → reject — q sums to 13/12≠1.
- r sums to 1, so r is a PMF → reject — r(1)=−1/6<0 violates nonnegativity.
- P(X≥1)=p(2)=1/4, since only 2 is greater than 1 → reject — The event is x≥1, which includes 1; P(X≥1)=1/4+1/4=1/2.
- E[X²]=(E[X])²=49/144 → reject — E[X²]=17/12, which differs from 49/144.
- p_Y(1)=p(1)=1/4, because g(1)=1 → reject — g(−1)=1 maps to 1 as well and must be added: p_Y(1)=5/12.





## Result and limitations

p is nonnegative with total exactly 1, so it is a PMF. P(X≥1)=p(1)+p(2)=1/2 and E[X]=7/12. The pushforward of Y=X² is p_Y(0)=1/3, p_Y(1)=5/12, p_Y(4)=1/4, again a PMF (proved for any finite range), and E[Y]=17/12, agreeing with Σx²p(x). q has every mass between 0 and 1 but total 13/12, and r sums to 1 but r(1)=−1/6, so neither is a PMF.


- Lemmas L_pushforward_total and L_regroup are proved for finite ranges only; countable or continuous cases need series or integrals and are not treated here.
- Joint distributions, discrete random processes and finite Markov chains (the MKO's formal next) are not treated, and no statistical inference is made.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: c76a1162145f6b40efb60946aa3c825a45dc36a902c036a45e633fa39245b697
- original source SHA-256: c76a1162145f6b40efb60946aa3c825a45dc36a902c036a45e633fa39245b697
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-discrete-probability-distribution-01.json)