Book X · Proposition 63
The square on the major straight line applied to a rational straight line produces as breadth the fourth binomial.Heath, 1908
Needs: X.57
Rests on: X.48-53
Depth: 3 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 _square(a, b, _sub=subtractive, _i=index, _by=source_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 line this proposition is about is the irrational one, the side
# of the area on the compound, which X.54-59 and X.91-96 named. The
# square was being taken on the compound itself, so the breadth came
# back as the square of a binomial and the conclusion had to be
# weakened to "one of the compound irrationals" to hold at all.
because(get(_by).wrapped, a, b)
irrational = sqrt(compound) # the side that proposition produces
breadth = irrational * irrational # applied to the assigned line, 1
claim("the line is the irrational the earlier proposition named", _by,
not isinstance(irrational, Fraction))
named = classify(breadth)
claim(f"the square applied to a rational line gives as breadth the "
f"{BINOMIAL_SPECIES[_i - 1]} "
f"{'apotome' if _sub else 'binomial'}", ref,
named.family == ("apotome" if _sub else "binomial")
and named.species == BINOMIAL_SPECIES[_i - 1])
claim("taking the side of that square returns the line", ref,
sqrt(breadth) == irrational)
return Out(breadth=breadth)