An unbounded obstruction to projection AM–GM in Loewner order

Dev D. Goyal

An unbounded obstruction to projection AM–GM in Loewner order

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Projection AM–GM inequality in Loewner order for symmetrized products of projections
Posed in: Motivated by Sun, Luo and Ye, Math. Oper. Res. 45(1) (2020); exact match with their published conjecture is conditional
Status: Counterexample
Result: Three rational rank-one orthogonal projections in ℝ³ have symmetrized product G ⋠ M³, M their mean (quadratic form −8/243), and for every real C some such triple with positive-definite mean has G ⋠ C·M³.

Abstract

Three rank-one orthogonal projections in dimension three violate the symmetrized-product Loewner AM–GM bound. No finite real multiplier repairs it, even with a positive-definite mean. The examples do not satisfy the additional nonsingular block structure of the motivating coordinate-descent application.

Details

Year: 2026
Discipline: Mathematics
Area: Matrix theory
Subject: Matrix theory
Result type: Focused research note and reproducible proof package
Formal proof: Standalone Lean package
Family: projection-amgm
Keywords: matrix AM–GM inequality, orthogonal projections, Loewner order, symmetrized products, operator inequalities

Statement and scope

Formal scope. Lean verifies a rational three-projection matrix obstruction and a parameterized obstruction for every real multiplier in dimension three; rank-one, positive-definite mean, rational all-multiplier choices, and the standard minimal-factor observation have complete conventional proofs.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 280 KB
PDF on GitHub: papers/mathematics/projection-amgm/paper.pdf
LaTeX source: papers/mathematics/projection-amgm/paper.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/projection-amgm/ 4 Lean files

Lakefile

papers/mathematics/projection-amgm/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/projection-amgm/README.md, which gives their context and working directory.

Reproduction

lake update
lake exe cache get
sh verify.sh

Reproduction

pdflatex -interaction=nonstopmode -halt-on-error paper.tex
pdflatex -interaction=nonstopmode -halt-on-error paper.tex

README: papers/mathematics/projection-amgm/README.md
Authorship: papers/mathematics/projection-amgm/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. The Omega Institute's public repository records a refutation with the same three projections and form −8/243, committed on 12 October 2026 (issue #15647), and a block-structured counterexample (issue #17674). No priority is claimed for the three-projection counterexample; the unbounded-multiplier theorem is not in that record. Priority and novelty record.

Source. The manuscript credits the motivating Sun–Luo–Ye projection comparison and distinguishes nearby norm inequalities. Exact correspondence with the published conjecture and historical priority remain conditional. The Omega Institute's public repository records a refutation with the same three projections and form −8/243, committed on 12 October 2026 (issue #15647), and a block-structured counterexample (issue #17674); no priority is claimed for the three-projection counterexample.

Questions and answers

Does the projection AM–GM inequality hold in Loewner order?

Not in the unrestricted form G ⪯ Mⁿ: three rational rank-one projections in dimension three violate it with quadratic form −8/243, and for every real C another triple violates G ⪯ C·M³. It holds for one or two projections, and the weaker G ⪯ M is consistent with the examples.

Does this disprove the Sun–Luo–Ye coordinate-descent conjecture?

That is not established. Exact correspondence with the published conjecture remains conditional, the examples lack the nonsingular block structure of the coordinate-descent application, and no convergence-rate claim is refuted. The Recht–Ré norm conjecture was refuted earlier by Lai–Lim and De Sa (2020).

Is the proof formally verified?

Lean 4 verifies the rational three-projection obstruction and the parameterized obstruction for every real multiplier. The rank-one, positive-definite-mean, rational-choice and two-factor statements have conventional proofs only.

Was the three-projection counterexample known before?

Yes. The Omega Institute's public repository records the same projections and the same value −8/243, committed on 12 October 2026 (issue #15647), about 17 days before this result was first committed here; it also gives a block-structured counterexample (issue #17674). The unbounded-multiplier theorem does not appear there. No priority is claimed for the counterexample.

Cite

Citation file papers/mathematics/projection-amgm/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026projectionamgm,
  author = {Goyal, Dev D.},
  title = {An Unbounded Obstruction to Projection {AM--GM} in Loewner Order},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory}
}