Book XII · Proposition 17

XII.17

Given two spheres about the same centre, to inscribe in the greater sphere a polyhedral solid which does not touch the lesser sphere at its surface.Heath, 1908

Every step, checked

• the two spheres are about one centre, and one is the greatergiven
• the lesser sphere has a positive radiusgiven
• every vertex of the polyhedron is on the greater sphereby XI.Def.14
• every vertex stands outside the lesser sphereby XI.Def.14
• and no face of it touches the lesser sphere, the least perpendicular from the centre to a face being greater than its radiusby XII.17

What it needs, and what needs it

Needs: XII.16

Used by: XII.18

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.17, Def.4, Post.5, XI.Def.14

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

What it takes on trust

• a sphere is described, and XI Def. 14; no postulate describes a sphere (×2)solid
• the proof evaluates a different number of facts on different configurations (seen: [12, 52]), so it is following more than one route through the diagramcase

The proposition as code

@proposition("XII.17", CONSTRUCTION, sample=samples3.two_radii)
def prop_XII_17(o: Point3, a: Point3, b: Point3) -> Out:
    """In the greater of two spheres about one centre, inscribe a polyhedron
    that does not touch the lesser at its surface."""
    hypothesis("the two spheres are about one centre, and one is the greater",
               sign(len2(o, a) - len2(o, b)) > 0)
    hypothesis("the lesser sphere has a positive radius", o != b)
    greater, lesser = length3(o, a), length3(o, b)
    outer = sphere_through(o, a, "the greater sphere")
    inner = sphere_through(o, b, "the lesser sphere")

    because(prop_XII_16, o, a, b)

    stage = 2
    while stage < 5:
        solid = polyhedron_in_sphere(o, greater, stage)
        if sign(inradius(solid, o) - lesser) > 0:
            break
        stage += 1
    _drawn(solid)

    claim("every vertex of the polyhedron is on the greater sphere", "XI.Def.14",
          all(on_sphere(vertex, outer) for vertex in solid.vertices))
    claim("every vertex stands outside the lesser sphere", "XI.Def.14",
          not any(inside_sphere(vertex, inner) for vertex in solid.vertices))
    claim("and no face of it touches the lesser sphere, the least perpendicular "
          "from the centre to a face being greater than its radius", "XII.17",
          sign(inradius(solid, o) - lesser) > 0)
    return Out(polyhedron=solid, stage=stage)