slug: das-mori-2026-purification-lower-bound-refutation
bibkey: das2026krylovpurification
doi: 10.1103/qgcx-wxpd
url: https://arxiv.org/abs/2408.00826v4
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Dynamics/PurificationLowerBoundQutritRefutation.result

A full-rank qutrit refutes the purification lower bound on Krylov operator complexity

Problem

R. N. Das and T. Mori, Krylov complexity of purification, Phys. Rev. Lett. 136, 030201 (2026), arXiv:2408.00826v4, compare the Krylov operator complexity C_K(ρ(t)) of a mixed state ρ(t) = U_t ρ U_t† (U_t = e^{−iHt}) with complexities of its purifications.

• The time-dependent purification. |Ψ^{U*}_ρ(t)⟩ = (U_t ⊗ U_t^)|Ψ_ρ⟩ (Eq. (2)), generated by H ⊗ I − I ⊗ H^.
• The complexities. C_S is the spread complexity Σ_n n|ψ_n(t)|² of a state in its Lanczos basis (Eq. (S.4)), and C_K is its operator analogue for the Liouvillian L = [H, ·] with the Hilbert–Schmidt inner product (Eqs. (S.5)–(S.7)).
• The conjecture. “Krylov operator complexity of the mixed state is upper bounded by the operator complexity of the time-independent purification and is lower bounded by the state complexity of the time-dependent purification, C_S(|Ψ^{U*}_ρ(t)⟩) ≤ C_K(ρ(t)) ≤ C_K(|Ψ^I_ρ(t)⟩) (4)”. The authors confirm it analytically for one-qubit states and numerically for Werner states.

The verbatim statements are in the literature note.

Issue #16717 fixes the reading.

• The claim is the left inequality of Eq. (4), for every full-rank density matrix, Hermitian H and t ≥ 0. Full rank is a special case of the source’s statement, so its failure refutes the source’s.
• For full-rank ρ, |Ψ_ρ⟩ is the canonical purification Σ_{ij}(√ρ)_{ij}|i⟩|j⟩.
• The left inequality is refuted.

Motivation

The left inequality would make the purified state’s spread complexity a lower bound on the mixed state’s operator complexity, which the authors use to interpret C_K(ρ(t)) through a pure state. A qutrit for which the purified state spreads further shows that the bound is not a general property of purification, although the source proves it for one-qubit states.

Gap

Issue #16717 records the literature check before any Lean:

• arXiv v1–v4; v4 is the published version and still states Eq. (4) as a conjecture;
• Semantic Scholar lists 6 citing works, whose full texts were scanned, together with Rabinovici–Sánchez-Garrido–Shir–Sonner (arXiv:2507.06286), Caputa–Di Giulio–Loc (arXiv:2606.20790) and the review arXiv:2503.10753; none tests or refutes the left inequality;
• web search returns no settlement;
• the repository had no entry for the paper.

not-found-in-searched-scope.

Route

Take ρ = diag(1, 4, 16)/21, H = [[2, 1, 0], [1, 2, 0], [0, 0, 4]] and t = π/2.

1. The purification. √ρ = diag(1, 2, 4)/√21, so |Ψ_ρ⟩ = (|00⟩ + 2|11⟩ + 4|22⟩)/√21. H has eigenvalues 1, 3, 4, and U = e^{−iHπ/2} = [[0, i, 0], [i, 0, 0], [0, 0, 1]].
2. The two Lanczos chains. Put F = [[0, 1, 0], [−1, 0, 0], [0, 0, 0]], and for A = D = diag(1, 4, 16) or A = S = diag(1, 2, 4) take Q₀ = A/‖A‖, Q₁ = F/√2 and Q₂ = T_A/‖T_A‖ with T_A = L²(A) − β_A A. Then LQ₀ = b₁Q₁, LQ₁ = b₁Q₀ + b₂Q₂ and LQ₂ = b₂Q₁, with (b₁², b₂²) = (6/91, 358/91) for D and (2/21, 82/21) for S. Both chains stop after three vectors. Vectorization maps L to H ⊗ 1 − 1 ⊗ Hᵀ, so the S chain is the chain of the purified state.
3. The values. UAU† = A − L²(A)/2 at t = π/2, so the evolved vector lies on Lanczos indices 0 and 2, with index-0 amplitudes 88/91 for D and 20/21 for S. Hence C_K(ρ(π/2)) = 2[1 − (88/91)²] = 1074/8281 and C_S(|Ψ^{U*}_ρ(π/2)⟩) = 2[1 − (20/21)²] = 82/441, and C_S − C_K = 4192/74529 > 0.

Falsifier

The refutation would not hold if:

• the module’s complexities were not the source’s spread and Krylov operator complexities;
• its purified state or its generator differed from the source’s time-dependent purification;
• the witness were not a full-rank density matrix with a Hermitian Hamiltonian at a time t ≥ 0.

The module defines both complexities as Σ_n n|⟨K_n, e^{−iLt}v̂⟩|² with K_n the Gram–Schmidt orthonormalization of the Krylov sequence of the normalized vector v̂, the operator space vectorized row-major with the Hilbert–Schmidt inner product, L = H ⊗ 1 − 1 ⊗ Hᵀ, and the purified state the vectorization of √ρ. The witness is positive definite with trace 1, H is real symmetric, and t = π/2.

Evidence

The canonical source is D5/S3/Quantum/Dynamics/PurificationLowerBoundQutritRefutation.lean (521 lines).

• It defines krylovVector, spreadComplexity, liouvillianMatrix, liouvillian, canonicalKet, operatorComplexity, purificationComplexity and claim, and proves result : ¬ claim with the witness above.
• It uses the frozen CartesianVariance.vectorize (the vectorization in both complexities), CartesianVariance.matrix_pairing, CartesianVariance.vectorize_norm_sq, partialTraceRight, trace_partialTraceRight, rankOneDensity, diagonalState, ptrace2_pure and RHLinalg.frobSq (through D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings), with pinned Mathlib Gram–Schmidt (InnerProductSpace.gramSchmidtNormed), the operator exponential (NormedSpace.exp) and Module.End.HasEigenvector.pow_apply.
• It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.
• result is the refutation result of a refutes utility, which CLAUDE.md §3.9 exempts from four-slot registration.

Frozen state: Golden/Frozen/state/D5/S3/Quantum/Dynamics/PurificationLowerBoundQutritRefutation.lean.json, statement sha256:2d1b7538dd9b04e296c47e8bbdb9bbbf44ba67fcee987a2032417f543efe1b79.

Declaration statements:

• result: sha256:c578bff105e79140e09ce8f72f992e887faf0b1600b2857b55114b5f9d72826b;
• claim: sha256:bcdb8e43d7d07a81977b19918e7c8ca225d0cfca1975db55e36c2cdd04816dea.

Triage

Tier 1 conjecture of a 2026 paper, preregistered in issue #16717 before any Lean. counterexample; resolution refuted.

Every other declaration is a definition used by a public statement or a compiler-generated proof on the proof path of result. The bind-only form is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; no escape witness is claimed. The utility is certified-instance with basis refutes the module’s claim. There is no digestion atom.

What the settlement shows

Proved by result: the left inequality of Eq. (4) fails: for ρ = diag(1, 4, 16)/21, H = [[2, 1, 0], [1, 2, 0], [0, 0, 4]] and t = π/2, C_S(|Ψ^{U*}_ρ(t)⟩) = 82/441 > 1074/8281 = C_K(ρ(t)).

Computed, not formalized (orchestrator, NumPy/SciPy, a generic Lanczos implementation with full reorthogonalization, 14 October 2026):

• for this witness C_S > C_K at all 600 sampled times in (0, 6], so the violation is not isolated in time;
• 5 of 300 random qutrit triples (ρ, H, t) violate the inequality, so it is not isolated in state space;
• control: over 500 random qubit states, Hamiltonians and times, max(C_S − C_K) = −8.8 × 10⁻⁶, reproducing the source’s proved qubit case.

Argued, not formalized.

• The mechanism of this witness: both Krylov chains have length three and the evolution at t = π/2 moves weight only between Lanczos indices 0 and 2, so each complexity is 2(1 − c²), with c the index-0 amplitude. The purified state starts from √ρ, whose spectrum diag(1, 2, 4) is less spread than ρ’s diag(1, 4, 16); its index-0 amplitude 20/21 is smaller than ρ’s 88/91, so its spread complexity is larger. The values are formalized; the reading of them as a spectral-spread effect is not.

Open.

• Whether the right inequality of Eq. (4), C_K(ρ(t)) ≤ C_K(|Ψ^I_ρ(t)⟩), holds in general; this settlement does not address it.
• The authors’ conjectures 2 and 3: the approximately constant ratio C_S(|Ψ^{U*}_ρ(t)⟩)/C_K(ρ(t)), and C_K(|Ψ^{U*,I}_ρ(t)⟩) ≥ 2C_S(|Ψ^{U*,I}_ρ(t)⟩) for the same purification scheme, where C_K is the operator complexity of the purified state, not of ρ(t).
• A characterization of the states and Hamiltonians for which the left inequality holds.

Effect on the paper. The lower bound of Eq. (4) is not a general property of purification; it holds for one-qubit states (as the source proves) but fails already for a full-rank qutrit. The Werner-state evidence of the source concerns a family for which the inequality happens to hold.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty or priority. The statements in “Computed, not formalized” and “Argued, not formalized” are not formalized.