math.LO — Logic

The 51-state beeper $M_{51}$: every battle ends, and what Peano Arithmetic can prove about it

Contributed by Annanay Kapila

We study an explicit 51-state, 2-symbol beeping Turing machine $M_{51}$ and its associated dispatch-level process $R$. An ordinal descent below $\varepsilon_0$ proves that every battle of $R$ terminates and hence that $M_{51}$ beeps infinitely often. A growth lemma shows that the battle counters and beep times eventually dominate every function provably computable in Peano Arithmetic. Together with a Rocq-checked simulation theorem, these results establish that quasihalting of $M_{51}$ is independent of Peano Arithmetic. The document includes the process definition, machine table, ordinal analysis, growth proof and an account of its external dependencies.

Author comments: Supporting materials: Rocq simulation development, https://github.com/a-kapila/maths-proofs/blob/2e2d689f198e7bd51d264cd5468d6b7606886d2e/beeping-busy-beaver-51/rocq51.tar.gz ; computational checks, https://github.com/a-kapila/maths-proofs/blob/2e2d689f198e7bd51d264cd5468d6b7606886d2e/beeping-busy-beaver-51/checks51.tar.gz . The Rocq materials support the simulation theorem; the complete independence argument is not claimed to be fully formalized.