{"id":"d82f0ac3-7fb9-4896-ad5f-301d93e4ff07","arxiv_id":"2608.12280","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"partial","parameter_count":0,"one_line_summary":"Every Bessel sequence with Bessel bound 1 has a sharp Gram-matrix representation by functions in the unit ball of L∞([0,1]), and this yields an optimal solution to Olevskii's orthonormal extension problem.","lead":"This paper proves that any Bessel sequence with bound one in a Hilbert space can be represented by bounded functions on [0,1] whose inner products reproduce the original inner products exactly, with the optimal constant one. It also settles Olevskii's extension problem: such sequences on a set E always extend to uniformly bounded orthonormal systems on [0,1], with an optimal bound depending only on the measure of the complement.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant mathematical objection identified; only a constant-typo and the unpinned Lean companion file remain.","rationale":"The reader's weakest assumption is the reliance on the Ball–Prodromou theorem in Proposition 2.3. I agree that this is the most load-bearing external dependency in the proof, but I verified that the theorem is correctly stated and that its hypotheses are satisfied in the intended application: the projected basis satisfies Σ u_j u_j^T = I_E, and the vector w produced by Theorem 2.1 indeed has coordinates in [-1,1]^N, yielding the needed support-function inequality. The rest of the proof, including the complex reduction (Corollary 2.4), the finite-dimensional construction (Theorem 2.5), the infinite extension (Theorem 2.7), and the extension to Olevskii's problem (Theorem 1.2), is internally consistent and correct. The only genuine issues are a harmless typo in the constant range ('0 < K < 1' should be '0 < K') and the lack of a pinned, sorry-free Lean file, which is a reproducibility concern but not a mathematical one. Accordingly, I find no load-bearing objection to the central theorem, and the reader's CONDITIONAL verdict remains appropriate.","tokens_in":11901,"tokens_out":21040,"duration_ms":167450,"concrete_test":"Pin the GitHub repository to a specific commit and run `lake build` on Showcase_WithProofs.lean; if the theorem `main` is then checked without `sorry` and the build succeeds, the formalization claim is settled.","verdict_should_be":"UNCHANGED","load_bearing_attack":"After reviewing the proof of Proposition 2.3, the application of the Ball–Prodromou theorem (Theorem 2.1) is correct: for E = E(A), the projected basis {u_j = P_E e_j} satisfies Σ u_j u_j^T = I_E, and the resulting w lies in E(A) with |w_j| ≤ 1, so w ∈ [-1,1]^N and the support-function inequality α(A) ≤ β(A) follows. The finite-to-infinite extension (Theorem 2.7) via the compactness of P(D^N) and the realization lemma is also rigorous: the finite intersection property is verified using finite-dimensional representations, and the limiting measure gives the required L∞ functions. Lemma 2.8 is correct, and the Olevskii application in Theorem 1.2 follows. I found no flaw that would threaten the central claim. The only caveats are minor: Theorems 1.1 and 2.5 state a constant '0 < K < 1' but then set K = 1, which is a clear typo (should be '0 < K' or 'K > 0'). More substantially, the Lean formalization claim is not reproducible as written: Showcase.lean contains two sorrys and the companion file is not pinned to a commit hash, so a reader cannot verify the claimed machine-checked proof at a fixed state. These do not affect the truth of the theorem, but they justify the reader's CONDITIONAL verdict.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper establishes a sharp infinite-dimensional version of Grothendieck's theorem for Bessel sequences: for any Hilbert space H and any Bessel sequence {x_j} with Bessel bound 1, there are functions f_j in the unit ball of L∞([0,1]) with ⟨x_j,x_k⟩ = ∫ f_j \\overline{f_k} for all j,k, and the constant 1 is optimal. The proof proceeds through a finite-dimensional convex-geometric statement (Proposition 2.3), proved via the Ball–Prodromou theorem, a complex lifting step (Corollary 2.4), a compactness argument for the passage from finite to countable index sets (Theorem 2.7), and a measure-preserving change of variables (Lemma 2.8) that yields the application to Olevskii's extension problem (Theorem 1.2) with an optimal constant. An appendix describes a Lean 4 formalization of the main theorem.","tokens_in":12135,"tokens_out":13952,"duration_ms":122727,"significance":"If correct, the result resolves a well-known open problem attributed to Olevskii, as stated in Pisier's survey, and it sharpens Kashin's off-diagonal result by preserving the diagonal and achieving the optimal constant K=1. The proof is clean and essentially parameter-free: the only external input is the Ball–Prodromou theorem, and the optimality lower bound is a one-line argument. The claimed Lean formalization, if in a reproducible state, would be a valuable machine-checked companion.","major_comments":[],"minor_comments":[{"comment":"The formalization is not reproducible as a fixed state: no commit hash or archive is given, and Showcase.lean is said to contain two `sorry`s. The paper should pin the repository to a specific commit and state explicitly that Showcase_WithProofs.lean is the machine-checked artifact, so that the formalization claim can be verified at a fixed state.","section":"§3.4 and the GitHub repository"},{"comment":"The constant is stated as '0 < K < 1' in several places, but the theorem then asserts K=1 and proves optimality; the upper bound '< 1' is inconsistent and should read '0 < K' (or 'K > 0').","section":"Theorems 1.1, 2.5, 2.7 and proof of Theorem 2.5"},{"comment":"The kernel is written z_j z_k, but the complex representation from Corollary 2.4 and Theorem 2.5 gives moments with kernel z_j \\overline{z_k}; with the printed kernel the finite-dimensional moments do not verify membership in C_jk. The argument should use z_j \\overline{z_k} throughout, and with that replacement the closedness and compactness reasoning are unaffected.","section":"Theorem 2.7, definition of C_jk and final display"},{"comment":"The displayed identity should be ζ_j^{(r)} \\overline{ζ_k^{(r)}}; the overline is missing in the text. The same missing conjugation appears in the display for g_jk in §1.5 and in the statement of Theorem 2.5.","section":"Corollary 2.4 and Theorem 2.5"},{"comment":"In the proof of Theorem 2.5, 'By Proposition 2.4' should be 'By Corollary 2.4'; in the proof of Theorem 2.7, the phrase 'Gram matrix of {x_j}_{j∈F}' should be 'the matrix H_F', since the vectors x_j are not otherwise defined in that proof; and in Theorem 2.5 the quantity in the statement should be G_jk, not ⟨x_j,x_k⟩.","section":"Proofs of Theorem 2.5 and Theorem 2.7"},{"comment":"The notation ∑ u_j · u_j = I_E should be explained as the sum of outer products; the verification in Proposition 2.3 relies on this interpretation.","section":"Theorem 2.1"}],"recommendation":"minor_revision","confidential_remarks":"I found no substantive mathematical obstruction in the main proof; the only issues are the complex-conjugate typo in Theorem 2.7 and the reproducibility state of the Lean repository, both of which are locally fixable. The LLM-assistance disclosure is transparent and does not affect my assessment."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know about arXiv:2608.12280. The main theorem is a genuinely sharp Grothendieck theorem for Bessel sequences: any Bessel sequence with bound 1 admits a representation of its full Gram matrix as inner products of functions in the unit ball of L∞([0,1]), with optimal constant K=1. That solves Olevskii's extension problem with the optimal bound. Previous work (Kashin–Szarek, Alon et al.) only handled off-diagonal entries with constants growing like log N, or gave K=2 without preserving the diagonal; this closes the gap.\n\nThe proof is good. The finite-dimensional core is Proposition 2.3: every Hermitian G with 0≤G≤I is a convex combination of rank-one terms ζζ* with |ζ_j|≤1. The support-function argument is correct, and the application of Ball–Prodromou is legitimate—the stress test verified that the projected basis satisfies the required identity. The passage from finite to countably infinite via compactness of the product of disks and Billingsley's realization lemma is standard and clean. The optimality of K=1 is a one-liner. The Olevskii application is a neat use of the complementary Gram matrix I-G, and the constant is shown optimal by the zero function example.\n\nSoft spots are minor. The statement says 'a constant 0<K<1' and then sets K=1; that's a typo, should be K>0. More notably, the Lean formalization appendix is not fully reproducible as written: Showcase.lean contains two sorrys, and the companion file Showcase_WithProofs.lean is not pinned to a commit hash. So a reader cannot verify the claimed machine-checked proof at a fixed state from the paper alone. That is a reproducibility condition, not a mathematical flaw.\n\nThe citation pattern looks fine; the Ball–Prodromou reference is appropriate and not load-bearing in a dubious sense. The self-citation to the authors' own paper on Fourier frames is irrelevant to the main argument.\n\nThis paper is for people working on Grothendieck-type inequalities, bounded orthonormal systems, or frame theory. It deserves a serious referee: the mathematical content is strong and likely correct. I would send it to review and ask the authors to fix the typo and pin the Lean repository to a specific commit (or provide the proof file in the submission artifacts).","headline":"Sharp K=1 Grothendieck theorem for Bessel sequences, solving Olevskii's problem; the math is solid, but the Lean formalization is not yet reproducible as written.","tokens_in":12706,"tokens_out":3138,"would_cite":true,"duration_ms":26382,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["46B15","46B25","42C15","68V20"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every Bessel sequence with Bessel bound 1 has its inner products reproduced by unit-bounded functions on [0,1], with the optimal constant 1.","keywords":["Grothendieck theorem","Bessel sequences","Gram matrix factorization","orthonormal extension","bounded orthogonal systems","convex hull of rank-one matrices","formalized mathematics"],"falsifier":"For a small fixed dimension, say $N=2$ or $N=3$, sample symmetric matrices $A$ and compare $\\max_{x \\in [-1,1]^N} x^T A x$ with $\\mathrm{tr}(A_+)$: the paper's finite-dimensional claim is exactly that the maximum is never smaller than the trace, so a single numerical counterexample would refute the convex-hull statement from which the main theorem follows.","tokens_in":11664,"feed_emoji":"📐","tokens_out":20871,"duration_ms":163830,"temperature":0.7,"pith_summary":"The paper establishes a sharp, diagonal-preserving version of Grothendieck's theorem for Bessel sequences. It proves that if a countable family of vectors in a Hilbert space has Bessel bound 1, then its Gram matrix can be represented exactly as the $L^2([0,1])$ inner-product matrix of functions from the unit ball of $L^\\infty([0,1])$, with constant 1 and no larger constant possible. This matters because it settles an open extension problem: any Bessel sequence in $L^2(E)$ with bound 1 extends to an orthonormal system on all of $[0,1]$, with an optimal pointwise bound on the complement of $E$. The proof runs through a finite-dimensional convex-geometric statement, an infinite passage by compactness, and a reported machine-checked formalization of the main existence claim.","feed_headline":"Bessel sequences factor through the L∞ unit ball with constant 1","feed_subtitle":"It settles an open extension problem with the optimal pointwise bound.","key_machinery":"The load-bearing device is the finite-dimensional convex-geometric statement that every real symmetric matrix $G$ with $0 \\le G \\le I$ lies in the convex hull of $\\{xx^T : x \\in [-1,1]^N\\}$; the complex analogue is obtained by doubling the dimension. Its proof compares support functions: for fixed symmetric $A$, the maximum of $\\langle A, G\\rangle$ over such $G$ is $\\mathrm{tr}(A_+)$, while the corresponding maximum over the convex hull of rank-one box matrices is $\\max_{x \\in [-1,1]^N} x^T A x$. A quoted geometric theorem supplies a vector $w$ in the positive spectral subspace with $w^T A w \\ge \\mathrm{tr}(A_+)$ and $|\\langle w,e_j\\rangle| \\le 1$ for every standard basis vector $e_j$, exactly bridging the two quantities. The finite convex combination is turned into piecewise-constant functions on $[0,1]$; a compactness argument in the space of probability measures on the countable product of closed disks, using a realization lemma, upgrades the representation to countably many vectors.","core_discovery":"The paper's central claim is that the Gram matrix of any Bessel sequence with bound 1 is, with no rescaling, the matrix of inner products of a sequence of functions each bounded in modulus by 1 on $[0,1]$, and that this is optimal because a unit vector already forces the constant to be at least 1. In Gram-matrix language: every Hermitian matrix $G$ with $0 \\le G \\le I$ is a convex combination of rank-one matrices $\\zeta\\zeta^*$ with $\\zeta$ in the closed unit disk $\\mathbb{D}$, from which simple functions on a partition of $[0,1]$ give the integral representation. A weak-compactness argument over probability measures on the infinite product of disks passes to countably infinite Gram matrices, and a measure-preserving rearrangement lemma transfers the representation from $[0,1]$ to any subset $A$ of positive measure. The authors draw the consequence that every Bessel sequence on $L^2(E)$ extends to an orthonormal system on $[0,1]$ with optimal pointwise bound on the complement, and they report a machine-checked formalization of the main existence theorem with constant 1.","pith_inferences":["An unstated corollary of the compactness route is that the representation should survive for index sets of any cardinality: the finite-intersection argument works on the product of disks regardless of the index set, so countability looks like a convenience of presentation rather than a necessity.","The finite-dimensional core is a concrete membership problem that can be probed independently: for fixed $N$, checking whether every $0 \\le G \\le I$ lies in the convex hull of box rank-one matrices is a finite convex optimization question, so numerical search over small dimensions would be an inexpensive check of the argument.","The machine-checked version establishes existence but not the one-line optimality of $K=1$ nor the extension theorem; completing those formalizations is a natural next step."],"forward_implications":["Every Hermitian matrix $G$ with $0 \\le G \\le I$, finite or countable, is entrywise the matrix $\\int_0^1 f_j \\overline{f_k}\\,dx$, with each $|f_j| \\le 1$ and no rescaling; the constant $1$ cannot be improved.","Every Bessel sequence in $L^2(E)$ with bound 1 extends to an orthonormal system on $[0,1]$ whose functions are bounded on the complement by $\\lambda([0,1]\\setminus E)^{-1/2}$.","The bound in the extension theorem is optimal for every measurable set $E$ whose complement has positive measure.","The result closes the diagonal gap left by earlier off-diagonal constructions: diagonal entries are preserved while the constant stays exactly 1.","In Gram-matrix terms, all positive semidefinite matrices between $0$ and $I$ are convex combinations of rank-one matrices generated by vectors in $[-1,1]^N$ in the real case and by points of the closed unit disk in the complex case."],"supporting_citations":[{"why":"Supplies the quoted finite-dimensional geometric theorem that produces the bounded-coordinate vector needed in the convex-hull core.","marker":"[3]"},{"why":"Gives the support-function characterization of convex compact sets used to prove the finite-dimensional core.","marker":"[22]"},{"why":"Provides the realization lemma used to convert the limiting probability measure into functions on [0,1].","marker":"[4]"},{"why":"Records the open form of the problem and the classical Grothendieck theorem being sharpened.","marker":"[21]"},{"why":"Raises the extension problem that the paper answers affirmatively.","marker":"[20]"},{"why":"Gives the earlier off-diagonal construction that the paper improves by preserving diagonal entries.","marker":"[12]"}],"fun_headline_variants":["Optimal Grothendieck for Bessel sequences: factor through L∞","Bessel sequences with bound 1 are L∞ inner products","Sharp theorem: Bessel sequences extend orthogonally with optimal bound","Olevskii's problem: optimal extension of Bessel sequences","Lean 4 proof: Bessel sequences factor through L∞ with constant 1"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire proof hinges on a quoted finite-dimensional geometric theorem guaranteeing that, for the positive part of any symmetric matrix, a vector $w$ can be chosen with $|\\langle w,e_j\\rangle| \\le 1$ for every standard basis vector $e_j$ and with $w^T A w$ at least the trace of that positive part; if the theorem is false or its hypotheses are not met by the projected vectors in the proof, the finite-dimensional core and with it the main theorem collapse.","fun_headline_variants_meta":{"raw":{"variants":["Optimal Grothendieck for Bessel sequences: factor through L∞","Bessel sequences with bound 1 are L∞ inner products","Sharp theorem: Bessel sequences extend orthogonally with optimal bound","Olevskii's problem: optimal extension of Bessel sequences","Lean 4 proof: Bessel sequences factor through L∞ with constant 1"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001287,"raw_usage":{"total_tokens":5291,"prompt_tokens":1011,"completion_tokens":4280,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":627,"completion_tokens_details":{"reasoning_tokens":4185}},"tokens_in":627,"tokens_out":4280,"duration_ms":28682,"temperature":1.0,"reasoning_tokens":4185,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T00:10:55.790601+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For a small fixed dimension, say $N=2$ or $N=3$, sample symmetric matrices $A$ and compare $\\max_{x \\in [-1,1]^N} x^T A x$ with $\\mathrm{tr}(A_+)$: the paper's finite-dimensional claim is exactly that the maximum is never smaller than the trace, so a single numerical counterexample would refute the convex-hull statement from which the main theorem follows.","supporting_citations":[{"cited_title":"Ball and Maria Prodromou","cited_arxiv_id":null,"evidence_quote":"Supplies the quoted finite-dimensional geometric theorem that produces the bounded-coordinate vector needed in the convex-hull core."},{"cited_title":"Weak convergence of measures: Applications in probability , volume No","cited_arxiv_id":null,"evidence_quote":"Provides the realization lemma used to convert the limiting probability measure into functions on [0,1]."},{"cited_title":"Grothendieck’s theorem, past and present","cited_arxiv_id":null,"evidence_quote":"Records the open form of the problem and the classical Grothendieck theorem being sharpened."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Raises the extension problem that the paper answers affirmatively."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the earlier off-diagonal construction that the paper improves by preserving diagonal entries."}],"review_version":1}