Book XII · Proposition 11

XII.11

Cones and cylinders which are of the same height are to one another as their bases.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: X.1 XII.2

Used by: XII.12 XII.13

Rests on: VI.Def.1

Depth: 2 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.11", THEOREM, sample=samples3.cone_figure)
def prop_XII_11(o: Point3, a: Point3, d: Point3) -> Out:
    """Cones and cylinders of the same height are to one another as their
    bases."""
    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(3, 2)
    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")
    apex = posit3(Point3(centre.x + axis[0], centre.y + axis[1],
                         centre.z + axis[2]), "Q")
    line3(o, d, "the first axis")
    line3(centre, apex, "the second axis, equal to it")
    for stage in STAGES:
        _ring(regular_polygon(o, radius, axis, stage))
        _ring(regular_polygon(centre, ratio * radius, axis, stage))

    because(prop_XII_2, o, *regular_polygon(o, radius, axis, 2))

    bases = (len2(o, a), ratio * ratio * len2(o, a))
    found = squeeze(lambda stage: (cone_bounds(o, radius, d, stage)
                                   / cone_bounds(centre, ratio * radius, apex, stage)),
                    bases[0] / bases[1], STAGES)
    cylinders = squeeze(lambda stage: (cylinder_bounds(o, radius, axis, stage)
                                       / cylinder_bounds(centre, ratio * radius,
                                                         axis, stage)),
                        bases[0] / bases[1], STAGES)
    claim("the enclosure of each ratio holds the ratio of the bases", "XII.2",
          found.held and cylinders.held)
    claim("and what is left over falls short of half itself at each stage",
          "X.1", found.narrowing and cylinders.narrowing)
    claim("therefore cones and cylinders of the same height are as their bases",
          "XII.11", found.held and cylinders.held)
    return Out(cones=found.enclosures, cylinders=cylinders.enclosures, bases=bases)