View source for 1RB1LA 0LC0RC 1LE1RD 1RE1RC 1LF0LA ---1LE

{{machine|1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE}}
{{TM|1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE}} is a [[BB(6)]] [[Cryptid]] similar to [[Space Needle]]. It was discovered by sheep on 7 April 2026.<ref>https://discord.com/channels/960643023006490684/1448375857046360094/1490772706269069313</ref>

Its single-argument-rules have been simulated for 10M iterations without reaching any <math>2^k</math> or <math>3 \cdot 2^k</math>.<ref>https://discord.com/channels/960643023006490684/1239205785913790465/1491589796663918684</ref>

== Analysis by Daniel Yuan ==
https://discord.com/channels/960643023006490684/1448375857046360094/1490792769483051228
<pre>
A(m,n) = 1^m E> 1^n

So I would say either

(0, 0) --> halt
(1, n) --> halt
(0, n) --> (2, n-1) for n >= 1
(2m, n) --> (3m+n-1, 2) for m >= 1
(2m+1, n) --> (m-1, m+n+3) for m >= 1

or

(0, 0) --> halt
(1, n) --> halt
(0, n+1) --> (2, n)
(2m+2, n) --> (3m+n+2, 2)
(2m+3, n) --> (m, m+n+4)


I like converting this into these rules:

(3, 0) --> halt
(4, n) --> halt
(3, n+1) --> (5, n)
(2m-1, n) --> (3m+n-4, 2) for m >= 3
(2m, n) --> (m, m+n+1) for m >= 3

That way we can see the effect of m dividing by 2
We can even reduce this to one number
Let A(n) = (n, 2)


Start at A(5), (the equivalent of (2, 2) using the original rules), then follow these rules:

A(2^k) --> halt
A(3*2^k) = (3*2^k, 2) --> (3, 3*(2^k-1)+2+k) --> (3, 3*(2^k)-1+k) --> (5, 3*(2^k)-2+k) --> (3*(2^k)+3+k), 2) --> A(3*2^k+3+k)
A((2m-1)*2^k) = ((2m-1)*2^k, 2) --> (2m-1, (2m-1)*(2^k-1)+2+k) --> (m-1+(2m-1)*2^k+k, 2) --> A((2m-1)*2^k+k+m-1) for m >= 3
</pre>

== Analysis by hipparcos ==
https://discord.com/channels/960643023006490684/1448375857046360094/1490909482493149306

in practice I think we only ever hit the <math>A((2m-1)*2^k) \rightarrow A((2m-1)*2^k+k+m-1)</math> for <math>m \geq 3</math> rule

so I think we can let <math>a = m-1</math> and write this as the problem:

Let <math>f(b) = b + k + a</math>, where <math>k</math> and <math>a</math> are non-negative integers satisfying <math>b = (2a+1) \cdot 2^k</math>.

Now consider the iterated application of the function <math>f^{n+1}(b) = f(f^n(b))</math>, <math>f^0(b) = b</math>. Does there exist a non-negative integer <math>n</math> such that <math>f^n(5)</math> equals a power of 2 or 3 times a power of 2?

== Non-halting form ==
As long as it is unknown if <code>3*2^k</code> is hit, the ultimate mathematical definition of the non-halting problem must include the <code>3*2^k</code> branch (full proof of the rules and this form was formalized in Lean<ref>https://github.com/rwst/bbchallenge/blob/main/1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE/machine.lean</ref>):

<math display="block">
f(n) =
\begin{cases}
\mbox{HALT} , & \mbox{for } n=2^i \Longleftrightarrow \mbox{oddPart} (n)=1,\\
n+v_2(n)+3, & \mbox{for oddPart} (n)=3,\\
n+v_2(n)+\frac{\mbox{oddPart}(n)-1}{2}, & \mbox{for oddPart} (n)>3,
\end{cases}
</math>

<math display="block">
\text{Conjecture: } \neg \exist \, k, \quad f^k(5)=\text{HALT}
</math>

== Analysis by Aristotle ==
<pre>
After extensive analysis, this theorem appears to be a Collatz-type conjecture — the iteration f is closely related to the map n → (3n-1)/2 on odd numbers,
and proving the orbit from 5 never reaches a power of 2 is analogous in difficulty to proving non-halting in Collatz-like systems.

Key structural lemma even_case_no_pow2: For any even n with 2-adic valuation a ≥ 2 and odd part m ≥ 5, the formula m * 2^a + a + (m-1)/2 is never a power of 2.
The proof uses modular arithmetic: the powers of 2 modulo 2^(a+1)+1 are exactly {±2^k : k = 0..a}, and the target residue 2a-1 is not in this set for a ≥ 2.

Key structural lemma oddPart3_no_pow2: For any a, the expression 3 * 2^a + a + 3 (the odd-part-3 case) is never a power of 2.
This uses bounding: for a ≥ 4, the value lies strictly between 2^(a+1) and 2^(a+2), and small cases are checked directly.

What these lemmas imply: The only "dangerous" inputs — values where f could output a power of 2 — are restricted to two specific infinite families:

Odd n = (2^(k+1)+1)/3 for even k ≥ 4 (via the map n → (3n-1)/2)

Even n with 2-adic valuation exactly 1 and specific odd part (via the a=1 case)
</pre>

== References ==

[[Category:BB(6)]]
[[Category:Cryptids]]