2025/10/06 by Andrieu, Mélodie, Shalom Eliahou, Eliahou, Shalom +2
Computer Science · #11A67 #11J71 (Secondary) #68R15 (Primary) 11K16 #Combinatorics (math.CO) #FOS: Mathematics #Number Theory (math.NT) #Numerical Methods and Algorithms #Polynomial and algebraic computation
paper · pdf · doi:10.48550/arxiv.2510.11723
openalex publication_date 2025/10/06 · openalex created_date 2025/10/17 · openalex updated_date 2026/07/29
A self-contained research artifact on the BB(6) busy-beaver frontier. New in this version: two machines of the published holdout list (BB6holdouts1094.txt, 2026-06-29) are proved never to halt from the blank tape, unconditionally, in Lean 4 — sorry-free, no nativedecide, no Mathlib, axiom audit [propext, Quot.sound]; the novelty of both was re-verified against that list up to TNF and left-right reversal. The artifact also contains a machine-independent mechanism library that yields the same rung law for any machine satisfying a six-atom interface (18 further list entries satisfy it, at six kernel rfls each), the paper-style writeups of the cryptid side (certified trace-template reductions; exact p-adic run-structure theorems with Lean formalization; a gate/structure/protection classification), a one-command verification battery, and the supporting lab notes including the novelty audit and the full corrections trail. Scope, stated flatly: BB(6) itself is not decided and this work does not shorten the distance to deciding it — the named cryptids remain open behind a single-orbit equidistribution conjecture, and no cryptid is decided here. Every claim carries an explicit epistemic label. Methodology: AI-assisted under a strict zero-false-proof discipline (adversarial red-teams, independent re-verification), documented in the notes.