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.
Lie bracket on the tangent space of a Lie group
Definition
Assume , let be a Lie group with identity , and write . For , let and be their unique left-invariant smooth extensions. Define the Lie-group tangent bracket by
The evaluation isomorphism Left-invariant vector fields evaluate isomorphically at the identity makes both extensions unique, so the definition is unambiguous. Moreover, The Lie bracket of left-invariant fields is left invariant makes left invariant, and hence its identity value determines it:
The bracket on fields is the library's fixed commutator from The Lie bracket of smooth vector fields. This explicitly fixes the sign for every later occurrence of , the Maurer--Cartan equation, and right-invariant fields. In particular, no opposite vector-field commutator convention is being imported from a source.
The assumption is inherited exactly through the supplied invariant-extension and bracket-closure results; evaluating the supplied vector-field bracket at adds no choice. A Lie group is nonempty. If , then and this is the unique zero bracket; the definition applies unchanged in dimension one. No metric or nondegeneracy hypothesis occurs, and the group is boundaryless by convention.