Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12
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.

Kleene star is the least concatenation-closed language containing L and ε

Statement

Let L be a language over an alphabet Σ.

  1. ε∈L∗.
  2. LL∗⊆L∗.
  3. If K is a language with ε∈K and LK⊆K, then L∗⊆K.

In particular, L∗ is the least language containing ε and closed under left concatenation by words from L; therefore it is also the least concatenation-closed language containing L and ε.

Facts & Assumptions

Given: A language L⊆Σ∗ and a language K⊆Σ∗.

[L1]

The powers of L satisfy L0={ε}, for n≥1 the set Ln consists of words u1⋯un with each ui∈L, and L∗=⋃n∈NLn by Language concatenation, powers, and Kleene star.

[L2]

Language concatenation is AB={ab:a∈A and b∈B} by Language concatenation, powers, and Kleene star.

Proof

technique · direct
1.1givenL1

By [L1], ε∈L0⊆L∗. This proves clause 1.

1.2L1L2

Let w∈LL∗. By [L2] there are u∈L and v∈L∗ with w=uv. Since v∈L∗, [L1] gives some n∈N with v∈Ln. Then w∈Ln+1 by the definition of Ln+1 in [L1], so w∈L∗ again. Thus LL∗⊆L∗, proving clause 2.

1.3givenL1base

Assume ε∈K and LK⊆K. We prove by induction on n∈N that Ln⊆K. For n=0, [L1] gives L0={ε}⊆K.

1.4ihL1L2induction

For the induction step, assume Ln⊆K. If w∈Ln+1, then by [L1] there are u∈L and v∈Ln with w=uv. The induction hypothesis gives v∈K, so w∈LK⊆K. Hence Ln+1⊆K.

1.5L1L2construct

If u,v∈L∗, choose m,n∈N with u∈Lm and v∈Ln. Writing u=u1⋯um and v=v1⋯vn with every ui,vj∈L, the concatenation uv is the (m+n)-fold product u1⋯umv1⋯vn, so uv∈Lm+n⊆L∗. Therefore L∗L∗⊆L∗, and L∗ is concatenation-closed.

1.6L2

Any concatenation-closed language K containing L and ε satisfies LK⊆K, because for u∈L⊆K and v∈K the concatenation uv lies in KK⊆K.

2.1step 1.3step 1.4L1discharge-induction

By steps 1.3 and 1.4, every Ln is contained in K. Since L∗=⋃n∈NLn by [L1], we get L∗⊆K. This proves clause 3.

3.1L1step 1.1step 2.1step 1.5step 1.6∎

Step 1.1 gives ε∈L∗, and [L1] gives L=L1⊆L∗. Together with step 1.5, this shows that L∗ is itself a concatenation-closed language containing L and ε. Now step 2.1 and step 1.6 show that every other such language contains L∗. This is exactly the stated minimality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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