Book X · Proposition 113

X.113

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

Every step, checked

• the scale is genuinegiven
• the breadth is the square divided by the apotomeby VI.16
• and it is a binomialby X.113

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.113", THEOREM, sample=lambda rng: (Fraction(rng.randint(2, 6)),))
def prop_X_113(scale) -> Out:
    """The dual of X.112: a rational square applied to an apotome."""
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    apotome = 3 - sqrt(2)
    square = scale * scale
    breadth = square / apotome
    # The breadth is to the scale as the scale is to the apotome, and VI.16 is
    # the proposition about four lines standing so.
    _lines = (breadth, scale, scale, apotome)
    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 apotome", "VI.16",
          breadth * apotome == square)
    claim("and it is a binomial", "X.113", classify(breadth).family == "binomial")
    return Out(breadth=breadth)