Formal Lean dependency explorer

Constant references extracted from compiled declaration types and proof/definition bodies. Arrows point from a dependency to the selected declaration.

Proof library and Solution included; Challenge excluded. Mathlib and Lean are terminal boundary nodes in this view.

Correspondence and publication status

Dependency views refreshed on 2026-10-09 from the verified readability revision. All 32 selected endpoints include the five named result interfaces; twelve thematic views cover the source import groups.

The 2026-10-08 proof additions address the independent review findings, including matrix H¹ derivative identification, literal integrated pointwise Γ₂, unrestricted operators and auxiliary assertions. See independent statement review and precise domains, final build and audit evidence and live publication evidence. Palomar v1 is publicly registered for the earlier Theorem 1.1 snapshot. Revision 9nfa8zoiz8te passes official mechanical verification; its editorial review and new registration remain unavailable while status/review endpoints return HTTP 500. Dependency edges record compiled references; they are separate from statement correspondence and external registration.

Full-paper overview

For ordered mathematical reading routes and the named result interfaces, see the reading guide.

The proof-library objective covers all asserted results in Sections 1–2 and Appendices A–B. The current independent review records how the 2026-10-08 additions resolve previously identified domain bridges and auxiliary assertions, together with precise domain qualifications. Theorem 1.9 is one component. Problems 1.11, 1.15 and 1.16 remain open; Appendix C experiments are outside certification.

This thematic import diagram shows direct dependencies of paper assembly. All twelve subproject diagrams cover the other groups, including Gaussian log-Sobolev and stochastic calculus foundations. These group imports are distinct from the exact declaration references below. See numbered coverage and proof routes and verification and restrictions.

dependencies Source imports — see independent statement review ComplexGaussianHermite Complex Gaussian and Hermite analysis DeficitsEquality Poincaré deficits and equality Endgame Paper assembly ComplexGaussianHermite->Endgame GaussianLSI Gaussian log-Sobolev and entropy DeficitsEquality->Endgame GeneratorSemigroup Diffusion operators and analytic semigroups GaussianLSI->Endgame GinibreMeasureGeometry Ginibre measure and holomorphic geometry GeneratorSemigroup->Endgame MatrixLift Matrix lift and eigenvector overlaps GinibreMeasureGeometry->Endgame NonQuadratic Nonquadratic potentials MatrixLift->Endgame PolynomialRadial Polynomial, radial and equilibrium sectors NonQuadratic->Endgame StochasticDynamics Ginibre stochastic dynamics PolynomialRadial->Endgame WeakSobolev Weak Sobolev domains and collision capacity StochasticDynamics->Endgame WeakSobolev->Endgame

Orange: statement/typeBlue: proof/definition bodyPurple: both

Click a dependency to inspect its direct references. The complete dependency lists below are searchable with your browser’s Find command.

Statement/type references

    Proof/definition references

      Interpretation

      These are direct syntactic constant references in Lean’s elaborated environment. They include private and generated declarations. Selecting dependencies repeatedly explores the local transitive closure. An external node is a boundary, not a claim that it has no further dependencies. Definitions as well as theorems occur in proof terms; this graph does not replace the axiom audit or certify correspondence with the paper.

      Graph documentation · Complete declaration JSON · Complete local import DAG (DOT)