Book XII · Proposition 13

XII.13

If a cylinder be cut by a plane which is parallel to its opposite planes, then, as the cylinder is to the cylinder, so will the axis be to the axis.Heath, 1908

Every step, checked

• the axis stands at right angles to the basegiven
• the base has a positive radius and the height is not nothinggiven
• the cutting plane is parallel to the basesby XI.14
• the enclosure holds the ratio of the axes at every stageby XII.11
• and what is left over falls short of half itself at each stageby X.1
• therefore as the cylinder is to the cylinder, so is the axis to the axisby XII.13

What it needs, and what needs it

Needs: X.1 XI.14 XII.11

Used by: XII.14

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

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

What it takes on trust

• a plane is described, and XI Def. 1-2; no postulate describes a plane (×2)solid

The proposition as code

@proposition("XII.13", THEOREM, sample=samples3.cone_figure)
def prop_XII_13(o: Point3, a: Point3, d: Point3) -> Out:
    """A cylinder cut by a plane parallel to its bases: as cylinder is to
    cylinder, so is the axis to the axis."""
    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)
    part = Fraction(2, 5)
    cut = posit3(Point3(o.x + part * axis[0], o.y + part * axis[1],
                        o.z + part * axis[2]), "P")
    sideways = vector_between(o, a)
    other = cross3(axis, sideways)
    ground = plane_through(o, a, Point3(o.x + other[0], o.y + other[1],
                                        o.z + other[2]), "the plane of the base")
    cutter = plane_through(cut,
                           Point3(cut.x + sideways[0], cut.y + sideways[1],
                                  cut.z + sideways[2]),
                           Point3(cut.x + other[0], cut.y + other[1],
                                  cut.z + other[2]), "the cutting plane")
    line3(o, d, "the axis")
    line3(o, a, "the radius of the base")
    for stage in STAGES:
        _drawn(prism(regular_polygon(o, radius, axis, stage), axis))

    nearer = tuple(part * component for component in axis)
    beyond = tuple((1 - part) * component for component in axis)
    found = squeeze(lambda stage: (cylinder_bounds(o, radius, nearer, stage)
                                   / cylinder_bounds(cut, radius, beyond, stage)),
                    part / (1 - part), STAGES)
    claim("the cutting plane is parallel to the bases", "XI.14",
          parallel_planes(cutter, ground) and cutter != ground)
    claim("the enclosure holds the ratio of the axes at every stage", "XII.11",
          found.held)
    claim("and what is left over falls short of half itself at each stage",
          "X.1", found.narrowing)
    claim("therefore as the cylinder is to the cylinder, so is the axis to the "
          "axis", "XII.13", found.held and found.narrowing)
    return Out(enclosures=found.enclosures, cut=cut)