Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27
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.

The labelled constructions translate into the usual exponential-generating-function rules

Statement

Let A and B be labelled classes with exponential generating functions A(x) and B(x) over a commutative Q-algebra. Then:

EGF⁡(A⋆B)=A(x)B(x).

If A(0)=0, then

EGF⁡(SEQ⁡(A))=11−A(x),

EGF⁡(SET⁡(A))=exp⁡(A(x)),

EGF⁡(CYC⁡(A))=log⁡11−A(x).

For the boxed product,

ddxEGF⁡(A□⋆B)=A′(x)B(x),

and the constant term is 0, so

EGF⁡(A□⋆B)=∫0xA′(t)B(t) dt.

Proof

technique · direct
1.1given

In the labelled product on an n-label set, choosing the k labels sent to the A-part contributes (nk) possibilities, and then one chooses an A-object on those labels and a B-object on the complement. Thus the size-n coefficient is ∑k=0n(nk)akbn−k, which is exactly the coefficient rule for the product of exponential generating functions.

2.1step 1.1given

For SEQ⁡(A), a sequence of length r is an r-fold labelled product of A with itself, so its EGF is A(x)r. Summing over all r≥0 gives ∑r≥0A(x)r, and because A(0)=0 this formal geometric series equals 1/(1−A(x)).

2.2step 1.1given

A labelled set of exactly r A-objects is the same data as an ordered r-tuple of pairwise disjoint A-objects modulo permutation of the r components. Therefore its EGF is A(x)r/r!, and summing over r≥0 gives exp⁡(A(x)) by Formal exp⁡ and log⁡ are inverse homomorphisms and formal binomial powers obey the expected addition laws.

2.3step 1.1given

A labelled cycle of exactly r≥1 A-objects has r linear representatives, so its EGF is A(x)r/r. Summing over r≥1 gives ∑r≥1A(x)r/r=log⁡(1/(1−A(x))) by Formal exp⁡ and log⁡ are inverse homomorphisms and formal binomial powers obey the expected addition laws.

2.4step 1.1given

In a boxed product, the smallest label lies in the A-part. On size-n labels this is equivalent to choosing a pointed A-object on some k≥1 labels, with the distinguished label forced to be the smallest, and then a B-object on the remaining labels. Pointing contributes the derivative A′(x), so the derivative of the boxed-product EGF is A′(x)B(x). Since no boxed product has size 0, the constant term is 0, and integrating from 0 to x gives the displayed formula.

3.1step 1.1step 2.1step 2.2step 2.3step 2.4∎

Steps 1.1-3.1 are exactly the labelled symbolic-method rules claimed in the statement.

Depends on

Used by

Dependency tree · two levels

15 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