🧬 biology

Designability of RNA Targets with Up to Two Length-2 Helices

This paper proves that RNA targets with at most two maximal helices of length 2 and no helices of length 1 remain designable under the four-letter Watson-Crick model, extending existing modulo- $m$ separability guarantees through a combination of local coloring transfers and global counting arguments, with the formal proof verified in Lean 4.

Original authors: Ashutosh S. Jogalekar

Published 2026-08-27✓ Author reviewed ⓘ

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Ashutosh S. Jogalekar

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ⚕️ This is an AI-generated explanation of a preprint that has not been peer-reviewed. It is not medical advice. Do not make health decisions based on this content. Read full disclaimer

Inside every living cell, ribonucleic acid, or RNA, acts as a versatile messenger and machine, carrying instructions and helping to build proteins. To do its job, a strand of RNA must fold into a specific three-dimensional shape. Scientists have long known how to predict what shape a given sequence of chemical letters will form, a process akin to watching a string of beads snap together into a knot. The reverse problem, however, is far more difficult: if a scientist wants a specific shape, can they work backward to find the exact sequence of letters that will fold into it, and only that shape? This is the challenge of RNA inverse folding. If researchers can solve this, they could design new RNA molecules to fight viruses, regulate genes, or build nanomachines. The difficulty lies in the fact that a single sequence might fold into many different shapes, and the goal is to find a sequence that locks into just one desired form, ignoring all the others.

For decades, mathematicians and biologists have studied a simplified version of this puzzle to understand the fundamental rules. In this idealized world, the RNA strand is made of four types of letters, and they pair up in strict, predictable ways: one letter always matches with another, and a third matches with a fourth. The energy of the molecule is determined simply by counting how many of these pairs form; more pairs mean a more stable shape. The goal is to prove that for certain complex shapes, there is always a unique sequence that creates them. Previous work had shown that if every "ladder" of pairs in the target shape was at least three rungs long, a solution could always be found. But nature often uses shorter ladders, and these tiny structures create a bottleneck. They offer so few options for arranging the letters that it becomes unclear whether a unique solution exists, or if the short ladders will force the molecule to fold into the wrong shape.

A new study by Ashutosh Jogalekar addresses this specific bottleneck. The researcher focused on RNA targets that contain very short ladders, specifically those with exactly two rungs, which are called isolated stacks. The question was whether the presence of these short structures makes a shape impossible to design, or if there is still a way to find a unique sequence. The paper proves that design is possible, but only if the number of these short ladders is strictly limited. The study demonstrates that if an RNA target contains no isolated ladders of just one rung, and has at most two ladders of exactly two rungs, a unique sequence can always be constructed. If a target has three or more of these short two-rung ladders, the method described in the paper fails to guarantee a solution, though it does not prove that no solution exists at all.

The proof relies on a clever system of assigning instructions to the RNA letters. Imagine the RNA structure as a tree, where the branches represent the ladders of pairs. The researcher assigns a specific "color" to each pair in the target shape, which dictates which chemical letters must be used. These colors are not physical paints but instructions: some colors demand a specific pair of letters, while others allow for a choice. The critical insight is that these instructions must be coordinated so that every loop in the structure receives a distinct set of letters, preventing the molecule from accidentally folding into a different shape. The study shows that when there are at most two short ladders, the system has enough flexibility to coordinate these instructions globally. The short ladders act as a limited resource; once two of them are used, the rest of the structure is forced to be longer, which provides the extra room needed to arrange the remaining letters correctly.

To ensure the result is not just a theoretical guess, the entire argument was translated into a formal language that a computer can check for logical errors. The researcher used a tool called Lean, which acts like a rigorous proofreader that verifies every single step of the logic. The computer confirmed that the construction works for every possible case within the defined limits. The study also included a detailed audit where an artificial intelligence system, acting as a blind reviewer, compared the mathematical description of the problem with the computer code to ensure they matched perfectly. This double-checking process gives a high degree of certainty that the proof is correct, even though the work has not yet been reviewed by human experts in the field.

The findings do not solve the problem for all RNA shapes, nor do they claim that shapes with three short ladders are impossible to design. Instead, the paper draws a clear boundary: it proves that the specific method of construction works perfectly for targets with zero, one, or two short ladders, provided no single-rung ladders exist. This provides a solid foundation for designing RNA molecules that are slightly more complex than previously guaranteed, offering a new set of reliable blueprints for scientists. By establishing these limits with mathematical precision and computer verification, the work clarifies exactly how much structural complexity can be handled before the rules of design become too tangled to guarantee a unique solution.

Technical Summary: Designability of RNA Targets with Up to Two Length-2 Helices

Problem Statement
The paper addresses the RNA inverse folding problem within a simplified combinatorial model: the four-letter Watson–Crick alphabet (A, U, C, G) where only canonical base pairs (A–U, C–G) are permitted, pseudoknots are forbidden, and adjacent nucleotides may pair. In this "maximum-pair" model, lower energy corresponds strictly to a higher number of base pairs. The central question is whether a specific target secondary structure can be uniquely designed—that is, whether there exists an RNA sequence for which the target is the unique compatible noncrossing structure with the maximum number of base pairs.

Previous work by Haleš et al. established designability for targets where every helix contains at least three base pairs, utilizing a "separated coloring" certificate. Boury et al. extended this to a linear-time algorithm using modulo- $m$ separation. However, targets containing short helices (specifically length-1 "isolated base pairs" and length-2 "isolated stacks") present combinatorial challenges because they offer fewer degrees of freedom to coordinate base-pair choices across neighboring loops. While targets with many isolated stacks are known to be designable, the specific conditions guaranteeing designability for targets with a bounded number of isolated stacks (specifically length-2 helices) had not been formally characterized in a target-preserving manner.

Methodology
The author employs a constructive proof strategy based on the "separated coloring" framework. The methodology proceeds in three main stages:

Coloring Certificate Construction:
The target structure is mapped to a rooted interval tree. The core of the proof is the construction of a "proper modulo-2 separated coloring."
- Properness: A local constraint ensuring that at any loop (multiloop, bulge, or hairpin), the incident base pairs (viewed from the loop) do not exceed the capacity to assign distinct nucleotide identities (G, C, A, U). Specifically, an exposure must contain at most one Black (B, G–C), one White (W, C–G), and two Gray (G, A–U) incidences.
- Separation: A global constraint ensuring that no gray paired node and no target-unpaired nucleotide share the same integer "level" (a running sum of parity increments along the tree path).
- Modulo-2 Separation: A stronger condition where gray pairs and unpaired nodes occupy disjoint residue classes modulo 2 (even vs. odd). The author proves that for the specific class of targets studied, a "uniform residue form" exists where all unpaired nodes share one parity ( $\xi$ ) and all gray pairs share the opposite ( $\eta$ ).
Inductive Construction with Bounded Resources:
The paper introduces a novel inductive argument on helix subtrees to handle targets with isolated stacks (length-2 helices).
- Feasible State Sets ( $F$ and $Q$ ): The proof distinguishes between subtrees containing no isolated stacks (guaranteed to support a set of entry states $F$ ) and those containing one or two isolated stacks (guaranteed to support a restricted set $Q$ ).
- Global Counting Argument: The critical innovation is a resource-counting lemma. If a multiloop has two outgoing child subtrees that both require a "gray" entry (indicating they contain isolated stacks), the global bound of "at most two isolated stacks" in the entire target forces the incoming helix to be long (length $\ge 3$ ). This length allows the incoming helix to utilize a specific "non-gray-ending" transfer word (e.g., GBB) from Boury et al.'s existing tables. This non-gray closure resolves the capacity conflict that would otherwise arise if the incoming helix were also short.
Sequence Construction and Uniqueness Proof:
Once a proper separated coloring is established, an explicit RNA sequence is constructed:
- Unpaired positions are assigned 'A'.
- Black/White pairs are assigned G–C/C–G.
- Gray pairs are assigned A–U/U–A with specific orientation rules to ensure local distinctness.
- The author proves that any alternative compatible fold with the same number of base pairs must pair the same set of nucleotides. Using prefix balance arguments (levels) and the separation property, they demonstrate that any fold pairing a target-unpaired position to a gray-pair nucleotide would violate the G–C prefix balance, leaving a G or C unpaired and thus reducing the total pair count.

Key Contributions

The At-Most-Two Theorem: The paper proves that every target structure satisfying the following conditions is designable in the four-letter Watson–Crick model:
- No isolated base pairs (length-1 helices).
- At most two isolated stacks (length-2 helices).
- All other helices have length at least 3.
- The target avoids local obstruction motifs $m_5$ (paired degree $>4$ ) and $m_{3\bullet}$ (unpaired child with paired degree $>2$ ).
Bounded-Resource Induction: The work provides the first formal guarantee for designability in the presence of short helices by introducing a global counting argument that coordinates local coloring constraints. It demonstrates that the "bottleneck" of two short helices at a junction can be resolved if the incoming helix is long, a condition enforced by the global count.
Formal Verification: The entire theorem, including the coloring construction, sequence generation, and uniqueness proofs, has been formalized in Lean 4. The source code was rebuilt in an isolated environment, and the proof was verified against a blinded mathematical specification.

Results

Designability Guarantee: The paper establishes a sufficient condition for designability that extends beyond the "all-long" (length $\ge 3$ ) class. It confirms that the presence of up to two isolated stacks does not preclude designability, provided the rest of the structure adheres to the length and motif constraints.
Sharpness of the Bound: The author provides a counterexample (a target with three isolated stacks) that admits a proper ordinary separated coloring and is designable, but fails to admit a proper modulo-2 separated coloring. This demonstrates that the "at most two" bound is tight for the specific modulo-2 coloring criterion used in the proof, though it does not necessarily imply that targets with three stacks are undesignable.
Algorithmic Complexity: The constructive proof yields a deterministic algorithm that runs in linear time ( $O(n)$ ) given the tree representation, matching the efficiency of previous methods for the "all-long" case.

Significance and Claims
The paper claims to provide a formally verified sufficient condition for RNA designability in a simplified model. Its significance lies in:

Extending the Designable Class: It bridges the gap between the "all-long" guarantees of Boury et al. and the general designability of structures with short helices, specifically quantifying the limit (two isolated stacks) for the modulo-2 coloring approach.
Rigorous Verification: The work highlights the integration of generative AI in research and formal verification, with the final theorem checked by the Lean kernel and a blinded automated audit.
Modesty of Scope: The author explicitly states that this is a combinatorial result in an idealized model (ignoring thermodynamics, wobble pairs, and salt effects). They do not claim to characterize all designable targets, nor do they claim that targets with more than two isolated stacks are undesignable. The result is a specific, constructive certificate for a well-defined structural class.

The paper concludes that the "at-most-two" bound is a genuine resource limit for the specific modulo-2 coloring construction presented, offering a new structural insight into how short helices interact with global coloring constraints in RNA inverse folding.

Technical Summary: Designability of RNA Targets with Up to Two Length-2 Helices

More like this