Search papers, labs, and topics across Lattice.
This study extends the designability guarantees for RNA sequences by proving that a motif-free target with at most two maximal helices of length 2 can still be designed, provided all other helices are of length 3 or more. The authors build on previous work by Boury et al. to show that the constraints imposed by the short helices can be effectively managed through a global counting argument. This result not only confirms the robustness of existing algorithms but also provides a concrete sequence that minimizes the number of distinct compatible noncrossing folds.
The ability to design RNA sequences with short helices opens new avenues for RNA engineering, challenging previous limitations in structural RNA design.
RNA inverse folding asks for an RNA sequence whose prescribed secondary structure is the unique maximum-base-pair compatible fold. In the four-letter Watson-Crick model (A-U and C-G pairs only, no pseudoknots, and zero minimum base-pair span), Hales et al. introduced a separated-coloring certificate and an even-odd device, while Boury et al. generalized this to modulo-$m$ separability, gave an $O(n 2^m)$ decision algorithm, and guaranteed designability when every helix has length at least 3. We prove that the guarantee still holds when a motif-free target has at most two maximal helices of length 2, no maximal helix of length 1, and all remaining helices of length at least 3. The proof builds on Boury et al.'s local helix-coloring transfers and adds a global counting argument showing that the demands created by at most two short helices can always be coordinated. This is a structural success guarantee for the existing modulo-2 algorithm, not a new general decision capability. The resulting coloring yields an explicit sequence whose every distinct compatible noncrossing fold has fewer pairs. No claim is made for nearest-neighbor thermodynamic energy models. The theorem and supporting lemmas are formalized in Lean 4 against pinned Mathlib and reproduced from a frozen public artifact; the kernel-reported axiom set is $\{\mathrm{propext},\mathrm{Classical.choice},\mathrm{Quot.sound}\}$. The work was developed with foundational generative-AI assistance under the author's direction and has not yet received independent human expert review.
