Pipeline-generated

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.

Unital star algebra and positive normalized state — Examples

1 · Prerequisites

2 · Summary

Assume Countable Choice. For the finite-support Weyl algebra on $S = R^{2}$ defined in Positive Weyl state without a continuous field generator, the Weyl relations and positivity of a normalized state do not ensure that every GNS orbit map $t \mapsto π (W (t v)) ξ$ is norm-continuous for every $v \in S$ and every vector $ξ$ in the GNS Hilbert space. The counterexample constructs a state whose cyclic unit vector $Ω$ satisfies $∥ π (W (t v)) Ω - Ω ∥ = \sqrt{2}$ whenever $v \neq 0$ and $t \neq 0$ , so the orbit is discontinuous at $t = 0$ in every nonzero direction. The construction is mathematical and makes no claim about a physical vacuum or preparation.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Positive Weyl state without a continuous field generator

Statement refuted

Assume Countable Choice, the hypothesis used to form the Hilbert completion in GNS Hilbert reconstruction with invariant operator domain. The claim that positivity and the Weyl relations alone make every GNS one-parameter unitary group $t \mapsto π (W (t v))$ strongly continuous for every $v \neq 0$ is false, even for the algebraic Weyl algebra of the standard symplectic plane.

Facts & Assumptions

Given: Countable Choice, $S = R^{2}$ , the displayed nondegenerate alternating form $σ$ , and the algebraic Weyl relations above.

[F1]

GNS Hilbert reconstruction with invariant operator domain: under Countable Choice, a positive normalized state on a unital complex star algebra has a Hilbert-space GNS representation on a common invariant dense domain, with cyclic unit vector and state recovery.

[A1]

The form $σ$ is real-bilinear and alternating: $σ (f, g) = - σ (g, f)$ and $σ (f, f) = 0$ for every $f, g \in S$ .

Example data

Let $S = R^{2}$ with standard symplectic form $σ ((q, p), (q^{'}, p^{'})) : = q p^{'} - p q^{'}$ . Define $A_{W}$ to be the complex vector space of finite linear combinations of formal basis elements $W (f)$ , $f \in S$ , with bilinear multiplication and involution specified on basis elements by

$W (f) W (g) : = e^{- i σ (f, g) / 2} W (f + g), W (f)^{*} : = W (- f), 1 : = W (0) .$

For the false claim, a positive normalized functional is a complex-linear $ω : A_{W} \to C$ with $ω (1) = 1$ and $ω (a^{*} a) \geq 0$ for every $a$ . Define

$ω (W (f)) : = {\begin{cases} 1, & f = 0, \\ 0, & f \neq 0, \end{cases}$

and extend linearly to finite sums. This Weyl algebra is algebraic: its vectors have finite support, and no norm or topology on $A_{W}$ is assumed. The Hilbert-space strong continuity considered below is norm continuity of each GNS orbit $t \mapsto π (W (t v)) ξ$ .

Counterexample

technique · direct

1.1givenA1algebra

Bilinearity of $σ$ gives $σ (f, g) + σ (f + g, h) = σ (g, h) + σ (f, g + h)$ , so the phase factors in $(W (f) W (g)) W (h)$ and $W (f) (W (g) W (h))$ agree. Also $(W (f) W (g))^{*} = e^{i σ (f, g) / 2} W (- f - g) = W (- g) W (- f)$ by alternation, and $W (0)$ is a two-sided unit. Thus the displayed operations define a unital complex star algebra.

1.2givenA1algebra

For $a = \sum_{f \in F} c_{f} W (f)$ with finite support $F \subset S$ , the Weyl relation gives $a^{*} a = \sum_{f, g \in F} \overline{c_{f}} c_{g} e^{i σ (f, g) / 2} W (g - f)$ . Only the terms $g = f$ contribute to $ω (a^{*} a)$ , and $σ (f, f) = 0$ , so $ω (a^{*} a) = \sum_{f \in F} ∣ c_{f} ∣^{2} \geq 0$ ; also $ω (W (0)) = 1$ . Hence $ω$ is a positive normalized state.

2.1F1givenstep 1.2

By [F1], its GNS quotient has dense span of the classes $[W (f)]$ . For $f, g \in S$ , $([W (f)], [W (g)])_{ω} = ω (W (g)^{*} W (f))$ is $1$ if $f = g$ and $0$ otherwise; these classes are an orthonormal family with dense span. Left multiplication satisfies $π (W (h)) [W (f)] = e^{- i σ (h, f) / 2} [W (h + f)]$ , so it permutes this orthonormal family with unit-modulus phases and extends to a unitary on the Hilbert completion, with inverse $π (W (- h))$ .

3.1A1step 2.1algebra

Fix $v \in S ∖ {0}$ and put $U (t) : = π (W (t v))$ for $t \in R$ . Since $σ (t v, s v) = t s σ (v, v) = 0$ , the Weyl relation gives $U (t) U (s) = U (t + s)$ and $U (0) = I$ . For every $t \neq 0$ , $U (t) Ω = [W (t v)]$ is orthogonal to $Ω = [W (0)]$ , and both are unit vectors; thus $∥ U (t) Ω - Ω ∥ = \sqrt{2}$ . This orbit is not continuous at $0$ , so $U$ is not strongly continuous.

4.1step 3.1algebra∎

Suppose a dense linear subspace $E$ had a norm derivative $\lim_{t \to 0} (U (t) ξ - ξ) / t$ for every $ξ \in E$ . Each such orbit would be continuous at $0$ . For any $x \in H_{ω}$ and $ε > 0$ , choose $ξ \in E$ with $∥ x - ξ ∥ < ε / 3$ ; unitarity gives $∥ U (t) x - x ∥ \leq 2 ∥ x - ξ ∥ + ∥ U (t) ξ - ξ ∥$ , so continuity on $E$ would imply continuity at $0$ for every $x$ , contradicting step 3.1 at $x = Ω$ . Therefore no dense domain supports a norm-differentiable generator for this unitary group. The example is purely algebraic and asserts no physical preparation or relativistic vacuum.

Sources

Christopher J. Fewster and Kasia Rejzner, Algebraic Quantum Field Theory—an introduction, lecture notes, arXiv:1904.04051v2 (2019), §4.2 Exercise 17