# `configuration_torus.lean` — Informal Summary

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

## Overview

Documentation-only file parking two former axioms as future proof targets:
`configuration_torus_polish` (Polish space instance) and `configuration_torus_borelSpace`
(cylindrical = Borel $\sigma$-algebra) for `Configuration(TorusTestFunction\; L)`.
Their intended use (Prokhorov's theorem) is now handled by `prokhorov_configuration` in
`GaussianField/ConfigurationEmbedding.lean`, which works for any `DyninMityaginSpace E`.

## Status

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

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

---

## Future proof targets

### `configuration_torus_polish`

**Statement**: $\text{Configuration}(\text{TorusTestFunction}\; L)$ is a Polish space.

**Strategy A**: Show `configBasisEval` is a closed embedding into $\mathbb{N} \to \mathbb{R}$ (which is Polish).
Requires Banach–Steinhaus for Fréchet spaces. Estimated ~300–500 LOC. Generalizes to all `DyninMityaginSpace E`.

**Strategy B**: Nuclear Fréchet dual theory — nuclear Fréchet $\Rightarrow$ Montel $\Rightarrow$ semi-reflexive,
plus metrizability + completeness of weak-* dual. Estimated ~800–1500 LOC of nuclear space infrastructure.

---

### `configuration_torus_borelSpace`

**Statement**: The cylindrical $\sigma$-algebra on $\text{Configuration}(\text{TorusTestFunction}\; L)$
equals the Borel $\sigma$-algebra of the weak-* topology.

**Strategy**: Follows from Polish (second-countable $\Rightarrow$ Borel = cylindrical).
Same infrastructure as `configuration_torus_polish`.

---

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