Book X · Proposition 23

X.23

A straight line commensurable with a medial straight line is medial.Heath, 1908

Every step, checked

• the first is medialgiven
• the scale is a genuine ratiogiven
• the second is commensurable with the firstby X.23
• and is itself medialby X.23

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.24

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.23",
    THEOREM,
    sample=lambda rng: (_medial_line(rng), Fraction(rng.randint(1, 5), rng.randint(1, 4))),
)
def prop_X_23(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
    claim("the second is commensurable with the first", "X.23", commensurable(medial, other))
    claim("and is itself medial", "X.23", is_medial(other))
    return Out(other=other)