Left-distributive embedding algebras

We consider algebras with one binary operation $\cdot$ and one generator, satisfying the left distributive law $a\cdot (b\cdot c)=(a\cdot b)\cdot (a\cdot c)$; such algebras have been shown to have surprising connections with set-theoretic large cardinals and with braid groups. One can construct a sequence of finite left-distributive algebras $A_{n}$, and then take a limit to get an infinite left-distributive algebra $A_{\infty }$ on one generator. Results of Laver and Steel assuming a strong large cardinal axiom imply that $A_{\infty }$ is free; it is open whether the freeness of $A_{\infty }$ can be proved without the large cardinal assumption, or even in Peano arithmetic. The main result of this paper is the equivalence of this problem with the existence of a certain left-distributive algebra of increasing functions on natural numbers, called an embedding algebra, which emulates some properties of functions on the large cardinal. Using this and results of the first author, we conclude that the freeness of $A_{\infty }$ is unprovable in primitive recursive arithmetic.