slug: zhang-jing-2025-block-normality-question-2-14
bibkey: zhangjing2025positive
doi: 10.13001/ela.2025.9201
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Matrix/ZhangJingBlockNormalityRefutation.result
url: https://doi.org/10.13001/ela.2025.9201

Zhang–Jing Question 2.14: block positivity and normality

Problem

Feng Zhang and Hefang Jing, More inequalities for positive semidefinite matrices, Electronic Journal of Linear Algebra 41 (2025), 595–601, Question 2.14, p. 601:

Let A ∈ M_n. Then [[f(|A|), A*], [A, g(|A|)]] ≥ 0 if and only if A is normal under the conditions that f(x)g(x) = x² for x ≥ 0, f(x) ≥ g(x) (x ≥ 1) and g(x) ≥ f(x) (0 ≤ x ≤ 1).

The notation on p. 595 is “|A| = (AA)^{1/2} and A is the conjugate transpose of A”. The assertion quantifies over every admissible pair of real functions, every natural dimension, and every complex matrix in that dimension. Preregistration: #18699.

Statement echo

No continuity, invertibility or spectral injectivity premise is added. The counterexample functions are continuous and satisfy the three required scalar conditions.

Motivation

The settling declaration is D5/S3/Quantum/Matrix/ZhangJingBlockNormalityRefutation.result. It refutes the universal equivalence using one fixed two-dimensional matrix. Its admission basis is open-problem-resolution (#18699; Refuted).

Gap

The scalar conditions permit two distinct positive singular values to have the same value under $g$. Commuting with $g(|A|)$ consequently need not force commuting with $|A|$.

Route

Set $g(x)=1+(x-1)/(1+(x-1{)}^2)$ and $f(x)=x^2/g(x)$. Take $A=\left(\begin{array}{cc}0& 3/2\\ 3& 0\end{array}\right)$. The proof verifies all three scalar conditions, obtains $|A|=\mathrm{diag}(3,3/2)$ using CFC.sqrt_unique, and applies the frozen EntropyProductionCoherenceDeletionIdentity.cfc_diagonal to evaluate both functional calculi. It verifies the block identity $M=(5/7)Q^{\ast }Q$, where $Q=[A,(7/5)I]$, and applies Matrix.posSemidef_conjTranspose_mul_self. The unequal $(0,0)$ entries of $A^{\ast }A$ and $A{A}^{\ast }$ contradict normality.

Falsifier

The refutation would fail if the scalar premises, square-root identification or Gram identity failed. They are checked inside result; the theorem has no additional hypotheses. No family-level or injectivity classification is claimed as a Lean theorem.

Evidence

The Lean module and its Blueprint mirror give the fixed-instance refutation. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Experiment: zhang-jing-2025-question-2-14 at 3324a54f7ffe4ef83526feecd6983cc5b30cda06. Command: python3 check.py in that directory; exit 0. Script SHA-256: 0f3353dca9ba3cf9f1f1fe34d524ea1e07756e3dae7ad117701ac124f7f8cb4d.

The computation checks admissibility on a grid in $[0,20]$; exactly verifies $|A|=\mathrm{diag}(3,3/2)$, nonnormality, $g(3)=g(3/2)=7/5$ and $cM=Q^{\mathsf{T}}Q$ at $s=2$; numerically checks block positivity and nonnormality for $s\in \{1.5,2,3,5,10,100\}$; and obtains minimum eigenvalue $-0.387192$ for the contrast $f(x)=x^{3/2}$, $g(x)=x^{1/2}$ at $s=2$. The finite grid and six numerical matrices do not prove uniform claims.

Triage

What the settlement shows

Prose derivations and surviving statements

For $t=x-1$, $(t\mp 1{)}^2\ge 0$ gives $|t|/(1+t^2)\le 1/2$, hence $1/2\le g(x)\le 3/2$. Also $g(x)-x=(1-x)(x-1{)}^2/(1+(x-1{)}^2)$. Thus $0<g(x)\le x$ for $x\ge 1$ and $g(x)\ge x\ge 0$ for $0\le x\le 1$. Dividing the corresponding square inequalities by positive $g(x)$ proves the two required inequalities for $f=x^2/g$; the product condition follows immediately.

For $s>1$, put $a=1+s$, $b=1+1/s$, $A_s=\left(\begin{array}{cc}0& b\\ a& 0\end{array}\right)$, $D=\mathrm{diag}(a,b)$ and $c=1+s/(1+s^2)>0$. Then $a>b>1$, $|A_s|=D$, $g(a)=g(b)=c$, and $f(D)=D^2/c$. The block row $Q=[A_s,cI]$ satisfies $Q^{\ast }Q=cM$, so $M\ge 0$. Yet $A_s^{\ast }{A}_s=\mathrm{diag}(a^2,b^2)\ne \mathrm{diag}(b^2,a^2)=A_s{A}_s^{\ast }$. For higher dimensions append identity scalar blocks to $A_s$: $f(1)=g(1)=1$, the extra source blocks are positive semidefinite, and a simultaneous index permutation presents their direct sum with $M$. The unequal entries persist.

For invertible $A=UD$ with positive $D=|A|$ and unitary $U$, assume $f,g>0$ on the spectrum and $fg=x^2$. Write $F=f(D)$ and $G=g(D)$. Since $D{F}^{-1}D=G$, the Schur complement says $M\ge 0$ iff $G-UG{U}^{\ast }\ge 0$. Its trace is zero; a positive semidefinite matrix of trace zero is zero. Therefore $M\ge 0$ iff $UG=GU$. If $g$ is injective on the finite spectrum of $D$, polynomial interpolation expresses $D$ as a polynomial in $G$, so $UG=GU$ implies $UD=DU$, equivalently normality. Conversely, normality gives commutation and a zero Schur complement. A collision $g(a)=g(b)$ at distinct positive $a,b$ permits a swapping unitary on those two eigenspaces and disproves the universal equivalence. This is a prose argument, not a Lean classification theorem.

For $f(x)=x^{2a}$ and $g(x)=x^{2(1-a)}$, $1/2\le a<1$ makes $g$ strictly increasing on $(0,\infty )$, so the invertible repair applies. At $a=1$, $g=1$ and $f=x^2$; the block is $[A,I{]}^{\ast }[A,I]$ for every $A$, so any nonnormal $A$ refutes the endpoint. For normal matrices, simultaneous diagonalization reduces the block to scalar positive semidefinite $2\times 2$ blocks whenever $f,g\ge 0$ on the spectrum and $fg=x^2$; this survives without invertibility under these nonnegativity assumptions. No statement here classifies the singular converse.

ASSUMED-UNVERIFIED

The source and literature screen are recorded in #18699. Literature completeness is ASSUMED-UNVERIFIED. The later articles DOI 10.1002/mma.70420, DOI 10.1007/s13226-026-00949-z and DOI 10.1007/s13226-026-00960-4 were not independently read by this implementation seat. No claim of exhaustive novelty is made. The all-$s$, direct-sum, Schur-complement, interpolation and power-case arguments above are prose proofs; the delivered Lean theorem proves the universal assertion false using its fixed witness.