Proof 3 of 6 · Ranked succession

Succession without elections

A precommitted rank order and bounded leases determine who may write after failure. Delayed observation only postpones a lower-ranked candidate; it never makes that candidate earlier.

What you are looking at

Three ranked machines, a logical beat counter, a current lease boundary, and a SHA-256-linked control log.

Do this

  1. Leave rank 3 lag enabled and run the guided scenario.
  2. Inspect the claim and resumption beats.
  3. Inject an unsafe rank-3 claim.

Watch for

Rank 2 claims only after expiry plus its grace. Rank 3's lag moves its eligibility later. Rank 1 returns only at the interim lease boundary.

What this demonstrates

Precommitted rank arithmetic can produce deterministic failover without an election. It does not prove liveness under partitions or authenticate the roster.

Logical beat0
Active leaderrank 1
Lease boundarybeat 4
Control chain: waiting Initializing the roster.
Lease safety: waiting Run a succession path.
Rank and resumption: waiting Run the guided scenario.

Append-only control history

Initializing…

Independent reproduction

Ask any LLM to build a separate proof

The specification requires an independent semantic verifier, not only a visualization of the same transition code.