Book XI · Proposition 23

XI.23

To construct a solid angle out of three plane angles two of which, taken together in any manner, are greater than the remaining one: thus the three angles must be less than four right angles.Heath, 1908

Every step, checked

• the arms are not in one planegiven
• any two of the given angles exceed the thirdgiven
• the three together fall short of four right anglesgiven
• the solid angle constructed is contained by the three given anglesby XI.23
• and it is a genuine solid angle, its arms not in one planeby XI.Def.11

What it needs, and what needs it

Needs: nothing earlier.

Used by: XI.26

Rests on: XI.Def.11

Depth: 0 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("XI.23", CONSTRUCTION, sample=samples3.tetrahedron)
def prop_XI_23(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """Construct a solid angle out of three plane angles, any two exceeding the
    third."""
    hypothesis("the arms are not in one plane", not coplanar(o, a, b, c))
    angles = (angle_at3(a, o, b), angle_at3(b, o, c), angle_at3(a, o, c))
    hypothesis("any two of the given angles exceed the third",
               all(_sum_exceeds(x, y, z) for x, y, z in
                   ((angles[0], angles[1], angles[2]),
                    (angles[1], angles[2], angles[0]),
                    (angles[0], angles[2], angles[1]))))
    hypothesis("the three together fall short of four right angles",
               _under_four_right_angles(*angles))

    # The solid angle asked for is the one these three angles already contain:
    # the construction is to set it up at a named point, which is the figure
    # carried over -- and carrying a figure over is exact.
    corner = posit3(Point3(0, 0, 0), "D")
    arms = []
    for point, name in ((a, "E"), (b, "F"), (c, "G")):
        step = vector_between(o, point)
        arms.append(posit3(Point3(corner.x + step[0], corner.y + step[1],
                                  corner.z + step[2]), name))
    for arm in arms:
        line3(corner, arm)

    made = (angle_at3(arms[0], corner, arms[1]),
            angle_at3(arms[1], corner, arms[2]),
            angle_at3(arms[0], corner, arms[2]))
    claim("the solid angle constructed is contained by the three given angles",
          "XI.23", made == angles)
    claim("and it is a genuine solid angle, its arms not in one plane", "XI.Def.11",
          not coplanar(corner, *arms))
    return Out(corner=corner, arms=tuple(arms), angles=made)