Book X · Proposition 16

X.16

If two incommensurable magnitudes be added together, the whole will also be incommensurable with each of them; and, if the whole be incommensurable with one of them, the original magnitudes will also be incommensurable.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• they are incommensurablegiven
• the whole is incommensurable with each of themby X.16
• and converselyby X.16

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.16",
    THEOREM,
    sample=_incommensurable_pair,
)
def prop_X_16(a, b) -> Out:
    hypothesis("the magnitudes are positive", sign(a) > 0 and sign(b) > 0, guard=True)
    hypothesis("they are incommensurable", not commensurable(a, b))
    claim("the whole is incommensurable with each of them", "X.16",
          not commensurable(a + b, a) and not commensurable(a + b, b))
    claim("and conversely", "X.16",
          (not commensurable(a + b, a)) == (not commensurable(a, b)))
    return Out(whole=a + b)