Book XIII · Proposition 11

XIII.11

If in a circle which has its diameter rational an equilateral pentagon be inscribed, the side of the pentagon is the irrational straight line called minor.Heath, 1908

Book X names the pentagon's side, as it named the segments of XIII.6. The name holds for either sense in which the diameter can be rational.

Every step, checked

• the circle has positive radiusgiven
• the diameter of the circle is rationalgiven
• the side of the pentagon is the irrational line called minorby X.76
• it is of the fourth degree over the rationals, so no rational line and no medial oneby X.21, X.73

What it needs, and what needs it

Needs: IV.11 X.21 X.73 X.76

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.19, Def.22, Def.3, Def.4, Post.1, Post.3, Post.5, X.85-90, X.Def.4

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×11)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×14)continuity

The proposition as code

@proposition(
    "XIII.11",
    THEOREM,
    sample=_rational_line,
    note="Book X names the pentagon's side, as it named the segments of XIII.6. "
    "The name holds for either sense in which the diameter can be rational.",
)
def prop_XIII_11(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    hypothesis("the diameter of the circle is rational",
               is_rational_in_square(2 * length(o, a)))
    corners = prop_IV_11(o, a).pentagon
    side = length(corners[0], corners[1])
    named = classify(side)

    because(prop_X_21, Fraction(1), sqrt(5))
    # The minor is a difference of two lines incommensurable in square whose
    # squares add to a rational and whose rectangle is medial. For this side
    # those are sqrt(R^2(5 + 2 sqrt 5))/2 and sqrt(R^2(5 - 2 sqrt 5))/2, and
    # X.76 is the proposition that names their difference.
    _r2 = len2(o, a)
    because(get("X.76").wrapped,
            sqrt(_r2 * (5 + 2 * sqrt(5))) / 2,
            sqrt(_r2 * (5 - 2 * sqrt(5))) / 2)
    # X.73 makes an apotome out of two *rational* lines commensurable in square
    # only; the terms of the minor are not rational, so the appeal has no pair
    # of lines here to be about.

    claim("the side of the pentagon is the irrational line called minor",
          "X.76", named.name == "minor")
    claim("it is of the fourth degree over the rationals, so no rational line "
          "and no medial one", ["X.21", "X.73"], named.algebraic_degree == 4)
    return Out(side=side, name=named.name)