The admissible dimensions of the Chan–Wei refutation: certifying Θ_N>0, monotonicity between resonances, and the block structure of the admissible set

For every n with 12 <= n < 150, n is admissible in the sense of arXiv:2608.10501v1 equation (1.5) if and only if n is one of 26, 27, 49, 50, 51, 80, 81, 82, 83, 120, 121, 122, 123 – the list the source prints verbatim – certified by exact rational enclosure of Theta_N built from the Gauss series of the digamma; with the two-sided numeric control 357/10000 < Theta(80) < 368/10000 (width 1.1e-3 around the smallest positive value in the range)

The admissible set for 12 <= n <= 400 is the source's printed list together with the four further blocks 167-171, 223-227, 286-291, 358-363; and [150, 166] is certified to contain no admissible dimension

Theta is STRICTLY INCREASING in ell on every interval (2m-2, 2m) between consecutive resonances – proved without derivatives, by termwise domination of the difference quotient Theta(L2) - Theta(L1) = d * sum_(k>=1) [1/((2k-L2)(2k-L1)) - 1/((2k-1+L2)(2k-1+L1))] after reindexing, each bracket positive because |2k - L| < 2k - 1 + L for L > 1/2, k >= 1 – hence in every window ((2m-3)²+2, (2m-1)²+2] the admissible dimensions form a SUFFIX, a block ending at the resonant dimension, and two sign evaluations settle a whole window

The admissible set for 12 <= n <= 14163 = 119² + 2, as 58 blocks settled by 116 sign certificates (exactly 940 admissible dimensions, 6.6 % of the range); the block lengths for m = 3..60 are 2,3,4,4,5,5,6,6,7,7,8,8,9,9,10,10,11,11,12,12,13,13,13,14,14,15,15,16,16,17,17,18,18,18,19,19,20,20,21,21,22,22,22,23,23,24,24,25,25,25,26,26,27,27,28,28,28,29; and the block-length law ceil((m+2)/2), which fits every window with 4 <= m <= 24, is FALSE – it fails first at m = 25, where the window (2211, 2403] has admissible set 2391,...,2403 of size 13 and not 14, and it is wrong at 31 of the 57 windows 4 <= m <= 60, including every m >= 36

The Gauss series psiG x = sum_(k>=0) (1/(k+1) - 1/(k+x)) = psi(x) + gamma_E, which is what defines sigmaₙu here, satisfies psiG 1 = 0 (i.e. psi(1) = -gamma_E), the digamma recurrence psiG (x+1) = psiG x + 1/x for EVERY real x (no hypothesis, under Lean's 1/0 = 0), and psiG (m+1) = Hₘ for every natural m

Cost and API measurements for this problem: Mathlib v4.32 DOES carry Complex.digamma:= logDeriv Gamma but with a five-lemma API and no series, reflection, duplication or numeric content, so the Gauss series is the route; once sigma_(-1/2) is evaluated from the same series rather than from its closed form pi/2 + 2 log 2, Theta_N contains NO transcendental constant at all (gamma_E, log 2 and pi all cancel) and reduces to -4 + 1/(1+ell) + sum_(k>=1) (2 ell + 1)² / ((4k+1)(2k-ell)(2k+1+ell)), whose terms are O(k⁻3); K = 120 series terms with 10⁻15 rational sqrt bounds decide every n <= 400 with enclosure width <= 4.4e-3, and K = 2000 decides the 116 block boundaries to n = 14163 with worst sign separation 1.9e-3 against a 4.8e-4 tail bound; the whole family builds in 58 s wall and 3.4 GB peak RSS with targeted imports (3.3 GB baseline, against 6.5 GB for import Mathlib)