Book X · Proposition 109

X.109

If from a medial area a rational area be subtracted, there arise two other irrational straight lines, either a first apotome of a medial straight line or a straight line which produces with a rational area a medial whole.Heath, 1908

Every step, checked

• the scale is genuinegiven
• the rational area is the lessgiven
• the remaining area is irrationalby X.109
• and its side is one of the named linesby X.109

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