Alphabeta Math
TheoremStatement: 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.

Ogden's lemma

Statement

If L is a context-free language, then there exists an integer p1 such that for every word zL and every choice of at least p marked positions in z, there is a decomposition z=uvwxy that is p-admissible with respect to the marked positions and satisfies uviwxiyL for every i0.

Facts & Assumptions

Given: A context-free language L.

[L1]

By Marked positions and admissible Ogden decompositions, a p-admissible decomposition is one in which vx contains at least one marked position while vwx contains at most p marked positions.

[L2]

By The language generated by a CFG, there exists a context-free grammar generating L.

[L3]

By Every context-free language has an equivalent grammar in Chomsky normal form, that grammar may be replaced by an equivalent grammar in Chomsky normal form.

[L4]

By Derivations and parse trees correspond, every word in the language of a CFG is the yield of some parse tree for that grammar.

[L5]

By Parse trees and their yields, a parse tree records the production used at each internal node and its yield is read from the terminal leaves from left to right.

Proof

technique · direct
1.1

Choose a context-free grammar G0 with L(G0)=L by [L2], then replace it by an equivalent Chomsky-normal-form grammar G=(V,Σ,P,S) by [L3]. Set p:=2V+1. Let zL and mark at least p positions of z. Because p1, the word z is nonempty, so by [L4] fix a parse tree T for z in the CNF grammar G.

L2L3L4givenchoose
2.1

Starting at the root of T, build a path to a marked leaf by always moving to a child whose subtree contains the larger number of marked positions; when both children contain marked positions, choose one of the heavier children. Call such a node a branch point. Each time the path passes through a branch point, the chosen child still contains at least half of the marked positions seen at that node. Therefore, if there were at most V branch points on the path, the terminal leaf at the end would still lie below at least p/2V=2 marked positions, impossible for one leaf. So the path contains at least V+1 branch points.

L5step 1.1
3.1

Among the last V+1 branch points on that path, choose two with the same variable label A, with the upper one above the lower one. Let the lower A-subtree yield w, and let the material in the upper A-subtree to the left and right of the lower subtree yield v and x, so that the whole word is z=uvwxy. The upper branch point has marked material outside the lower subtree, so the concatenation vx contains a marked position. Also, if the upper A-subtree contained more than 2V marked positions, then repeating the branch-point-halving argument inside that subtree would produce more than V branch points below it on the chosen path, contradicting that we selected the upper A among the last V+1 branch points. Hence vwx contains at most 2V<p marked positions. By [L1], the decomposition is p-admissible.

L1step 2.1choose
4.1

The upper occurrence of A derives the lower one by a derivation segment AvAx, and the lower subtree derives w. Repeating or deleting that segment while keeping the rest of the parse tree fixed produces derivations of uviwxiy for every i0. Therefore every such word lies in L(G)=L.

L4step 3.1
5.1

Hence the integer p satisfies Ogden's lemma for L.

step 3.1step 4.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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