Book X · Proposition 24

X.24

The rectangle contained by medial straight lines commensurable in length is medial.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: X.23

Depth: 1 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.24",
    THEOREM,
    sample=lambda rng: (_medial_line(rng), Fraction(rng.randint(1, 5), rng.randint(1, 4))),
)
def prop_X_24(medial, scale) -> Out:
    hypothesis("the first is medial", is_medial(medial))
    hypothesis("the scale is a genuine ratio", sign(scale) > 0, guard=True)
    other = medial * scale
    hypothesis("the two are commensurable in length", commensurable(medial, other))
    because(prop_X_23, medial, scale) if is_medial(medial) else None

    claim("both are medial", "X.23", is_medial(medial) and is_medial(other))
    claim("and the rectangle they contain is medial", "X.24",
          is_medial_area(medial * other))
    return Out(rectangle=medial * other)