Book X · Proposition 59

X.59

If an area be contained by a rational straight line and the sixth binomial, the "side" of the area is the irrational straight line called the side of the sum of two medial areas.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: X.53

Used by: X.65

Rests on: X.48-53

Depth: 2 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(ref, THEOREM,
             sample=lambda rng, _i=index: _binomial_of_species(_i))
def _side(a, b, _sub=subtractive, _kind=kind, _by=species_ref) -> Out:
    hypothesis("both terms are rational in square",
               is_rational_in_square(a) and is_rational_in_square(b))
    hypothesis("they are commensurable in square only", not commensurable(a, b))
    compound = (a - b) if _sub else (a + b)
    hypothesis("the compound is positive", sign(compound) > 0)
    # The area is applied to the assigned rational line, which is 1, so
    # the area and the compound are one magnitude. This step used to
    # compare them and cite X.20 for it, which asserted nothing: what
    # the proposition stands on is which species the compound is, and
    # that is what X.48-53 and X.85-90 determine.
    because(get(_by).wrapped, a, b)
    named_compound = classify(compound)
    claim(f"the area is contained by a rational line and the "
          f"{BINOMIAL_SPECIES[index - 1]} "
          f"{'apotome' if _sub else 'binomial'}", _by,
          named_compound.family == ("apotome" if _sub else "binomial")
          and named_compound.species == BINOMIAL_SPECIES[index - 1])

    side = sqrt(compound)
    claim("the side of the equal square is irrational", ref,
          not isinstance(side, Fraction))
    named = classify(side)
    claim(f"and it is the line called {_kind}", ref,
          named.family == _kind if index == 1 else named.name == _kind)
    return Out(side=side)