Book X · Proposition 108

X.108

If from a rational area a medial area be subtracted, the "side" of the remaining area becomes one of two irrational straight lines, either an apotome or a minor straight line.Heath, 1908

Every step, checked

• the scale is genuinegiven
• the medial area is the lessgiven
• the remaining area is irrationalby X.108
• and its side is an apotome or a minor lineby X.108

What it needs, and what needs it

Needs: nothing earlier.

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("X.108", THEOREM, sample=lambda rng: (Fraction(rng.randint(3, 8)),))
def prop_X_108(scale) -> Out:
    """A medial area subtracted from a rational one."""
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    rational_area = scale * scale
    medial_area = sqrt(2)
    hypothesis("the medial area is the less", sign(rational_area - medial_area) > 0)
    side = sqrt(rational_area - medial_area)
    claim("the remaining area is irrational", "X.108",
          not isinstance(rational_area - medial_area, Fraction))
    claim("and its side is an apotome or a minor line", "X.108",
          classify(side).family in ("apotome", "medial-based")
          or classify(side).name in SPECIES)
    return Out(side=side)