The OBDD split exponent sₛtar(n) of a restricted integer multiplication: exact values, optimal variable orderings, and the failure of the obvious closed form

s_*(n) = 1, 1, 1, 2, 2, 2, 3, 3, 3, 3, 3 for n = 2,..., 12 – the first eleven values of the OBDD split exponent that arXiv:2608.30664 introduces and never evaluates

s_*(n) = 4, 4, 4, 4, 5, 5, 5, 5, 5, 6 for n = 13,..., 22; in particular s_* first reaches 5 at n = 17 and 6 at n = 22

an explicit optimal x-variable ordering pi_wopt for each n = 2,..., 12, certified optimal (its ordVal equals s_*(n))

an explicit optimal x-variable ordering pi_wopt for each n = 13,..., 22, certified optimal

the bounds n/8 <= s_*(n) <= n/2 of arXiv:2608.30664 Lemma lem.snbound hold at every n from 2 to 22, and the upper bound is strict (2 s_*(n) < n) for every n from 3 to 22

negative controls: s_*(20) is neither >= 6 nor <= 4; the level certificate evaluates to false at the false threshold K = 6; blocked is vacuously true at the top of the lattice, so the hypothesis m + d < n is load-bearing; ordVal of the empty list is 0, so the permutation hypothesis is load-bearing; and the natural ordering x₀ <... < xₙ₋₁ attains exactly the source's upper bound n/2 at n = 16 and n = 20, twice s_*

s_*(n) = floor(sqrt(2n)) - 1 for every n from 2 to 16, and this closed form is FALSE at n = 17 (where s_* = 5 and the formula gives 4); s_*(n) is not ceil(n/4) either (it fails at n = 8)

the lattice reduction and its certificate: a partition w.r.t. an ordering pi is a prefix of pi, so s_*(n) is a minimum-bottleneck maximal chain in the Boolean lattice (2ⁿ sets, not n! orderings), and a level-m depth-d blocking certificate with m + d < n refutes every ordering at once; the reduction and the certificate soundness are proved kernel-clean (no native_decide)

s_*(n) = 6, 6, 6, 7, 7, 7, 7, 7, 8 for n = 23,..., 31, from the external C search (not kernel-bound); in particular s_* first reaches 8 at n = 31

|Split(L,R;a,b)| equals the number of residue classes mod h = b-a inside 0,...,b that meet both L and R; and that count is monotone in b, so the inner double maximum of eqn.Ssmul is attained at b = n-1 and s_* needs only n-1 of the C(n,2) pairs (a,b)

a self-contained counting lower bound: if every residue-class split count of a partition with |L| = m is at most K then m(n-m) <= sumₕ₌₁ⁿ⁻¹ min(n-h, K(ceil(n/h)-1)); hence s_*(n) = Omega(n / log n), and in particular s_*(239) >= 21 > 20 = floor(sqrt(2*239)) - 1

the eight first-occurrence thresholds T(K) = minn: s_*(n) = K are 2, 5, 8, 13, 17, 22, 26, 31, and T(K) = ceil((9K-11)/2) exactly for 3 <= K <= 8; equivalently s_*(n) = floor((2n+11)/9) for every n from 2 to 31 with the single exception n = 4 – a LINEAR law s_* 2n/9, strictly inside the source's own range [n/8, n/2]. Proved here on the kernel-bound range 2 <= n <= 22 (n!= 4), with n = 23..31 measured

the compiled mirror LeanProblemSpec/ObddSplit/Core.lean (imports nothing, built into libObddCore.so) and its kernel-clean equivalence to Defs/Lower – core_gFast, core_blocked, coreₗevelCert, certₛound_core, sStarₑqₒfCore – so that a –load-dynlib native_decide certifies the very levelCert that certₛound consumes

s_*(23) = s_*(24) = s_*(25) = 6 and s_*(26) = 7, kernel-bound – the table of the paper's own (eqn.Ssmul) extended from n <= 22 to n <= 26

an explicit optimal x-variable ordering pi_wopt for each of n = 23, 24, 25, 26, certified optimal (ordVal n l = s_*(n))

negative controls and cross-checks for the extended range: the compiled certificate is false at the false threshold at both n = 25 (K = 7) and n = 26 (K = 8); s_*(25) is neither >= 7 nor <= 5; the compiled and interpreted routes agree at n = 22; the natural ordering attains 24/2 = 12 at n = 24; s_* is non-decreasing on 22 <= n <= 26; the source's n/8 <= s_* <= n/2 holds at every n <= 26; and the closed form floor(sqrt(2n)) - 1, refuted at n = 17, is right again at n = 25

the whole kernel-bound table in closed form, s_*(n) = 1 if n = 4 and floor((2n+11)/9) otherwise, for 2 <= n <= 26 – the linear law of row OS12, kernel-bound four values further

s_*(32) = s_*(33) = s_*(34) = 8 and s_*(35) = s_*(36) = 9, from the external C search (not kernel-bound); hence T(9) = 35, exactly the value the linear law of row OS12 predicted before it was computed. The law now agrees at 34 of the 35 values 2 <= n <= 36 (only n = 4 fails) and gives eight of the nine thresholds T(1..9) = 2, 5, 8, 13, 17, 22, 26, 31, 35

the source's size-vs-width constants: its Corollary 2.3 assumes constants c₁, c₂ > 0, its Theorem 3.3 supplies c₁ = 1 but its Theorem 3.5 supplies 8n, and substituting that into the corollary's own conclusion gives |B(SMulⁿₙ₋₁)| <= 8n² 2^(s_*(n)) rather than the n 2^(s_*(n)) its introduction displays; by the same substitution the two theorems give 2^(s_*) <= Width <= 8n 2^(s_*), where a Theta(2^(s_*)) statement needs the upper factor to be independent of n

the first seven first-occurrence thresholds T(K) = minn >= 2: s_*(n) = K are 2, 5, 8, 13, 17, 22, 26 for K = 1,..., 7, kernel-bound – each as s_*(T(K)) = K together with s_*(n) < K for every 2 <= n < T(K)