Certified Digits for Jump-Omega

Along with the results on Jump-Omega, I want to introduce a further halting probability that I call Leap-Omega. It takes this work beyond the finite-jump hierarchy. I’ve kept the introduction brief here and a separate paper will present the full development with proofs. Even a machine that can solve the halting problem cannot compute the entire binary expansion of a 2-random halting probability. This paper certifies the first 55 digits of one concrete example. What Jump-Omega is. A halting probability is the probability that a machine eventually halts when its input bits are chosen by fair coin tosses. The machine studied here extends a specified reading of the Calude–Dinneen register machine with an instruction that answers halting questions about the original machine. Its halting probability, Jump-Omega, is a concrete instance of the classical relativized halting probability Ω′. The machine, encoding, oracle and indexing of questions are specified in the paper. The result. The first 55 binary digits are 0.0001000000010000111010101111011011111010010011000001010… with outward decimal bounds [0.0627581456158597463, 0.0627581456158597666]. How the digits are certified. The computation bounds the probability from below and above until both bounds have the same leading digits. It uses only certified oracle answers. When an answer is unknown, the corresponding branch stays in the upper bound at full measure, so uncertainty can widen the interval without invalidating a certified digit. Adaptive grouping gives different groups of unresolved programs their own bounds and search depths; the proof remains valid however those groups are chosen. Every oracle answer used for the reported digits is settled by syntax or a finite run, so the same finite prefix also occurs for suitable decidable oracles. Proofs and verification. Lean 4 proofs establish that the underlying machine is prefix-free and Chaitin-universal, and that its extension has these properties relative to each oracle. A written proof establishes 2-randomness. The numerical checkers and their agreement with the Lean semantics have been tested, but are not formally verified. The 76-bit certificate was checked in full by one checker on two machines and in part by a second. The 80-bit certificate passed one complete check, and the ordinary-machine 84-bit interval passed full checks by independent C and Python implementations. A second checker agrees on every adaptive-extension record, while the extension's overall counts, bounding factors and combination of bounds were checked by one implementation. The paper states the certificate conditions and the scope of each check. Files and supplementary material. This record contains the paper PDF, LaTeX sources and a prepared arXiv source ZIP for later submission. The research package and supplementary material contain the checkers, certificates, Lean sources and verification records needed to re-check the reported results without repeating the searches. MSC 2020: Primary 03D32; Secondary 68Q30, 68V05, 68V20, 03D80.