Book IX · Proposition 32

IX.32

Each of the numbers which are continually doubled beginning from a dyad is even-times even only.Heath, 1908

'Even-times even only' means a power of two: divisible by two down to two itself and never by an odd number.

Every step, checked

• a genuine doubling is asked forgiven
• the number is reached by continual doubling from a dyadby Def.VII.8
• it is even-times even only, no odd number measuring itby Def.VII.8

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.8

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("IX.32", THEOREM, sample=lambda rng: (2 ** rng.randint(2, 12),),
             note="'Even-times even only' means a power of two: divisible by two "
             "down to two itself and never by an odd number.")
def prop_IX_32(number: int) -> Out:
    hypothesis("a genuine doubling is asked for", number >= 4, guard=True)
    # The doubling is carried out rather than named by an exponent. Written as
    # ``number = 2 ** power``, the claim that the number is reached by doubling
    # compared it with the expression it was assigned, and a number that is no
    # power of two could not have been offered to refute it. Here the chain
    # overshoots when it is not, and the claim fails.
    chain = [2]
    while chain[-1] < number:
        chain.append(chain[-1] + chain[-1])
    claim("the number is reached by continual doubling from a dyad", "Def.VII.8",
          chain[-1] == number and in_continued_proportion(chain))
    claim("it is even-times even only, no odd number measuring it", "Def.VII.8",
          not any(measures(d, number) for d in range(3, number + 1, 2)))
    return Out(number=number)