M08-v1: Two optimized full swaps minimize heat in the original qutrit task
Internal candidate, 2026-10-21. No external review or global novelty claim.

Statement. In the exact original M08 model, Q*=Qswap. More strongly, the
same lower bound holds after dropping the gross-positive-work constraint,
allowing arbitrary quantum unitaries and branch-dependent choices of both
gaps. The optimizing swaps have (g1,g2)=(a*,2), where
 a*=1.4459206660687878334052002313168853554336454483620368...,
 Q*=0.4647890802734670691076396477277501767481540451861256... .
The ellipses are display values; the proof defines a* by an exact equation.

1. Definitions and benchmark.
Let p(g)_j=e^(-gj)/(1+e^-g+e^-2g), j=0,1,2, and e(g)=p(g)_1+2p(g)_2.
Define q(a)=a[e(1)-e(a)]+2[e(a)-e(2)]. Its derivative is
 q'(a)=e(1)-e(a)+(2-a)e'(a).
For t=e^-a,
 e'(a)=-t(t^2+4t+1)/(1+t+t^2)^2,
 e''(a)=t(1-t)(1+t)(t^2+7t+1)/(1+t+t^2)^3>0 for a>0.
Thus q''=-2e'+(2-a)e''>0 on[1,2]; q'(1)<0 and q'(2)>0.
There is exactly one root a* in(1,2), and it is the global swap minimizer.
The checker encloses it by sign-certified bisection starting in[1.44,1.46].

Choose the exact multiplier lambda=(lambda0,3,0), where
 lambda0=[e(a*)-e(2)-2e'(2)-3p_1'(2)]/p_0'(2).
It is enclosed near5.6959953529968454487789441915732642, in particular0<lambda0<6.
Put z*=q(a*)-lambda dot p(2).
We prove for every allowed pair of gaps and every quantum protocol
 Q1+Q2-lambda dot diag(rho_final)>=z*.                         (A)
Averaging(A) and using the exact final target gives Qtotal>=q(a*).
Branch-dependent gaps and quantum final coherences are permitted in(A).

2. Quantum-to-population reduction at fixed gaps.
For the second collision set
 f(rho)=min_U Tr[(I tensor H2-Lambda tensor I)U(rho tensor p(g2))U*]
        -Tr(H2 p(g2)), Lambda=diag(lambda).
It is concave as an infimum of affine functions of rho. It is invariant
under target input unitaries, which can be absorbed into U. For any first
collision, rotate its target output so its marginal is diagonal. This
preserves first-machine heat and f. The joint diagonal y equals D x,
x=p(1) tensor p(g1), where D is doubly stochastic (the squared unitary
entries). By Birkhoff's theorem y is a convex combination of permutations
of x. The objective first-machine heat plus f of the row sums is concave
in y; its value is at least the minimum over the permutation vertices.
At such a vertex the second input is diagonal. Rearrangement minimizes its
linear cost by assigning descending input masses to ascending destination
costs g2*j-lambda_i. Therefore the exact quantum support is a finite
minimum over two population permutations. No assumption about a classical
optimal protocol is made before this reduction; work is safely relaxed.

3. Reduction from9! to280 first-stage possibilities.
For a first permutation, partition the nine input masses into three output
rows. The second optimized support depends only on the unordered row sums.
Within each row, descending sorting places masses at machine energies
0,g1,2g1 and minimizes first heat, without changing row sums. Row labels
are immaterial. Hence all supports are attained among unordered partitions
of nine distinct labels into triples, number9!/(3!^3 3!)=280. Each is
generated uniquely by placing the least remaining label in the first triple
and recursing. Coincident numerical masses need no extra case: retaining
all label partitions merely repeats an attainable value.
For a partition let y be its3x3 row-passive table, m its row sums, and let
x2 be the nine products m_i p(g2)_j in descending order. Its support is
 g1 sum_ij j y_ij -g1 e(g1)
 + sum_r x2_sorted[r] c_sorted[r] -g2 e(g2),
where c_ij=g2*j-lambda_i is sorted ascending. The minimum is called F(g1,g2).

4. Uniform semiconcavity, including ordering boundaries.
For any thermal p(g) on{0,1,2}, p'_j=p_j(e-j) and
p''_j=p_j[(e-j)^2-Var(E)]. Thus ||p'||1<=sqrt(Var(E))<=1 and
||p''||1<=2Var(E)<=2. For each fixed pair of permutations write its first
heat as g1 sum_j (A_j-j)p_j(g1), with0<=A_j<=2. Its second g1 derivative
is at most2*2*1+3*2*2=16. The terminal cost has range at most6+lambda0<12,
so its second g1 derivative is at most12. Hence f_11<=28.
For its second-stage g2 dependence write
 g2 sum_j(A_j-j)p_j(g2)-sum_j B_j p_j(g2),
with0<=A_j<=2 and0<=B_j<=lambda0. Its second derivative is at most
4+12+lambda0<22. Hence f_22<=22. First heat has no g2 dependence.
These estimates hold on the whole square[1,3]^2, including outside the
budget triangle. The minimum of concave functions is concave; subtracting
14g1^2 or11g2^2 shows that the finite minimum F preserves the respective
separate semiconcavity bounds. Consequently on a rectangle of widths h1,h2,
 F(g1,g2)-z* >= min_corners(F-z*) -(28h1^2+22h2^2)/8.            (B)
This is bilinear interpolation applied in each coordinate. No smoothness
of the minimum or fixed ordering on the rectangle is required.

5. Global cover and exact remote arithmetic.
cover.json contains a finite dyadic subdivision of[1,3]^2. check.py
reconstructs its binary splits from the root, always splitting the longest
side (first coordinate on a tie). It verifies every leaf and that all
listed leaves are used. Cells with lower-left sum>=4 have no interior in
the allowed triangle; the boundary follows by continuity. There are1006
remote leaves and18 local leaves, all local leaves lying in
 B0=[7/5,3/2]x[39/20,41/20].
For each remote leaf(B) is certified strictly positive. The minimum remote
lower margin is at least2.7066193286321e-6. This proves(A) off B0.

Vertex values are independently recomputed by qutrit_exact.py, using
200-bit Arb enclosures for exponentials, the root and lambda. No floating
search value enters an inequality. Thermal probabilities and lambda0 are
floored to integers at scale S=2^60, with certified error<=1/S per component.
All partition products, sorting, costs, heat and minima are then evaluated
with Python integers and a common exact rational denominator. The value
returned is this integer approximation minus the Arb z* and1000/S.
Here is a conservative error proof. Each thermal vector has L1 error<=3/S,
and its floored vector has mass<=1. The first joint law has L1 error<=6/S;
row sums have no greater error. The second joint law has error<=9/S.
First heat has error<=3*2*(6+3)/S=54/S. Terminal expectation has absolute
cost<=6 and law error<=9/S, plus multiplier error<=1/S, giving<=55/S.
Second bath heat error<=3*2*3/S=18/S. Total error<=127/S. Minima over
permutations and rearrangement are1-Lipschitz in the uniform value error;
therefore1000/S is more than sufficient, independently of ordering ties.
The benchmark and multiplier uncertainty remain in Arb balls. The remote
replay checks all inequalities with directed error enclosure.

6. Exact local proof.
Partition155 is[(0,3,6),(1,4,7),(2,5,8)], with original label3i+j.
Its row sums are p(g1) and its first heat is g1[e(1)-e(g1)]. On B0, the
second input order is[0,3,1,6,4,2,7,5,8] and its destination cost order is
[0,1,3,2,4,6,5,7,8]. The checker verifies all adjacent affine differences
strictly positive using Arb intervals. This assignment is the full swap.
Thus this partition has support
 s(a,b)=a e(1)+(b-a)e(a)-b e(b)-lambda dot p(b).
Its gradient vanishes at(a*,2) by the definitions of a* and lambda0.
Its Hessian entries are
 s_aa=-2e'(a)+(b-a)e''(a), s_ab=e'(a),
 s_bb=-2e'(b)-b e''(b)-lambda0 p_0''(b)-3p_1''(b).
The checker subdivides B0 into20x20 rational rectangles and encloses each
entry directly in Arb. All cells have s_aa>=.652338 and determinant>=.205686,
so the Hessian is positive definite everywhere on the convex box. Thus
s>=s(a*,2)=z* throughout B0. To ensure no other first-stage partition is
smaller, the same semiconcavity argument is applied to the minimum over the
other279 partitions. An adaptive rational subdivision has31 leaves with
strict lower margin>=5.7149762e-6. This completes(A) everywhere.

7. Original feasibility and equality.
The two swaps use g1=a*, g2=2, so1<=g_i<=3 and their sum<4. They send the
initial target first to p(a*) and then exactly to p(2). Each swap is an
allowed U(9), implementable in the specified time and norm budget by its
principal logarithm. Its work is(g_i-1)(e_input-e_output), positive at both
stages. Gross work therefore equals net work,
 q(a*)+e(2)-e(1)=.1890623706570403958169895856414234...<2.
They attain the lower heat bound, proving Q*=Qswap with the original
branchwise work convention. The proof neither claims a coherence advantage
nor substitutes a sampled swap benchmark.

8. Provenance and limits.
The input statement and older quantum support reduction are unchanged.
Taranto et al., arXiv:2404.06649v2, Appendix B.1 prove the qubit result;
this certificate is for the exact three-level/two-collision constrained
problem specified in M08, not arbitrary qutrit schedules or dimensions.
Source comparison supports that distinction; exhaustive novelty is pending.
The checker uses python-flint0.9.0/FLINT3.6.0. It may be run from a clean
copy with those dependencies on PYTHONPATH. It writes only stdout. Internal
review and independent arithmetic reconstruction are not external review.
