Book X · Proposition 26

X.26

4 medial area does not exceed a medial area by a rational area.Heath, 1908

A negative result, and one Euclid needs: it keeps the medial areas from collapsing into the rational ones.

Every step, checked

What it needs, and what needs it

Needs: nothing earlier.

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(
    "X.26",
    THEOREM,
    sample=lambda rng: (_medial_line(rng), _medial_line(rng)),
    note="A negative result, and one Euclid needs: it keeps the medial areas "
    "from collapsing into the rational ones.",
)
def prop_X_26(a, b) -> Out:
    hypothesis("both are medial", is_medial(a) and is_medial(b))
    first, second = a * a, b * b
    hypothesis("the areas are unequal and both medial",
               is_medial_area(first) and is_medial_area(second) and first != second)
    difference = first - second if sign(first - second) > 0 else second - first
    claim("a medial area does not exceed a medial area by a rational area", "X.26",
          not is_rational_area(difference))
    return Out(difference=difference)