Fill's segment conjecture for biased adjacent-transposition chains: a proof at n=3, its sharp form, and a counterexample at n=4

The n = 3 spectrum, derived in the kernel: 4(K²-K) squares to (D-1) times itself, so every eigenvalue lies in 0, 1, (1 +/- sqrt D)/2 with D = p₁2 p₂3 p₃1 + p₃2 p₂1 p₁3; an explicit eigenvector (entries polynomial in p and sqrt D, last coordinate 2 p₁2 p₂3 p₁3) realises (1 + sqrt D)/2; hence IsGreatest over the eigenvalues below 1, i.e. the spectral gap is (1 - sqrt D)/2

The segment reduction at n = 3: with A = p₁2 - 1/2, B = p₂3 - 1/2, C = p₁3 - 1/2 and M = (A+B)C - AB, D along p(t) = (1-t)p + t p_* is exactly 1/4 - (1-t)² M; equivalently the convexity discriminant D'(t)² - 2 D(t) D"(t) is identically M

Fill's stronger conjecture (d) holds at n = 3: for every regular parameter vector and every t in [0,1], the stated function IS the spectral gap of K(t) (an IsGreatest over the eigenvalues below 1), and it is nonincreasing (AntitoneOn) and convex (ConvexOn) on [0,1]

Sharpness at n = 3: for an arbitrary parameter vector the conclusion of (d) holds iff M >= 0 – M < 0 makes the gap STRICTLY INCREASING on [0,1] and strictly concave (its midpoint value strictly exceeds the chord) – and regularity implies M = A(C-B) + BC >= 0; since 1/4 - M = D(0) and D(1) = 1/4, M >= 0 is equivalent to the Gap-Problem inequality lambda_(K(0)) >= lambda_(K(1)) at that vector

The equality set at n = 3: for a regular vector the gap is constant along the segment iff M = 0 iff p₁2 = p₂3 = 1/2, i.e. iff label 2 is neutral in the sense of Jain-Mizgerd; otherwise M > 0 and the gap is strictly decreasing and strictly convex

The uniform endpoint is essential: (3/4,3/4,3/4) and (1/2,1/2,7/8) are both regular, D = 3/16 at the first and at the midpoint (5/8,5/8,13/16) of the segment joining them while D = 1/4 at the second, so the gap at that midpoint strictly exceeds the average of the endpoint values – the spectral gap is NOT a convex function on the regular polytope, only along segments aimed at p_*

Fill's stronger conjecture (d) is FALSE at n = 4: its convexity half fails for the regular vector p₁2 = p₁3 = p₂3 = 1/2, p₁4 = p₂4 = p₃4 = 99/100, where beta(0) >= 8355691/10⁷ and beta(9/100) >= 8456041/10⁷ (exact Rayleigh witnesses) while beta(9/200) <= 8405689/10⁷ (exact LDL^T PSD certificate), so lambda(9/200) - (lambda(0) + lambda(9/100))/2 >= 177/10⁷ > 0

Controls tying the Lean object to the source's object: K3 as a matrix agrees with its operator form, every row sums to 1, and K is self-adjoint for the inner product weighted by the source's stationary distribution wₓ = prod_(r<s) p_(xᵣ,xₛ)

Search output: the monotonicity half of (d) survived every search (400 random regular vectors at n = 4, 120 at n = 5, plus adversarial optimisation; minimum forward difference always positive), while the convexity half fails at n = 4 only near the degenerate boundary (in the family pᵢ₄ = q, pᵢj = 1/2 otherwise, the threshold is q* about 0.963, and 400 regular vectors with all pᵢj <= 0.95 gave no violation at all) but at n = 5 already for q about 0.80 in the same family, with margins ten to twenty times larger

Fill's stronger conjecture (d) is FALSE at n = 4 in the kernel: for the regular vector p₁2 = p₁3 = p₂3 = 1/2, p₁4 = p₂4 = p₃4 = 199/200 and the equally spaced segment points t = 0, 5/99, 10/99, the spectral gap satisfies gap(5/99) - (gap(0) + gap(10/99))/2 in [1/80000, 63/2000000], strictly positive; and at the founding journal's own witness pᵢ4 = 99/100, t = 0, 9/200, 9/100 the same quantity is >= 177/10⁷ – so the convexity half of (d) fails, with no sorry and no native_decide

The complete spectrum of Fill's n = 4 chain on the regular family pᵢj = 1/2 (i < j <= 3), pᵢ4 = q, generically in q: the S₃ relabelling symmetry splits R²4 into K-invariant blocks of dimensions 4 + 4 + 8 + 8 (the two 8-blocks carrying the SAME matrix), and every eigenvalue is a root of (mu-1)(mu-2/3)((mu-2/3)² - 2r/9), of mu(mu-1/3)((mu-1/3)² - 2r/9), or of Pquart r ((6 mu - 3)²) where Pquart r w = w⁴ - (6+16r) w³ + (9+60r+64r²) w² - (4+32r+160r²) w + 192 r³ and r = q(1-q); conversely every root w of Pquart is realised, the eigenvalue being 1/2 + sqrt(w)/6 with an explicit eigenvector whose entries are polynomials in mu and q

Controls tying the Lean n = 4 object to the source's chain: the 24-permutation table and the adjacent-transposition neighbour table are decide-checked to be 24 distinct bijections and genuine adjacent transpositions, the operator is proved equal to the source's own rule Kₓy = p_(xᵣ, xᵣ₋₁)/(n-1) with the diagonal taking up the rest, every row sums to 1, and K is reversible and stationary for the source's own piₓ = prod_(r<s) p_(xᵣ,xₛ)

Negative and non-vacuity controls at n = 4: the midpoint upper bound cannot be lowered to 8401/10⁴ (an eigenvalue lies above it), the convexity violation is bracketed between 1/80000 and 63/2000000 so it is genuinely of order 10⁻5, the MONOTONICITY half of (d) is untouched (the gap is still strictly decreasing at the three points), and beta4 is the genuine least upper bound (the eigenvalue set below 1 is nonempty at each of the three points)