Book X · Proposition 1

X.1

Two unequal magnitudes being set out, if from the greater there be subtracted a magnitude greater than its half, and from that which is left a magnitude greater than its half, and if this process be repeated continually, there will be left some magnitude which will be less than the lesser magnitude set out.Heath, 1908

The bisection principle, and the engine of Book XII's method of exhaustion. Euclid needs it before he can say anything about limits.

Every step, checked

• the magnitudes are positivegiven
• the second is the lessgiven
• the process terminatesby X.1
• and leaves a magnitude less than the lesser set outby X.1

What it needs, and what needs it

Needs: nothing earlier.

Used by: XII.2 XII.10 XII.11 XII.12 XII.13 XII.14 XII.15 XII.18

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.1",
    THEOREM,
    sample=lambda rng: (_magnitude(rng), Fraction(rng.randint(1, 3), rng.randint(4, 9))),
    note="The bisection principle, and the engine of Book XII's method of "
    "exhaustion. Euclid needs it before he can say anything about limits.",
)
def prop_X_1(greater, part) -> Out:
    """Take away more than half, repeatedly, and any magnitude is undercut."""
    hypothesis("the magnitudes are positive", sign(greater) > 0 and sign(part) > 0, guard=True)
    lesser = greater * part
    hypothesis("the second is the less", sign(greater - lesser) > 0)

    remaining, steps = greater, 0
    while sign(remaining - lesser) >= 0 and steps < 200:
        remaining = remaining - remaining * Fraction(3, 5)  # more than half taken
        steps += 1

    claim("the process terminates", "X.1", steps < 200)
    claim("and leaves a magnitude less than the lesser set out", "X.1",
          sign(lesser - remaining) > 0)
    return Out(steps=steps, remainder=remaining)