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

Annanay Kapila

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

Primarily AI-generated textHuman understanding: some partsmath.LO — Logic

Contributed by Annanay Kapila ↗

Version 1 / Nov 11, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

The text is primarily AI-generated. Some parts of this contribution, but not all, have been checked and understood by a human. The accompanying simulation theorem is formalized in Rocq. The manuscript was converted from Markdown with LaTeX to TeX for submission, preserving its mathematical expressions and code blocks.

References

No bibliography entries.

Version history

v1 · 35 pagesSubmitted by Annanay KapilaSupporting 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.CurrentNov 10, 2026