2026-08-26
In the four-letter Watson-Crick max-pair model, motif-free targets with at most two isolated stacks are uniquely designable. Lean 4 kernel-checks the theorem.
RNA inverse folding asks for a sequence whose unique optimal fold is a prescribed secondary structure. Real thermodynamics is messy. This paper uses the four-letter combinatorial model of Haleš et al.: only A-U and C-G pairs, no pseudoknots, adjacent bases may pair, and energy is minus the pair count. A sequence is a design when the target is its unique compatible noncrossing structure with the most pairs.
Haleš's proper separated coloring is already a design certificate: local nucleotide ports stay distinct, and gray-pair levels stay apart from unpaired A's. Boury et al. turned levels into a finite-state modulo-m condition and proved that every target whose helices all have length at least 3, and that avoids the local obstructions m5 and m3•, admits a linear-time modulo-2 coloring. An isolated stack of length 2 has no spare internal switch, so that all-long guarantee stops there.
The new step is a global resource-counting induction, not a new local color word. The target is an interval tree. Each maximal helix is a color word over B, W, and G, which prescribe G-C, C-G, and A-U orientations. Under modulo 2, unpaired nodes occupy residue ξ and gray pairs occupy the opposite residue η. The length-2 transfer table is small. In the η→η case, if the loop above also demands a gray head, the only word is GG and the close is gray. Once two child subtrees already contain the two isolated stacks allowed in the target, the incoming helix cannot also have length 2, so it has length at least 3 and can use Boury et al.'s published non-gray-ending words GBB or GWW. The loop exposure then becomes a legal {W,G,B} instead of three grays.
Induction maintains a feasible entry-state set F for subtrees with no isolated stack and a weaker set Q for subtrees that contain at least one. The construction is top-down and deterministic. It produces an explicit sequence, then reuses Haleš's counting-plus-uniqueness argument to show every other compatible fold has fewer pairs.
The full theorem RNA.atMostTwoShortHelixDesignability is formalized in Lean 4. Frozen source rebuilt in an isolated container: 46 files, 20,738 lines, 1,616 declarations including 1,102 theorems, 3,070 Lake jobs in 894.10 seconds. The transitive axiom set is {propext, Classical.choice, Quot.sound}, with no sorry. A blinded Claude Code session compared an anonymous mathematical specification with the Lean sources and reported "faithful and complete." ChatGPT, Codex, and Claude Code were used throughout problem framing, proof work, Lean, and writing. The human author directed the work and takes responsibility.
The theorem is sufficient, not a characterization. Every (m5, m3•)-free target with no isolated base pair, at most two isolated stacks, and all remaining helices of length at least 3 admits a modulo-2 separated coloring and is designable in this model. A three-isolated-stack example can fail to admit a proper modulo-2 coloring, yet the displayed target is still ordinarily separated and designable, so "at most two" is a resource limit of this construction, not a structural boundary of designability.
The algorithmic claim is equally narrow. Boury et al.'s DP already decides modulo-2 separability in linear time for fixed m. This paper does not improve that bound. It guarantees that on the class K≤2 the modulo-2 procedure cannot report nonseparability, and it supplies an explicit top-down witness that does not search the full state table. The coloring itself is linear time when the tree and maximal helices are stored explicitly.
For people watching AI-assisted formal math, this is a public record that takes generative tools to a reproducible formal endpoint: kernel acceptance, isolated rebuild, axiom audit, and a blinded spec comparison, ranked in that order, with multi-model agreement treated as non-evidence. For RNA design it extends Boury et al.'s all-long guarantee by two short helices and yields deterministic sequences that can seed inverse-folding software. It is not a Turner-energy designer, and the paper says so.
The model excludes G-U wobble, pseudoknots, stacking, loop entropy, ions, ensemble objectives, and 3D constraints, and it allows minimum arc length θ=0. Avoiding m3• is biologically tight: a non-root loop with two or more branch helices cannot contain an unpaired base. At release, the manuscript and proof had not received a completed independent human expert review; the blinded audit is also an AI session. Kernel checking does not establish biological realism, novelty, or correctness outside the formal model. A literature search through 19 August 2026 is not a proof of novelty. Which targets with three or more isolated stacks still color is left open.