1RB1RA 1LC1LE 1RE0LD 1LC0LF 1RZ0RA 0RA0LB - Revision history

RobinCodes: Added the fact that @mxdys Rocq-proved this machine.

2025-10-23T17:11:47Z

Added the fact that @mxdys Rocq-proved this machine.

← Older revision		Revision as of 17:11, 23 October 2025
Line 2:		Line 2:
	{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB\|halt}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.		{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB\|halt}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.

	~~As of Sep 21~~ 2025, ~~this TM does not have~~ a Rocq proof.		On 20 Oct 2025, @mxdys [https://github.com/ccz181078/busycoq/blob/BB6/verify/SOTCv1.v gave a Rocq proof] confirming the result.

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==

Polygon: /* Analysis by Katelyn Doucette */ Removed link to nonexistent user page

2025-10-09T19:24:45Z

Analysis by Katelyn Doucette: Removed link to nonexistent user page

← Older revision		Revision as of 19:24, 9 October 2025
Line 48:		Line 48:
	</pre>		</pre>

	== Analysis by ~~[[User:isokate\|~~Katelyn Doucette]]==		== Analysis by Katelyn Doucette ==
	The machine follows these rules:		The machine follows these rules:

Int-y1: start on different state

2025-09-28T07:38:08Z

start on different state

← Older revision		Revision as of 07:38, 28 September 2025
Line 5:		Line 5:

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==
	Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE\|halt}} which has identical behavior but with different starting ~~conditions~~. The sister machine halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.		Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE\|halt}} which has identical behavior but with a different starting state. The sister machine halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.

	<pre>		<pre>

Int-y1: add category BB(6)

2025-09-27T04:53:34Z

add category BB(6)

← Older revision		Revision as of 04:53, 27 September 2025
Line 76:		Line 76:

	@poppuncher's rules were evaluated by [[User:sligocki\|Shawn Ligocki]].		@poppuncher's rules were evaluated by [[User:sligocki\|Shawn Ligocki]].

			[[Category:BB(6)]]

Int-y1: no rocq

2025-09-21T22:40:38Z

no rocq

← Older revision		Revision as of 22:40, 21 September 2025
Line 1:		Line 1:
	{{Machine\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}}		{{Machine\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}}
	{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB\|halt}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.		{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB\|halt}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.

			As of Sep 21 2025, this TM does not have a Rocq proof.

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==

Polygon: Added "halt" to bbch-link of sister machine

2025-08-16T18:29:57Z

Added "halt" to bbch-link of sister machine

← Older revision		Revision as of 18:29, 16 August 2025
Line 3:		Line 3:

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==
	Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. The sister machine halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.		Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE\|halt}} which has identical behavior but with different starting conditions. The sister machine halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.

	<pre>		<pre>

Polygon: Added "halt" to bbch-link

2025-08-16T18:29:23Z

Added "halt" to bbch-link

← Older revision		Revision as of 18:29, 16 August 2025
Line 1:		Line 1:
	{{Machine\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}}		{{Machine\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}}
	{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.		{{TM\|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB\|halt}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==

Polygon: Changed wording

2025-08-13T16:41:07Z

Changed wording

← Older revision		Revision as of 16:41, 13 August 2025
Line 3:		Line 3:

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==
	Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. ~~Which, in contrast, instead~~ halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.		Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. The sister machine halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.

	<pre>		<pre>

Polygon: Clarified that the score given belongs to the sister machine

2025-08-13T16:39:32Z

Clarified that the score given belongs to the sister machine

← Older revision		Revision as of 16:39, 13 August 2025
Line 3:		Line 3:

	== Analysis by @poppuncher ==		== Analysis by @poppuncher ==
	Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. In contrast, ~~this machine~~ instead halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.		Most of the initial analysis was done on its sister machine {{TM\|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. Which, in contrast, instead halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.

	<pre>		<pre>

Isokate: Created page with "{{Machine|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}} {{TM|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}} is a tetrational halting BB(6) TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly $10 \uparrow \uparrow 6.96745$ . == Analysis by @poppuncher == Most of the ini..."

2025-06-11T01:50:27Z

Created page with "{{Machine|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}} {{TM|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}} is a tetrational halting BB(6) TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>. == Analysis by @poppuncher == Most of the ini..."

New page

{{Machine|1RB1RA_1LC1LE_1RE0LD_1LC0LF_---0RA_0RA0LB}}
{{TM|1RB1RA_1LC1LE_1RE0LD_1LC0LF_1RZ0RA_0RA0LB}} is a tetrational halting [[BB(6)]] TM first discovered and analyzed by @poppuncher. It was shared on Discord on 5 Jun 2025 ([https://discord.com/channels/960643023006490684/1380384286942822561 Discord Link]). It is a translated counter that halts with a final sigma score of roughly <math>10 \uparrow \uparrow 6.96745</math>.

== Analysis by @poppuncher ==
Most of the initial analysis was done on its sister machine {{TM|1RB0RF_1LC0RA_1RZ0LD_1LE1LD_1RB1RC_0LD0RE}} which has identical behavior but with different starting conditions. In contrast, this machine instead halts with a smaller, though still enormous, sigma score of roughly <math>10 \uparrow \uparrow 5.77573</math>. The following explanation describes this sister machine, but aside from the starting conditions and states, it applies to the larger machine as well.

<pre>
basically, there is a unary counter on one side and a weird binary counter on the other side.

the weird binary counter behaves as if counting the number of bit flips required to increment a binary number (let's call it A) of a given length n, until it reaches 2^n. the number of flips are written to the unary counter, which then resets, and the process starts again with a new binary string.

For example, let n = 6 and A = 48, which is 110000 in binary, then it will count up to 1000000. there is a formula for the number of bit flips required, which is 2^(n+1) - 2*A - 1 + pop_count(A), where pop_count is the number of '1's in the binary representation of A. In this example
it evaluates to 2^7-2*48-1+2 = 33.

Note that leading zeroes are allowed, so if n = 9 and A = 48, then
we are counting 000110000 until it reaches 1000000000, and the count will be 2^10-2*48-1+2 = 417.

now for the halting part, i can prove that the following rules:
A> 0 1^(5n+0) -> (10 110)^n <D 01
A> 0 1^(5n+1) -> (10 110)^n 10 <D 01
A> 0 1^(5n+2) -> (10 110)^n 110 <D 01
A> 0 1^(5n+3) -> (10 110)^n 10 10 10 <D 01
A> 0 1^(5n+4) -> Halt(3n+3)

the binary counter encodes the binary string such that "10" on the tape corresponds to 0, and "110" corresponds to 1, (also the most significant bit is on the right, so we need to flip it)

for example at t = 159, the tape is 0^inf 10 10 10 10 110 110 <D 01 0^inf, which corresponds to 110000 (this is also the example earlier, with n = 6 and A = 48).
with this in mind, i got the following rules:
A(n) is the numerical value of the binary string, L(n) is the length of the string, P(n) is the count of '1's in the string, and R(n) is the amount of increments made on the unary counter, counting the number of bit flips before it resets
initial conditions: A(1) = 0, L(1) = 2
P(n) := pop_count(A(n))
R(n) := 2^(1 + L(n)) - 2*A(n) - 1 + P(n)
k(n) := R(n)//5 (division without remainder)
r(n) := R(n) % 5, (so R(n) = 5*k(n) + r(n))

then we have P(1) = 0, R(1) = 7;

the rules:
if R(n) mod 5 == 4 then halt
otherwise
let a(r) = {0, 1, 1, 3} (for 0 <= r < 4)
then
L(n+1) = L(n) + 1 + 2 * k(n) + a(r(n))
A(n+1) = 2 ^ (2 + L(n)) * ( 2^(2*k(n)) - 1 ) / 3 + (if r(n) = 2 then 2 ^ ( L(n)+1 + 2*k(n) ) otherwise 0)
P(n+1) = pop_count(A(n+1)) = k(n) + (if r(n) = 2 then 1 otherwise 0)
</pre>

== Analysis by [[User:isokate|Katelyn Doucette]]==
The machine follows these rules:

<pre>
Let s = 2^{b+2} - 2 + 2^{b+2}((4^k - 1)/3) + k

START = A(1, 3)

A(5k + 0, b) -> A(s + 1, b + 2k + 1)

A(5k + 1, b) -> A(s + 1 + 2^{(b+2k+1)+1}, b + 2k + 2)

A(5k + 2, b) -> A(s + 2, b + 2k + 2)

A(5k + 3, b) -> A(s + 1 + 2^{b+2k+2}(7), b + 2k + 4)

A(5k + 4, b) -> Halt(b + 3k + 4)
</pre>

And runs through seven of these resets before reaching <math>5k + 4</math> and halting.

These configurations are identifiable as the transition of this form:
<code>1^(5k+r) 01 <B (01)^b</code>

== Evaluation==
Both @poppuncher and [[User:isokate|Katelyn Doucette]]'s rules were evaluated on both machines and line up with one another providing high confidence that the analyses and final sigma scores are correct.

@poppuncher's rules were evaluated by [[User:sligocki|Shawn Ligocki]].