Ellipsoid fitting in Rocq

This repository holds Rocq proofs, checked by the Rocq kernel, of theorems on fitting an ellipsoid to n random points x_1, ..., x_n of R^d. The base is the sharp threshold of Misiakiewicz and Wen for independent standard Gaussian points, ellipsoid_fitting_main in theories/MainTheorem.v. The probability that some positive semidefinite matrix S satisfies x_i^T S x_i = d for every i tends to 1 if limsup n/d^2 < 1/4, and to 0 if liminf n/d^2 > 1/4. The main result beyond Gaussian points is the optimal condition number, condition_kappa_theorem in extension/ConditionKappaTheorem.v. Take i.i.d. points whose law is a finite or countable mixture of product laws, with coordinates of mean 0, variance 1 and subgaussian norm at most K in every component and unconditional fourth moment kappa > 1. For every C > 1, an exact fit of condition number at most C exists with probability tending to one if n/d^2 tends to some alpha with 0 < alpha < alpha(C, kappa), and to zero if alpha > alpha(C, kappa). For 0 < alpha < alpha*(kappa), the optimal condition number of the sample tends in probability to C_star(alpha, kappa), the inverse of C -> alpha(C, kappa). This theorem rests on Theorem 1.2 of Koehler and Sohn, which extends the Gaussian threshold to independent subgaussian coordinates, and on its extension to mixtures. The repository also holds proofs of thirteen theorems from manuscripts of the OpenAI math collection, and the library GaussianAnalysis on which these proofs build.

What is proved

The statement files below, with the definitions they import, are what a reader has to trust; each has a header comment that describes it. make check checks that the code of each, comments aside, is unchanged since a commit that the checker names, that each theorem has its statement as its type, and that its axioms are among those of its expected list. Every list is a subset of check/assumptions.expected, the eight classical axioms of the Gaussian theorem: nothing from the papers is assumed. The symbols are defined in the header of each statement file, except for S1 to S7, whose short headers leave them to their code and to the definitions they import.

Result	Statement	Theorem	Axiom check
Gaussian points. Misiakiewicz and Wen (arXiv:2608.10184v1): the threshold 1/4 for a positive semidefinite fit (thm:main), well-conditioned fits of trace d below it (thm:conditioned) and the balanced positive definite alternative (cor:alternative)	theories/MainStatement.v	ellipsoid_fitting_main, MainTheorem.v	Assumptions.v
Beyond Gaussian points. Koehler and Sohn (arXiv:2608.27372v1), Theorem 1.2: for independent coordinates of mean 0, variance 1, fourth moment kappa > 1 and subgaussian norm at most K, the threshold alpha*(kappa), well-conditioned fits below it and the limit e*(alpha, kappa) of the fitting error above it	extension/UniversalityStatement.v	universality_theorem, UniversalityTheorem.v	UniversalityAssumptions.v
The same conclusions for finite mixtures of product laws, with a number of components that may grow with d	extension/MixtureStatement.v	mixture_theorem, MixtureTheorem.v

How to read the proofs

• theories/ (logical root EllipsoidFitting, 588 .v files): the Gaussian theorem, with its statement and definitions at the top.
• extension/ (EllipsoidUniversality, 177 .v files): the results beyond Gaussian points; see its README.
• applications/ (GaussianApplications, 57 .v files): T1 to T14 except T8, which was deferred; see its README.
• library/ (GaussianAnalysis, 128 .v files): general results over any R : realType; 75 of its statements were reviewed and accepted.
• check/: the axiom and identity checks of the 37 theorems and the regression tests of the checker, scripts/check_sources.py.

Building and checking

Tested with OCaml 5.3.0, Rocq 9.1.1 (rocq-core), Rocq Stdlib 9.0.0, Hierarchy Builder 1.10.3, MathComp 2.6.0, MathComp finmap 2.2.4 and MathComp-Analysis 1.16.0 (with reals-stdlib and analysis-stdlib). In a new opam switch:

opam switch create ellipsoid-fitting ocaml-base-compiler.5.3.0
opam repo add rocq-released https://rocq-prover.org/opam/released
opam repo add coq-released https://coq.inria.fr/opam/released
opam install --deps-only ./rocq-ellipsoid-fitting.opam
make build ROCQ_SWITCH=ellipsoid-fitting JOBS=3

ROCQ_SWITCH= uses the rocq on your PATH; without it, the Makefile uses the switch rocq-analysis. With 12 GiB of memory, use JOBS=3. The package has no install step: the modules are used from the clone. Without Rocq, in a clone with its full history, python3 -I -B scripts/check_sources.py --before-build applies the checker's rules to the sources: no Admitted or Axiom, the statement files unchanged, the pinned files intact.

A bare make runs make check, which applies these rules, builds, then compiles the check files and compares their outputs with the expected ones. It runs in the pinned Docker image ellipsoid-rocq:2026-10-01 (image id sha256:d28a2af774271dc1c3592aa423b064ae134a16bc22220ff5faf897b7aa9468fb), which is not public. Elsewhere it is expected to fail: the checker requires OCaml 5.3.0, findlib 1.9.8 and a rebuilt exporter plugin identical to the one that wrote the references of check/identity/. It last passed on 25 October 2026, on commit 5893184e (run d8bb8f380183817de780a550701eabc6); the later commits change only documentation and metadata, whose content the checker does not read. The GitHub workflow build.yml is disabled: its public image has OCaml 4.14.2 and findlib 1.9.6, and its last run, on 25 October 2026, stopped on a stack overflow during the build.

Documents

• The website (sources in LLM4Rocq/ellipsoid-fitting-web): the results, a guide to GaussianAnalysis with a dated phase 12 browser, how the proofs were made and PDFs of the notes.
• doc/README.md: an index of doc/.
• doc/details.md: the former long README, kept as a record, with the description of each check; its header names its out-of-date parts.
• doc/history/agent-rules.md: the rules given to the AI agents who worked on the repository, formerly AGENTS.md. The new AGENTS.md says how a change is checked and overrides them.
• doc/shifted-gaussian.tex, with doc/statements.bib: the note Centered ellipsoid fitting for non-centered Gaussian data, the informal proof of S1 to S7.

Status, citing and license

AI agents, including Claude and Codex, contributed to the formalization, review and documentation under the direction of Marc Lelarge (Inria), who maintains this research artifact. Issue reports are welcome; responses may be delayed. The MIT license (LICENSE, NOTICE) covers the code and the documents. Cite this work with CITATION.cff. The tag shifted (24 October 2026, commit 305747af) is the mathematical release, shifted-docs (27 October 2026) the documentation release, whose GitHub release has the PDF of the note: git does not track PDFs. CHANGELOG.md lists the tags.