Metadata
slug: johnson-mondal-tsatsomeros-2026-embeddable-pick-refutation
bibkey: johnson2026powersroots
doi: 10.48550/arXiv.2609.06298
url: https://arxiv.org/abs/2609.06298v1
triage: theorem
motivation_gids:
- D5/S3/Quantum/Matrix/EmbeddablePickRefutation.result
Pick functions do not preserve embeddable matrices
Problem
C. R. Johnson, S. Mondal, and M. J. Tsatsomeros, Powers, Roots, and Positivity, arXiv:2609.06298v1, Table 2, “Behavior of Matrix Classes under Pick Functions and Fractional Powers”, p. 22, row 13 reads verbatim:
Embeddable Matrix | Open | Yes
The note below the table states verbatim:
The entries marked Open indicate cases for which preservation under Pick functions remains an open question.
Remark 3.28, p. 17, states verbatim:
The embedding problem, introduced in [11], asks whether a given stochastic matrix A can be realized as the transition matrix of a continuous-time Markov process. It was shown in [24] that a nonsingular stochastic matrix A is embeddable if and only if A = e^B for some essentially nonnegative matrix B satisfying Be = 0.
Motivation
Row 13 records preservation by fractional powers. Preservation by positive Pick functions would additionally require entrywise nonnegativity of their images of embeddable stochastic matrices.
Gap
A single embeddable stochastic matrix with an image having a negative entry disproves preservation. The restriction to upper-triangular matrices with positive diagonal ensures spectrum inside , as required by Remark 2.9. Refuting this restriction refutes the general preservation statement.
Route
Let
The generator has nonnegative off-diagonal entries and zero row sums. Since and , the exponential series gives
This matrix has nonnegative entries, row sums 1, positive diagonal, and determinant . It is therefore embeddable in the sense of Remark 3.28. Set , , , and , so . This is the finite-measure representation in Lemma 2.8. Its pole is outside , its imaginary part is , and its real values are positive on .
Falsifier
Writing , the explicit inverse is
Exact multiplication verifies . The Pick calculus gives , hence
The inequality follows from the certified rational bounds . Thus is not stochastic and cannot be embeddable.
Evidence
D5/S3/Quantum/Matrix/EmbeddablePickRefutation.lean defines IsStochastic, IsEmbeddable, and claim, and proves result : ¬ claim. The companion frozen module InfinitelyDivisiblePickRefutation provides the reused public definitions pickFun and pickCalc. All witnesses and helper lemmas are private.
The proof checks the power tail, sums the exponential series, uses commutation to identify the generator exponential, and verifies stochasticity, nonsingularity, generator conditions, triangularity, positive diagonal, the explicit inverse, and the negative entry. The matrix exponential is Mathlib’s topology-based NormedSpace.exp. The designated result has only the standard axioms propext, Classical.choice, and Quot.sound; it uses no sorry or additional axiom. Complex analyticity, the spectrum description, and the general analytic representation are mathematical explanations rather than separately formalized assertions here.
Triage
What the settlement shows
-
Proved (Lean) — embeddable preservation fails.
D5/S3/Quantum/Matrix/EmbeddablePickRefutation.resultshows that the embeddable stochastic matrix is mapped by the positive Pick function to a matrix with negative entry. Under the source’s finite-measure calculus identification, row 13 is answered No. -
Reasoning — the shared mechanism. Rows 12 and 13 share the mechanism that Pick functions positive on do not preserve entrywise positivity on non-normal matrices. The row-12 theorem uses a nilpotent shift exponential; the present theorem uses an absorbing Markov generator. The exact inverse gives the sign obstruction in each case. These witnesses give no classification of all smaller matrices or all Pick functions.
-
Open — semipositive matrices. Row 7 is not settled by these results.
ASSUMED-UNVERIFIED
No exhaustive literature or priority claim is established. Lemma 2.8 and Remark 2.9 identify the finite sums with Pick functions and their matrix calculus; the general analytic representation is cited rather than formalized. The settlement concerns arXiv:2609.06298v1, Table 2, row 13.