Metadata

slug: hwang-kim-2024-near-order-log-euclidean-wasserstein
bibkey: hwangkim2024nearorder
doi: 10.1007/s11117-024-01099-4
url: https://arxiv.org/abs/2407.07438v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Matrix/HwangKimNearOrderRefutation.result

Hwang–Kim: log-Euclidean to Wasserstein near order

Problem

Jinmi Hwang and Sejong Kim, Near-order relation of power means, arXiv:2407.07438v1, page 17, final unnumbered question of §6:

It would be an interesting problem to study whether the weak log-majorization relation generalizes to the near-order or entrywise eigenvalue relation. Note that (6.21) is a generalization of (4.14). From this point of view, we give an open question:

$LE (ω; A) ⪯ Ω (ω; A) .$

The question quantifies over every dimension $m \geq 1$ , every input count $n \geq 2$ , positive definite complex matrices $A_{j}$ , and weights $w_{j} > 0$ with $\sum_{j} w_{j} = 1$ . Equation (6.21) is a different, proved comparison; the question itself has no equation number.

Statement echo

Source clause	Lean counterpart	Fidelity
Positive definite matrices in $P_{m}$	`claim`, `Matrix (Fin m) (Fin m) ℂ`, `Matrix.PosDef`	All complex inputs; real witnesses are a specialization.
Positive probability weights	`claim`, positivity of every weight and its finite sum equal to one	No weight is omitted.
$A ⪯ B ⟺ I \leq A^{- 1} # B$	`NearOrder`, existing `PsiMeanTraceConcavity.geometricMean` at weight $1/2$	Source equation (3.5), with the same operand order.
$LE = exp (\sum_{j} w_{j} lo g A_{j})$	`logEuclidean`	Literal functional-calculus expression, source equation (4.10).
Bures–Wasserstein distance	`buresWassersteinDistance`	Literal square-root trace expression from §2; real parts read the real traces.
$Ω = ar g min_{X > 0} \sum_{j} w_{j} d_{W} (X, A_{j})^{2}$	`wassersteinBarycenter`	`Classical.epsilon` selects the actual positive definite minimizer predicate, including comparison with every positive definite matrix.
Universal final comparison	`claim`	Every dimension, input count, input and positive probability vector is retained.
Failure of the universal comparison	`result`	Exactly the negation of `claim`.

The multivariable argmin definition is Bhatia–Jain–Lim, arXiv:1803.03357, page 1, equation (2); see the source note and barycenter note. The existing geometric-mean owner is reused directly. The multivariable means retain the source expressions. Definitions outside admissible positive definite inputs have no bearing on the quantified claim.

Motivation

The source asks whether its weak log-majorization comparison strengthens to near order. Preregistration #21282 identifies that exact question and its literal conventions. The settlement is Refuted, by D5.S3.Quantum.Matrix.HwangKimNearOrderRefutation.result.

Gap

Weak log-majorization does not supply positivity of $L^{- 1} # W - I$ . Noncommuting eigenspaces allow the necessary determinant condition for that positivity to fail even with two strictly positive inputs.

Route

Use equal weights and

$A = (4001), B = \frac{1}{64} (19 - 315 - 315 61), K = \frac{1}{8 265} (35 - 315 - 315 125) .$

The private theorems witnessA_pos, witnessB_pos, witnessK_pos and witnessK_riccati verify strict positivity and $K A K = B$ . wasserstein_witness identifies the actual least-squares selector with $W = (I + K) A (I + K) /4$ ; its proof uses the trace-norm variational inequality and its equality condition to establish the minimizing matrix uniquely. logEuclidean_witness identifies the actual logarithmic expression with the explicit spectral matrix $L$ .

Write $d = 5/8 + 10/ 265$ . The private theorems witnessL_det, witnessW_det, and nearOrder_riccati give $det L = 1$ , $det W = d^{2}$ , and a positive definite $C = L^{- 1} # W$ satisfying $C L C = W$ . The determinant equation and positivity give $det C = d$ . If $I \leq C$ , then $det (C - I) = 1 + d - tr C \geq 0$ . Cayley–Hamilton trace identities yield

$tr W + d tr L = tr (L C) tr C, tr (L W) + 2 d = tr (L C)^{2} .$

Thus near order forces

$T = (tr W + d tr L)^{2} - (1 + d)^{2} (tr (L W) + 2 d) \leq 0.$

witness_trace_test proves $T > 3/2500$ by rational intervals for $2$ and $265$ , and trace_obstruction gives the contradiction. These names refer to private declarations in the settling module.

Falsifier

The universal claim implies near order for the displayed pair and equal weights. The kernel-checked result derives a contradiction at exactly those inputs. An incorrect argmin identification or an incorrect positive trace certificate would invalidate that route; both are proved inside the module rather than assumed as hypotheses of the public claim.

Evidence

The formal source is HwangKimNearOrderRefutation.lean. Its only public theorem is result; the axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Exact external checker

Experiment directory at commit 0633f84b7cbcfd429c7fb70d140978a010582b1c. The checked file is check.py, SHA-256 2d4d6daa173673ea7668a6fdec975ac704d56b763e14c456fdcd927c7f714eee. Command: python3 /tmp/op-hk2407/continuation/check.py, using the exact bytes obtained from that commit; Python 3.14.8, SymPy 1.14.0; exit 0, ALL_CHECKS_OK. The checker verifies the explicit real symmetric matrices, strict positivity, noncommutation, Riccati and logarithmic identities, rational root brackets, and $3/2500 < T < 121/100000$ . It also verifies symbolic second-order rotation-family identities, including the whole second-order Riccati equation. These symbolic identities and finite integer cross-checks do not constitute a Lean proof of a uniform analytic family.

Triage

What the settlement shows

Item	Status and evidence kind	Exact scope
Near order fails for two strictly positive $2 \times 2$ matrices at equal weights.	Proved, kernel-checked: `result`, with `witnessA_pos`, `witnessB_pos`, `logEuclidean_witness` and `wasserstein_witness`.	Literal source conventions in `claim`; this is a refutation of the universal assertion.
The explicit inputs are real symmetric and noncommuting.	Computed: the exact external checker in Evidence, exit 0 and the recorded SHA-256.	The displayed pair only; noncommutation is not a separately delivered Lean theorem.
Near order forces $tr C \leq 1 + det C$ , contradicted by the positive $T$ certificate.	Proved, kernel-checked: `trace_obstruction` and `witness_trace_test`, used by `result`.	Positive $2 \times 2$ matrices with the stated determinant and Riccati hypotheses; Cayley–Hamilton trace identities and PSD determinant nonnegativity.
$3/2500 < T < 121/100000$ and the rotation-family jet identities.	Computed: the exact external checker in Evidence, exit 0 and the recorded SHA-256.	The two-sided bound is for this explicit witness. The family calculation verifies symbolic second-order identities and the stated finite coefficient cross-checks, not a universal analytic Lean theorem.
Lean formalization of the all- $r$ small-rotation family, common scaling, unitary and direct-sum extensions, and the commuting-case reduction.	Open: no such theorem is delivered.	These are follow-up formalization targets, independent of the already refuted universal claim.
The separate entrywise-eigenvalue question.	Open: `result` states no entrywise-eigenvalue comparison.	Weak log-majorization is not refuted; the source’s comparison survives.

The obstruction concerns positivity of a relative geometric mean minus the identity; the eigenvalue-product comparison does not impose that positivity. At a commuting boundary, one eigenvalue of this difference is zero, and rotation can destroy its semidefiniteness. The symbolic family calculation explains this mechanism without enlarging the kernel-checked scope.

For the scalar commuting reduction, the surviving comparison follows in prose from weighted AM–GM on the square roots: $\prod_{j} a_{j}^{w_{j}} \leq (\sum_{j} w_{j} a_{j})^{2}$ . Simultaneous diagonalization applies this coordinatewise. This explanation is not an additional Lean theorem; the formalization remains open as listed. The refutation invalidates the proposed strengthening, not any proved theorem in the source; no source theorem is asserted here to depend on the open question.

Literature status

The definitions and standard comparison results are literature-attested. The exact witness and rotation coefficient have status suspected-novel within the read scope recorded on #21282. That screen includes Gan–Huang arXiv:2312.15394v2 and Hiai arXiv:2508.20309v2; their comparison statements do not settle this exact question. The journal body and four citing bodies were unread in that screen. Completeness is ASSUMED-UNVERIFIED, with no unconditional priority claim.

ASSUMED-UNVERIFIED

Agreement of the final question between arXiv:2407.07438v1 and the journal body.
Completeness of the literature screen, including unread citing works with DOIs 10.1007/s43037-025-00424-7, 10.1080/03081087.2025.2564162, 10.1016/j.jmaa.2025.130187 and 10.1007/s00025-025-02491-6.
Priority beyond the sources actually read; the formal proof certifies the mathematical refutation independently of that bibliographic boundary.

Keyboard shortcuts

trureturing — Discovering truth