Gaussian Sampling Complexity
Exact-oracle lower bounds, Gaussian expectations and the laws behind the proof.
Main paper results remain open in Lean. Verified building blocks are listed separately below.
Suggested reading order
- Start with the exact Section 2 algorithm, TV and deterministic query-cap contract.
- Read Theorem 3.1 and Theorem 4.1 separately before comparing their proof ingredients.
- Expand the comparison below: exact compiled declaration reuse and conceptual mechanism links are different relations.
- All source-route nodes are currently red; source review is not Lean verification.
Paper, notation and source conventions
On Complexity of Gaussian Sampling
Source: 2610.20492v1. Pinned source version
- Precision A is real symmetric and \(I_d\preceq A\preceq\kappa I_d\); the target is the actual centered Gaussian \(\mathcal N(0,A^{-1})\).
- Exact matrix-vector access \(x\mapsto Ax\) is equivalent to exact value-and-gradient access for \(f_A(x)=\langle x,Ax\rangle/2\). No noisy, finite-precision or Hessian oracle is substituted.
- Queries, stopping decisions and output are Borel functions of an input-independent random seed and previous replies; the output need not lie in the query/reply span.
- T is a deterministic cap for every admissible input AND every seed realization. Accuracy is uniform over inputs after averaging over the private seed, measured in TV with normalization sup_B |P(B)-Q(B)|.
1. Main statements
RED · source theorem known · local proof open
Theorem 3.1: hidden determinant sign
Source: 2610.20492v1. Theorem 3.1, equation (3); Section 3.3
Open this theorem in the interactive research workspace
Statement
Every randomized adaptive Gaussian sampler in the Section 2 oracle model obeys the following explicit lower bound.
- Precision A is real symmetric and \(I_d\preceq A\preceq\kappa I_d\); the target is the actual centered Gaussian \(\mathcal N(0,A^{-1})\).
- Exact matrix-vector access \(x\mapsto Ax\) is equivalent to exact value-and-gradient access for \(f_A(x)=\langle x,Ax\rangle/2\). No noisy, finite-precision or Hessian oracle is substituted.
- Queries, stopping decisions and output are Borel functions of an input-independent random seed and previous replies; the output need not lie in the query/reply span.
- T is a deterministic cap for every admissible input AND every seed realization. Accuracy is uniform over inputs after averaging over the private seed, measured in TV with normalization sup_B |P(B)-Q(B)|.
- Every integer \(d\ge1\), \(\kappa\ge4\), and \(0<\varepsilon\le1/16\). No warm-start input is required; the minimizer 0 is already known.
Lean statement — not formalized yet
A future declaration must bind the probability laws, normalization, regularity, source algorithm and oracle model explicitly. The formula is a source theorem contract, not Lean code.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Proof architecture and calculations · 5 steps
This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.
Remove zero-query and dimension-saturated cases
\[T\ge1,\qquad 2T+1>d\ \Longrightarrow\ T\ge d/2\]Compare \(I_d\) with \(\operatorname{diag}(\kappa,1,\ldots,1)\) on the event \(|x_1|\le1/2\). The remaining proof uses \(n=2T+1\) and \(k=\lfloor d/n\rfloor\); the exceptional cases are separate source obligations.
Source: 2610.20492v1. Section 3.3, zero-query cases
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Hide a common sign in independent orthogonal blocks
\[A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top),\quad O_j\mid b\sim\mu_{n,b}\]The blocks are independent conditional on one common determinant sign b. Lemma 3.4 proves spectral admissibility. Two primitive forward/inverse observations per block simulate one matvec; this is 2T per block, not 2T in total.
Source: 2610.20492v1. Equations (4)-(6); Lemma 3.4; Appendix B.1
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Prove equality of averaged output laws
\[2T<n\ \Longrightarrow\ \bar\rho_+=\bar\rho_-\]Borel frames and conditional Haar residual maps produce sign-independent replies whenever two unexposed dimensions remain. Induct across adaptive queries, including cross-block dependence, then average the independent algorithm seed.
Source: 2610.20492v1. Lemma 3.2; Lemmas B.2-B.3 and transcript indistinguishability
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Separate the targets and amplify across blocks
\[\mathrm{TV}(\bar\pi_+,\bar\pi_-)\ge1-\exp\!\left\{-\frac{k}{8}e^{-10n/\sqrt\kappa}\right\}\]A radial exponential test detects one block via determinant cancellation and spherical Poisson identities. Hellinger affinity tensorizes across conditionally independent blocks. This does not assert independence after forgetting the common sign.
Source: 2610.20492v1. Lemma 3.3; Appendix A.1 and B.2
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Mix the per-input guarantee and invert the separation bound
\[\mathrm{TV}(\bar\pi_+,\bar\pi_-)\le2\varepsilon,\quad ke^{-10n/\sqrt\kappa}\le32\varepsilon\]Convexity of TV under mixing and the common output law give the upper bound. Use \(k\ge d/(2n)\), \(n\le3T\), the exponential comparison and concavity of log. Do not assume these proof ingredients as public hypotheses of Theorem 3.1.
Source: 2610.20492v1. Section 3.3, equations (9)-(10) and final logarithmic inversion
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Lean proof — not formalized yet
Formalization will first match the named technology interfaces, then assemble this source theorem. No placeholder proof or source-cited wrapper has been added.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Strict boundary
Source theorem known; all paper-specific Lean edges remain open. Determinant sign concerns the hidden orthogonal O, not the positive determinant of SPD precision A. The result is for a worst-case deterministic query cap, not an expected-cost lower bound without a separate reduction.
Further source statements · 1
RED · source theorem known · local proof open
Theorem 4.1: a known spectrum and hidden eigenbasis
Source: 2610.20492v1. Theorem 4.1; Sections 4.1-4.4
Open this theorem in the interactive research workspace
Statement
Even when the precision spectrum is supplied to the algorithm, the fixed-spectrum hard family gives the following lower bound.
- Precision A is real symmetric and \(I_d\preceq A\preceq\kappa I_d\); the target is the actual centered Gaussian \(\mathcal N(0,A^{-1})\).
- Exact matrix-vector access \(x\mapsto Ax\) is equivalent to exact value-and-gradient access for \(f_A(x)=\langle x,Ax\rangle/2\). No noisy, finite-precision or Hessian oracle is substituted.
- Queries, stopping decisions and output are Borel functions of an input-independent random seed and previous replies; the output need not lie in the query/reply span.
- T is a deterministic cap for every admissible input AND every seed realization. Accuracy is uniform over inputs after averaging over the private seed, measured in TV with normalization sup_B |P(B)-Q(B)|.
- For every fixed \(\delta\) in (0,1), there exists \(d_0(\delta)\) such that every integer \(d\ge d_0(\delta)\), \(2\le\kappa\le d^{1-\delta}\), and \(0<\varepsilon\le1/10\) satisfies the bound.
Lean statement — not formalized yet
A future declaration must bind the probability laws, normalization, regularity, source algorithm and oracle model explicitly. The formula is a source theorem contract, not Lean code.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Proof architecture and calculations · 5 steps
This is a source-linked proof route, not a complete reconstruction of all cited lemmas. The dependencies below remain separate formalization tasks.
Fix the eigenvalues and randomize only the eigenbasis
\[\theta_i=\frac{(i-1/2)\pi}{d},\quad\lambda_i=\frac{\kappa+1}{2}+\frac{\kappa-1}{2}\cos\theta_i,\quad A=O\Lambda O^\top\]Haar O hides the eigenbasis. The eigenvalues and Gaussian normalizing constant may be known. Lemma 4.6 checks admissibility; the affine relation to the \(\kappa=2\) construction preserves one-query replies.
Source: 2610.20492v1. Section 4.1; Remark 4.2; Lemma 4.6
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Represent arbitrary adaptive output with an extra Gaussian start
\[O^\top X\in\mathcal K_q=\operatorname{span}\{\Lambda^j g_a:1\le a\le q+1,\ 0\le j\le q\}\quad\text{a.s.}\]The extension must preserve the joint law of (O,X). Independent Gaussian starting vectors are produced by the deferred-rotation representation, not assumed for the original output. The extra q+1 start handles outputs outside the reply span; coefficients can depend on the whole experiment.
Source: 2610.20492v1. Lemma 4.3; Appendix C.1; cited OpenAI preprint Lemma 9.2
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Control the cosine statistic uniformly over the whole random space
\[n=2q+1<d,\quad \tau_{d,q}=C\left[(q+1)\sqrt{\frac{\log d}{d}}+\frac{(q+1)(q+1+\log d)\log d}{d}\right]\]For an integer \(q\ge0\) and independent standard Gaussian starts, Lemma 4.4 gives \(|u^{\mathsf T}D_nu|\le2\tau_{d,q}\|u\|^2\) for EVERY u in \(K_q\) on one event of probability at least 0.99, provided \(\tau_{d,q}\le1/2\). The constant C is universal. Uniformity is essential because the coefficients are adaptive; cosine cancellation and Gram concentration are separate dependencies.
Source: 2610.20492v1. Lemma 4.4; Appendix C.2
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Compute target signal and fluctuations
\[\rho_\kappa=\frac{\sqrt\kappa-1}{\sqrt\kappa+1},\quad M=\frac{d}{\sqrt\kappa}\frac{1-\rho_\kappa^{2d}}{1+\rho_\kappa^{2d}},\quad (-1)^n\mu_n=\frac{d}{\sqrt\kappa}\frac{\rho_\kappa^n-\rho_\kappa^{2d-n}}{1+\rho_\kappa^{2d}}\]Both quadratic-form variances are at most 2M. With \(\beta=|\mu_n|/M\), use \(\tau\le\beta/4\) and \(M\beta^2\ge320\). These inequalities must be derived uniformly from \(d\ge d_0(\delta)\), not supplied as extra theorem assumptions.
Source: 2610.20492v1. Lemma 4.5; Appendix C.3; Section 4.3
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Use an input-dependent event to contradict uniform TV accuracy
\[\mathbb E_A\rho_A^{\mathrm{Alg}}(E_A)\le0.01,\quad\pi_A(E_A)\ge0.9,\quad0.89\le\varepsilon\le0.1\]The test event E_A uses a Chebyshev polynomial of A and is measurable. It is an analysis witness depending on the fixed input, not a free oracle operation made available to the sampler.
Source: 2610.20492v1. Section 4.3
Track or question this step in Live Formalization
Lean step — not formalized yet
This mathematical step is still open in Lean. The future declaration must expose exactly the objects and side conditions named above; no source-cited wrapper is counted as a proof.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Lean proof — not formalized yet
Formalization will first match the named technology interfaces, then assemble this source theorem. No placeholder proof or source-cited wrapper has been added.
No corresponding ASTIS declaration is asserted. Search locations below are candidates, not established dependencies or copied library proofs.
Strict boundary
Source theorem known; no local Lean realization is asserted. Section 4.4 limits this uniform-Krylov/test analysis: it yields no growing \(\log(1/\varepsilon)\) term, and saturation at \(\dim K_q=\min(d,(q+1)^2)\) obstructs the current uniform-space estimate. These are limitations of this proof, not an impossibility theorem for stronger fixed-spectrum lower bounds.
3. What has been verified?
32 source-mapped declarations; 0 independently reviewed. These are building blocks, not completed paper results.
Browse statements and their mathematical proofs
A radial test bounds mixture TV
- A radial test bounds mixture TV
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The literal full precision, including its residual identity block
- The literal full precision, including its residual identity block
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Sum the actual single-block estimates in the original coordinates
- Sum the actual single-block estimates in the original coordinates
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The quadratic potential has its unique minimum at zero
- The quadratic potential has its unique minimum at zero
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The actual first-column law
- The actual first-column law
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Normalize the actual positive and negative determinant Haar priors
- Normalize the actual positive and negative determinant Haar priors
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
A non-first principal minor has finite weighted expectation zero
- A non-first principal minor has finite weighted expectation zero
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Average the actual signed Gaussian normalization factor
- Average the actual signed Gaussian normalization factor
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Compute the actual signed Gaussian test expectation
- A signed Gaussian expectation
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Reduce the signed Gaussian formula to the norm axis
- Reduce the signed Gaussian formula to the norm axis
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Rotate the literal signed Gaussian kernel average
- Rotate the literal signed Gaussian kernel average
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The Laplacian of a product
- The Laplacian of a product
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Exact volume density of the actual Gaussian with SPD precision
- Exact volume density of the actual Gaussian with SPD precision
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Identify the source Gaussian law with its literal precision density
- Identify the source Gaussian law with its literal precision density
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Expectations of the Gaussian mixtures
- Expectations of the Gaussian mixtures
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Compute the literal mixture transform by genuine joint Fubini
- Compute the literal mixture transform by genuine joint Fubini
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Construct the actual determinant-conditioned Gaussian mixtures
- Construct the actual determinant-conditioned Gaussian mixtures
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Factor the actual precision as a positive square
- Factor the actual precision as a positive square
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Fix the positive branch of the determinant square root
- Fix the positive branch of the determinant square root
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Move the determinant sign inside the normalization factor
- Move the determinant sign inside the normalization factor
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
An explicit separation ratio has an exponential floor
- An explicit separation ratio has an exponential floor
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The full orthogonal group has a unique Haar probability
- The full orthogonal group has a unique Haar probability
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Construct the full orthogonal Haar draw
- Construct the full orthogonal Haar draw
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Characterize the constructed probability law
- Characterize the constructed probability law
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
A fixed rotation or reflection preserves the draw
- A fixed rotation or reflection preserves the draw
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Normalize the signed Gaussian expectation
- Normalize the signed Gaussian expectation
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Evaluate the finite radialized Gaussian test average
- Evaluate the finite radialized Gaussian test average
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
A positive tilt matches the Poisson denominator
- A positive tilt matches the Poisson denominator
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Single-block precision: the literal formula (4)
- Single-block precision: the literal formula (4)
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Orthogonality and Cauchy–Schwarz give the single-block spectral bounds
- Orthogonality and Cauchy–Schwarz give the single-block spectral bounds
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
From Haar columns to surface measure
- From Haar columns to surface measure
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
The selected Gaussian surface integral
- The selected Gaussian surface integral
Read full statement and proof →
Source assumptions, verification evidence and optional Lean are beside the proof on that page.
Compare proof mechanisms and prerequisites
How the two proofs organize their ingredients
One canonical Lean node is shared only when the exact compiled declaration is actually consumed, with its hypotheses matched. Residual Haar symmetry is currently a conceptual link: it does not identify determinant-component posterior laws with deferred-rotation Krylov laws.
| Comparison | Determinant sign | Hidden eigenbasis |
|---|---|---|
| Information hidden from the algorithm | A common determinant sign of hidden orthogonal blocks; exact averaged transcript equality. | A Haar eigenbasis with a deterministic, disclosed spectrum; output lives in an extended random Krylov space. |
| Key quantitative estimate | TV separation >= 1-exp(-(k/8)exp(-10n/sqrt(kappa))); Hellinger amplification. | Uniform cosine bound tau_{d,q} versus target signal beta=|mu_n|/M and variance <= 2M. |
| Parameter boundary | d>=1, kappa>=4, epsilon<=1/16; accuracy-dependent lower bound capped by dimension. | Fixed delta; d sufficiently large; 2<=kappa<=d^(1-delta), epsilon<=1/10; known-spectrum guarantee, no growing precision term. |
| Organization of possible shared Lean nodes | Measure/kernel core -> adaptive posterior factorization -> transcript equality; independent radial/spectral branch -> amplified separation; join by mixing and triangle. | Measure/kernel core -> deferred rotations -> Krylov representation; independent cosine/Gram and target-moment branches; join by an input-dependent measurable test. |
| Mechanism link, without identifying lemmas | Residual Haar symmetry is a conceptual relation to the other route; determinant-conditioned posterior is a different proposition. | Rotational symmetry is reused as a proof mechanism, but its extended-experiment and uniform-space adapters stay separate. |
| Comparison to PBPS / Gaussian Cloud / midpoint | Match exact oracle, target subclass, TV normalization, initialization and deterministic cap before comparing a lower bound to upper results. | Expected query costs, arbitrary log-concave targets, integrator-specific bias and finite-precision access are different contracts; a hyperedge must expose each adapter. |
Source proof outline
Initial theorem-and-main-lemma outline only. Exhaustive paragraph/display/citation coverage and exact Lean Statement Seals remain pending.
All links below describe source proof use. No solid Lean implication or compiled node is asserted.
Expand 18 source nodes and their inputs
Section 2 oracle / algorithm / TV model
Source: Section 2. Lean: open.
Source inputs: source definition or background obligation
SPD block admissibility
Source: Lemma 3.4; Appendix B.3. Lean: open.
Source inputs: Section 2 oracle / algorithm / TV model
Borel frames and conditional determinant-component Haar laws
Source: Lemma B.2. Lean: open.
Source inputs: source definition or background obligation
Adaptive residual posterior factorization across blocks
Source: Lemma B.3. Lean: open.
Source inputs: Borel frames and conditional determinant-component Haar laws
Equal averaged transcript and output laws
Source: Lemma 3.2; Appendix B.1. Lean: open.
Source inputs: Section 2 oracle / algorithm / TV model; Adaptive residual posterior factorization across blocks
Determinant cancellation and radial test separation
Source: Appendix A.1; B.2.1-B.2.2. Lean: open.
Source inputs: source definition or background obligation
Hellinger affinity tensorization
Source: Lemma 3.3; B.2.3. Lean: open.
Source inputs: Determinant cancellation and radial test separation
Convexity under mixing and TV triangle
Source: Section 3.3. Lean: open.
Source inputs: SPD block admissibility; Equal averaged transcript and output laws; Hellinger affinity tensorization
Zero-query and dimension-saturated cases
Source: Section 3.3. Lean: open.
Source inputs: source definition or background obligation
Logarithmic inversion and floor bounds
Source: Section 3.3 equations (9)-(10). Lean: open.
Source inputs: Convexity under mixing and TV triangle
Explicit accuracy-dependent lower bound
Source: Theorem 3.1. Lean: open.
Source inputs: Logarithmic inversion and floor bounds; Zero-query and dimension-saturated cases
Known cosine-grid spectrum and admissibility
Source: Section 4.1; Lemma 4.6. Lean: open.
Source inputs: Section 2 oracle / algorithm / TV model
Joint-law-preserving output/Krylov representation
Source: Lemma 4.3; Appendix C.1. Lean: open.
Source inputs: Section 2 oracle / algorithm / TV model
Uniform random-space cosine quadratic estimate
Source: Lemma 4.4; Appendix C.2. Lean: open.
Source inputs: source definition or background obligation
Target mean and variance identities
Source: Lemma 4.5; Appendix C.3. Lean: open.
Source inputs: source definition or background obligation
Input-dependent measurable test and uniform delta-regime
Source: Section 4.3. Lean: open.
Source inputs: Joint-law-preserving output/Krylov representation; Uniform random-space cosine quadratic estimate; Target mean and variance identities; Known cosine-grid spectrum and admissibility
Known-spectrum lower bound
Source: Theorem 4.1. Lean: open.
Source inputs: Input-dependent measurable test and uniform delta-regime
Dimension saturation and precision ceiling of this analysis
Source: Section 4.4; Lemma 4.7. Lean: open.
Source inputs: Joint-law-preserving output/Krylov representation; Target mean and variance identities; Uniform random-space cosine quadratic estimate
Source discrepancies retained for review
- v1 Conclusion says a gap remains for all \(\kappa\) ≤ d^(2-\(\delta\)), while Theorem 3.1 and Introduction claim matching in this regime. Keep this as a source discrepancy; do not silently repair the theorem or repeat the conclusion as an accepted open problem.
- Lemma A.1 contains both n≥2 and a trailing n≥3 phrase. The determinant application uses \(n=2T+1\)≥3; any generalized spherical lemma needs its own dimension audit.
- The Introduction also claims to confirm the conjecture whenever sqrt(\(\kappa\)) log d ≤ d. The explicit Theorem 3.1 bound alone does not cover this entire region: with \(\kappa\)=d^2/(log d)^2 and fixed \(\varepsilon\), it gives order d log(log d)/log d, whereas the conjectured expression is order d. Retain this as a source-claim-versus-theorem-coverage discrepancy, not a refutation or silent repair of Theorem 3.1.