Book VIII · Proposition 20

VIII.20

If one mean proportional number fall between two numbers, the numbers will be similar plane numbers.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.21

Depth: 0 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(
    "VIII.20",
    THEOREM,
    sample=lambda rng: _with_a_mean_proportional(rng),
)
def prop_VIII_20(first: int, second: int, mean: int) -> Out:
    """The converse of VIII.18: a mean proportional makes the numbers similar planes.

    The two numbers and their mean are given.  Building them from a pair of
    sides made the conclusion -- that sides can be found -- true of the sides
    already in hand, so the search below never had to succeed.
    """
    hypothesis("the numbers are genuine", first > 1 and second > 1, guard=True)
    hypothesis("a mean proportional falls between them", first * second == mean * mean)
    # Def. VII.21 asks for sides in proportion, so they have to be produced.
    # A side is a number, so neither may be a unit.
    sides = None
    for width in range(2, first):
        if first % width:
            continue
        length = first // width
        for other in range(2, second):
            if second % other:
                continue
            partner = second // other
            if length > 1 and partner > 1 and width * partner == length * other:
                sides = ((width, length), (other, partner))
                break
        if sides:
            break
    claim("the two are similar plane numbers, with proportional sides", "Def.VII.21",
          sides is not None
          and sides[0][0] * sides[0][1] == first
          and sides[1][0] * sides[1][1] == second
          and sides[0][0] * sides[1][1] == sides[0][1] * sides[1][0])
    return Out(sides=sides)