TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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.

$B_{n}$ is exactly the set of words of length $2 n$ over ${(,)}$ in which every prefix has at least as many $($ as $)$ and the totals are equal

Statement

For a word $w$ over $Σ = {(,)}$ and $r \leq ∣ w ∣$ let $d_{w} (r)$ be the number of letters $($ among the first $r$ letters of $w$ minus the number of letters $)$ among them. Call $w$ a nonnegative prefix word when $d_{w} (r) \geq 0$ for every $r \leq ∣ w ∣$ and $d_{w} (∣ w ∣) = 0$ .

For every $n \in N$ ,

$B_{n} = {w \in Σ^{2 n} : w is a nonnegative prefix word}$

(Balanced bracket words, defined by the recursive grammar). Moreover the alphabet bijection $(\mapsto U$ , $) \mapsto D$ carries $B_{n}$ onto the set of ballot words of length $2 n$ , hence onto $D_{n}$ through step words (Dyck paths of semilength $n$ ).

Facts & Assumptions

Given: a natural number $n$ , and the sets $B_{m}$ of Balanced bracket words, defined by the recursive grammar.

[F1]

$B$ is the least grammatical subset of $Σ^{*}$ , so a grammatical $X \subseteq B$ equals $B$ ; every nonempty member of $B$ is $(u) v$ with $u, v \in B$ ; $B_{m}$ is the set of members of length $2 m$ ; $B_{0} = {ε}$ ; and $B_{m + 1}$ is the set of words $(u) v$ with $u \in B_{i}$ and $v \in B_{m - i}$ for some $i \leq m$ (Balanced bracket words, defined by the recursive grammar).

[F2]

$D_{m}$ corresponds bijectively, through step words, to the ballot words of length $2 m$ , that is the words over ${U, D}$ in which the two letters occur equally often and every prefix has at least as many $U$ as $D$ (Dyck paths of semilength $n$ ).

[L1]

The map $Θ$ sending $(i, P, Q)$ with $i \leq m$ , $P \in D_{i}$ , $Q \in D_{m - i}$ to the diagonal path whose step word is $U$ , that of $P$ , $D$ , that of $Q$ , is a bijection onto $D_{m + 1}$ (Every Dyck path of semilength $n + 1$ factors uniquely as $U P D Q$ with $P \in D_{i}$ and $Q \in D_{n - i}$ ).

[L2]

For $f : A \to B$ : $f$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ( $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

[L3]

For a step set $S$ , a point $P$ and $ℓ \in N$ , the map sending a lattice path to its step word is a bijection $L_{S} (P; ℓ) \to S^{ℓ}$ (For each start point the step word is a bijection onto $S^{n}$ ).

[L4]

If a property of naturals holds at $n$ whenever it holds at every $m < n$ , then it holds at every natural number (Strong (complete) induction).

[L5]

If $A$ is finite and $f : A \to B$ is a bijection then $B$ is finite and $∣ B ∣ = ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1F2L2L3

The letter map $λ$ with $λ (() = U$ and $λ ()) = D$ is a bijection $Σ \to {U, D}$ , with the two-sided inverse $U \mapsto ($ , $D \mapsto)$ , so composing a word with $λ$ is a bijection $Σ^{2 m} \to {U, D}^{2 m}$ by [L2]. It carries $d_{w}$ to the difference between the numbers of $U$ and $D$ letters among the first $r$ , so $w$ is a nonnegative prefix word exactly when $λ \circ w$ is a ballot word of length $2 m$ ; and by [F2] and [L3] those correspond bijectively to $D_{m}$ .

1.2F1

Every member of $B$ is a nonnegative prefix word. The set $X$ of members of $B$ that are is grammatical: $ε$ qualifies, since $d_{ε} (0) = 0$ ; and if $u, v \in X$ and $w = (u) v$ , then $d_{w} (0) = 0$ , $d_{w} (r) = 1 + d_{u} (r - 1) \geq 1$ for $1 \leq r \leq 1 + ∣ u ∣$ , $d_{w} (2 + ∣ u ∣) = 1 + d_{u} (∣ u ∣) - 1 = 0$ , and $d_{w} (r) = d_{v} (r - 2 - ∣ u ∣) \geq 0$ for $2 + ∣ u ∣ \leq r \leq ∣ w ∣$ , the last value being $d_{v} (∣ v ∣) = 0$ . So $X \subseteq B$ is grammatical and [F1] gives $X = B$ .

2.1F1L1L4step 1.1

Conversely every nonnegative prefix word of length $2 m$ lies in $B_{m}$ , by [L4] on $m$ . At $m = 0$ the word is $ε$ , which lies in $B_{0}$ by [F1]. Let $m = p + 1$ and assume the claim at every index below $m$ . Let $w \in Σ^{2 m}$ be a nonnegative prefix word. By step 1.1 the word $λ \circ w$ is the step word of a path in $D_{p + 1}$ , so [L1] writes that path as $Θ (i, P, Q)$ with $i \leq p$ , $P \in D_{i}$ and $Q \in D_{p - i}$ ; applying the inverse letter map to the three blocks writes $w = (u) z$ with $u$ of length $2 i$ and $z$ of length $2 (p - i)$ , both nonnegative prefix words by step 1.1 read backwards. Since $i < m$ and $p - i < m$ , the inductive hypothesis puts $u \in B_{i}$ and $z \in B_{p - i}$ , so $w \in B_{m}$ by [F1].

3.1L5step 1.2step 2.1∎

Steps 1.2 and 2.1 are the two inclusions, so the displayed equality holds for every $n$ . Combining it with step 1.1 gives the second assertion, and [L5] transports cardinalities along it.

Remarks

What the theorem buys. The grammar is the definition, so this is the statement that the left-to-right condition a reader would have written down is the same notion. Without it the counting arguments would have to be run twice, once for each description, and the two would never be known to agree.
Where the first-return lemma enters. Only in the harder inclusion, and only to produce the factorisation the grammar needs. The lemma is a statement about paths, and the alphabet bijection of step 1.1 is what makes it applicable to words; the transport is stated as a bijection rather than left as an identification.

Depends on

Used by

Dependency tree · two levels

31 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

D. Guichard, An Introduction to Combinatorics and Graph Theory, §3.5 (standard reference, not scraped)

BnBn​ is exactly the set of words of length 2n2n over {(,)}{(,)} in which every prefix has at least as many (( as )) and the totals are equal