# Ginibre Poincaré: concrete Lean development

This version adds a genuine normalized Gaussian probability measure on `ℂⁿ`.
Each real coordinate is Mathlib's centered Gaussian law with variance
`1 / (2n)`; two such laws form one complex coordinate, and a finite product
forms the configuration law.  Lean therefore proves directly that the
reference Gaussian measure has total mass one.

The equality of this product law with the explicit density

```text
(n / π)^n exp (-n |z|²) dz
```

is proved by `complexGaussianDensityIdentification`, using locally proved
finite-product density and measure-preserving transport lemmas.

The project also defines the actual particle configuration space, collision
set, Vandermonde determinant, Gaussian and Ginibre weights, Ginibre measure,
normalized ground-state transform, real Fréchet gradient, coordinate
Wirtinger derivatives, and the exact smooth-core theorem statement.
The Vandermonde square is proved Gaussian-integrable and nonzero on a
positive-measure open set, so the Ginibre normalizing mass is proved positive
and finite and the normalized Ginibre measure has total mass one.

The public theorem `concrete_theoremOneNine` proves both exact
sum-of-squares identities of Theorem 1.9 on the explicit collision-free
smooth symmetric core.  Its proof includes the complex Hermite Hilbert basis,
lowering/creation identities, Parseval, the weighted mode-energy `HasSum`,
the holomorphic zero-mode geometry, and the concrete generator square
completion.  `transformedCenteredObservable_finiteMode_formCore` supplies the
associated finite-mode form-domain approximation.

## Build

The source archive intentionally contains no `.lake` directory and no copy of
Mathlib.  From a fresh extraction, download the pinned Lean dependencies and
their binary cache with:

```bash
make download
```

Then compile every local module and run the axiom audit with:

```bash
make check
```

`make download` runs `lake update` followed by `lake exe cache get`; the
checked-in manifest pins Mathlib and its transitive dependencies. `make check`
uses that single checkout at `.lake/packages/mathlib`, builds sequentially
with one Lean worker, and does not create another dependency tree. The default
`make` target is equivalent to `make check`. `make setup` remains an alias for
`make download`.

A successful run ends with:

```text
Lean validation of all completed modules succeeded.
```

## Scope

The exact declarations and their scope are documented in `STATUS.md`.
Theorem 1.9 is proved for `IsTheoremOneNineCore`; the project does not silently
postulate an analytic certificate or claim an unspecified larger operator
domain.