How round can a random ellipsoid be?

Read the mathematics. Find the exact theorem.

The Rocq repository is public. This article explains the optimal-condition theorem at fourth moment three and its proof. The library overview, a section of the released-result guide, documents the reusable mathematics: the nine subject areas and 128 modules of the release. The declaration browser, with search and full signatures, is a dated snapshot of phase 12 (13 October 2026). The released-result guide covers the wider released development: other fourth moments, translated samples, reusable probability and matrix results, and applications including exponential PSD-rank bounds.

The latest mathematical release covered here is shifted (24 October 2026), which includes phase14. The commits after the tag, through the documentation release shifted-docs (27 October 2026), change no Rocq statement or proof. The numerical curve below remains an illustration, not a proof or a finite-dimensional simulation.

What the earlier results established

Ellipsoid fitting is connected to matrix decomposition and statistics. Saunderson, Chandrasekaran, Parrilo and Willsky related it to correlation matrices and the separation of a matrix into diagonal and low-rank parts. These connections help explain why an apparently geometric question appears in factor analysis.

1. 2024

   Maillard and Kunisky used the replica method from statistical physics to predict the transition and the spectral shape of fitting matrices. These calculations supplied detailed predictions, rather than a rigorous proof.

2. 2025

   Bandeira and Maillard proved a sharp transition for approximate fitting, with spectral restrictions. Their Gaussian comparison identifies when the error can become small. Small error alone still leaves the exact equations unresolved.

3. 2026

   The Gaussian exact-fitting transition was proved in work by Misiakiewicz and Wen, de la Cerda, Potechin, Tulsiani and Xu, and Koehler and Sohn; Arslan gives a further result. The Gaussian threshold itself is therefore part of the foundation for this project.

The closest antecedent is Koehler and Sohn’s universality theorem. For independent subgaussian coordinates, it shows that the fitting threshold depends on the common fourth moment κ through a scalar function α_⋆(κ). Gaussian coordinates are one case: κ = 3 gives α_⋆(3) = 1/4.

The same paper already proves convergence of the optimal fitting error at every positive sampling density for a class of dependent data. That result assumes, among other conditions, a dimension-free variance tensorization inequality. The extension here reaches mixtures outside that assumption and supplies exact fitting. Merely allowing some dependence, or proving an error limit at all positive densities, would not describe the distinction accurately.

Three claims to keep separate

Bandeira and Maillard, Section 3.1.3, already study the cone of positive semidefinite matrices whose largest eigenvalue is at most C times the smallest, and its asymptotic Gaussian-width function f(C). Our calculation identifies their implicitly defined function, in their normalization, as

The explicit calculation is a refinement of an existing width problem. The strongest contribution is the sharp optimal-condition theorem for exact fitting. That theorem appears new in the sources checked; publication priority remains unconfirmed by the targeted search.

One hidden label can couple a whole point

To generate a point from a mixture, first draw a label a with probability w_d,a. Then draw its coordinates independently from laws μ_d,a,1, …, μ_d,a,d. Once the label is hidden, the coordinates may be strongly dependent. The point law is

Different points receive independent labels. The theorem permits dependence within a point; the sampled points themselves remain independent and identically distributed.

The component assumptions are substantial, but easy to state:

• Every component coordinate is centered and has variance one.
• One constant K works in the tail bound E exp(Z²/K²) ≤ 2, for every dimension, label and coordinate. This is a uniform subgaussian assumption.
• The fourth moment equals the same κ > 1 after averaging over labels, coordinate by coordinate. Individual components may have different fourth moments.

The number of finite components may grow arbitrarily with the dimension. Countably many components are also allowed, without a prescribed rate of decay for their weights.

Under these assumptions, the fitting threshold remains α_⋆(κ). Below it, there is a positive definite exact fit with a condition bound depending only on the fixed parameters. Above it, there is no positive semidefinite fit with high probability. The normalized, trace-constrained squared fitting error also has the same deterministic limit at every α > 0. Zero limiting error at the critical density does not settle the probability of exact fitting there.

The fourth-moment condition explains why this is more than an application of the product theorem to each component. The components need not satisfy its common-fourth-moment assumption individually. The proof must average some estimates over labels while keeping other estimates uniform conditional on those labels.

Mixture universality has precedents in other models, notably the work of Dandi, Stephan, Krzakala, Loureiro and Zdeborová on generalized linear models. Those results concern risks and Gibbs measures under their own hypotheses; an exact positive definite quadratic interpolant requires additional work.

The sharp optimum for exact fitting

The condition number of a positive definite matrix is the ratio of its largest eigenvalue to its smallest. It measures how unequal the ellipsoid’s axes are:

Draw the points independently from an admissible finite or countable mixture with averaged fourth moment three, and fix a target C > 1. The sharp optimal-condition theorem says that exact fits satisfying cond(S) ≤ C have probability tending to one below α_C and to zero above it. This statement concerns the actual sampled data. No claim is made at equality.

The curve increases continuously from 0 to 1/4 as C goes from 1 to infinity. Its inverse, denoted C_⋆(α), gives the limiting optimal condition number among all exact fits, for 0 < α < 1/4. “Optimal” here means an infimum; the statement does not assume a minimizing matrix exists for each finite sample.

Why the optimized formula has this form

The curve measures how much Gaussian matrix energy survives after imposing the condition-number bound. The formula subtracts the energy lost in the best possible spectral clipping. Here “energy” means squared Frobenius norm: the sum of the squared eigenvalues.

Write K_C for the cone of positive semidefinite matrices satisfying λ_max(S) ≤ Cλ_min(S). Its useful measure of size is the statistical dimension: the expected squared length of the projection of a standard Gaussian matrix onto the cone. This acts like an effective number of degrees of freedom when imposing random linear constraints. It belongs to the established conic-geometric framework; Bandeira and Maillard already consider this particular cone.

1. A condition bound means fitting the spectrum inside an interval. Membership in K_C means that, for some t ≥ 0, every eigenvalue lies in [t, Ct]. To approximate a symmetric Gaussian matrix by such a matrix, keep its eigenvectors and clip its eigenvalues:

The scale t is free. Choose the interval that requires the least total squared movement of the eigenvalues.

2. The semicircle law turns that movement into two tail costs. Divide the eigenvalues of a standard Gaussian symmetric matrix by √d. Their limiting law ν_sc has density √(2 − z²)/π on [−√2, √2]. If Z has this law, then EZ² = 1/2. Define the upper-tail moments m(u) = E(Z − u)₊ and v(u) = E(Z − u)₊², where a₊ = max(a, 0). The squared clipping error is

The first term is the cost of raising the lower tail; the second is the cost of cutting the upper tail. Symmetry of Z gives E(t − Z)₊² = v(−t).

3. Subtract the smallest clipping cost from the total energy. Projection onto a closed convex cone satisfies a Pythagorean identity: the original squared length equals the projected squared length plus the squared distance to the cone. For a standard Gaussian matrix G in the space of symmetric matrices with the Frobenius inner product, this gives

Divide by d² and let the dimension grow. The total energy tends to 1/2, and the best clipping cost gives the distance term. The limiting statistical dimension per d² is therefore

The optimizing equation also has a direct interpretation. Increasing t raises the floor by dt, but raises the ceiling by C dt. At the optimum, the marginal cost of raising the floor balances the benefit of lifting the ceiling:

This root characterization and its uniqueness are short mathematical consequences of the formal curve lemmas, rather than separately exported formal statements.

The endpoints now have a geometric explanation:

• At C = 1, the interval collapses to a single value. Only nonnegative scalar matrices remain. The cone is a ray, so its statistical dimension divided by d² vanishes: α₁ = 0.
• As C → ∞, the optimal clipping approaches z ↦ z₊. Symmetry means that half of the total spectral energy 1/2 survives, giving the limit 1/4.

This calculation explains the geometric threshold. Proving that it governs exact fitting of the actual quadratic data, including the stated mixtures, is the additional theorem. The Gaussian projection calculation supplies the candidate curve; comparison and exact correction establish its role for the sampled points.

The exact optimized curve and its root characterization were not located in the sources checked. The leading coefficient 8/(3π) near the threshold is already obtainable from the trial profiles in Bandeira–Maillard and Misiakiewicz–Wen, although neither paper states it. The contribution here includes the matching lower bound and transfer to exact fits on data.

Endpoint asymptotics and earlier condition bounds

At low density the optimum approaches a sphere. Near the fitting threshold it diverges at an explicitly determined rate:

Earlier bounded-conditioning results do not identify this optimum. For example, Misiakiewicz and Wen, Remark 3.6, give a condition bound of order (1/4 − α)⁻² for the fit their proof constructs. Here the optimal limit grows as 8 / [3π(1/4 − α)]. Their construction bound does not assert optimality. In their Gaussian comparison model, their trial spectral profile already yields the same leading coefficient 8/(3π). The exact curve and the matching lower bound for data are stronger conclusions.

These are successive limits: first let the dimension tend to infinity at fixed density, then approach an endpoint of the curve. The theorem does not give a joint critical-window limit.

Gaussian geometry, then an exact correction

The proof has to solve two different problems. It must locate the threshold accurately, and it must turn a small residual into a solution of every equation. The first task uses Gaussian comparison. The second uses interpolation with control of the matrix perturbation.

1. The cone tells us where the threshold should be

A condition bound restricts the fitting matrix to a convex cone: all its eigenvalues must lie in some interval [t, Ct] with t ≥ 0. The common scale t is free. To project a symmetric matrix onto this cone, keep its eigenvectors and clip its eigenvalues to the best such interval.

This reduction is an established idea in condition-constrained matrix approximation. The role of cone size in Gaussian phase transitions is likewise part of the theory developed by Amelunxen, Lotz, McCoy and Tropp. Bandeira and Maillard, Section 3.1.3, already study this cone and its width function f(C). They obtain bounds using a trial spectral profile, without solving the full optimization.

Here the full scalar optimization evaluates that existing width problem in the semicircle limit. The mean squared clipping error is v(−t) + v(Ct); subtracting its minimum from 1/2 gives α_C. Gaussian min–max comparison produces a small-residual witness below this threshold and a positive residual gap above it. These comparison tools build on Gordon’s work and the convex Gaussian min–max method.

2. Why the dependent features still compare to Gaussian ones

The actual measurements are rank-one quadratic forms. Introduce the centered matrix feature W_i = (x_ix_i^⊤ − I)/√d. Conditional centering and unit variance, together with averaged fourth-moment matching, give the same covariance as a tractable Gaussian matrix model.

Covariance matching is only the start. The proof also bounds fluctuations of quadratic functions of the features and tails of their linear functions. The extra variance caused by mixing is controlled uniformly in the number of labels. This lets a barrier-based replacement argument exchange the feature rows for Gaussian rows one at a time. The comparison follows the universality route of Koehler and Sohn; the mixture estimates justify using it for the present dependent laws.

The Gaussian comparison model has Gaussian matrix features. It is not simply a new sample of Gaussian points: outer products of Gaussian points are themselves non-Gaussian.

3. Small error becomes zero error

Suppose the density is below α_C. First work with a slightly stricter condition bound C₋ < C that still admits a Gaussian witness. The space between the two bounds leaves room for a perturbation.

The barrier argument gives a data matrix with small average residual and a controlled largest residual. A separate interpolation theorem produces a symmetric correction Δ that removes all residual differences. Its operator norm, the largest absolute eigenvalue, is small enough to fit inside the reserved spectral margin. The corrected matrix stays positive definite and obeys the target condition bound. Its quadratic values are all equal and positive; rescaling makes them all exactly one.

This correction is where conditional independence is particularly useful. Given all point labels, the coordinate estimates hold uniformly over the component laws. Small-ball bounds prevent the interpolation map from becoming too degenerate. Averaging over labels then gives the desired statement for the mixture.

Above the threshold, the proof uses the other half of Gaussian comparison. An alleged exact fit would contradict the positive residual gap. Applying these two conclusions at condition bounds just below and just above C_⋆(α) proves convergence of the optimum.

4. A carefully chosen truncation handles countably many labels

Retain enough labels that the discarded mass is at most (d + 1)⁻³. Replace the tail by one product law whose coordinate marginals are the normalized tail marginals. This preserves the component assumptions and the averaged fourth moments exactly.

The original and truncated samples can differ only when a tail label is drawn. That probability is at most n times the tail mass, which tends to zero on the scale n ≍ d². The finite theorem therefore transfers. The proof preserves its constants; the separate formal statements each quantify their constants existentially.

Strong dependence can coexist with exact fitting

A two-component example makes the gain in scope concrete. Start from the uniform law on [−√3, √3]. Tilt it in two opposite directions using a bounded, centered fourth-degree Legendre polynomial. For each point, choose one sign and use that tilted law for every coordinate.

Each coordinate still has the original uniform marginal. Yet many coordinates together reveal the hidden sign. The mixture satisfies the fitting theorem at fourth moment κ = 9/5, while a standard tool for controlling dependence becomes exponentially costly.

That tool is variance tensorization. It asks whether the variance of every bounded function can be bounded by a constant T times the sum of its expected conditional variances when one coordinate is allowed to vary and all others are fixed. For a product law, T = 1 works. In this latent-sign example, for every fixed tilt strength 0 < s ≤ 1, every valid T eventually satisfies

The reason is intuitive: a function that guesses the hidden sign has substantial global variance, but changing one coordinate usually does not change its guess. A matching upper bound in the broad sense of exponential growth is also proved; the two exponential rates are not asserted to coincide.

This supplies a concrete separation from results requiring a dimension-independent tensorization constant. Exact fitting survives even when that hypothesis fails badly. The paired-coordinate example gives another specialization, with fitting constants uniform over its full admissible dependence interval. Neither example should be mistaken for the fourth-moment-three setting of the optimized curve.

A rare impossible point explains the robustness scale

Let Q_d be an admissible mixture and let P_d be another point law. Total variation measures their largest probability difference on a measurable event. For a sample of n independent points, the standard product bound is

Consequently, d² TV(P_d, Q_d) → 0 transfers the fitting conclusions. When the reference fourth moment is three, it transfers the optimal-condition curve as well. The perturbed law needs no moment or tail assumptions. All that matters for this argument is the probability of distinguishing the entire sample from the reference sample.

Why require a little less than order d⁻²? Start from an admissible finite mixture and contaminate a point with probability λ/n by replacing it with zero, where λ > 0 is fixed and n is eventually larger than λ. A zero point can never satisfy x^⊤Sx = 1. In the subcritical regime, the clean sample fits with probability tending to one, but the contaminated sample’s fitting probability tends to

More precisely, the fit probability equals this factor times the clean fit probability, and n TV ≤ λ. The finite-sample identity is a separate proved lemma. The example shows that an order-d⁻² assumption cannot guarantee fitting probability tending to one for every perturbation.

The total-variation inequality itself is elementary and well established. Its role here is to attach robustness to the stronger exact-fitting and optimal-condition results.

The boundary of the theorem matters

Countably many mixture components do not automatically cover a continuously distributed hidden variable. The project constructs a continuous mixture whose point law, in every dimension d ≥ 2, has total-variation distance one from every countable mixture of product laws.

Its first two coordinates lie on the relation y = x or xy = −1. A countable collection of product laws can place mass on that relation only through countably many relevant atoms. Removing the corresponding first coordinates leaves a set of full mass for the continuous mixture and zero mass for every competing component. This is a measure-theoretic obstruction to the truncation-and-transfer strategy. It is not a theorem that these continuously mixed points fail to fit.

Other questions also remain beyond the statements: fitting probabilities exactly at a threshold, joint limits as the density approaches criticality with the dimension, and uniform limits as the fourth moment approaches one.

The central contribution is the sharp optimal-condition theorem for exact fitting of the actual data: at averaged fourth moment three, it identifies both the threshold under each condition cap and the limit of the best attainable condition number, including for admissible finite and countable mixtures. Its explicit curve refines an established Gaussian-width problem, and probability-level transfer makes the conclusions robust to sufficiently small perturbations of the point law.

Provenance of the proofs and scope of the contribution

This appendix also appears as Appendix B of the mathematical write-up of 15 October 2026 (earlier notes; sources not published). Numbered section and lemma links open the corresponding page of that PDF.

The main contribution is the sharp prescribed-condition theorem for the stated mixture class, together with the calculation of its curve $\alpha(C,\kappa)$. Much of its proof architecture is inherited. This appendix identifies the inherited results, the arguments adapted to new constraints, and the particular conclusions obtained here. “New” below means additional mathematical content relative to the cited antecedents; the targeted comparison has not established publication priority. The source versions are those in the bibliography, checked on 12 October 2026.

A known theorem can have a new formal proof without becoming a new mathematical result. An extension can require a substantial argument while retaining an existing method. An elementary corollary can have useful new scope without constituting a new proof technique. The account below applies these distinctions to the dependencies of Sections 10–13.

Results and analytic inputs inherited from the literature

The unrestricted fitting problem.

The Gaussian conclusions in Section 7 come from Misiakiewicz and Wen (2026), Theorems 1.2–1.3, Corollary 1.4. The fixed trace and fixed fitting level are simultaneous constraints; their conjunction is an imported theorem, not a consequence of rescaling an arbitrary fit. The row-coupling argument that passes from a fixed density to a one-sided bound on $n/d^2$, and the separation argument for the balanced certificate, are standard deductions.

Koehler and Sohn (2026), Theorem 1.2, Proposition 1.4(ii), Theorem 1.7 supply the independent-coordinate threshold, Gaussian loss, and a general all-density loss theorem. Thus neither fourth-moment dependence of the unrestricted threshold nor convergence of the loss at every positive density is new here. The extension concerns the admissible dependent mixtures, including examples without a dimension-independent variance-tensorization bound, and the sharp constraint on the condition number. Existence of some bounded-condition fit was already included in their Theorem 1.2(i); optimizing its condition number is a further claim.

The unrestricted scalar calculation.

Section 10.1 closely adapts Koehler and Sohn (2026), Lemmas 5.7–5.9 and Proposition 5.10. The cutoff equation and the unrestricted fourth-moment duality belong to that antecedent. They are retained to fix normalizations and identify the limiting range of the constrained curve. The signed dual problem for the clipped profile in Section 10.4 is a different calculation.

The probabilistic comparison machinery.

Gaussian concentration, Gordon comparison, and the convex Gaussian min–max theorem are established inputs (Gordon (1988); Thrampoulidis, Oymak and Hassibi (2015)). The projection interpretation of Gaussian width and its connection with statistical dimension are also established (Amelunxen, Lotz, McCoy and Tropp (2014), Theorem I, Proposition 10.2). Their use in Section 11.5 does not introduce a new comparison principle. The witness and gap apply these tools to the evaluated cone, track its inner and outer radii, and remove the free intercept by projecting off the constant vector. Their explicit constants are quantitative bounds for this application; no sharpness is claimed for those constants.

On the data side, the direct source is Koehler and Sohn (2026): Theorem 2.9 and Section 2.2.3 for barrier comparison; Propositions 2.1 and 2.6 and Section 4.2 for approximation and feature regularity; Theorems 1.9 and 2.3 and Section 3 for interpolation; Proposition 2.4 for vector anti-concentration; and Lemmas 2.11–2.12 and Section 4.3 for regularization removal. The Lindeberg replacement, leave-one-out residual estimate, sparse and light-tail decomposition, and ridge-removal strategy in Section 12 follow this architecture. These substantial ingredients should receive credit even where the exposition states their usable form instead of repeating their proofs. The vector anti-concentration bound used in interpolation and the small-ball localization used in ridge removal are distinct inherited inputs.

The condition cone: known geometry and the added calculation

The object and the projection method are known.

Tropp (2015), Sections 3.1–3.2 treats the condition cone and its dual. Bandeira and Maillard (2025), Section 3.1.3 studies the same cone and its asymptotic width: Lemma 3.5 in arXiv v2, Lemma 3.6 in the published version. The curve at fourth moment three evaluates their width function, with the normalization $f(C)=2\sqrt{\alpha_C}$. It is not the introduction of a previously unknown cone or Gaussian width problem.

Clipping eigenvalues to $[t,Ct]$ and optimizing the scalar level is established condition-constrained matrix approximation. The primary abstract of Tanaka and Nakata (2014) confirms the reduction for unitarily invariant norms; we do not assign a theorem number from its unavailable full text. Won et al. (2013), Theorem 1, Section 2.2 gives a related clipping optimization for a covariance likelihood, a different objective. Spectral alignment, convex projection, and scalar first-order optimality are therefore not claimed as original methods.

What is calculated here.

Sections 10.2–10.5 solve the condition-constrained semicircle problem for every $C>1$ and $\kappa>1$. The particular addition is the coupled pair of clipping points, its unique root, and the identification of the optimized value with $\alpha(C,\kappa)$. The root argument does not assume monotonicity of the auxiliary map $L_{C,\kappa}$. The optimality remainder stays coercive for negative $c=(\kappa-3)/2$, since $1+c>0$. The signed scalar dual has a minimum for $c>0$ and a maximum for $c<0$; using one direction for both signs would not prove the stated range. These are specific derivations for the constrained problem using ordinary convex and quadratic optimization.

The integral and arcsine formulas, strict monotonicity, full range, inverse, and fourth-moment-three compatibility complete that characterization. They are consequences of the optimized profile, proved by integration, perturbation, and continuity. Replacing an almost-everywhere admissible profile by its pointwise clipped version is likewise an elementary representative argument. None of these methods is a separate originality claim.

What the endpoint coefficient establishes.

The lower-clipping trial of Bandeira and Maillard (2025) and the positive-part-plus-constant trial of Misiakiewicz and Wen (2026), Lemma 2.2 already yield the leading coefficient $8/(3\pi)$ after expansion; the calculation is displayed in Section 8. The papers do not state that expansion, but its availability from their trials prevents a claim that the coefficient itself is new. The additional conclusion is the matching obstruction, the exact curve at all $C$, and its transfer to exact data fits. Section 10.7 also derives the small-density expansion and controlled remainders from the curve. Inverting the curve gives the asymptotic of $C_\star$; inversion is not an independent method.

The replica prediction of Maillard and Kunisky (2024), Sections 1.3.1 and 3.3 is a conceptual antecedent: it optimizes a lower eigenvalue constraint. It is one-sided, so it neither imposes the ratio constraint nor supplies the rigorous theorem proved here.

The fourth-moment deformation: a substantive adaptation

The antecedent is more than the semicircle law.

The map $T_\kappa$, Haar diagonal control, and diagonal-to-trace reduction already occur in Koehler and Sohn (2026), Section 5.1, Lemmas 5.13–5.14, Proposition 5.15. The present extension substitutes the condition cone $T_\kappa\mathcal K_C$ for the transformed positive semidefinite cone. The covariance map is inherited; evaluating the new constrained support function is the problem to be solved.

The added comparison argument.

Sections 11.2–11.3 maximize the trace-penalized quadratic on $\mathcal K_C$. Uniqueness gives orthogonal equivariance of the maximizer $X(H)$; the center of its weighted projection is $\mathcal A_c^{-1}H$. Rotation invariance controls the diagonal fluctuation of $X(H)$, while strong concavity bounds the possible improvement of the original objective away from $X(H)$. Both estimates are required to compare the two suprema. The second estimate makes the argument work directly for $-1<c<0$ as well as $c\ge0$, without treating the condition cone as if it were the positive semidefinite cone and had its duality properties.

This adapts the existing reduction, with an additional argument needed by the condition constraint. The elementary rotation identity itself is not new: the proof here obtains it from a two-coordinate rotation and uses an integrable equivariant maximizer, rather than conditioning on a bounded spectral profile. This is an expository variant, not a claim of priority for the identity.

The shifted limit.

Section 11.4 combines the trace penalty with the known condition-cone projection. Its finite-dimensional expression retains the random trace term until a uniform estimate removes it. The shift and clipping level both vary, so pointwise semicircle convergence would not justify substituting the random optimizing shift. A compact two-parameter net supplies the needed uniformity, and the signed scalar identity identifies the limit. The particular constrained limit is an addition here; finite nets and equicontinuity are standard tools. This separates the new limit from the familiar method used to exchange optimization and convergence.

Mixtures and the sharp threshold for data

Mixture regularity is an additional verification.

Section 12.1 conditions on the latent label for the product estimates, then uses total variance. The covariance of a component need not equal the averaged covariance. Its fluctuation contributes the additional squared covariance-spread term in Lemma 12.1. Controlling that term proves feature regularity for the full mixture without imposing dimension-independent tensorization on the point law. Applying a common-fourth-moment product theorem separately to each component would miss this issue: only the averaged fourth moment is fixed. This verification extends the class of point laws covered by the fitting conclusions; the comparison theorem is inherited.

Conditional interpolation closely follows the existing proof.

Section 12.2 needs estimates uniform over independent arrays whose coordinate laws can differ between rows. The formal development tracks this uniformity in the existing sparse and light-tail argument. Once the nuclear-norm bound is available, allowing every residual follows by convex separation. Removing a range restriction is thus a consequence of the bound, not a new interpolation principle. For mixtures, conditioning on the entire tuple of labels and intersecting the exceptional sets transfers that uniform estimate without a factor depending on the number of components. This is the specific assembly needed to permit an unbounded number of labels.

The prescribed-condition assembly is the main data addition.

Sections 12.3–12.4 preserve a strict spectral margin while applying the inherited approximation and correction machinery. A finite collection of spectral windows covers the normalized condition cone. Simultaneous concentration permits a deterministic choice of window; choosing a random window first would not directly justify the expectation comparison. Below the curve, the small operator-norm correction fits all points while staying inside the prescribed condition bound. Above the curve, the Gaussian gap and control of the free intercept exclude every fit under that bound. The two directions together, for the same explicitly evaluated curve, are stronger than existence of some bounded-condition fit.

Compact-projection measurability, the second-moment bound on the intercept, and bracketing the infimum by two fixed condition bounds complete this theorem and the limit of the optimum. These are necessary technical steps using standard methods, not separate claims of mathematical originality. No attainment assumption is hidden in the argument for the optimal data condition number.

Transfers and examples: new conclusions from standard methods

Countable mixtures and robustness.

Truncation and coupling are standard. The important detail in Section 12.7 is to replace the discarded tail by one product of its coordinate-mixture marginals. This preserves the averaged fourth moment exactly, as well as the common subgaussian bound. Deleting and renormalizing the tail would not do so. Combined with constants independent of the number of finite components, this gives the countable result without a uniform tail-decay assumption.

The product estimate $\operatorname{TV}(P^{\otimes n},Q^{\otimes n})\le n\operatorname{TV}(P,Q)$ is elementary. The robustness conclusions apply it to the proved measurable fitting events and exceptional sets; they introduce no new total-variation principle. The absence of moment assumptions on the perturbed law follows from this probability-level transfer. Zero-point contamination and the limit $(1-\lambda/n)^n\to e^{-\lambda}$ identify an obstruction at the boundary scale. This shows why $o(d^{-2})$ cannot be replaced by $O(d^{-2})$ in a uniform inheritance theorem. It does not assert that every particular larger perturbation destroys fitting.

Paired and latent-sign laws.

The paired density belongs to the classical family of Sarmanov (1966). Its fourth-Legendre specialization, the full interval $[-1,7/3]$, and the two product-mixture decompositions in Section 13 are explicit calculations. Their purpose is to put the example inside the fitting theorem with constants valid at both endpoints. They are not a new construction of dependent density families. Similarly, conditioning on the latent sign gives the displayed covariance identities by standard total-covariance calculations. The particular calibration preserves the required marginal moments while making persistent dependence explicit.

Tensorization bounds.

The conditional-variance energy is classical: it is the Dirichlet form of single-coordinate heat-bath updates (Caputo, Menz and Tetali (2015), Section 1.1, equations (1.5)–(1.6)). General deterioration of functional inequalities under mixing also predates this example (Schlichting (2019)). The additive test for the linear lower bound, the bounded component-detecting test for the exponential lower bound, Hoeffding’s inequality, and comparison with a product density are standard mechanisms. The contribution is their explicit application to the same law that satisfies the fitting theorem. It gives the stated linear bound, the constants $1/15552$ and $1/2$ in the exponential lower bound, and the upper bound $2((1+s)/(1-3s/7))^d$ throughout $0\le s\le1$. The upper proof compares integrated conditional variances and retains one density ratio. The generic comparison is not claimed as new, and the exponential rates are not claimed to be optimal.

The continuous latent obstruction.

The countable-atoms and Fubini argument is a standard singular-support argument; even an atomless diagonal law illustrates its mechanism. Here the two-point conditional law on $\{a,-1/a\}$ additionally has mean zero, variance one, and bounded support. Its continuous mixture retains these calibrations, yet is at total-variation distance one from every countable product mixture in dimension at least two. The null set is chosen after the candidate countable mixture, removing all relevant coordinate atoms. This handles arbitrary competing product factors, including atomic ones. The calibrated example is the addition; the general singularity mechanism is classical, and the result makes no claim about the probability of ellipsoid fitting for this law.

What is proved here, cited here, and formally checked

The mathematical exposition proves the constrained scalar calculation, the condition-cone comparison, the mixture application, and the transfers and examples. It states the barrier comparison, nuclear-norm estimate, unrestricted Gaussian-loss result, and prescribed-trace Gaussian theorem as analytic inputs. Their complete antecedent proofs are not reproduced in this document. Appendix A identifies the corresponding internal formal proofs: the Rocq development also proves those inputs, using its listed classical axioms.

Thus the principal candidate for an original mathematical contribution is the exact curve and sharp optimal-condition theorem for the stated finite and countable mixture class, together with the adaptations above that establish it. The supporting identities, examples, and robustness results have the individual status described above. Neither formal verification nor an independently written proof establishes publication priority; that remains a qualified literature assessment.

The reusable Rocq libraries

Adapted from Appendix C of the mathematical write-up of 15 October 2026 (earlier notes; sources not published). The inventory below is updated to the shifted release; the detailed examples retain the scope of that appendix. Source paths are relative to the project root or its library/ directory; numbered links open the corresponding page of that PDF. The current library overview links directly to the public sources.

The development separates general mathematics from the ellipsoid-fitting theorems. At release shifted, library/ contains 128 Rocq modules under the logical root GaussianAnalysis. These modules construct probability laws and prove analytic, geometric, and optimization results with explicit hypotheses independent of the point model. The fitting statements and their applications reside in theories/, under EllipsoidFitting, and extension/, under EllipsoidUniversality. This appendix describes the reusable interfaces and their role in the proof. Appendix B separately addresses mathematical provenance: formalizing an established inequality in a new library is not a claim that the inequality is new.

Foundations, organization, and conventions

The library builds on MathComp’s algebra and finite-dimensional matrix types and MathComp-Analysis’s topology, measures, integration, and one-dimensional normal law. Its analytic statements are parameterized by an abstract R : realType; algebraic lemmas use weaker structures when sufficient. The paper instantiates these results at Stdlib’s real numbers through bridge modules outside the library. The code is organized for reuse within this project; no upstream incorporation into MathComp-Analysis is asserted.

Two conventions are essential when using the interfaces. A matrix’s ambient MathComp norm is the largest absolute entry. Euclidean and Frobenius geometry instead use mxdot and frobenius, and the operator norm is opnorm. Substituting the ambient norm in a Gaussian or spectral bound would change its dimension dependence. Also, probabilities and nonnegative integrals often take values in the extended reals. A real-valued expectation formula requires the stated integrability hypotheses; an integral expression alone is not a finiteness certificate.

The following counts are the source modules registered in _CoqProject at release shifted, rather than a count of individual declarations. The nine directories group topics; they are not nine independent packages or a strict hierarchy of dependencies.

Gaussian analysis, comparison, and small-ball estimates

A finite-dimensional Gaussian probability.

In gaussian/gauss.v, gauss is the standard Gaussian probability on MathComp row vectors. The characterization gauss_unique, coordinate Fubini, and block-product identities make independence available as measure identities. The matrix measurability interface measurable_fun_mxP reduces measurability to entries. The calculus modules prove gauss_ibp under derivative, continuity, and polynomial-growth hypotheses, and gauss_interpolation for smooth functions along a differentiable matrix path with the stated growth and boundedness controls. These are reusable analytic theorems, rather than formal assumptions standing in for integration by parts or differentiation under an integral.

The precise comparison interfaces.

gauss_mulmx_law identifies Gaussian linear images with the same covariance, even when their input dimensions differ. gauss_concentration gives the Gaussian exponential-moment bound for globally Lipschitz functions in Euclidean norm. gauss_poincare_lipschitz gives its variance bound; this exported result should not be confused with the more general gradient-energy Poincaré inequality.

The module comparison/cgmt.v implements the comparison for $\inf_{x\in B}\|Ax\|$ used in Section 11.5. For a nonempty set $B$ bounded by radius $\rho$ and a positive row dimension, cgmt_lower compares means with additive error $\rho$; cgmt_upper additionally requires $B$ closed and convex. Concentration and the interfaces cone_escape_zero_tail and cone_escape_lower_tail turn this into witness and separation bounds for cone sections. This is the implemented specialization, not an unrestricted arbitrary-objective min–max API.

Fourier analysis and anti-concentration.

The characteristic function is represented by its cosine and sine integrals, with multiplication implemented on pairs of reals. The Brascamp–Lieb modules prove the geometric rank-one inequality through the Mehler semigroup, first for bounded positive functions and then for nonnegative measurable functions. Combined with Gaussian regularization and whitening, this yields vector_small_ball. It allows independent, nonidentically distributed scalar laws with common second-moment and anti-concentration bounds. If the coefficient vectors satisfy $\sum_i w_iw_i^{\mathsf T}\succeq I_m$ and $\|w_i\|\le\rho$, it bounds $\Pr(\|\sum_i X_iw_i-z\|\le\eta\sqrt m)$ by $(C\eta)^m$, uniformly in $z$, provided $\eta\ge C\rho$. The constant depends only on the common moment and anti-concentration parameters. The moment-based specialization vector_small_ball_moments is used by extension/Sat/OneStage.v. If the characteristic-function modulus is integrable, cf_rV_inversion identifies a continuous bounded density by Fourier inversion. The small-ball proof does not require this result.

Matrix geometry and the spectral limit

Condition cones and deterministic interpolation.

The spectral and norm modules provide real symmetric diagonalization, Hoffman–Wielandt estimates, and operator/nuclear norm duality. In matrix/condition_cone.v, cond_cone_dist reduces the distance of a symmetric matrix to $\mathcal K_C$, for $C\ge1$, to scalar eigenvalue clipping. cond_support_sqr relates this distance to Gaussian support, and cond_slice_frobenius gives the radius bounds for its trace slice. These are deterministic geometric statements; their random spectral limit is proved separately. On the data side, range_duality_sym in matrix/nuclear.v converts a nuclear norm lower bound into a symmetric interpolating matrix with a controlled operator norm. The random-matrix and covering modules establish the estimates to which that duality is applied.

A general trace-penalized maximizer.

matrix/trace_projection.v works on any nonempty closed convex set $K$ of square matrices, not just symmetric matrices or condition cones. For $n\ge1$ and $c>-1$, define

Rotation and semicircle interfaces.

random_matrix/goe_rotation.v proves GOE rotation invariance and diagonal-fluctuation estimates for measurable equivariant matrix functions that preserve symmetry. goe_diag_var_identity assumes entrywise square integrability; goe_diag_var_tail uses truncation to avoid that assumption in its tail bound. The proof uses Gaussian invariance and elementary rotations, without constructing Haar measure.

There is a normalization change at the application boundary. For a matrix $A$ with independent standard normal entries, the library’s goe_mx is

Mixtures, scalar optimization, and transfer to data

Probability constructors and exact sample laws.

The files probability/mixture.v and probability/countable_mixture.v define mixtures on an arbitrary measurable type. They prove weighted integration, total variance for finite mixtures, and exact sample expansions tuple_prod_mixture and tuple_prod_cmixture. For countable mixtures, nonnegative integration needs measurability; signed integration additionally requires integrability under every component and summability of the weighted absolute integrals. The finite result mixture_cover transfers measurable covers of a common bad set by intersection, without a union bound over labels. The bad set itself need not be measurable.

The interface tuple_prod_tv in probability/total_variation.v bounds the discrepancy of product laws by the sum of their coordinate total variations. It permits different laws in every coordinate and needs no moments or densities. The density constructors and countable-atom lemmas support the explicit dependent examples. For reuse, density_law takes a proof that the density is valid; the totalized constructor density_prob falls back to its reference law when that condition fails.

Regularity of mixed features.

The definition regular_feature combines centering, covariance, a directional fourth-moment bound, a variance bound for quadratic forms, and positivity of the covariance operator norm. mixture_regular_feature_dot, in convex/feature_mixture.v, is a finite-mixture closure theorem for this class. Let centered components have covariance $\Sigma_i$, common fourth-moment bound $A\|\theta\|^4$, and common quadratic-form variance bound $\tau^2\|T\|_F^2$. With $\Sigma=\sum_iw_i\Sigma_i$, assume

A scalar optimizer for general laws.

The files probability/variational.v and probability/clip_profile.v separate scalar optimization from semicircle integration. For a symmetric law with finite second moment, $C\ge1$, $t\ge0$, and $c>-1$, the clipped profile $q(x)=\min\{\max\{x-a,t\},Ct\}$ is optimal for $2\mathbb E[Xq(X)]-\mathbb E[q(X)^2]-c(\mathbb E q(X))^2$ when its balance and fixed-point conditions hold. clip_optimal proves global optimality, and clip_dual_le, clip_dual_ge, and clip_dual_opt give the dual comparisons with the correct signs. The generic theorem assumes these scalar conditions; it does not solve the semicircle root equation. That solution and the arcsine formula belong to extension/ConditionKappa/.

The formal equality clip_value_ae identifies the pointwise and almost-everywhere constrained suprema for every probability law and all real $c,C$. It does not require symmetry or a second moment. The separate lemma clip_admissible_ae_integrable proves finiteness of all three integrals under a finite-second-moment assumption. This separates an elementary representative argument from the analytic assumptions of the optimizer theorem.

Measurable optimization and barrier comparison.

probability/measurable_minimizer.v proves measurability of a minimizer from quadratic growth, a fixed countable sequence approximating its value, and measurability of the objective along that sequence. Its least-squares exports measurable_ls_min and ls_min_tuple_set give measurability and invariance under changes to an unused row. Together with independent rows, that invariance justifies the leave-one-out argument. These are mathematical selections, not certified numerical algorithms.

The convex modules isolate the deterministic analysis of self-concordance, log-determinant barriers, minimizers, and insertion costs from the probabilistic replacement step. barrier_lindeberg_mean, barrier_lindeberg_variance, and barrier_lindeberg_concentration compare regularized least-squares values for two regular feature laws with the same covariance. The final interfaces use independent identically distributed rows under each law, a nonempty relatively open convex domain, a nonnegative sc_function, a nonnegative regularity parameter $\tau$, and positive ridge and barrier parameters. Both the mean comparison and concentration bound require $n\gamma\ge36$; the variance bound does not.

One hypothesis deserves care: sc_function includes divergence at the boundary along finite exit segments. The comparison permits an unbounded domain and dispenses with the additional gradient-versus-Hessian parameter bound of sc_barrier; it does not dispense with boundary blow-up. Barrier removal is a library result; the ridge-removal step is unsat_ridge_removal in extension/Unsat/Ridge.v. Section 12.2 gives the quantitative comparison used in the fitting proof.

Application boundaries and reuse

The generic library ends before the model-specific assembly. The covariance deformation of the condition cone and its spectral limit, the finite cover of condition-preserving spectral slices, and the sharp data theorem are in extension/ConditionKappa/ and extension/Condition/. Likewise, the exact product-mixture identities are generic, but replacement of a discarded label tail by a product preserving its coordinate moments is proved in extension/Countable/Truncation.v. The explicit paired, latent-sign, and continuous-latent laws remain application modules. This distinction prevents an application theorem from being mistaken for a library interface available under weaker hypotheses.

For example, the trace-projection module has logical name GaussianAnalysis.matrix.trace_projection. With the project’s load path and compiled dependencies, representative interfaces can be inspected with:

From GaussianAnalysis.matrix Require Import trace_projection.
From GaussianAnalysis.probability Require Import clip_profile.
Check trace_argmaxP.
Check clip_optimal.
Print Assumptions clip_optimal.

The source header of each module states its definitions and main results. library/README.md provides the larger declaration index; the actual theorem and its section hypotheses determine the contract. The documented toolchain is Rocq 9.1.1, MathComp 2.6.0, and MathComp-Analysis 1.16.0, with Hierarchy Builder 1.10.3.

The checker rejects library imports from either paper namespace, Stdlib’s real-analysis modules, or the MathComp bridges Rstruct and Rstruct_topology. It also rejects unfinished proofs and new axiom declarations in the checked sources. This structural independence does not mean axiom-freedom: the development uses classical foundations, and a reused lemma’s actual dependencies are those reported by Print Assumptions. Appendix A records the reports for the main theorems; those counts are not per-module axiom counts. Kernel checking establishes the formal implication, while mathematical review must still verify that the interface states the intended hypotheses and conclusion.

Sources and mathematical details

The mathematical write-up (PDF of 15 October 2026, 61 pages; earlier notes; sources not published) gives the results and assumptions explained in this article. The shifted-sample note (PDF, 20 pages, built from doc/shifted-gaussian.tex at commit 15d9fb22) covers S1–S7. The note is unchanged through the documentation release shifted-docs of 27 October 2026. For the current exact contracts, start from the released statement and proof links; the repository README records the releases and toolchain.

1. Saunderson, Chandrasekaran, Parrilo and Willsky (2012), Diagonal and Low-Rank Matrix Decompositions, Correlation Matrices, and Ellipsoid Fitting.The connection to matrix decomposition and factor analysis.
2. Maillard and Kunisky (2024), Fitting an Ellipsoid to Random Points: Predictions Using the Replica Method.Predictions for the transition and spectral geometry.
3. Bandeira and Maillard (2025), Exact Threshold for Approximate Ellipsoid Fitting of Random Points.Gaussian equivalence and approximate fitting; Section 3.1.3 introduces the bounded-condition cone and its implicit width function.
4. Misiakiewicz and Wen (2026), The Sharp SAT/UNSAT Phase Transition in Random Ellipsoid Fitting.Exact Gaussian fitting; Remark 3.6 bounds the condition number of the constructed fit, without claiming optimality.
5. de la Cerda, Potechin, Tulsiani and Xu (2026), Sharp Phase Transition for Ellipsoid Fitting.
6. Koehler and Sohn (2026), Universality and Sharp Thresholds for Ellipsoid Fitting.The direct antecedent for fourth-moment universality and the barrier comparison route.
7. Arslan (2026), The Strict Threshold for Gaussian Ellipsoid Fitting.
8. Tanaka and Nakata (2014), Positive Definite Matrix Approximation with Condition Number Constraint.Spectral optimization under a condition-number bound.
9. Amelunxen, Lotz, McCoy and Tropp (2014), Living on the Edge: Phase Transitions in Convex Programs with Random Data.Statistical dimension and Gaussian conic geometry.
10. Thrampoulidis, Oymak and Hassibi (2015), Regularized Linear Regression: A Precise Analysis of the Estimation Error.The convex Gaussian min–max comparison framework.
11. Dandi, Stephan, Krzakala, Loureiro and Zdeborová (2023), Universality Laws for Gaussian Mixtures in Generalized Linear Models.A precedent for mixture universality in a different class of models.