9.1. Side-by-Side Views🔗

These grafts reuse the Collatz entries below so the first graph render shows an in-progress proof state next to a completed definition card.

DefinitionStep

Group: A small exploratory demo chapter about the Collatz iteration. It is not part of Hehner's book; it exists so the Blueprint graph has an intentionally unfinished node from day one. (1)

Group member previews

Preview

Theorem 9.2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 1

Reverse dependency previews

Preview

Theorem 9.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Collatz step sends an even natural number n to n / 2 and an odd one to 3 * n + 1.

Lean code for DefinitionStep

def collatzStep (n : Nat) : Nat :=
  if n % 2 == 0 then n / 2 else 3 * n + 1

def collatzTerminatesAtOne (n : Nat) : Prop :=
  ∃ steps : Nat, Nat.repeat collatzStep steps n = 1

EffortmediumTagsplayfulfamousincomplete

For every positive natural number n, repeated application of the Collatz step eventually reaches 1. This is the usual termination statement of the Collatz conjecture, phrased in terms of Definition 9.2.1.

EffortmediumTagsplayfulfamousincomplete

No proof is currently known. This theorem is intentionally left unfinished so the generated graph and summary show an in-progress goal immediately.