Book X · Proposition 4

X.4

Given three commensurable magnitudes, to find their greatest common measure.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• all three are commensurablegiven
• the measure found measures all threeby X.3
• and every common measure of the three measures itby X.3

What it needs, and what needs it

Needs: X.3

Rests on: Def.X.1

Depth: 2 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(
    "X.4",
    CONSTRUCTION,
    sample=lambda rng: _commensurable_pair(rng)
    + (_commensurable_pair(rng)[0] * Fraction(rng.randint(1, 4), rng.randint(1, 3)),),
)
def prop_X_4(a, b, c) -> Out:
    hypothesis("the magnitudes are positive", all(sign(x) > 0 for x in (a, b, c)), guard=True)
    hypothesis("all three are commensurable",
               commensurable(a, b) and commensurable(b, c))
    first = common_measure(a, b)
    measure = common_measure(first, c)

    because(prop_X_3, a, b) if commensurable(a, b) else None

    claim("the measure found measures all three", "X.3",
          all(isinstance(x / measure, Fraction)
              and (x / measure).denominator == 1 for x in (a, b, c)))
    claim("and every common measure of the three measures it", "X.3",
          commensurable(measure, a) and commensurable(measure, b)
          and commensurable(measure, c))
    return Out(measure=measure)