Book X · Proposition 55
If an area be contained by a rational straight line and the second binomial, the "side" of the area is the irrational straight line which is called a first bimedial.Heath, 1908
Needs: X.49
Used by: X.61
Rests on: X.48-53
Depth: 2 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@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)