Semiprime Interleaving: A Combinatorial Encoding of Prime Ratio Record Minima

A Lean 4 formalization of a combinatorial statistic that encodes prime ratio record minima through the merge behavior of anchored semiprime sets. The interleaving statistic L(n) measures how two consecutive "anchored semiprime sets" merge when sorted. The main result (Keystone Lemma) establishes: L(n) = n if and only if the prime ratio r_n = p_{n+1}/p_n is a strict record minimum. As a corollary, every twin prime index achieves L(n) = n, since twin gaps minimize the normalized ratio. The converse holds under an explicit density hypothesis, which is proven to be logically equivalent to the desired implication (not independent of it). Scope and limitations: This framework does not constitute progress toward the twin prime conjecture. It provides a combinatorial lens for viewing known ratio inequalities, not new arithmetic content. The primary contributions are: (1) a clean encoding with pedagogical value, and (2) a complete formal verification in Lean 4 (~2300 lines, no sorry).