# Formalization status

## What is proved in Lean source

The project contains explicit proof terms for:

- the collision characterization of the Vandermonde zero set;
- nonvanishing on collision-free configurations;
- the permutation-sign transformation law of the Vandermonde;
- positivity and the zero set of the Ginibre weight;
- symmetry-to-alternation under multiplication by the Vandermonde;
- permutation invariance of the coordinate sum;
- construction of the centered real Gaussian probability measure with
  variance `1 / (2n)`;
- construction of one complex Gaussian coordinate from two independent real
  coordinates;
- construction of the finite product Gaussian probability measure on `ℂⁿ`;
- the identity `complexGaussianMeasure n Set.univ = 1` and the corresponding
  `IsProbabilityMeasure` instance;
- the scalar endgame of the main proof;
- the infinite-series deficit algebra;
- the abstract three-term Pythagorean identity;
- the universal generator square-completion identity.
- the joint abstract form of both sum-of-squares identities in Theorem 1.9,
  obtained from Parseval, zero-mode geometry, and the Hermite energy formula.
- the explicit density and absolute continuity of each real Gaussian
  coordinate used to construct the complex product law;
- an algebraic definition of the univariate bivariate-indexed complex Hermite
  polynomials, including axis formulas, the first mixed polynomial, and the
  corresponding basic formal partial-derivative identities;
- the exact general formal lowering identities for both variables of the raw
  complex Hermite polynomials;
- the paper-normalized univariate complex Hermite polynomials and their exact
  `sqrt (n*p)` and `sqrt (n*q)` lowering identities;
- the multivariate normalized Hermite functions as finite coordinate
  products, with exact axis formulas and continuity;
- the exact Fréchet/Wirtinger lowering formula for every coordinate of each
  multivariate normalized complex Hermite polynomial;
- integrability of every mixed complex Gaussian monomial and every
  univariate normalized complex Hermite polynomial, together with the
  degree-zero norm identity;
- a finite dependent-product density theorem for `Measure.pi` and
  `withDensity`, together with transport of densities through
  measure-preserving measurable equivalences;
- unconditional identification of the full product Gaussian law with its
  explicit Lebesgue density, and strict positivity of the raw Ginibre mass;
- finiteness of every separable coordinate norm monomial under the concrete
  product Gaussian measure;
- a global polynomial majorant for the Vandermonde square, its Gaussian
  integrability, finiteness of the raw Ginibre mass, and the unconditional
  mass-validity and normalized-probability statements;
- Gaussian nullity of the collision locus, almost-everywhere nonvanishing of
  the Vandermonde density, and reverse absolute continuity from the Gaussian
  law to the normalized Ginibre law;
- normalized multiplication by the Vandermonde as a genuine complex-linear
  `L²` isometry from the Ginibre space into the Gaussian space, and as an
  isometric equivalence onto its range;
- the measurable inverse Vandermonde multiplier off the null collision set,
  yielding a full complex-linear isometric equivalence between the
  AE-symmetric Ginibre and AE-alternating Gaussian `L²` subspaces;
- the concrete real Ginibre pregenerator at speed `αₙ = n`, together with
  its generator and shifted-generator squared `L²` quantities, its exact
  collision-free symmetric core, and invariance under centering.
- the Vandermonde ground-state `∂̄` product rule and the unconditional exact
  ground-state Dirichlet-energy identity for smooth symmetric observables.
- smoothness and all Gaussian `L²`/derivative-square integrability conditions
  for the normalized ground-state transform, proving ground-state
  admissibility unconditionally.
- unconditional mixed Gaussian moments, one- and multivariate complex-Hermite
  orthogonality, completeness of the normalized multivariate Hermites in
  Gaussian `L²`, and Parseval decomposition by antiholomorphic degree;
- exact finite-mode lowering, Parseval, and Gaussian `∂̄` energy identities,
  including collision-safe aggregation of lowered coefficients;
- the closed zero-mode/positive-mode Hermite projections and the Parseval
  split of the transformed centered Ginibre observable;
- the symmetric Ginibre holomorphic/conjugate/remainder orthogonal geometry,
  including the exact variance decomposition;
- the normalized concrete Ginibre integration-by-parts identity and
  stationarity of the pregenerator on the collision-free smooth core;
- concrete Ginibre `L²` representatives of the pregenerator and shifted
  pregenerator, their exact norm-square bridges, and the generator/energy
  inner-product identity;
- the concrete generator square-completion identity;
- unconditional identification of the transformed Gaussian zero-mode norm
  with the Ginibre holomorphic-projection norm, including the required
  subtype-to-ambient projection bridges;
- a concrete assembly theorem for both identities of Theorem 1.9 from one
  explicit weighted Hermite energy `HasSum` hypothesis.  Its weighted-tail
  summability is derived internally rather than assumed separately.
- the noncompact Gaussian integration-by-parts ingredients and the exact
  creation/lowering coefficient identity for every compactly supported smooth
  Gaussian function;
- the weighted Hermite-energy `HasSum` identity for the compact ground-state
  transform, including identification of the normalized Vandermonde ground
  state with the algebraic antiholomorphic degree-zero span;
- invariance of every positive Hermite mode under centering, and hence the
  unconditional concrete weighted mode-energy identity;
- `concrete_theoremOneNine`, the unconditional concrete pair of exact
  sum-of-squares identities for every collision-free smooth symmetric core
  observable;
- the Hermite weighted form domain and an explicit finite-mode form core:
  truncations converge in Gaussian `L²` and their omitted weighted energy
  tends to zero, both abstractly and for the transformed concrete observable.

No theorem-valued certificate is defined.

Theorem 1.9 is unconditional on its stated collision-free smooth symmetric
core.  In particular, Lean proves the weighted mode-energy identity

```lean
HasSum (fun k => ((k + 1 : ℕ) : ℝ) *
  concretePositiveHermiteModeMass hn f hf k)
  (smoothGinibreEnergy n f / 4)
```

as `concrete_weightedModeEnergy`, and uses it in
`concrete_theoremOneNine`.  Convergence and evaluation are recorded together
as `HasSum`, rather than merely asserting an equality with `tsum`.

## Gaussian density identification

The reference Gaussian measure is now a genuine `ProbabilityMeasure`, hence
its total mass is proved to be one.  The equality between this product law and
the explicit density measure

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

is expressed by

```lean
ComplexGaussianDensityIdentificationStatement
```

and is now proved unconditionally by
`complexGaussianDensityIdentification`.  Its proof identifies the two real
coordinate densities, transports their product through the standard
measurable equivalence with `ℂ`, and then forms the finite `n`-coordinate
product.

## Earlier exact statement interfaces

The following propositions use the literal configuration space, measures,
Fréchet/Wirtinger derivatives, and holomorphic-distance infima:

- `GaussianDbarEstimateStatement`;
- `GroundStateDistanceIdentityStatement`;
- `GinibreHalfDistanceStatement`;
- `SmoothGinibrePoincareStatement`.

`SmoothGinibrePoincareStatement` is derived from five explicit analytic
hypotheses in `GinibrePoincare.Concrete.MainProofReduction`.  The five analytic
statements themselves are stated only as propositions and are not postulated
as theorems.

## Scope

The publication theorem is formalized on `IsTheoremOneNineCore`, the explicit
collision-free smooth compact symmetric core used by the concrete generator.
The accompanying `HermiteWeightedDomain` and finite-mode form-core theorem
provide the domain/approximation statement used by the Hermite argument.  No
claim is made here about a larger, separately chosen self-adjoint realization
unless it is explicitly defined in a future extension.