Book XIII · Proposition 18

XIII.18

To set out the sides of the five figures and to compare them with one another.Heath, 1908

Every step, checked

• the sphere has a positive radiusgiven
• the diameter of the sphere is rationalgiven
• the side of the pyramid is greater than the side of the octahedron, and that than the side of the cubeby XIII.15
• the side of the cube is greater than the side of the icosahedron, and that than the side of the dodecahedronby XIII.17
• the first three have to the diameter a ratio a number can name, and the last two have notby X.73
• and there is no sixth figureby XI.21

What it needs, and what needs it

Needs: X.73 XI.21 XIII.13 XIII.14 XIII.15 XIII.16 XIII.17

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

Depth: 5 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("XIII.18", THEOREM, sample=samples3.sphere_about)
def prop_XIII_18(o: Point3, a: Point3) -> Out:
    """Set out the sides of the five figures and compare them with one another."""
    hypothesis("the sphere has a positive radius", o != a)
    hypothesis("the diameter of the sphere is rational",
               is_rational_line(sqrt(4 * space_len2(o, a))))
    line3(o, a, "the radius of the sphere all five are comprehended in")

    sides = (because(prop_XIII_13, o, a).side2,
             because(prop_XIII_14, o, a).side2,
             because(prop_XIII_15, o, a).side2,
             because(prop_XIII_16, o, a).side2,
             because(prop_XIII_17, o, a).side2)
    across = 4 * space_len2(o, a)

    claim("the side of the pyramid is greater than the side of the octahedron, "
          "and that than the side of the cube", "XIII.15",
          sign(sides[0] - sides[1]) > 0 and sign(sides[1] - sides[2]) > 0)
    claim("the side of the cube is greater than the side of the icosahedron, "
          "and that than the side of the dodecahedron", "XIII.17",
          sign(sides[2] - sides[3]) > 0 and sign(sides[3] - sides[4]) > 0)
    claim("the first three have to the diameter a ratio a number can name, and "
          "the last two have not", "X.73",
          all(isinstance(span / across, Fraction) for span in sides[:3])
          and not any(isinstance(span / across, Fraction) for span in sides[3:]))
    claim("and there is no sixth figure", "XI.21",
          len(_regular_solids()) == 5
          and set(_regular_solids()) == {(3, 3), (3, 4), (3, 5), (4, 3), (5, 3)})
    return Out(sides=sides, diameter2=across, figures=_regular_solids())