Book XII · Proposition 14

XII.14

Cones and cylinders which are on equal bases are to one another as their heights.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: X.1 XII.2 XII.13

Used by: XII.15

Rests on: VI.Def.1, XI.Def.3, XI.Def.8

Depth: 4 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("XII.14", THEOREM, sample=samples3.cone_figure)
def prop_XII_14(o: Point3, a: Point3, d: Point3) -> Out:
    """Cones and cylinders on equal bases are to one another as their heights."""
    hypothesis("the axis stands at right angles to the base",
               dot3(vector_between(o, a), vector_between(o, d)) == 0)
    hypothesis("the base has a positive radius and the height is not nothing",
               o != a and o != d)
    radius, axis = _cone_figure(o, a, d)
    ratio = Fraction(7, 4)
    centre = posit3(Point3(o.x + 9 * (a.x - o.x), o.y + 9 * (a.y - o.y),
                           o.z + 9 * (a.z - o.z)), "P")
    taller = tuple(ratio * component for component in axis)
    apex = posit3(Point3(centre.x + taller[0], centre.y + taller[1],
                         centre.z + taller[2]), "Q")
    line3(o, d, "the first axis")
    line3(centre, apex, "the second axis")
    for stage in STAGES:
        _ring(regular_polygon(o, radius, axis, stage))
        _ring(regular_polygon(centre, radius, axis, stage))

    because(prop_XII_13, o, a, d)

    found = squeeze(lambda stage: (cylinder_bounds(o, radius, axis, stage)
                                   / cylinder_bounds(centre, radius, taller, stage)),
                    1 / ratio, STAGES)
    cones = squeeze(lambda stage: (cone_bounds(o, radius, d, stage)
                                   / cone_bounds(centre, radius, apex, stage)),
                    1 / ratio, STAGES)
    claim("the two bases are equal, the figures inscribed in them at every "
          "stage being equal", "XII.2",
          all(polygon_area(regular_polygon(o, radius, axis, stage))
              == polygon_area(regular_polygon(centre, radius, axis, stage))
              for stage in STAGES))
    claim("the enclosure holds the ratio of the heights at every stage",
          "XII.13", found.held and cones.held)
    claim("and what is left over falls short of half itself at each stage",
          "X.1", found.narrowing and cones.narrowing)
    claim("therefore cones and cylinders on equal bases are as their heights",
          "XII.14", found.held and cones.held)
    return Out(cylinders=found.enclosures, cones=cones.enclosures)