Delayed injective bookkeeping

Every pair (α, ξ) receives a distinct later recursion index. The construction follows the manuscript: well-order all requirements in initial order type and recursively choose a fresh point in the full-size tail above α.

theorem ScottishBook155.exists_bookkeepingSchedule : ∃ (s : RecursionIndexZero × RecursionIndexZero → RecursionIndexZero), Function.Injective s ∧ ∀ (p : RecursionIndexZero × RecursionIndexZero), p.1 < s p

An injective schedule placing every requirement strictly after the stage whose point it names.

noncomputable def ScottishBook155.bookkeepingSchedule : RecursionIndexZero × RecursionIndexZero → RecursionIndexZero

A fixed schedule chosen from exists_bookkeepingSchedule.

Equations

• ScottishBook155.bookkeepingSchedule = Classical.choose ScottishBook155.exists_bookkeepingSchedule

theorem ScottishBook155.bookkeepingSchedule_injective : Function.Injective bookkeepingSchedule

theorem ScottishBook155.bookkeepingSchedule_gt (p : RecursionIndexZero × RecursionIndexZero) : p.1 < bookkeepingSchedule p

noncomputable def ScottishBook155.bookkeepingReceivingStage (p : RecursionIndexZero × RecursionIndexZero) : RecursionIndexZero

The stage which receives the point named by a bookkeeping requirement. The schedule names the transition; the point is present at its successor.

Equations

• ScottishBook155.bookkeepingReceivingStage p = Order.succ (ScottishBook155.bookkeepingSchedule p)

theorem ScottishBook155.bookkeepingSchedule_lt_receivingStage (p : RecursionIndexZero × RecursionIndexZero) : bookkeepingSchedule p < bookkeepingReceivingStage p

theorem ScottishBook155.bookkeepingReceivingStage_gt (p : RecursionIndexZero × RecursionIndexZero) : p.1 < bookkeepingReceivingStage p