Book X · Proposition 115
From a medial straight line there arise irrational straight lines infinite in number, and none of them is the same as any of the preceding.Heath, 1908
Book X ends by showing its own list is not the end: from one medial line an unending series of new irrationals arises.
Needs: nothing earlier.
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition("X.115", THEOREM, sample=lambda rng: (rng.choice([2, 3, 5, 7]),),
note="Book X ends by showing its own list is not the end: from one "
"medial line an unending series of new irrationals arises.")
def prop_X_115(radicand: int) -> Out:
hypothesis("the radicand is not a square", not _is_square_int(radicand))
medial = sqrt(sqrt(radicand))
hypothesis("the line is medial", is_medial(medial))
# Each mean proportional between the assigned line and the one before is a
# new irrational, and its degree over the rationals doubles every time.
chain = [medial]
for _ in range(3):
chain.append(sqrt(chain[-1]))
claim("every line of the chain is irrational", "X.115",
all(not isinstance(term, Fraction) for term in chain))
claim("each is incommensurable with the one before", "X.115",
all(not commensurable(chain[i], chain[i + 1]) for i in range(len(chain) - 1)))
claim("and their degrees over the rationals go on doubling, so the series "
"never closes", "X.115",
[degree(term) for term in chain] == [4, 8, 16, 32])
return Out(chain=chain)