CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-14

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.

BCH truncation fails when higher commutators do not vanish

Counterexample

Assume ${A C}_{ω}$ . In the upper-unitriangular subgroup of ${GL}_{4} (R)$ , put the strictly upper-triangular Lie-algebra elements

$X = E_{01} + E_{12}, Y = E_{23} .$

Then the quadratic truncation $Z_{0} = X + Y + \frac{1}{2} [X, Y]$ does not satisfy $e^{Z_{0}} = e^{X} e^{Y}$ . The omitted cubic BCH term is $\frac{1}{12} [X, [X, Y]] = E_{03} / 12 \neq 0$ .

Facts & Assumptions

Given: The displayed $4 \times 4$ matrices $X$ and $Y$ .

[F1]

Matrix units are defined by their entries, and matrix multiplication is the usual finite row-by-column sum; hence $E_{i j} E_{k l} = δ_{j k} E_{i l}$ . Matrix units $E_{i j}$ and the Kronecker delta. Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

[F2]

For matrix Lie groups, the Lie-group exponential is the matrix exponential. Matrix exponential as the Lie-group exponential.

[F3]

Countable choice is inherited through the matrix-Lie-group exponential interface [F2]; the finite polynomial calculation below uses no further choice. The Axiom of Countable Choice ( ${A C}_{ω}$ ).

Refutation

technique · explicit counterexample

1.1

By [F1], $[X, Y] = E_{13}$ , $[X, [X, Y]] = E_{03}$ , and $[Y, [X, Y]] = 0$ . Every product of four strictly upper-triangular $4 \times 4$ matrices is zero. The coefficient of the surviving cubic commutator will be determined directly below, without applying a local BCH theorem outside its neighbourhood.

F1algebra

1.2

The failure can be checked without relying on formal uniqueness. Since $X^{2} = E_{02}$ , $X^{3} = Y^{2} = 0$ , direct multiplication gives $e^{X} e^{Y} = I + E_{01} + E_{12} + E_{23} + \frac{1}{2} E_{02} + E_{13} + \frac{1}{2} E_{03}$ .

F1F2algebra

1.3

For $Z_{0} = E_{01} + E_{12} + E_{23} + \frac{1}{2} E_{13}$ , [F1] gives $Z_{0}^{2} = E_{02} + E_{13} + \frac{1}{2} E_{03}$ , $Z_{0}^{3} = E_{03}$ , and $Z_{0}^{4} = 0$ . Hence $e^{Z_{0}} = I + E_{01} + E_{12} + E_{23} + \frac{1}{2} E_{02} + E_{13} + \frac{5}{12} E_{03}$ .

F1F2algebra

1.4

The $E_{03}$ coefficients in steps 1.2 and 1.3 are respectively $1 / 2$ and $5 / 12$ , so $e^{Z_{0}} \neq e^{X} e^{Y}$ . Moreover $E_{03}$ annihilates every strictly upper-triangular matrix on either side, so it commutes with $Z_{0}$ and has square zero. Hence $e^{Z_{0} + E_{03} / 12} = e^{Z_{0}} (I + E_{03} / 12) = e^{X} e^{Y} .$ The exponential is injective on strictly upper-triangular $4 \times 4$ matrices: for $N^{4} = 0$ , its polynomial inverse is $\log (I + K) = K - K^{2} / 2 + K^{3} / 3$ , and direct finite expansion gives $\log (e^{N}) = N$ . Thus $Z_{0} + E_{03} / 12$ is the exact logarithm and the omitted term is precisely $[X, [X, Y]] / 12$ . The matrix calculation is choice-free; ${A C}_{ω}$ is stated only for [F2]. No endpoint, metric, or biconditional occurs.

discharge-construct: witnessF1F2F3step 1.1step 1.2step 1.3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

Michael Müger, Notes on the Baker-Campbell-Hausdorff-Dynkin theorem (standard reference, not scraped)
Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)