Skelet 17 - Revision history

Polygon: updated link to Coq/Rocq proof, the previous link went to a 404 error

2026-11-07T14:28:51Z

updated link to Coq/Rocq proof, the previous link went to a 404 error

← Older revision		Revision as of 14:28, 7 November 2026
Line 6:		Line 6:
	Building upon this work, Chris Xu produced a full proof of its non-halting that can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf		Building upon this work, Chris Xu produced a full proof of its non-halting that can be found here: https://chrisxudoesmath.com/papers/skelet17.pdf

	Adapting the above, a formal proof of its non-halting by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/~~Skelet17~~.md		Adapting the above, a formal proof of its non-halting by mxdys can be found here: https://github.com/ccz181078/Coq-BB5/blob/main/CoqBB5/BB5/BB5_Skelet17.v

	== TM Behavior ==		== TM Behavior ==

Sligocki: /* Irregularity */ Link to dyuan's Discord message

2026-10-01T19:16:33Z

Irregularity: Link to dyuan's Discord message

← Older revision		Revision as of 19:16, 1 October 2026
Line 95:		Line 95:
	* Gray Code value (denoted by <math>n</math>): the integer that is obtained by calculating the parity of each number (except the last) in the list, considering the result as a Gray Code bitstring corresponding to some integer and "recovering" this integer.		* Gray Code value (denoted by <math>n</math>): the integer that is obtained by calculating the parity of each number (except the last) in the list, considering the result as a Gray Code bitstring corresponding to some integer and "recovering" this integer.
	* Increment value (denoted by <math>\sigma</math>): the parity of the entire sequence, mapped to <math>\{-1, 1\}</math>. During Increment steps, Skelet 17 counts forwards when <math>\sigma = +1</math> or backwards if <math>\sigma = -1</math>.		* Increment value (denoted by <math>\sigma</math>): the parity of the entire sequence, mapped to <math>\{-1, 1\}</math>. During Increment steps, Skelet 17 counts forwards when <math>\sigma = +1</math> or backwards if <math>\sigma = -1</math>.
	* Length of the sequence (including leading zeros).		*Length of the sequence (including leading zeros).

	When started on a blank tape, the machine visits configurations of the form <math>(0, 2, 4, ..., 2^{2k+2}, 0)</math> infinitely often (the step numbers where it occurs approximately equal powers of 16: 14, 251, 4088, 65537, 1048646, 16777607, 268437188, etc).		When started on a blank tape, the machine visits configurations of the form <math>(0, 2, 4, ..., 2^{2k+2}, 0)</math> infinitely often (the step numbers where it occurs approximately equal powers of 16: 14, 251, 4088, 65537, 1048646, 16777607, 268437188, etc).
Line 107:		Line 107:
	=== Irregularity ===		=== Irregularity ===

	Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.		Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.<ref>dyuan01. 2 Aug 2024. Discord: https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	== See also ==		== See also ==

Polygon: /* TM Behavior */ fixed a typo

2026-03-29T12:40:30Z

TM Behavior: fixed a typo

← Older revision		Revision as of 12:40, 29 March 2026
Line 97:		Line 97:
	* Length of the sequence (including leading zeros).		* Length of the sequence (including leading zeros).

	When started on a blank tape, the machine visits configurations of the form <math>(0, 2, 4, ..., 2^{2k+2}, 0)</math> infinitely often (the step numbers where it occurs approximately equal ~~power~~ of 16: 14, 251, 4088, 65537, 1048646, 16777607, 268437188, etc).		When started on a blank tape, the machine visits configurations of the form <math>(0, 2, 4, ..., 2^{2k+2}, 0)</math> infinitely often (the step numbers where it occurs approximately equal powers of 16: 14, 251, 4088, 65537, 1048646, 16777607, 268437188, etc).

	=== Analysis by bisimulation ===		=== Analysis by bisimulation ===

Polygon: Added time for proof of irregularity

2026-03-02T18:07:13Z

Added time for proof of irregularity

← Older revision		Revision as of 18:07, 2 March 2026
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of non-halting in [[Coq-BB5]]<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> ~~and is also~~ [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of 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 Turing Machine\|irregular]] in August 2024.<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf

Polygon: Added See also section

2026-02-26T16:46:53Z

Added See also section

← Older revision		Revision as of 16:46, 26 February 2026
Line 108:		Line 108:

	Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.		Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.

			== See also ==
			* [[Skelet 1]]
			* [[Skelet 10]]
			* [[Finned 3]]

	== References ==		== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]

Polygon: Added it having needed an individual proof in Coq-BB5

2026-02-22T09:58:18Z

Added it having needed an individual proof in Coq-BB5

← Older revision		Revision as of 09:58, 22 February 2026
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of non-halting in [[Coq-BB5]]<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> and is also [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf

Polygon: Referenced irregularity

2026-02-21T13:09:39Z

Referenced irregularity

← Older revision		Revision as of 13:09, 21 February 2026
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf
Line 108:		Line 108:

	Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.		Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.

			== References ==

	[[Category:BB(5)]]		[[Category:BB(5)]]

Polygon: fixed a typo

2026-02-20T13:33:10Z

fixed a typo

← Older revision		Revision as of 13:33, 20 February 2026
Line 94:		Line 94:

	* Gray Code value (denoted by <math>n</math>): the integer that is obtained by calculating the parity of each number (except the last) in the list, considering the result as a Gray Code bitstring corresponding to some integer and "recovering" this integer.		* Gray Code value (denoted by <math>n</math>): the integer that is obtained by calculating the parity of each number (except the last) in the list, considering the result as a Gray Code bitstring corresponding to some integer and "recovering" this integer.
	* Increment value (denoted by <math>\sigma</math>): the parity of the entire sequence, mapped to <math>\{-1, 1\}</math>. ~~Dirung~~ Increment steps, Skelet 17 counts forwards when <math>\sigma = +1</math> or backwards if <math>\sigma = -1</math>.		* Increment value (denoted by <math>\sigma</math>): the parity of the entire sequence, mapped to <math>\{-1, 1\}</math>. During Increment steps, Skelet 17 counts forwards when <math>\sigma = +1</math> or backwards if <math>\sigma = -1</math>.
	* Length of the sequence (including leading zeros).		* Length of the sequence (including leading zeros).

Polygon: Added it being irregular to the introduction

2025-12-04T18:40:37Z

Added it being irregular to the introduction

← Older revision		Revision as of 18:40, 4 December 2025
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]].		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf

Polygon: /* Analysis by bisimulation */ added irregularity (migrated from cosearch)

2025-12-04T18:38:10Z

Analysis by bisimulation: added irregularity (migrated from cosearch)

← Older revision		Revision as of 18:38, 4 December 2025
Line 104:		Line 104:

	Such skipped intermediate steps are denoted by asterisks in the table to preserve the "real" step counts (e.g. steps 7* and 7**).		Such skipped intermediate steps are denoted by asterisks in the table to preserve the "real" step counts (e.g. steps 7* and 7**).

			=== Irregularity ===

			Consider a list like [a, b, c, ... k, z] (assume z is even). It can be converted to something like [something dependent on a to k] <B 10^z. As it turns out, if we artificially make z sufficiently large, the gray counter will eventually reach 0 before ever switching directions and eventually halt. On the flip side, there is no limit to how large the last element can be in the forward behavior of Skelet 17. So by always selecting the next A_n <B B_n to be the one such that z is large enough to make A_m <B 10^z halt for all m < n, we have constructed an infinite sequence such that A_n <B B_n are all visited, but A_m <B B_n halt for m < n.
	[[Category:BB(5)]]		[[Category:BB(5)]]

← Older revision		Revision as of 18:07, 2 March 2026
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of non-halting in [[Coq-BB5]]<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> ~~and is also~~ [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of 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 Turing Machine\|irregular]] in August 2024.<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf

← Older revision		Revision as of 09:58, 22 February 2026
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is one of the few TMs to have required an individual proof of non-halting in [[Coq-BB5]]<ref name="bbchallenge 2025">https://arxiv.org/pdf/2509.12337 Determination of the fifth Busy Beaver value</ref> and is also [[Irregular Turing Machine\|irregular]].<ref>https://discord.com/channels/960643023006490684/1082035052961091705/1269022847502647357</ref>

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf

← Older revision		Revision as of 18:40, 4 December 2025
Line 1:		Line 1:
	{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}		{{machine\|1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA}}{{Stub}}
	{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]].		{{TM\|1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA}}, called '''Skelet #17''', was one of [[Skelet's 43 holdouts]] and one of the last holdouts in [[BB(5)]]. It is also [[Irregular Turing Machine\|irregular]].

	The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf		The first step towards its resolution was made by savask, who showed the connection to [[wikipedia:Gray_code\|Gray Code]]: https://docs.bbchallenge.org/other/skelet17_savasks_analysis.pdf