Polygon: Completed move

2026-02-21T17:12:30Z

Completed move

← Older revision		Revision as of 17:12, 21 February 2026
Line 1:		Line 1:
	#~~REDIRECT~~ [[~~1RB1RE_1LC1RB_0RA0LD_1LB1LD_~~---~~0RA~~]]		{{machine\|1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA}}
			{{TM\|1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA}}, also called '''Finned #3''', is a non-halting [[Irregular Turing Machine\|irregular]] [[BB(5)]] TM. It belongs to a group of 5 sporadic machines, called finned machines, which had to be individually proven as non-halting in [[Coq-BB5]].<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> It was proven to be irregular in March 2023 by lijil.<ref>https://discuss.bbchallenge.org/t/10756090-finned-3-is-irregular/137</ref>

			== Analysis by lijil ==
			<pre>
			With the CTL-deciders proving to be very strong there is the question which machines cannot be proven by it. 10756090 is an example of such a machine. We can prove that there is no regular language that includes all configuration the TM reaches, but rejects all configurations that lead to halting:

			Write C(n,m) for (10)^n A0 1^m

			Then the TM follows these rules:

			C(n,m) → halt, if n+m is odd
			C(n,m) → C(((n+m)/2)+1,n+1), if n+m is even
			I’ll leave the proof as an exercise for the reader.
			We start in C(0,0) and C(n,n) → C(n+1,n+1) for all n, so the machine is infinite and visits C(n,n) for all n.

			To see how it behaves with n != m we consider the difference n-m after applying rule 2:
			((n+m)/2)+1-(n+1) = (n+m-2n)/2 = -(n-m)/2

			So the TM divides the difference of the exponents by 2 (and flips the sign) until the difference becomes odd. Then it halts. This can only go on forever if the difference is 0 to begin with.

			Thus C(n,m) → halt, if n!=m

			It is impossible for a regular language to separate {C(n,n) for all n} and {C(n,m) for all n!=m}

			To finish it off with an argument by savask:
			“If there was a regular language containing all non-halting configs of your machine, then we could intersect it with a language (10)* A0 1* and obtain that (10)^n A0 1^n is regular”
			</pre>

			== References ==

			[[Category:BB(5)]]

Polygon: Created redirect to new page

2025-08-27T16:29:48Z

Created redirect to new page

New page

#REDIRECT [[1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA]]

Finned 3 - Revision history

Polygon: Completed move

Polygon: Created redirect to new page