Book X · Proposition 112

X.112

The square on a rational straight line applied to the binomial straight line produces as breadth an apotome the terms of which are commensurable with the terms of the binomial and moreover in the same ratio; and further the apotome so arising will have the same order as the binomial straight line.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: VI.16

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4, Post.5, V.Def.5

Depth: 17 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition("X.112", THEOREM, sample=lambda rng: (Fraction(rng.randint(2, 6)),))
def prop_X_112(scale) -> Out:
    """A rational square applied to a binomial gives an apotome as breadth."""
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    binomial = 3 + sqrt(2)
    square = scale * scale
    breadth = square / binomial
    # The breadth is to the scale as the scale is to the binomial, and VI.16 is
    # the proposition about four lines standing so.
    _lines = (breadth, scale, scale, binomial)
    because(prop_VI_16, *[Point(x, level) for level, side in enumerate(_lines)
                          for x in (0, side)])

    claim("the breadth is the square divided by the binomial", "VI.16",
          breadth * binomial == square)
    claim("and it is an apotome, the terms of the binomial being reversed in sign",
          "X.112", classify(breadth).family == "apotome")
    return Out(breadth=breadth)