# `gaussian_field_axioms.lean` — Informal Summary

> **Source**: [`future/gaussian_field_axioms.lean`](../../future/gaussian_field_axioms.lean)
> **Generated**: 2026-03-10
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

Documentation-only file parking three former Gaussian field axioms as future proof
targets. None are active axioms or imported by any module. The three axioms are:
(1) `measure_unique_of_charFun` — measure uniqueness via Minlos theorem,
(2) `not_supported_of_not_hilbertSchmidt` — converse support via Kolmogorov's
three-series theorem, and (3) `supportHilbertSpace_exists` — construction of
the weighted $\ell^2$ support Hilbert space.

## Status

**Main result**: N/A (documentation only, no Lean declarations)

**Length**: 131 lines, 0 definition(s) + 0 theorem(s)/lemma(s)

---

## Future proof targets

### `measure_unique_of_charFun`

**Statement**: If a probability measure $\mu$ on $\text{Configuration}(E)$ has
characteristic functional $\int e^{i\omega(f)}\,d\mu = e^{-\frac{1}{2}\lVert Tf\rVert^2}$
for all $f \in E$, then $\mu = \text{measure}(T)$.

**Key blocker**: Cylinder set $\sigma$-algebra = Borel for nuclear spaces (not in Mathlib).
Estimated ~800–1200 LOC.

---

### `not_supported_of_not_hilbertSchmidt`

**Statement**: If $\sum_n \lVert T(e_n)\rVert^2 = \infty$, then a.s. $\sum_n \lvert\omega(e_n)\rvert^2 = \infty$.

**Key blocker**: Kolmogorov's three-series theorem or 0-1 law (not in Mathlib).
Estimated ~500–800 LOC.

---

### `supportHilbertSpace_exists`

**Statement**: For any positive weight sequence $w : \mathbb{N} \to \mathbb{R}_+$, there exists
a separable real Hilbert space $H_-$ with injective continuous embedding into
$\text{Configuration}(E)$, range $\{\omega : \sum_n w_n \omega(e_n)^2 < \infty\}$,
and inner product $\langle x, y\rangle = \sum_n w_n\, x(e_n)\, y(e_n)$.

**Key blocker**: Completeness via Banach–Steinhaus (available in Mathlib, needs adaptation).
Estimated ~300–500 LOC.

---

*This is a documentation-only file with no Lean declarations.*