Claims and evidence for the vibemathed entry: dimension-independent Hlawka constants for Schatten norms (savarin/hlawka-schatten @ 1829591)

CLAIMS.md

Claims and evidence: dimension-independent Hlawka constants for Schatten norms

This file pairs every factual sentence in our vibemathed entry with the exact place that backs it. Every repository link points to one fixed commit of savarin/hlawka-schatten, 1829591, so the line numbers cannot drift.

What is claimed, and what is not. Audenaert and Kittaneh's Problem 7 asks for the best dimension-independent Hlawka constant, if one exists. This repository settles two things:

• Existence, for every p. A constant exists exactly when 1 < p < ∞.
• The best constant for diagonal matrices, when p ≥ 256.

The best constant for general matrices remains open.

Row types:

• Lean: a machine-checked theorem. The link goes to its statement.
• argument: a short step of reasoning that is not formalized. Check it by reading.
• external: a source outside the repository, cited by page.
• search: a literature-search claim. It means we found nothing, not that nothing exists.
• CI: the automatic build at this commit.
• disclosure: a limitation we report.

How to check the Lean rows. CI run 35949577091 built the whole library at this commit and ran both boundary audits. To rebuild locally:

lake exe cache get && lake build
python3 scripts/check_boundary.py comparator-existence.json
python3 scripts/check_boundary.py comparator-construction-diagonal.json

The question

#	Claim	Evidence	Type	Note
1	Hlawka's inequality: in an inner product space, N(x) + N(y) + N(z) − N(x+y+z) is at most the sum of the three pair deficits N(x) + N(y) − N(x+y), N(x) + N(z) − N(x+z) and N(y) + N(z) − N(y+z).	arXiv:1201.5232v3, p. 13: "For the 2-norm, the sharpest value of C2 is known to be 1, as (48) then reduces to Hlawka's inequality"	external	Classical; Audenaert–Kittaneh cite it as their ref. [32].
2	Audenaert and Kittaneh asked for the best dimension-independent constant C, if it exists, with triple deficit ≤ C × (sum of the three pair deficits), and in particular for the best C_p for the Schatten p-norm.	arXiv:1201.5232v3, Problem 7, eq. (48), p. 12: "Find the best (dimension-independent) constant C – if it exists – … In particular, find the best constant Cp when the norm in question is the Schatten p-norm."	external	The problem asks for the best constant; existence is its "if it exists" part.
3	They showed that C_∞ is infinite, reported numerically that C_1 is at least 40, and noted that C_2 = 1.	arXiv:1201.5232v3, p. 13: "numerical simulations show that C1 is at least 40, indicating that it might be arbitrarily large as well"	external	Their p = ∞ witness is e11+e22, e11+e33, e22+e33.

Existence for every 1 < p < ∞

#	Claim	Evidence	Type	Note
4	For every real p > 1 there are constants 0 < m ≤ M such that M/m is a Hlawka constant for the Schatten p-norm on linear maps between any two finite-dimensional complex inner product spaces.	Statement: ExistenceChallenge.lean L66–73. Proof: Classification.lean L16–30, used by ExistenceSolution.lean L47–60	Lean	m and M are chosen before the spaces, which is what "dimension-independent" means. Maps between different spaces (rectangular matrices) are included.
5	The Schatten p-norm is the p-th root of the sum of the p-th powers of the singular values, using Mathlib's singular values.	ExistenceChallenge.lean L29–43	Lean	The statement file imports only Mathlib (L6–7).
6	"C is a Hlawka constant" means that for all x, y, z the triple deficit is at most C times the sum of the three pair deficits.	ExistenceChallenge.lean L45–60	Lean	This is inequality (48), with the norm as N.
7	The proof yields a constant, not the best one.	ExistenceChallenge.lean L67–73 asserts existence only.	argument	So Problem 7's "find the best constant" is still open for general matrices (row 18).

No constant at p = 1 or p = ∞

#	Claim	Evidence	Type	Note
8	At p = 1 (trace norm) no finite constant exists, already for 2 × 2 complex matrices.	Statement: ExistenceChallenge.lean L74–76. Proof: TraceEndpoint.lean L253–258	Lean	This turns Audenaert–Kittaneh's numerical C_1 ≥ 40 (row 3) into a proof that C_1 is infinite.
9	The p = 1 witness is built from two rank-one projectors.	TraceEndpoint.lean L84–91, with c² + s² = 1 (L119)	Lean	X = [[c², cs], [cs, s²]], Y = [[c², −cs], [−cs, s²]], Z = diag(0, −2s²).
10	At p = ∞ (operator norm) no finite constant exists on 3 × 3 complex matrices.	Statement: ExistenceChallenge.lean L77–78. Proof: EndpointObstruction.lean L105–112	Lean	Not new: Audenaert–Kittaneh already proved this (row 3). It is re-proved here with a different witness.
11	Witness: diag(−1, 1, 1), diag(1, −1, 1), diag(1, 1, −1). Each has norm 1 and each pairwise sum has norm 2, so every pair deficit is 0. The sum of all three, diag(1, 1, 1), has norm 1, so the triple deficit is 2.	EndpointObstruction.lean L66–73	Lean	No C can make 2 ≤ C × 0.

The best constant for diagonal matrices, p ≥ 256

#	Claim	Evidence	Type	Note
12	K_p is the largest ratio of triple deficit to pair-deficit sum along the cyclic family (−t, 1, 1), (1, −t, 1), (1, 1, −t), for t ∈ [1/2, 2].	ConstructionDiagonalChallenge.lean L51–65	Lean	It is an explicit formula: the ratio is at L58–61, and the supremum over [1/2, 2] at L63–65.
13	For every real p ≥ 256, K_p is a Hlawka constant for the Schatten p-norm on complex diagonal matrices of every size.	Statement: ConstructionDiagonalChallenge.lean L67–71. Proof: ComplexTransfer.lean L88–90, used by ConstructionDiagonalSolution.lean L55–62	Lean	The three matrices may have different norms and arbitrary complex entries, because the definition quantifies over all x, y, z (L46–49).
14	For p ≥ 256 and size at least 3, no smaller constant works.	Statement: ConstructionDiagonalChallenge.lean L73–77. Proof: CyclicWitness.lean L125–129, used by ConstructionDiagonalSolution.lean L64–72	Lean	The library lemma needs only p > 1, so K_p is a lower bound for every p > 1. The checked statement covers only p ≥ 256.
15	Some t ∈ [1/2, 2] attains K_p.	Statement: ConstructionDiagonalChallenge.lean L79–83. Proof: Cyclic.lean L105–107	Lean	The library version holds for all p > 1.
16	939p/2000 < K_p ≤ p, so the best diagonal constant grows linearly in p.	TailEstimates.lean L166–168 (p ≥ 256) and ScalarEnvelope.lean L13–14 (p > 1)	Lean	These are library theorems, compiled by CI. They are not among the four statements the boundary audit checks (row 24).
17	For n ≥ 3 and p ≥ 256, every Hlawka constant for the Schatten p-norm on n × n complex matrices is at least K_p.	Diagonal matrices are matrices, so a constant that works for all n × n matrices works for the diagonal ones, and row 14 applies. The diagonal norm is the same singular-value norm as in row 5 (ConstructionDiagonalChallenge.lean L29–32).	argument	This is not stated separately in Lean (README L55–58). With row 16, it means the existence constant of row 4 exceeds 939p/2000 when p ≥ 256.

Not claimed

#	Claim	Evidence	Type	Note
18	The best constant for general (non-diagonal) matrices is not determined, apart from the classical C_2 = 1.	README L61–62; row 1	disclosure	This is the open part of Problem 7.
19	The best diagonal constant for 1 < p < 256 is not determined. The cutoff 256 is what the proof needs; it is not claimed to be optimal.	README L58–62; ConstructionDiagonalChallenge.lean L69	disclosure	K_p remains a lower bound there (row 14).

Novelty and review

#	Claim	Evidence	Type	Note
20	We found no earlier proof of either result. We searched the Marinescu–Niculescu survey (arXiv:2407.03278), Audenaert–Kittaneh and its forward citations, and recent Schatten-norm work through September 2026.	README L94–97	search	Finding nothing is not proof that nothing exists. The search is to be re-run on posting day.
21	The p = 1 result appears to be new.	Audenaert–Kittaneh had only a numerical lower bound (row 3), and the search in row 20 found no proof.	search	Same limits as row 20.
22	Human experts have not examined the proofs in depth, the novelty of the ideas has not been established, and other proof assistants were not searched.	README L99–101	disclosure

How it is checked

#	Claim	Evidence	Type	Note
23	Lean 4 and Mathlib are both pinned at v4.35.0-rc2.	lean-toolchain; README L141	Lean
24	The four checked statements use only the axioms propext, Classical.choice and Quot.sound, and the statement files import only Mathlib.	comparator-existence.json L8, comparator-construction-diagonal.json L10. Audited by scripts/check_boundary.py in CI (build.yml L20–23)	CI
25	The automatic build passes at this commit.	CI run 35949577091, success, 2026-09-24 02:59 UTC. It builds the library (build.yml L19) and runs both audits.	CI
26	The only sorrys in any Lean file are the four deliberate placeholders in the statement files. The Solution files fill them from the library.	ExistenceChallenge.lean L79; ConstructionDiagonalChallenge.lean L71, L77, L83	search	grep -rnw sorry --include='*.lean' . prints exactly these four lines. A naive search also finds admit once, as an English word in a docstring (Sparsification.lean L15), plus explanatory uses of "sorry" and "axiom" in README.md, formalization.yaml and scripts/check_boundary.py. No Lean file mentions native_decide or axiom.
27	Palomar's Comparator checks that each Solution proves exactly its statement. Its last recorded local run, with negative controls, passed at commit 79aa498 on Lean v4.33.0, before the upgrade to v4.35.0-rc2. It has not been re-run at this commit.	README L190–194	disclosure

Who did what

The repository's own disclosure, in formalization.yaml.

#	Claim	Evidence	Type	Note
28	GPT 5.6 Sol, running in Codex, built the existence Lean proof in small kernel-checked layers, working from audited mathematical proof artifacts.	formalization.yaml L34–36, L124–133, L145–146	disclosure
29	The Ball–Carlen–Lieb uniform convexity framework motivated the approach. The proof derives the comparison it needs directly, rather than invoking their theorems.	formalization.yaml L58–72	disclosure
30	The sharp diagonal argument came out of two weeks of directed proof search. The author identified the proof strategy, diagnosed repeated dead ends where agents stalled, and refined the approach through failure analysis at each stage. AI agents executed computational searches and produced candidate lemmas.	formalization.yaml L147–152	disclosure
31	GPT 6 Astra, running in Codex, formalized the diagonal argument in Lean.	formalization.yaml L37–38, L134–143	disclosure
32	The author, GPT 5.6 Sol and Claude Fable 5.1 reviewed the work. The existence proof source was independently audited before formalization, the diagonal proof was reviewed against the blueprint, and both statement files were checked against their proof sources.	formalization.yaml L174–187	disclosure	This is agent review, not independent human review (row 22).

Wording in the repository that this entry does not repeat

README L41 says "The existence result answers their question". Problem 7 asks for the best constant (row 2), so the existence result answers only its "if it exists" part. The entry uses the narrower wording.