Map Folding Growth Rate Conjecture

### What is the conjecture

Let $a_n$ denote the number of distinct flat foldings of a $1 \times n$ rectangular strip with horizontal and vertical creases marked as mountain or valley folds. The sequence $\{a_n\}$ (OEIS A000136) begins:

$$a_1 = 1, \quad a_2 = 2, \quad a_3 = 6, \quad a_4 = 16, \quad a_5 = 50, \quad a_6 = 144, \quad a_7 = 462, \quad a_8 = 1392, \quad \ldots$$

**The Growth Rate Conjecture**: Determine the precise limiting ratio:

$$\lim_{n \to \infty} \frac{a_{n+1}}{a_n}$$

It is known that this limit exists and lies in the interval $[3.3868, 3.9821]$, indicating exponential growth of $a_n$. However:
- The exact value of the limit remains unknown.
- It is unclear whether the limit has a closed form or is a transcendental number.
- Whether this limit can be expressed in terms of known mathematical constants is an open question.

The similar problem for $2 \times n$ maps (OEIS A001415) also lacks a known growth rate formula.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://mathworld.wolfram.com/MapFolding.html, https://oeis.org/A000136, https://en.wikipedia.org/wiki/Map_folding, https://thatsmaths.com/2019/02/14/folding-maps-a-simple-but-unsolved-problem/, https://www.robertdickau.com/mapfolding.html

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-13)

Building blocks (1-3; from search results):
- Sequences and their asymptotic limits (available in Mathlib via limit theory)
- OEIS integer sequences framework and definitions
- Real number intervals and inequalities

Missing pieces (exactly 2; unclear/absent from search results):
- Formal encoding of the specific sequence $\{a_n\}$ from map folding (requires definition via the enumeration problem)
- Characterization of what "growth rate of the sequence" means precisely in formal terms and bounds on the limiting ratio

Rating justification: The mathematical framework for limits and sequences exists in Mathlib, but the challenge is formally defining the specific sequence $a_n$ arising from map folding enumeration. Once that enumeration is defined, stating the growth rate conjecture is relatively straightforward using standard sequence limit machinery.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-40

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)