Book X · Proposition 70

X.70

A straight line commensurable with the side of the sum of two medial areas is the side of the sum of two medial areas.Heath, 1908

Every step, checked

• the scale is a genuine ratiogiven
• the compound is positivegiven
• the line is of the kind in questiongiven
• the second line is commensurable with the firstby X.12
• and it is a line of the very same kindby X.70

What it needs, and what needs it

Needs: X.12

Depth: 1 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(ref, THEOREM,
             sample=lambda rng, _k=kind: _terms_for(_k)
             + (Fraction(rng.randint(1, 5), rng.randint(1, 4)),))
def _same_kind(a, b, scale, _k=kind, _sub=subtractive) -> Out:
    hypothesis("the scale is a genuine ratio", sign(scale) > 0, guard=True)
    compound = (a - b) if _sub else (a + b)
    hypothesis("the compound is positive", sign(compound) > 0)
    wanted = (SUBTRACTED_NAMES if _sub else ADDED_NAMES)[_k]
    named = classify(compound)
    hypothesis("the line is of the kind in question",
               named.name == wanted or named.family == wanted)

    other = compound * scale
    because(prop_X_12, compound, compound, scale)
    claim("the second line is commensurable with the first", "X.12",
          commensurable(compound, other))
    other_named = classify(other)
    claim("and it is a line of the very same kind", ref,
          other_named.name == named.name
          or other_named.family == named.family)
    return Out(other=other)