A computable nonnegative extended real: a computable sequence of dyadic numerators a n, whose value a n / 2 ^ n is within 2 ^ (-n) of x. The two bounds are stated additively, so no truncated subtraction occurs.

The standard notion — a computable sequence of rationals converging to x with error 2 ^ (-n) — yields such a numerator sequence by rounding, but that rounding step is not formalized here, for want of computable arithmetic on ℚ. The additive form is preferred over the dyadic floor form IsFloorComputableENNReal because no uniform transformation turns an approximation sequence into a floor sequence: that would mean deciding, from the approximations alone, which side of a dyadic grid point x falls on. @audit:ok

The dyadic floor form of computability: a n * 2 ^ (-n) sits in the cell of width 2 ^ (-n) below x. It implies IsComputableENNReal, as isComputableENNReal_of_floor records; there is no uniform converse, since producing a floor sequence from an approximation sequence would mean deciding which side of a dyadic grid point x lies on. @audit:ok

The step-bounded evaluator: the self-delimiting machine run with budget k, following decodePayload_eq_dispatch with eval replaced by evaln k.

The bounded evaluator is sound and complete for the unbounded machine: x is an output of prefixUniversalEval p exactly when some finite budget k already produces it.

Running the self-delimiting machine with a finite budget is primitive recursive in the budget and the program jointly.

All bit strings of length exactly n.

All bit strings of length at most t.

The programs of length at most t on which the machine already halts within budget t.

The stage-t approximation to Ω from below: the mass of the programs of length at most t on which the machine halts within budget t.

The numerator of omegaApprox t written over the denominator 2 ^ t.

The numerators of the lower approximation form a computable sequence, so the stage approximations to Ω are computable over the denominators 2 ^ t.

The stage approximations increase to the halting probability: each is a subsum of the halting weight, and every finite subsum is reached at some stage, so their supremum is Ω.

The search predicate behind the stage lookup, written over the common denominator 2 ^ (n + 2 + t) so that every comparison is between natural numbers: a (n + 2) * 2 ^ (-(n+2)) ≤ omegaApprox t + 2 ^ (-(n+1)).

The least stage satisfying searchPred is a computable function of the requested precision, because the predicate compares natural numbers over a common power of two.

Chaitin's constant is not computably approximable: no computable sequence of dyadic numerators a satisfies |Ω - a n * 2 ^ (-n)| ≤ 2 ^ (-n) for every n.

A computable approximation from above, combined with the computable approximation omegaApprox from below, locates a stage past which no program of length at most n can still halt, and hence decides the halting set of the self-delimiting machine, contradicting prefixUniversalEval_dom_not_computablePred.

The textbook statement speaks of a computable real in the sense of a computable sequence of rationals. That notion can be phrased in Lean, ℚ being Primcodable, but deriving IsComputableENNReal from it takes a rounding step and hence computable division on ℚ, for which Mathlib has no Primrec arithmetic; the two are therefore not linked here, and the negation is proved for IsComputableENNReal itself. @audit:ok