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.

Regular Weyl systems, projective symmetry and massive particles — Examples

1 · Prerequisites

2 · Summary

The path example separates a phase common to one isolated branch from a relative phase in an explicitly controlled two-arm model. The finite-matrix counterexample uses only finite trace sums to rule out exact canonical commutation relations in positive dimension. It makes no claim about differentiating unbounded generators.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Boost-translation loop phase

Example

Assume AC and Countable Choice. For $z \in C$ , write $e^{z} : = \exp z : = \sum_{k = 0}^{\infty} z^{k} / k!$ for the complex exponential, whose series converges for every $z$ . Let $d x$ be Lebesgue measure on $R^{d}$ . Let $d$ be a positive integer, let $m > 0$ and $ℏ > 0$ , and take $a, v \in R^{d}$ . Put $θ = m v \cdot a / ℏ$ and let $T (a) f (x) = f (x - a)$ and $B_{m} (v) f (x) = e^{i m v \cdot x / ℏ} f (x)$ on $L^{2} (R^{d}, d x; C)$ . Their loop $B_{m} (v) T (a) B_{m} (v)^{*} T (a)^{*}$ equals $e^{i θ} I$ , so a common scalar phase leaves squared overlap unchanged on an isolated component. In the explicitly defined two-arm path model below, applying the loop to exactly one arm gives recombination squared overlap $\cos^{2} (θ / 2)$ , while applying the same scalar to both arms gives squared overlap $1$ .

Example references

Mass cocycle for translations and boosts

The complex exponential by its power series

$\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$

The real exponential function and the number $e$ by a power series

Pythagorean and parity identities for all six trigonometric functions on their natural domains

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

Facts & Assumptions

Given: A positive integer $d$ , real parameters $m > 0$ , $ℏ > 0$ , vectors $a, v \in R^{d}$ , and the translation and modulation operators of the mathematical model.

[A1]

Assume AC and Countable Choice, as required by the supplier theorem. The Axiom of Choice The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

The unitary families $T (a)$ and $B_{m} (v)$ satisfy $B_{m} (v) T (a) B_{m} (v)^{*} T (a)^{*} = e^{i m v \cdot a / ℏ} I$ . Mass cocycle for translations and boosts

[F2]

The scalar complex exponential is the everywhere-convergent power series $\exp z = \sum_{k = 0}^{\infty} z^{k} / k!$ , also written $e^{z}$ . The complex exponential by its power series

[F3]

$\exp (z + w) = \exp z \exp w$ for $z, w \in C$ . $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential

[F4]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ . $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$

[F5]

The real exponential is defined by its power series, so $e^{0} = 1$ . The real exponential function and the number $e$ by a power series

[F6]

For every real $x$ , $\cos (- x) = \cos x$ and $\sin (- x) = - \sin x$ . Pythagorean and parity identities for all six trigonometric functions on their natural domains

[F7]

Complex modulus is multiplicative, so $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ . Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

Verification

1.1givenA1F1

Put $θ = m v \cdot a / ℏ$ . The loop identity in [F1] gives the scalar operator $e^{i θ} I$ on the system Hilbert space, so it multiplies every vector in an isolated component by the same scalar and leaves squared moduli of inner products unchanged there.

2.1F2F3F4F5F6F7step 1.1algebra∎

Let $H = L^{2} (R^{d}, d x; C)$ . On the path space $C^{2}$ set $∣ 0 ⟩ = (1, 0)^{T}$ , $∣ 1 ⟩ = (0, 1)^{T}$ , and $⟨ j ∣ : = ∣ j ⟩^{*}$ . Its orthogonal projectors are $∣ 0 ⟩ ⟨ 0 ∣ = diag (1, 0)$ and $∣ 1 ⟩ ⟨ 1 ∣ = diag (0, 1)$ , so they are self-adjoint, square to themselves, have zero product and sum to $I_{2}$ . Interpret the finite path-system product as $H \oplus H$ with $∣ 0 ⟩ \otimes f = (f, 0)$ , $∣ 1 ⟩ \otimes f = (0, f)$ and squared norm $∥ (f, g) ∥^{2} = ∥ f ∥^{2} + ∥ g ∥^{2}$ ; completeness follows componentwise from that of $H$ . In this explicit product model define the controlled loop $C = ∣ 0 ⟩ ⟨ 0 ∣ \otimes L + ∣ 1 ⟩ ⟨ 1 ∣ \otimes I$ , where $L = B_{m} (v) T (a) B_{m} (v)^{*} T (a)^{*}$ . By step 1.1, $C = U_{θ} \otimes I$ with $U_{θ} = diag (e^{i θ}, 1)$ . Equip the path space with inner product $u^{*} w$ and put $u_{+} = (1, 1)^{T} / \sqrt{2}$ . The recombining path overlap is $u_{+}^{*} U_{θ} u_{+} = (1 + e^{i θ}) / 2$ . The addition law [F3] and Euler formula with parity [F4, F6] give $(1 + e^{i θ}) / 2 = e^{i θ / 2} (e^{- i θ / 2} + e^{i θ / 2}) / 2 = e^{i θ / 2} \cos (θ / 2)$ . By [F4, F5], $∣ e^{i θ / 2} ∣ = e^{0} = 1$ , and modulus is multiplicative by [F7], so the squared modulus of this overlap is $\cos^{2} (θ / 2)$ . If the same scalar is applied to both arms, the path gate is $e^{i θ} I_{2}$ , whose matrix coefficient has squared modulus $1$ by [F4, F5].

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Finite matrices cannot satisfy exact canonical commutation relations

Statement refuted

For every positive integer $d$ and every $ℏ > 0$ , there exist matrices $Q, P \in M_{d} (C)$ such that $Q P - P Q = i ℏ I_{d}$ .

Facts & Assumptions

Given: A positive integer $d$ , $ℏ > 0$ , arbitrary complex $d \times d$ matrices $Q, P$ , and $tr (M) : = \sum_{j = 1}^{d} M_{j j}$ for $M \in M_{d} (C)$ .

[A1]

The proposed pair, if it existed, would satisfy $Q P - P Q = i ℏ I_{d}$ .

Counterexample

1.1givenalgebra

By the definition of matrix multiplication, $tr (Q P) = \sum_{j = 1}^{d} \sum_{k = 1}^{d} Q_{j k} P_{k j}$ and $tr (P Q) = \sum_{j = 1}^{d} \sum_{k = 1}^{d} P_{j k} Q_{k j}$ . Interchanging the finite indices $j, k$ in the second sum and commuting complex scalars makes the sums equal, so $tr (Q P - P Q) = 0$ .

2.1A1step 1.1algebra∎

Taking the trace in [A1] gives $0 = i ℏ tr (I_{d}) = i ℏ d$ , which is impossible because $d \geq 1$ and $ℏ > 0$ . Therefore the proposed universal existence statement is false.

Remarks

This proof concerns bounded finite matrices. It does not differentiate a Weyl relation for unbounded generators or supply a domain argument for such a differentiation.

Regular Weyl systems, projective symmetry and massive particles — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

Boost-translation loop phase

Example

Example references

Facts & Assumptions

Verification

Finite matrices cannot satisfy exact canonical commutation relations

Statement refuted

Facts & Assumptions

Counterexample

Remarks

Sources