AI 中文总结
该研究在RNA反向折叠的Watson-Crick模型下，证明了含最多两个长度为2螺旋的RNA靶标仍可设计，完善了现有模2算法的可设计性保证。
AI 中文摘要
RNA反向折叠旨在寻找满足指定二级结构且该结构为唯一最大碱基对兼容折叠的RNA序列。在四字母Watson-Crick模型（仅含A-U和C-G配对，无假结，最小碱基对跨度为0）中，Hales等人引入了分离着色证书和奇偶装置；Boury等人将其推广为模m可分性，给出了O(n 2^m)的判定算法，并保证当每个螺旋长度至少为3时的可设计性。我们证明，当无基序的靶标最多含两个长度为2的最大螺旋、无长度为1的最大螺旋且其余所有螺旋长度至少为3时，该保证仍然成立。该证明基于Boury等人的局部螺旋着色转移，并补充了全局计数论证，表明最多两个短螺旋产生的需求总能协调。这是现有模2算法的结构成功保证，而非新的通用判定能力。所得着色产生的显式序列，其每个不同的兼容非交叉折叠的碱基对数量更少。本研究未对最近邻热力学能量模型提出主张。该定理及支撑引理在Lean 4中针对固定的Mathlib进行了形式化，并从冻结的公共工件中复现；内核报告的公理集为{propext, this http URL, this http URL}。本研究在作者指导下借助基础生成式AI辅助完成，尚未获得独立人类专家的评审。
英文摘要
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.
Comments39 pages, 7 figures. Formally verified in Lean 4; developed with foundational AI assistance; not yet independently reviewed. Artifact: https://doi.org/10.5281/zenodo.22101755 ; Source: https://github.com/ajogalekar/rna-at-most-two-short-helices
