Book XI · Proposition 1
A part of a straight line cannot be in the plane of reference and a part in a plane more elevated.Heath, 1908
Heath calls the proof invalid: Euclid argues from a picture, and what he needs is a definition of 'plane' he never gives.
Needs: nothing earlier.
Rests on: XI.Def.7
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
@proposition(
"XI.1",
THEOREM,
sample=samples3.cutting_lines,
note="Heath calls the proof invalid: Euclid argues from a picture, and what "
"he needs is a definition of 'plane' he never gives.",
)
def prop_XI_1(o: Point3, a: Point3, b: Point3) -> Out:
"""No part of a straight line is in one plane and the rest above it."""
hypothesis("the three points are not in a straight line", not collinear3(o, a, b))
surface = plane_through(o, a, b, "the plane of reference")
# The proposition denies a configuration, so there is no figure of it to
# draw: what is checked is that the denial holds. Every point of the line
# OA lies in the plane, and that is what "no part of it is more elevated"
# says. Euclid argues instead that the part outside would make two straight
# lines with common ends, which is where Heath's objection falls.
stretch = line3(o, a, "the straight line OA")
along = [stretch.at(Fraction(k, 4)) for k in range(-8, 9)]
claim("every point of the line lies in the plane of reference, so no part "
"of it is elevated above", "XI.Def.7",
all(on_plane(point, surface) for point in along))
claim("and the line is not merely touching it at the two named points",
"XI.Def.7", on_plane(stretch.at(Fraction(1, 3)), surface))
return Out(plane=surface, line=stretch)