M10-v1: an explicit candidate at alpha = 5/2
Frozen construction, 20 October 2026. Original: campaign/originals/M10.tex.
This file contains a complete candidate argument; its review status is separate.

1. State and conventions
Let A, B, C have dimensions 4, 8, 2, respectively. Define rho_ABC to be
diagonal with exactly the twelve rational probabilities in witness.json.
All probabilities are nonnegative and their sum is
2/40000 + 6/16 + 2(7499/40000) + 2/8 = 1.
Thus this is a legitimate, entirely classical, finite-dimensional density matrix.
rho_AB is its ordinary partial trace over C, with no conditioning or renormalization.

For any diagonal bipartite state with probabilities p(a,x), the canonical
purification is sum_(a,x) sqrt(p(a,x)) |a,x> |a,x>.
Tracing XX* leaves an operator supported on span{|a,a>}, represented there by
G_aa' = sum_x sqrt(p(a,x) p(a',x)).
The remaining eigenvalues on AA* are zero. This follows by tracing the actual
canonical purification, not by an arbitrary Gram-matrix relaxation.

2. The two reflected density matrices
Put e = 1/4 and d = 1/10000. For x=(b,c), the above Gram matrix is
G = (1/4) [[1,e,0,0],[e,1,e,0],[0,e,1,e],[0,0,e,1]].
For x=b, after summing p(a,b,c) over c BEFORE taking its square root, it is
H = G + (d/4)(E_03+E_30).
Indeed b=1,2,3 supply adjacent edges, b=4,5,6,7 supply the diagonal remainder,
and b=0 contributes separate endpoint diagonals before tracing C but adds an
endpoint off-diagonal entry afterwards. Both matrices have trace one.

3. Explicit spectrum
Let G(d)=(1/4)[[1,e,0,d],[e,1,e,0],[0,e,1,e],[d,0,e,1]].
Reflection of the four coordinates splits 4G(d) into the two blocks
[[1+d,e],[e,1+e]] and [[1-d,e],[e,1-e]].
Set a(d)=(e+d)/2 and b(d)=sqrt((e-d)^2+4e^2)/2.
The four eigenvalues are (1+s*a(d)+t*b(d))/4 for s,t in {+1,-1}.
They are strictly positive for d=0 and d=1/10000.

4. Decisive comparison
Write T(d)=sum_(s,t) [(1+s*a(d)+t*b(d))/4]^(5/2).
The attached checker uses exact rational interval arithmetic: each square root
is enclosed by rationals whose squared endpoints bracket its argument. It
computes every term as lambda^2 sqrt(lambda), with outward rational arithmetic.
It asserts
    14/10^9 < T(0)-T(1/10000) < 15/10^9.
The difference is therefore strictly positive, without relying on floating
point signs. The numerical value is approximately 1.46662006250844e-8.

Because 1/(1-alpha)=-2/3 at alpha=5/2,
    S_R^(5/2)(A:B) - S_R^(5/2)(A:BC)
       = (2/3) log[T(0)/T(1/10000)] > 0.
The checker additionally certifies the lower bound 6/10^8 on this entropy gap,
using log(u/v) >= (u-v)/u for u>v>0. Logs are natural.

5. Exact mapping to the original
The original universally quantifies over all finite-dimensional rho_ABC and
all noninteger alpha>2. The one admissible state above and alpha=5/2 contradict
that universal inequality, provided the attached calculation and definition
mapping survive verification. A theorem for every noninteger exponent is not
required for this negative answer. No assertion about integer exponents is made.

6. Attribution and boundaries
The canonical-purification definition and classical Gram representation are
inherited from the reflected-entropy literature, including Hayden, Lemm and
Sorce, arXiv:2302.10208v2. The construction was motivated by the possible
negative entries of noninteger conventional powers of doubly nonnegative
matrices; compare Guillot, Khare and Rajaratnam, arXiv:1303.4701.
Whether this application is already present in later literature must be
assessed separately. An internally checked certificate is not external review.
