1RB3RB1LB---2RB 2LA1RA4LB2LA2RA - Revision history

DrDisentangle: nonhalting proof unfinished

2026-04-19T07:24:33Z

nonhalting proof unfinished

← Older revision		Revision as of 07:24, 19 April 2026
Line 77:		Line 77:
	</pre>		</pre>

	The proof given by @dyuan01 is not yet verified.		This version of the rules was proven in Lean. The nonhalting proof given by @dyuan01 is not yet verified. Opus got stuck and Aristotle couldn't finish from that point either. See the current state, esp. the Aristotle summary in https://github.com/rwst/bbchallenge/tree/main/1RB3RB1LB---2RB_2LA1RA4LB2LA2RA
			(to be continued..)

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

DrDisentangle: /* Opus 4.7 Review */ rm spaces

2026-04-18T16:42:52Z

Opus 4.7 Review: rm spaces

DrDisentangle: Opus Review

2026-04-18T15:10:00Z

Opus Review

@@ Line 20: / Line 20: @@
 == Review ==
 Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.
 The proof given by @dyuan01 is not yet verified.
 [[Category:BB(2,5)]]

RobinCodes: I also feel like this page isn't a stub. There is present analysis, current progress, everything other TM pages have.

2025-10-29T17:10:52Z

I also feel like this page isn't a stub. There is present analysis, current progress, everything other TM pages have.

← Older revision		Revision as of 17:10, 29 October 2025
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA~~}}{{Stub~~}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}
	{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is similar to [[Skelet 17]]. [https://discord.com/channels/960643023006490684/1259770421046411285/1267650177389432913 A proof was given by Daniel Yuan (@dyuan01) of the machine's nonhalting on July 30th 2024.] {{TM\|1RB3RA2LB1LB1RB_2LA2RA4LA1LA---\|undecided}} is equivalent to this machine.		{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is similar to [[Skelet 17]]. [https://discord.com/channels/960643023006490684/1259770421046411285/1267650177389432913 A proof was given by Daniel Yuan (@dyuan01) of the machine's nonhalting on July 30th 2024.] {{TM\|1RB3RA2LB1LB1RB_2LA2RA4LA1LA---\|undecided}} is equivalent to this machine.

RobinCodes: Added proof by @dyuan01, improved structure, noted equivalence to 1RB3RA2LB1LB1RB_2LA2RA4LA1LA---.

2025-10-25T17:46:59Z

Added proof by @dyuan01, improved structure, noted equivalence to 1RB3RA2LB1LB1RB_2LA2RA4LA1LA---.

← Older revision		Revision as of 17:46, 25 October 2025
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{Stub}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{Stub}}
	{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is ~~suspected to be~~ similar to [[Skelet 17]].		{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is similar to [[Skelet 17]]. [https://discord.com/channels/960643023006490684/1259770421046411285/1267650177389432913 A proof was given by Daniel Yuan (@dyuan01) of the machine's nonhalting on July 30th 2024.] {{TM\|1RB3RA2LB1LB1RB_2LA2RA4LA1LA---\|undecided}} is equivalent to this machine.

	~~Analysis shared by Daniel Yuan (@dyuan01) on Discord,~~ [https://discord.com/channels/960643023006490684/~~1084047886494470185~~/~~1251145215461560391~~ on ~~June 14th~~ 2024]:

			=== Analysis shared by Daniel Yuan (@dyuan01) on Discord, [https://discord.com/channels/960643023006490684/1084047886494470185/1251145215461560391 on June 14th 2024]: ===
	I just checked whenever the beaver reaches the 1 on the left side, and calculated the tape for when it next reaches the left side. It would be nice if someone can verify these rules.		I just checked whenever the beaver reaches the 1 on the left side, and calculated the tape for when it next reaches the left side. It would be nice if someone can verify these rules.

Line 15:		Line 14:
	[2n+1, 2a, 2b, …, 2m+1, x, …] -> [2n, 2a, 2b, …, 2m+1, x+1, …]		[2n+1, 2a, 2b, …, 2m+1, x, …] -> [2n, 2a, 2b, …, 2m+1, x+1, …]
	[2n+2, a, b, …] -> [2n+1, a+1, b, …]		[2n+2, a, b, …] -> [2n+1, a+1, b, …]
	~~</pre>~~

	And you should start at [1, 1].		And you should start at [1, 1].
			</pre>

	== Review ==		== Review ==
	Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.		Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.

			The proof given by @dyuan01 is not yet verified.
	[[Category:BB(2,5)]]		[[Category:BB(2,5)]]

Polygon: Added Category:BB(2,5)

2025-09-27T16:12:29Z

Added Category:BB(2,5)

← Older revision		Revision as of 16:12, 27 September 2025
Line 21:		Line 21:
	== Review ==		== Review ==
	Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.		Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.
			[[Category:BB(2,5)]]

Polygon: Used Template:Stub

2025-08-10T22:23:16Z

Used Template:Stub

← Older revision		Revision as of 22:23, 10 August 2025
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{Stub}}
	{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].		{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].

Line 21:		Line 21:
	== Review ==		== Review ==
	Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.		Matthew House (@LegionMammal978) reviewed the above analysis on [https://discord.com/channels/960643023006490684/1084047886494470185/1251210996224364766 June 14th 2024] and agrees with it.

	~~[[Category:Stub]]~~

Polygon: Combined introduction with link to bbch

2025-08-10T21:20:34Z

Combined introduction with link to bbch

← Older revision		Revision as of 21:20, 10 August 2025
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}
			{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}} is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].
	~~This~~ is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].

	Analysis shared by Daniel Yuan (@dyuan01) on Discord, [https://discord.com/channels/960643023006490684/1084047886494470185/1251145215461560391 on June 14th 2024]:		Analysis shared by Daniel Yuan (@dyuan01) on Discord, [https://discord.com/channels/960643023006490684/1084047886494470185/1251145215461560391 on June 14th 2024]:

DF376 at 13:06, 13 August 2024

2024-08-13T13:06:20Z

← Older revision		Revision as of 13:06, 13 August 2024
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA\|undecided}}

	This is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].		This is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].

Int-y1: standardize heading

2024-07-24T02:09:54Z

standardize heading

← Older revision		Revision as of 02:09, 24 July 2024
Line 1:		Line 1:
	{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}		{{machine\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}{{TM\|1RB3RB1LB---2RB_2LA1RA4LB2LA2RA}}
	~~https://bbchallenge.org/~~1RB3RB1LB---2RB_2LA1RA4LB2LA2RA is a 2~~-state~~ 5~~-symbol~~ machine whose behavior is suspected to be similar to [[Skelet 17]].
			This is a [[BB(2,5)]] machine whose behavior is suspected to be similar to [[Skelet 17]].

	Analysis shared by Daniel Yuan (@dyuan01) on Discord, [https://discord.com/channels/960643023006490684/1084047886494470185/1251145215461560391 on June 14th 2024]:		Analysis shared by Daniel Yuan (@dyuan01) on Discord, [https://discord.com/channels/960643023006490684/1084047886494470185/1251145215461560391 on June 14th 2024]:
Line 17:		Line 18:
	</pre>		</pre>

	And you should start at [1, 1]		And you should start at [1, 1].

	== Review ==		== Review ==

← Older revision		Revision as of 16:42, 18 April 2026
Line 23:		Line 23:
	== Opus 4.7 Review ==		== Opus 4.7 Review ==
	<pre>		<pre>
	Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits		Bug 1: "2a, 2b, …" includes 0 but rules only hold for positive even digits

	The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are		The notation 2a, 2b, … in rules 2–5 denotes "even digits" but reads naturally as allowing 0. The rules are
	false when any middle digit is 0.		false when any middle digit is 0.

	Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd —		Counterexample: [1, 0, 2]. Rule 5 would predict [0, 0, 2, 0] (odd-increment applied to leftmost inner odd —
	but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual		but there's no inner odd, so actually rule 3 fires with middle [0], predicting [0, 0, 2, 0]). The actual
	TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like).		TM simulation instead collapses over the zero and produces [3, 2] in 9 steps (rule-1-like).

	Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the		Root cause: a digit y encodes 4^y on the tape (so y = 0 means NO 4s). Without the 4-run to sweep over, the
	separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire.		separator interaction is different, and the sweep dynamics used to derive rules 3–5 don't fire.

	Bug 2: rule 1 can produce length-1 lists		Bug 2: rule 1 can produce length-1 lists

	[0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition		[0, a] → [a+3] has length 1 — subsequent rules require length ≥ 2. So rule 1 needs an explicit precondition
	that the input list has length ≥ 3 (i.e., there IS a b after a).		that the input list has length ≥ 3 (i.e., there IS a b after a).

	Corrected rules		Corrected rules

	[x, y, z] := 1 <B 4^x 12 4^y 12 4^z (encoding; B is state, 1<B means state B on symbol 1)		[x, y, z] := 1 <B 4^x 12 4^y 12 4^z (encoding; B is state, 1<B means state B on symbol 1)
	Start: [1, 1]		Start: [1, 1]

	(R1) [0, a, b, …] → [a+3, b, …]		(R1) [0, a, b, …] → [a+3, b, …]
	where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist).		where the input has length ≥ 3 (the "…" allows empty tail, but `b` must exist).

	(R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0] → Halt		(R2) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 0] → Halt
	middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0.		middle digits are strictly positive even (each 2aᵢ+2 ≥ 2); j ≥ 0.

	(R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0]		(R3) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+2] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+2, 0]
	middle positive even, last digit positive even; j ≥ 0.		middle positive even, last digit positive even; j ≥ 0.

	(R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1]		(R4) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, 1]
	middle positive even, last digit odd; j ≥ 0.		middle positive even, last digit odd; j ≥ 0.

	(R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …]		(R5) [2n+1, 2a₁+2, 2a₂+2, …, 2aⱼ+2, 2m+1, x, …] → [2n, 2a₁+2, …, 2aⱼ+2, 2m+1, x+1, …]
	middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail).		middle positive even, then an odd 2m+1, then at least one more digit x (plus possibly a tail).

	(R6) [2n+2, a, …] → [2n+1, a+1, …]		(R6) [2n+2, a, …] → [2n+1, a+1, …]
	leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty).		leading is positive even (≥ 2); a arbitrary; tail arbitrary (may be empty).

	Consequences for the non-halt argument		Consequences for the non-halt argument

	- R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a		- R2 (halt) is still the "bad" pattern, but defined over positive even middles only — configurations with a
	0 in the middle don't trigger R2; they just aren't reached.		0 in the middle don't trigger R2; they just aren't reached.
Line 70:		Line 70:
	reached from [1, 1]. This is an invariant to be proved, not a property to be checked.		reached from [1, 1]. This is an invariant to be proved, not a property to be checked.
	- Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2).		- Rules R3, R4, R5 each require the middle digits to be strictly positive (≥ 2).

	The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already		The structural proof in §3 of the paper (the 3 "secure types") is not affected by this fix — it already
	treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a		treats the middle digits as an abstract even-valued block. But the rule derivation (§2, currently a