Book XIII · Proposition 16

XIII.16

To construct an icosahedron and comprehend it in a sphere, like the aforesaid figures; and to prove that the side of the icosahedron is the irrational straight line called minor.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• the diameter of the sphere is rational, being the line every other is named againstgiven
• every vertex of the icosahedron is on the sphereby XI.Def.14
• it is contained by twenty equal and equilateral triangles, five edges meeting at each cornerby XI.Def.27
• and the side of the icosahedron is the irrational straight line called minorby X.76
• it is of the fourth degree over the rationals, so neither a rational line nor a medial oneby X.73

What it needs, and what needs it

Needs: X.73 X.76 XIII.15

Used by: XIII.17 XIII.18

Rests on: X.85-90, XI.Def.14, XI.Def.25, XI.Def.26, XI.Def.27

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

What it takes on trust

• a sphere is described, and XI Def. 14; no postulate describes a spheresolid

The proposition as code

@proposition("XIII.16", CONSTRUCTION, sample=samples3.sphere_about)
def prop_XIII_16(o: Point3, a: Point3) -> Out:
    """Construct an icosahedron in a sphere, and prove its side is the
    irrational straight line called minor."""
    hypothesis("the sphere has a positive radius", o != a)
    hypothesis("the diameter of the sphere is rational, being the line every "
               "other is named against",
               is_rational_line(sqrt(4 * space_len2(o, a))))
    globe = sphere_through(o, a, "the given sphere")
    line3(o, a, "the radius")
    corners, edges = _figure(o, a, _icosahedron(), "an edge of the icosahedron")

    because(prop_XIII_15, o, a)

    side2, across = _edge2(corners, edges), 4 * space_len2(o, a)
    side = sqrt(side2 / across)
    named = classify(side)
    # X.76 makes the minor out of two lines incommensurable in square whose
    # squares add to a rational area and whose rectangle is medial. The two are
    # the terms the side itself divides into, so the appeal is carried out on
    # the figure's own magnitudes and not on a pair chosen to suit it.
    because(get("X.76").wrapped, named.terms[0], -named.terms[1])

    claim("every vertex of the icosahedron is on the sphere", "XI.Def.14",
          all(on_sphere(corner, globe) for corner in corners))
    claim("it is contained by twenty equal and equilateral triangles, five "
          "edges meeting at each corner", "XI.Def.27",
          len(corners) == 12 and len(edges) == 30
          and _at_each_corner(corners, edges) == {5}
          and all(space_len2(corners[i], corners[j]) == side2 for i, j in edges))
    claim("and the side of the icosahedron is the irrational straight line "
          "called minor", "X.76", named.name == "minor")
    claim("it is of the fourth degree over the rationals, so neither a rational "
          "line nor a medial one", "X.73", named.algebraic_degree == 4)
    return Out(icosahedron=corners, side2=side2, side=side, name=named.name)