# Fractions: deciding equal value, normalizing to lowest terms with a positive denominator, and adding fractions

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

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-fraction-01 · production-20261019-adopted-96



## Goal and scope

(1) Decide whether (−6)/(−8) and 9/12 represent the same rational number; (2) bring (−6)/(−8) to lowest terms with a positive denominator and show that the value is unchanged; (3) compute 3/4+5/6 and show that 'numerator plus numerator over denominator plus denominator', giving 8/10, is not the sum; (4) explain why 3/0 is not a valid fraction representation.

Inside the MKO's scope: integer numerators and denominators with nonzero denominators (assumption a1), the value of p/q being the rational number p·(1/q). The guide proves the equality criterion ps=rq and the addition formula from rational arithmetic; it does not prove the general uniqueness of the lowest-terms positive-denominator representation (see open items), and does not change the canonical MKO or its English edition.





## Givens and symbols


- mul_inverse_nonzero
- zero_product
- frac_rules
- mul_assoc
- mul_comm
- numeric_evaluation


- G1 — p, q, r and s are integers and every number used as a denominator is nonzero (MKO assumption a1); for q≠0, p/q denotes the rational number p·(1/q).
- G2 — The representations to handle: (−6)/(−8), 9/12, 3/4, 5/6 and 6/8, and the expression 3/0.


- \frac{p}{q} — a fraction representation, with value p·(1/q)
- ps=rq — the cross-product equation
- \gcd(m,n) — the greatest common divisor of m and n
- \mathbb{Q} — the rational numbers





## Rules and sources


- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
- 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.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
- iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
- divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- 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.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_fraction_def · cited — For integers p and q with q≠0, p/q represents a rational number. Two valid representations p/q and r/s have the same value exactly when ps=rq; reduction and positive-denominator normalization change the representation without changing the value. · mko-fraction
- gcd_def · prerequisite — For integers m, n not both 0, gcd(m,n) is the largest positive integer dividing both; p/q is in lowest terms with a positive denominator when q>0 and gcd(p,q)=1.
- L_cross · lemma — For integers p, q, r, s with q≠0 and s≠0: p/q=r/s ⇔ ps=rq.
- L_add · lemma — For integers p, q, r, s with q≠0 and s≠0: p/q+r/s=(ps+rq)/(qs).





## Main derivation

S01 · definitionBefore

\frac{-6}{-8},\ \frac{9}{12}

After

\text{valid representations, since}\ -8\neq 0,\ 12\neq 0

Conditions: -8\neq 0; 12\neq 0

Rule: mko_fraction_def · Uses: G1, G2, mko_fraction_def

Leaf basis: mko_fraction_def + numeric_evaluation

By the MKO, p/q with an integer p and a nonzero integer q is a valid representation. The denominators −8 and 12 are both nonzero, so both expressions represent rational numbers. A negative numerator or denominator does not affect validity.



S02 · equivalentBefore

\frac{-6}{-8}=\frac{9}{12}

After

(-6)\cdot 12=9\cdot(-8)

Conditions: -8\neq 0; 12\neq 0

Rule: L_cross · Uses: S01, L_cross

Leaf basis: L_cross

By Lemma L_cross with p=−6, q=−8, r=9, s=12, the two representations have equal value exactly when the cross products agree. The lemma needs q≠0 and s≠0, which S01 checked.



S03 · equivalentBefore

(-6)\cdot 12=9\cdot(-8)

After

-72=-72

Conditions: none

Rule: numeric_evaluation · Uses: S02

Leaf basis: numeric_evaluation

Compute both cross products exactly: (−6)·12=−72 and 9·(−8)=−72. The two sides are equal, so the cross-product equation is true.



S04 · impliesBefore

(-6)\cdot 12=9\cdot(-8)\ \text{true}

After

\frac{-6}{-8}=\frac{9}{12}

Conditions: none

Rule: modus_ponens · Uses: S02, S03

Leaf basis: modus_ponens + iff_intro

The equivalence of S02 together with the true cross-product equation of S03 gives (−6)/(−8)=9/12: two representations with different denominators and different signs name the same rational number.



S05 · equivalentBefore

\frac{-6}{-8}

After

\frac{(-6)(-1)}{(-8)(-1)}=\frac{6}{8}

Conditions: k=-1\neq 0

Rule: frac_rules · Uses: S01, frac_rules

Leaf basis: frac_rules + numeric_evaluation

Positive-denominator normalization: by frac_rules (a/b=(ak)/(bk) for k≠0), multiply numerator and denominator by k=−1 to get 6/8, whose denominator is positive. Check: (−6)·8=−48=6·(−8), so by L_cross the value is the same.



S06 · equivalentBefore

\frac{6}{8}

After

\frac{3\cdot 2}{4\cdot 2}=\frac{3}{4}

Conditions: k=2\neq 0

Rule: frac_rules · Uses: S05, gcd_def, frac_rules

Leaf basis: frac_rules + gcd_def + numeric_evaluation

Reduction: the positive divisors of 6 are 1, 2, 3, 6 and those of 8 are 1, 2, 4, 8; the largest common one is 2, so gcd(6,8)=2. Since 6=3·2 and 8=4·2, frac_rules with k=2≠0 gives 6/8=3/4.



S07 · equivalentBefore

\frac{9}{12}

After

\frac{3\cdot 3}{4\cdot 3}=\frac{3}{4}

Conditions: k=3\neq 0

Rule: frac_rules · Uses: S04, gcd_def, frac_rules

Leaf basis: frac_rules + gcd_def + numeric_evaluation

gcd(9,12)=3 (the positive divisors of 9 are 1, 3, 9 and those of 12 are 1, 2, 3, 4, 6, 12), and 9=3·3, 12=4·3, so 9/12=3/4. Both original representations reduce to the same 3/4, in agreement with S04.



S08 · impliesBefore

\frac{3}{4}

After

4>0,\ \gcd(3,4)=1:\ \text{lowest terms, positive denominator}

Conditions: none

Rule: gcd_def · Uses: S06, S07, gcd_def

Leaf basis: gcd_def + divides_def + numeric_evaluation

The positive divisors of 3 are 1 and 3, and 3 does not divide 4, so gcd(3,4)=1; the denominator 4 is positive. Hence 3/4 is in lowest terms with a positive denominator. (−6)/(−8), 6/8, 9/12 and 3/4 are four representations of one value: as the MKO says, reduction and normalization change the representation, not the value.



S09 · equivalentBefore

\frac{3}{4}+\frac{5}{6}

After

\frac{3\cdot 6+5\cdot 4}{4\cdot 6}=\frac{38}{24}

Conditions: 4\neq 0; 6\neq 0

Rule: L_add · Uses: L_add

Leaf basis: L_add + numeric_evaluation

By Lemma L_add with p=3, q=4, r=5, s=6: numerator 3·6+5·4=18+20=38 and denominator 4·6=24.



S10 · equivalentBefore

\frac{38}{24}

After

\frac{19\cdot 2}{12\cdot 2}=\frac{19}{12}

Conditions: k=2\neq 0

Rule: frac_rules · Uses: S09, gcd_def, frac_rules

Leaf basis: frac_rules + gcd_def + numeric_evaluation

gcd(38,24)=2: 38=2·19 with 19 prime and not dividing 24, so the only common positive divisors are 1 and 2. Since 38=19·2 and 24=12·2, reduction gives 19/12; gcd(19,12)=1 and 12>0, so this is in lowest terms with a positive denominator. Hence 3/4+5/6=19/12.



S11 · impliesBefore

\frac{3+5}{4+6}=\frac{8}{10}\ \text{vs}\ \frac{19}{12}

After

8\cdot 12=96\neq 190=19\cdot 10,\ \text{so}\ \frac{8}{10}\neq\frac{19}{12}

Conditions: 10\neq 0; 12\neq 0

Rule: L_cross · Uses: S10, L_cross

Leaf basis: L_cross + contrapositive + numeric_evaluation

'Numerator plus numerator over denominator plus denominator' gives 8/10. By L_cross, 8/10=19/12 exactly when 8·12=19·10; but 96≠190, so 8/10≠19/12. This textual operation is not fraction addition (third paragraph of the MKO).



S12 · impliesBefore

\frac{6}{8}\ (=\tfrac{3}{4})\ \text{and}\ \frac{5}{6}

After

\frac{6+5}{8+6}=\frac{11}{14}\neq\frac{8}{10},\quad \frac{6\cdot 6+5\cdot 8}{8\cdot 6}=\frac{76}{48}=\frac{19}{12}

Conditions: 8\neq 0; 6\neq 0; 14\neq 0; 48\neq 0

Rule: L_cross · Uses: S05, S06, L_cross, L_add

Leaf basis: L_cross + L_add + numeric_evaluation

Replacing 3/4 by the equal 6/8 and repeating the textual operation gives 11/14; but 11·10=110≠112=8·14, so 11/14≠8/10. The same pair of values yields two different results, so the textual operation is not an operation on numbers at all; it depends on the notation. Genuine addition by L_add gives 76/48, and 76·12=912=19·48, so it is still 19/12: the result depends only on the values.



S13 · impliesBefore

\frac{3}{0}

After

\text{not a valid representation: } 0\ \text{has no inverse}

Conditions: none

Rule: mul_inverse_nonzero · Uses: G1, mul_inverse_nonzero, mko_fraction_def

Leaf basis: mul_inverse_nonzero + mul_zero + mko_fraction_def

3/0 would mean 3·(1/0), but 0 has no inverse (0·t=0≠1 for every t), so 3/0 names no rational number, and in particular not zero. The MKO defines p/q only for q≠0. L_cross also holds only for nonzero denominators: forced onto 3/0 and 6/0, the cross products 3·0=0=6·0 agree, yet there are no values to compare.



S14 · impliesBefore

S04,\ S08,\ S10,\ S11,\ S13

After

\frac{-6}{-8}=\frac{9}{12}=\frac{3}{4},\ \ \frac{3}{4}+\frac{5}{6}=\frac{19}{12}\neq\frac{8}{10},\ \ \frac{3}{0}\ \text{invalid}

Conditions: none

Rule: and_intro_elim · Uses: S04, S08, S10, S11, S13

Leaf basis: and_intro_elim

The four goals are completed by S04 (equal value), S05 to S08 (normalization with unchanged value), S09 to S11 (addition and the wrong textual operation) and S13 (zero denominator).







## Substeps and lemmas

S02.1 · impliesBefore

q\neq 0,\ s\neq 0

After

qs\neq 0

Conditions: none

Rule: zero_product · Uses: zero_product

Leaf basis: zero_product + de_morgan_logic

By the zero-product property, qs=0 ⇔ q=0 or s=0. Neither holds, so qs≠0, and therefore 1/(qs) exists.



S02.2 · impliesBefore

\frac{p}{q}=\frac{r}{s}

After

ps=rq

Conditions: q\neq 0; s\neq 0

Rule: eq_congruence · Uses: G1, eq_congruence, mul_inverse_nonzero

Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one

Multiply both sides by qs: the left side is p·(1/q)·q·s=p·1·s=ps, and the right side is r·(1/s)·q·s=r·q·(s·(1/s))=rq (associativity, commutativity, q·(1/q)=1 and s·(1/s)=1). So ps=rq.



S02.3 · impliesBefore

ps=rq

After

\frac{p}{q}=\frac{r}{s}

Conditions: qs\neq 0

Rule: eq_congruence · Uses: S02.1, eq_congruence, frac_rules

Leaf basis: eq_congruence + frac_rules + mul_comm

By S02.1, qs≠0; multiply both sides by 1/(qs): the left side is (ps)/(qs)=p/q (frac_rules, cancelling the nonzero s), and the right side is (rq)/(qs)=(rq)/(sq)=r/s (commutativity, then cancelling the nonzero q). So p/q=r/s. S02.1 to S02.3 together prove Lemma L_cross.



S09.1 · equivalentBefore

\frac{p}{q}+\frac{r}{s}

After

\frac{ps}{qs}+\frac{rq}{qs}

Conditions: q\neq 0; s\neq 0

Rule: frac_rules · Uses: frac_rules, mul_comm

Leaf basis: frac_rules + mul_comm

By scaling in frac_rules (k≠0): p/q=(ps)/(qs) with k=s≠0, and r/s=(rq)/(sq)=(rq)/(qs) with k=q≠0 and commutativity sq=qs. The two fractions now share the denominator qs.



S09.2 · equivalentBefore

\frac{ps}{qs}+\frac{rq}{qs}

After

\frac{ps+rq}{qs}

Conditions: qs\neq 0

Rule: frac_rules · Uses: S09.1, S02.1, frac_rules

Leaf basis: frac_rules + distributive

Adding over a common denominator: a/c+b/c=(a+b)/c with c=qs≠0 (S02.1). S09.1 and S09.2 together prove Lemma L_add.







## Reverse audits


- S14 · sufficient_goal_reduction · S04, S08, S10, S11, S13, and_intro_elim — Goal G: (1) to (4). Sufficient condition H: S04, S08, S10, S11 and S13 each hold; H⇒G by conjunction introduction. H is proved forwards from the lemmas and exact computation, and G is never used as a premise.
- S13 · premise_audit · mul_inverse_nonzero, mko_fraction_def — The conclusion says only that 3/0 is not a valid representation; cross products are not claimed to give it a value.
- S12 · premise_audit · L_cross, L_add, S06 — Every comparison goes through L_cross, and all denominators used (8, 6, 10, 14, 48, 12) are nonzero.
- S11 · premise_audit · L_cross, S10, numeric_evaluation — This uses L_cross in contrapositive form: unequal cross products give unequal values; both denominators 10 and 12 are nonzero.
- S10 · inverse_equivalence · frac_rules, gcd_def — Reduction changes the representation, not the value; N11 to N13 recompute it.
- S09.2 · inverse_equivalence · frac_rules, S02.1 — This is an identity for every nonzero c, so it holds both ways.
- S09.1 · inverse_equivalence · frac_rules, mul_comm — Scaling up and reducing undo each other; they need s≠0 and q≠0.
- S09 · inverse_equivalence · L_add — The lemma is an equality of numbers, so both sides name the same rational and the step is two-way; the lemma is proved in S09.1 and S09.2.
- S08 · premise_audit · gcd_def, S06, S07 — This step claims only that 3/4 meets the lowest-terms conditions; it does not claim that lowest-terms representations of rationals are unique in general, which needs a further theorem.
- S07 · inverse_equivalence · frac_rules, gcd_def — The backward move multiplies by 3; k=3≠0.
- S06 · inverse_equivalence · frac_rules, gcd_def — The backward move multiplies numerator and denominator by 2; both directions use only k=2≠0.
- S05 · inverse_equivalence · frac_rules, L_cross — Multiplying by −1 again returns the original representation; k≠0 is needed.
- S04 · premise_audit · S02, S03, modus_ponens — The conclusion comes from the cross products, not from comparing denominators.
- S03 · inverse_equivalence · numeric_evaluation — Exact evaluation does not change whether the equation holds (N1, N2).
- S02.3 · premise_audit · S02.1, frac_rules, eq_congruence — Multiplying by 1/(qs) needs qs≠0; if zero denominators were allowed, ps=rq would not lead back to any relation between values (see error control 2).
- S02.2 · premise_audit · eq_congruence, mul_inverse_nonzero, mul_assoc, mul_comm — The simplification needs 1/q and 1/s to exist, that is q≠0 and s≠0. This is the ⇒ direction; ⇐ is in S02.3.
- S02.1 · premise_audit · zero_product — Both denominators must be nonzero; if either is 0 then qs is 0.
- S02 · inverse_equivalence · L_cross, S01 — Both directions of the lemma are proved in S02.2 and S02.3.
- S01 · premise_audit · G1, mko_fraction_def — This step only checks the validity condition (nonzero denominators) and derives no relation between values.





## Error controls and negative controls

Different denominators do not mean different valuesThe MKO points out that the written form of a fraction is not unique. (−6)/(−8), 6/8, 9/12 and 3/4 all have different denominators but the same value. To decide whether two representations are equal, compare the cross products ps and rq (L_cross), not the numerators or denominators.

A zero denominator does not mean zeroThe MKO notes that a zero denominator does not mean zero. 0/5 is zero (zero numerator, nonzero denominator), but 3/0 is not a representation at all, because 0 has no inverse. The cross-product criterion holds only for nonzero denominators: forced onto 3/0 and 6/0, 3·0=6·0 would 'prove' them equal, which is meaningless.

Adding numerators and denominators separately is not fraction additionThe textual operation turns 3/4 and 5/6 into 8/10, but the true sum is 19/12, and 8·12=96≠190=19·10. Worse, writing 3/4 as 6/8 first gives 11/14≠8/10: the result depends on the notation, so it is not an operation on numbers. The correct formula is p/q+r/s=(ps+rq)/(qs) (L_add).


- 9/12 and (−6)/(−8) have different denominators, so their values differ → reject — (−6)·12=−72=9·(−8), so they are equal by L_cross.
- 3/0=0 → reject — 0 has no inverse, so 3/0 is not a valid representation; zero is represented by fractions such as 0/5, with zero numerator and nonzero denominator.
- 3/4+5/6=(3+5)/(4+6)=4/5 → reject — The sum is 19/12, and 4·12=48≠95=19·5.
- Since 3·0=6·0, we have 3/0=6/0 → reject — L_cross needs nonzero denominators; 3/0 and 6/0 name no numbers.





## Result and limitations

(−6)/(−8)=9/12 because (−6)·12=−72=9·(−8); its lowest-terms positive-denominator form is 3/4, and reduction and normalization change only the representation. 3/4+5/6=(18+20)/24=38/24=19/12, while the 'add numerators and denominators separately' result 8/10 is not 19/12 and even changes with the notation. 3/0 is not a valid representation, and a zero denominator does not mean zero.


- This guide only verifies that 3/4 and 19/12 are in lowest terms with positive denominators; it does not prove the general uniqueness (every rational has exactly one such representation), which needs Euclid's lemma or Bézout's identity and is left for later.
- N17 is a polynomial-identity check in p, q, k showing that scaling preserves cross-product equality; it supplements S05 and S06, and the argument does not depend on it.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
- original source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
- 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-fraction-01.json)