ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The positive-type Gaussian on the real line and its cyclic model

Example

Assume the Axiom of Choice. Let $G = (R, +)$ with its usual topology and put $w (s) : = \frac{e^{- s^{2} / 4}}{2 \sqrt{π}}, ξ (s) : = \sqrt{w (s)} = \frac{e^{- s^{2} / 8}}{\sqrt{2 \sqrt{π}}}, φ (t) : = e^{- t^{2}} .$ On complex $L^{2} (R, d s)$ define $(π (t) f) (s) : = e^{i t s} f (s), H_{0} : = \overline{{span}_{C} {π (t) ξ : t \in R}} .$ Then $ξ \in H_{0}$ has norm one, $H_{0}$ is a cyclic invariant Hilbert subspace, and $π ∣_{H_{0}}$ is a strongly continuous unitary representation with $φ (t) = ⟨ π (t) ξ, ξ ⟩ (t \in R) .$ Consequently $φ$ is normalized positive type and this pointed cyclic representation is unitarily equivalent to its canonical GNS representation.

Facts & Assumptions

Given: AC, the additive real group with its usual topology, and the functions $w, ξ, φ$ displayed above.

[A1]

AC implies Countable Choice; the L² Hilbert-space theorem, the half-line improper-integral comparison, and the reflection-invariance theorem assume Countable Choice (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ), $L^{2}$ with the integral pairing is a Hilbert space, A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral, For a nonzero real $c$ , dilation by $c$ multiplies Lebesgue outer measure by $∣ c ∣^{n}$ , and reflection in the origin preserves it).

[A2]

The Gaussian improper integral is $\sqrt{π}$ ; substitution applies to monotone differentiable maps on improper intervals; a mixed improper integral splits at its finite interior point (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ , Change of variable in an improper integral, Improper integrals with several singular ends).

[A3]

A nonnegative locally Riemann-integrable function with finite improper integral on a half-line has the same finite Lebesgue integral there; reflection preserves Lebesgue measure and hence nonnegative integrals. A singleton has Lebesgue measure zero, and the integral of a nonnegative measurable function over a null set is zero (A nonnegative improper Riemann integral on a half-line agrees with the Lebesgue integral, For a nonzero real $c$ , dilation by $c$ multiplies Lebesgue outer measure by $∣ c ∣^{n}$ , and reflection in the origin preserves it, Measure-preserving transformations and systems, A measurable function between measurable spaces, Integral invariance under measure-preserving maps, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, A nonnegative integral over a null set vanishes, Additivity of the nonnegative Lebesgue integral).

[A4]

The complex $L^{2}$ quotient is a Hilbert space under $⟨ f, g ⟩ = \int f \overline{g}$ , linear in the first variable; a closed linear subspace inherits a Hilbert-space structure (Complex Lp classes and Euclidean test-function conventions, Real and complex inner-product spaces and their induced length, $L^{2}$ with the integral pairing is a Hilbert space, Hilbert space, Linear subspace of a vector space, Normed subspace, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, A closed subspace of a Banach space is Banach, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset).

[A5]

The real exponential and sine and cosine are differentiable with their usual derivatives; the chain, product, and second-FTC rules apply, and $e^{- R^{2} / 4} \to 0$ as $R \to + \infty$ (The exponential function is smooth and $(\exp)^{'} = \exp$ , The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ , Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[A6]

Differentiation under the integral sign applies under a measurable integrable majorant, and dominated convergence applies to complex-valued integrands; the complex $L^{2}$ pairing uses the first-variable-linear convention (Differentiation under the integral sign, Dominated convergence, The Lebesgue integral is linear on $L^{1} (μ)$ , Integrable real and complex functions, and their integrals, Complex Lp classes and Euclidean test-function conventions).

[A7]

The complex exponential satisfies its addition law, Euler's identity and $∣ e^{i u} ∣ = 1$ for real $u$ ; its real-parameter phase is continuous. Continuous real and complex functions are Borel measurable, and Borel sets are Lebesgue measurable under Countable Choice ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , A function differentiable at $c$ is continuous at $c$ , Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Group and abelian group, The reals form a field, Topological group: multiplication and inversion are continuous, Continuous functions on Euclidean spaces are Borel measurable, Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable, Arithmetic and lattice operations preserve measurability whenever they are defined).

[A8]

For a strongly continuous unitary representation, each diagonal coefficient is continuous positive type; a cyclic pointed representation with that coefficient is uniquely unitarily equivalent to the canonical GNS representation (Continuous positive-type functions and normalization, Cyclic vector and cyclic unitary representation, Topological group: multiplication and inversion are continuous, GNS construction for a continuous positive-type function, Uniqueness of the pointed cyclic GNS representation, Diagonal unitary coefficients have positive type).

Proof

technique · direct

1.1A7

The additive real field gives the group laws for $(R, +)$ , and addition and negation are continuous by the algebra of continuous real maps on a metric space, so $G$ is a topological group.

1.2A2

Let $h_{0} (s) = e^{- s^{2} / 4}$ ; evenness, reflection of the negative improper tail, and the mixed-integral convention give $\int_{0}^{\infty} e^{- x^{2}} d x = \sqrt{π} / 2$ , so the substitution $s = 2 x$ yields $\int_{0}^{\infty} h_{0} (s) d s = \sqrt{π}$ .

1.3A5

For $R > 0$ , FTC gives $\int_{0}^{R} s e^{- s^{2} / 4} d s = 2 (1 - e^{- R^{2} / 4})$ , whose limit is $2$ ; both $h_{0}$ and $h_{1} (s) : = ∣ s ∣ e^{- s^{2} / 4}$ are continuous and nonnegative on $[0, \infty)$ , and their half-line improper integrals are respectively $\sqrt{π}$ and $2$ .

1.4A5A7

For fixed $t$ , $q_{t} (s) : = e^{- s^{2} / 4} e^{i t s}$ has derivative $q_{t}^{'} (s) = (- s / 2 + i t) q_{t} (s)$ by Euler's identity and the real product and chain rules; its continuous components are integrable on $[- n, n]$ , and their Riemann and Lebesgue integrals agree, so componentwise FTC gives $q_{t} (n) - q_{t} (- n) = \int_{- n}^{n} (- s / 2 + i t) q_{t} (s) d s$ .

1.5A4A7

The formula $∣ e^{i t s} ∣ = 1$ makes multiplication by $e^{i t s}$ a well-defined complex-linear isometry on $L^{2} (R)$ ; the exponential addition law gives $π (t + u) = π (t) π (u)$ and $π (- t)$ is its inverse, so $π$ is a unitary representation.

1.6A4A6A7

For $f \in L^{2}$ and $t_{n} \to t$ , the squared orbit difference has integrand $∣ e^{i t_{n} s} - e^{i t s} ∣^{2} ∣ f (s) ∣^{2}$ , which converges pointwise to zero and is bounded by $4 ∣ f (s) ∣^{2}$ ; dominated convergence gives $∥ π (t_{n}) f - π (t) f ∥_{2} \to 0$ , hence $π$ is strongly continuous because $R$ is metrizable.

1.7A4A8

The algebraic orbit span is linear, and its norm closure $H_{0}$ is a closed linear subspace: for $x, y$ in the closure, the metric-closure criterion approximates them by span elements within $ε / 3$ , whose sum is within $2 ε / 3$ of $x + y$ ; scalar multiples follow from norm homogeneity. Thus [A4] and the closed-subspace completeness theorem make $H_{0}$ a Hilbert space. The group law sends each orbit vector to another orbit vector, and continuity of $π (u)$ and its inverse shows $π (u) H_{0} = H_{0}$ ; by construction $ξ \in H_{0}$ is cyclic.

2.1A1A3step 1.2step 1.3

The half-line comparison turns the values in steps 1.2 and 1.3 into Lebesgue integrals; for either even function $h \in {h_{0}, h_{1}}$ , splitting into positive and negative open half-lines and the null singleton gives $\int_{R} h = 2 \int_{(0, \infty)} h$ by reflection invariance and integral additivity. Thus $\int_{R} w = 1$ and $\int_{R} ∣ s ∣ w (s) d s = 2 / \sqrt{π} < \infty$ .

3.1A5A6A7step 2.1

The functions $s \mapsto e^{i t s} w (s)$ are measurable and have modulus $w (s)$ , so they are integrable; for each fixed $s$ , differentiation in $t$ gives $\partial_{t} (e^{i t s} w (s)) = i s e^{i t s} w (s)$ , whose modulus is bounded by the integrable majorant $∣ s ∣ w (s)$ . Hence differentiation under the integral sign gives $F^{'} (t) = i \int_{R} s e^{i t s} w (s) d s$ for $F (t) : = \int_{R} e^{i t s} w (s) d s$ .

3.2A6A7step 2.1step 1.4

The boundary terms in step 1.4 tend to zero, and dominated convergence passes the truncated integrals to their full-line integrals because $∣ q_{t} ∣ = e^{- s^{2} / 4}$ and $∣ s q_{t} ∣ = ∣ s ∣ e^{- s^{2} / 4}$ are integrable by step 2.1; therefore $\int s q_{t} (s) d s = 2 i t \int q_{t} (s) d s$ , or $\int s e^{i t s} w (s) d s = 2 i t F (t)$ .

4.1A5step 2.1step 3.1step 3.2

Steps 3.1 and 3.2 give $F^{'} (t) = - 2 t F (t)$ , while step 2.1 gives $F (0) = 1$ ; the product and chain rules show $(e^{t^{2}} F (t))^{'} = 0$ , so applying the real FTC to each component on every compact interval yields $F (t) = e^{- t^{2}}$ for all $t \in R$ .

5.1A4A8step 2.1step 4.1step 1.5step 1.6step 1.7

The norm identity $∥ ξ ∥_{2}^{2} = \int w = 1$ holds, and the first-linear $L^{2}$ pairing gives $⟨ π (t) ξ, ξ ⟩ = \int e^{i t s} w (s) d s = F (t) = e^{- t^{2}}$ by step 4.1; [A8] now gives normalized positive type and identifies $(π ∣_{H_{0}}, H_{0}, ξ)$ with the canonical GNS triple.

6.1A1A3A8∎

AC is propagated through Countable Choice exactly for the L² and measure-theoretic suppliers in [A1] and [A3], and is used directly by the canonical GNS construction and pointed uniqueness in [A8]; the Gaussian integral calculation and the phase representation use no further choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

249 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Semyon Dyatlov, Lecture notes for 18.155: distributions, elliptic regularity, and applications to PDEs (standard reference, not scraped)
Bekka, de la Harpe and Valette, Kazhdan's Property (T) (standard reference, not scraped)
Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (standard reference, not scraped)