LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$[x^{k}] (1 - 4 x)^{1 / 2} = - \frac{2}{k} (\binom{2 k - 2}{k - 1})$ for $k \geq 1$ , and $1$ for $k = 0$

Statement

Work in $Q ⟦ x ⟧$ , a commutative $Q$ -algebra (The Catalan generating function $C (x) = \sum_{n \geq 0} C_{n} x^{n}$ in $Q ⟦ x ⟧$ ), and let $(1 - 4 x)^{1 / 2}$ denote the formal binomial power $(1 + u)^{c}$ of Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra with $u = - 4 x$ and $c = 1 / 2$ ; by Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra it is the unique series in $1 + x Q ⟦ x ⟧$ whose square is $1 - 4 x$ . Then

$[x^{0}] (1 - 4 x)^{1 / 2} = 1,$

and for every $k \geq 1$ , in $Q$ ,

$k [x^{k}] (1 - 4 x)^{1 / 2} = - 2 (\binom{2 k - 2}{k - 1}), equivalently [x^{k}] (1 - 4 x)^{1 / 2} = - \frac{2}{k} (\binom{2 k - 2}{k - 1}) .$

The displayed quotient formula is stated for $k \geq 1$ only, and is not a statement about $k = 0$ : at $k = 0$ the value is $1$ .

Facts & Assumptions

Given: the series $(1 - 4 x)^{1 / 2}$ above; write $A_{k} : = [x^{k}] (1 - 4 x)^{1 / 2}$ .

[F1]

$Q ⟦ x ⟧$ is a commutative $Q$ -algebra, and a natural number written where a rational is expected denotes its image under an injective embedding preserving addition and multiplication (The Catalan generating function $C (x) = \sum_{n \geq 0} C_{n} x^{n}$ in $Q ⟦ x ⟧$ ).

[L1]

In a commutative $Q$ -algebra, for $u \in x R ⟦ x ⟧$ and $c \in R$ , $(1 + u)^{c} = \sum_{n \geq 0} \frac{c (c - 1) \dots (c - n + 1)}{n!} u^{n}$ , where the numerator is the empty product $1$ at $n = 0$ (Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws).

[L2]

For $u \in x R ⟦ x ⟧$ and $c \in R$ , $(1 + u)^{c} : = \exp (c \log (1 + u))$ , and the displayed families are summable because ${ord}_{x} (u^{n}) \geq n$ (Formal exponential, logarithm, and binomial powers over a commutative $Q$ -algebra).

[L3]

For a commutative $Q$ -algebra $R$ , $u \in x R ⟦ x ⟧$ and $k^{'} \geq 1$ , there is a unique $v \in 1 + x R ⟦ x ⟧$ with $v^{k^{'}} = 1 + u$ , namely $v = (1 + u)^{1 / k^{'}}$ (Every $1 + u$ with $u \in x R ⟦ x ⟧$ has a unique $k$ th root with constant coefficient $1$ in a commutative $Q$ -algebra).

[L4]

$[x^{n}] (f + g) = [x^{n}] f + [x^{n}] g$ , $[x^{n}] (r f) = r [x^{n}] f$ , and $[x^{n}] (x^{k} f) = [x^{n - k}] f$ for $k \leq n$ and $0$ for $k > n$ (Coefficient extraction is $R$ -linear, separates formal series, shifts under multiplication by $x^{k}$ , and converts products to finite convolution).

[L5]

For $m, j \in N$ with $j \leq m$ : $(\binom{m}{j}) \cdot j! \cdot (m - j)! = m!$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ ).

[L6]

$(\binom{m}{0}) = 1$ for every $m$ , and $(\binom{m}{j})$ is a natural number (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L7]

$m! \neq 0$ for every $m \in N$ , and $σ (m)! = m! \cdot σ (m)$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L8]

For all $x^{'}, y^{'}, c^{'} \in N$ with $c^{'} \neq 0$ : if $x^{'} \cdot c^{'} = y^{'} \cdot c^{'}$ then $x^{'} = y^{'}$ (Cancellation for multiplication by a nonzero factor).

[L9]

$Q$ is a field, so every nonzero rational is invertible (The rationals form a field).

[L10]

A property that holds at $0$ and passes from every natural number to its successor holds at every natural number: if a property $P$ satisfies $P (0)$ and ( $P (n) \Rightarrow P (σ (n))$ ) for all $n$ , then $P (n)$ holds for all $n \in N$ (The principle of mathematical induction).

Proof

technique · direct

1.1

With $u = - 4 x$ we have $u^{n} = (- 4)^{n} x^{n}$ , so by [L1] and [L4] the coefficient of the binomial series at the index $k$ receives a contribution only from the term $n = k$ , giving $A_{k} = \frac{(1 / 2) (1 / 2 - 1) \dots (1 / 2 - k + 1)}{k!} (- 4)^{k}$ for every $k \in N$ ; at $k = 0$ the numerator is the empty product and $A_{0} = 1$ . Consequently $(k + 1) A_{k + 1} = (1 / 2 - k) (- 4) A_{k} = 2 (2 k - 1) A_{k}$ for every $k \in N$ .

F1L1L2L4

1.2

For every $k \geq 1$ the identity $k (\binom{2 k}{k}) = 2 (2 k - 1) (\binom{2 k - 2}{k - 1})$ holds in $N$ . Both $k \leq 2 k$ and $k - 1 \leq 2 k - 2$ , so [L5] gives $(\binom{2 k}{k}) k! k! = (2 k)!$ and $(\binom{2 k - 2}{k - 1}) (k - 1)! (k - 1)! = (2 k - 2)!$ . Multiplying the first by $k$ and using $(2 k)! = (2 k) (2 k - 1) (2 k - 2)!$ from [L7] gives $k (\binom{2 k}{k}) k! k! = 2 k^{2} (2 k - 1) (2 k - 2)!$ ; multiplying the second by $2 (2 k - 1) k^{2}$ and using $k! = k (k - 1)!$ gives $2 (2 k - 1) (\binom{2 k - 2}{k - 1}) k! k! = 2 (2 k - 1) k^{2} (2 k - 2)!$ . The two right-hand sides agree, so cancelling the nonzero factor $k! k!$ by [L7] and [L8] gives the identity.

L5L7L8

2.1

For every $k \geq 1$ one has $k A_{k} = - 2 (\binom{2 k - 2}{k - 1})$ , by induction on $k$ . At $k = 1$ the formula of step 1.1 gives $A_{1} = \frac{1 / 2}{1} (- 4) = - 2$ , and $- 2 (\binom{0}{0}) = - 2$ by [L6]. Assume it at some $k \geq 1$ . Multiplying the recursion of step 1.1 by $k$ gives $k (k + 1) A_{k + 1} = 2 (2 k - 1) k A_{k} = - 4 (2 k - 1) (\binom{2 k - 2}{k - 1})$ , which by step 1.2 is $- 2 k (\binom{2 k}{k})$ ; since $k$ is a nonzero rational, [L9] allows cancelling it and yields $(k + 1) A_{k + 1} = - 2 (\binom{2 k}{k})$ , which is the formula at $k + 1$ .

L6L9L10step 1.1step 1.2

3.1

Dividing by the nonzero rational $k$ turns step 2.1 into the quotient form, and step 1.1 gives the value at $k = 0$ . As a check, the first coefficients are $A_{0} = 1$ , $A_{1} = - 2$ , $A_{2} = - \frac{2}{2} (\binom{2}{1}) = - 2$ , $A_{3} = - \frac{2}{3} (\binom{4}{2}) = - 4$ , $A_{4} = - \frac{2}{4} (\binom{6}{3}) = - 10$ and $A_{5} = - \frac{2}{5} (\binom{8}{4}) = - 28$ .

L3L9step 1.1step 2.1∎

Remarks

The index $k = 0$ is genuinely outside the formula. The quotient $- \frac{2}{k} (\binom{2 k - 2}{k - 1})$ has no value at $k = 0$ , and the coefficient there is $1$ , not $0$ . Stating the formula with its range is not pedantry: the closed form of the Catalan generating function takes coefficients at positive indices only, and a statement covering $k = 0$ would be false.
Where the uniqueness clause is used. [L3] identifies the binomial power $(1 - 4 x)^{1 / 2}$ as the series in $1 + x Q ⟦ x ⟧$ squaring to $1 - 4 x$ , which is what lets a series produced by an entirely different computation be recognised as this one. No branch is chosen and no limit is taken.

Depends on

Used by

Dependency tree · two levels

55 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

A. Postnikov (notes by A. Lin), MIT 18.212 Algebraic Combinatorics, Spring 2019 (standard reference, not scraped)
D. Guichard, An Introduction to Combinatorics and Graph Theory, §3.5 (standard reference, not scraped)

[xk](1−4x)1/2=−2k(2k−2k−1)[xk](1−4x)1/2=−k2​(k−12k−2​) for k≥1k≥1, and 11 for k=0k=0