Book IX · Proposition 2

IX.2

If two numbers by multiplying one another make a square number, they are similar plane numbers.Heath, 1908

Every step, checked

• the numbers are genuinegiven
• their product is squaregiven
• the two given numbers are similar plane numbersby Def.VII.21
• and no pair whose product is square fails to beby IX.2

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(
    "IX.2",
    THEOREM,
    # Random pairs almost never have a square product, so a valid instance is
    # built. The sweep inside the proposition is what tests the theorem.
    sample=lambda rng: (rng.randint(1, 5) * rng.randint(2, 5) ** 2,
                        rng.randint(1, 5) * rng.randint(2, 5) ** 2),
)
def prop_IX_2(a: int, b: int) -> Out:
    """The converse of IX.1, tested by looking for a counterexample."""
    hypothesis("the numbers are genuine", a > 1 and b > 1, guard=True)
    hypothesis("their product is square", is_square(a * b))

    def similar_planes(first: int, second: int) -> bool:
        """Both are the same multiple of a square: d*x^2 and d*y^2."""
        measure = gcd(first, second)
        return is_square(first // measure) and is_square(second // measure)

    claim("the two given numbers are similar plane numbers", "Def.VII.21",
          similar_planes(a, b))
    claim("and no pair whose product is square fails to be", "IX.2",
          all(similar_planes(x, y)
              for x in range(2, 40) for y in range(2, 40) if is_square(x * y)))
    return Out(sides=(gcd(a, b), a // gcd(a, b), b // gcd(a, b)))