Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Every canonical factor map into a free product is injective

Statement

Every canonical factor homomorphism ιi:GijGj\iota_i:G_i\to\ast_jG_j is injective.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

Every element of iIGi\ast_{i\in I}G_i has a unique reduced syllable expression. The identity is represented by the empty word, and no nonempty reduced word represents the identity. (Normal form theorem for free products).

[L2]

A group homomorphism is injective if and only if its kernel is trivial. For a group homomorphism f:GHf:G\to H, ff is injective exactly when kerf={eG}\ker f=\{e_G\}. (A group homomorphism is injective if and only if its kernel is trivial).

Proof

technique · direct
1.1

A nonidentity gGig\in G_i maps to the nonempty one-syllable reduced word (i,g)(i,g), which is nonidentity by normal form.

givenL1L2
2.1

Thus the kernel of ιi\iota_i is trivial, and the trivial-kernel criterion gives injectivity. This also covers a trivial factor.

step 1.1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 29 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources