Book XI · Proposition 38

XI.38

If the sides of the opposite planes of a cube be bisected, and planes be carried through the points of section, the common section of the planes and the diameter of the cube bisect one another.Heath, 1908

Every step, checked

• the three arms are not in one planegiven
• the solid is a cube, its edges equal and at right anglesgiven
• the common section of the two planes is a straight lineby XI.3
• it meets the diameterby XI.Def.7
• and the two bisect one anotherby XI.38

What it needs, and what needs it

Needs: XI.3

Rests on: XI.Def.7

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

What it takes on trust

• a line-plane intersection is used, though no postulate asserts that a line meets a plane (×2)continuity
• a plane-plane intersection is used, though no postulate asserts that two planes meetcontinuity
• a plane is described, and XI Def. 1-2; no postulate describes a plane (×2)solid

The proposition as code

@proposition("XI.38", THEOREM, sample=samples3.cube_corner)
def prop_XI_38(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """In a cube, the common section of the planes through the bisected sides of
    opposite faces, and the diameter, bisect one another."""
    hypothesis("the three arms are not in one plane", not coplanar(o, a, b, c))
    hypothesis("the solid is a cube, its edges equal and at right angles",
               len2(o, a) == len2(o, b) and len2(o, b) == len2(o, c)
               and dot3(vector_between(o, a), vector_between(o, b)) == 0
               and dot3(vector_between(o, b), vector_between(o, c)) == 0
               and dot3(vector_between(o, a), vector_between(o, c)) == 0)
    cube = _built(parallelepiped(o, a, b, c, "the cube"))
    corners = cube.vertices

    # Each plane is carried through the points bisecting the sides of one pair
    # of opposite faces. Two such planes are taken, as Euclid takes them.
    first = plane_through(midpoint_of(corners[0], corners[1]),
                          midpoint_of(corners[3], corners[2]),
                          midpoint_of(corners[4], corners[5]),
                          "the first plane through the points of section")
    second = plane_through(midpoint_of(corners[0], corners[3]),
                           midpoint_of(corners[1], corners[2]),
                           midpoint_of(corners[4], corners[7]),
                           "the second such plane")
    section = meet_planes(first, second)
    diameter = line3(corners[0], corners[6], "the diameter of the cube")

    # Where the common section leaves the cube, and where the diameter does:
    # the two segments whose bisection is the thing asserted.
    ends = (meet_line_plane(section, cube.face_plane(0)),
            meet_line_plane(section, cube.face_plane(1)))
    middle = posit3(midpoint_of(*ends), "S")

    claim("the common section of the two planes is a straight line", "XI.3",
          isinstance(section, Line3))
    claim("it meets the diameter", "XI.Def.7", on_line3(middle, diameter))
    claim("and the two bisect one another", "XI.38",
          middle == midpoint_of(corners[0], corners[6])
          and len2(ends[0], middle) == len2(middle, ends[1]))
    return Out(section=section, diameter=diameter, middle=middle)