Alphabeta MathHow 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.
Formal exponential, logarithm, and binomial powers over a commutative -algebra
Definition
A commutative -algebra here means a commutative ring equipped with a unital ring homomorphism . We identify each rational with its image in .
For , define
For , define the formal binomial power
Since , each displayed family is summable. The unit criterion makes a unit. These symbols name formal series only; no analytic exponential, logarithm, branch, or convergence is involved.
Depends on
Used by
- The Eulerian-polynomial exponential generating function in ℚ(t)⟦ x⟧ Corollary
- The symmetric-group cycle-index series is coefficientwise exponential Corollary
- Exponential generating functions over a commutative ℚ-algebra Definition
- The Catalan generating function C(x)=∑_n≥0Cₙxⁿ in ℚ⟦ x⟧ Definition
- [xᵏ](1-4x)^1/2=-2/kC(2k-2, k-1) for k≥1, and 1 for k=0 Lemma
- 2x C(x)=1-(1-4x)^1/2, where (1-4x)^1/2 is the unique square root with constant coefficient 1 Theorem
- Baker–Campbell–Hausdorff theorem Theorem
- Formal exp and log are inverse homomorphisms and formal binomial powers obey the expected addition laws Theorem
- M(x)=1+x M(x)+x²M(x)², and 2x²M(x)=1-x-(1-2x-3x²)^1/2 Theorem
- Over a commutative ℚ-algebra, CYC(A) has generating function ∑_k≥ 1φ(k)/k log1/1-A(xᵏ) Theorem
- Over a commutative ℚ-algebra, MSET(A) has generating function exp(∑_k≥ 1A(xᵏ)/k) Theorem
- Over a commutative ℚ-algebra, PSET(A) has generating function exp(∑_k≥ 1(-1)ᵏ⁻¹A(xᵏ)/k) Theorem
- R(x)=1+x R(x)+x R(x)², and 2x R(x)=1-x-(1-6x+x²)^1/2 Theorem
Dependency tree · two levels
17 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
- Benjamin Sambale, An Invitation to Formal Power Series (standard reference, not scraped)