Book IX · Proposition 18

IX.18

Given two numbers, to investigate whether it is possible to find a third proportional to them.Heath, 1908

Euclid asks when a problem is *possible*, and answers with a test -- a decision procedure, not a construction.

Every step, checked

• both are numbersgiven
• a third proportional exists exactly when the first measures the square of the secondby VII.19
• and when it does, it is that quotientby VII.19

What it needs, and what needs it

Needs: VII.19

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(
    "IX.18",
    CONSTRUCTION,
    sample=_third_proportional_case,
    note="Euclid asks when a problem is *possible*, and answers with a test -- "
    "a decision procedure, not a construction.",
)
def prop_IX_18(a: int, b: int) -> Out:
    hypothesis("both are numbers", a > 1 and b > 1, guard=True)
    possible = measures(a, b * b)
    if possible and b * b // a > 1:
        # A is to B as B is to the third, so VII.19 speaks of these four.
        because(prop_VII_19, a, b, b, b * b // a)

    claim("a third proportional exists exactly when the first measures the square "
          "of the second", "VII.19", possible == (b * b % a == 0))
    claim("and when it does, it is that quotient", "VII.19",
          not possible or a * (b * b // a) == b * b)
    return Out(possible=possible, third=(b * b // a) if possible else None)