Book X · Proposition 114

X.114

If an area be contained by an apotome and the binomial straight line the terms of which are commensurable with the terms of the apotome and in the same ratio, the "side" of the area is rational.Heath, 1908

Every step, checked

• the scale is genuinegiven
• the apotome is positivegiven
• the area contained is rationalby X.114
• so the side of the equal square is rational in squareby X.114

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.114", THEOREM, sample=lambda rng: (Fraction(rng.randint(2, 6)),))
def prop_X_114(scale) -> Out:
    """An area contained by an apotome and a binomial with the same terms."""
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    binomial = scale + sqrt(2)
    apotome = scale - sqrt(2)
    hypothesis("the apotome is positive", sign(apotome) > 0)
    area = binomial * apotome
    claim("the area contained is rational", "X.114", is_rational_area(area))
    claim("so the side of the equal square is rational in square", "X.114",
          is_rational_in_square(sqrt(area)))
    return Out(area=area, side=sqrt(area))