LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pending

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.

Paired-prefix lower bound for soft-attention 2DYCK prediction

Statement

Fix $p \in (0, 1)$ and let $D_{n}$ be a probability law on valid length- $(n - 1)$ prefixes over ${(,), [,]}$ . Let $E_{n}$ be a union of disjoint equal-mass pairs ${x, x^{'}}$ in the support of $D_{n}$ such that each prefix in a pair ends in a closing bracket and has positive stack height after that bracket; $x^{'}$ is obtained by changing the type of the top unmatched opening bracket in $x$ , at a position before the final prefix symbol. Assume that, conditional on $x$ , the next-symbol law assigns probability $p / 2$ to each opening bracket and probability $1 - p$ to the closing bracket matching its top unmatched opening, and that the law conditional on $x^{'}$ swaps the two possible closing-bracket types while leaving the opening probabilities unchanged. If $D_{n} (E_{n}) \geq P_{0} > 0$ for all sufficiently large $n$ , then every fixed soft-attention predictor satisfying the one-symbol influence hypotheses has

\underset{n \to \infty}{lim inf} (L_{n} - L_{n}^{*}) \geq P_{0} (1 - p) \log 2,

where $L_{n}$ is expected next-symbol cross-entropy and $L_{n}^{*} = E_{x \sim D_{n}} H (r_{x})$ is the optimal conditional cross-entropy. This lemma requires the positive-mass paired-prefix hypothesis; it does not assert that a particular PCFG supplies that hypothesis.

Statement references

Hahn, §6: paired-prefix argument and constant 2DYCK cross-entropy gap

Facts & Assumptions

Given: The probability law $D_{n}$ , disjoint pairs $E_{n}$ , next-symbol distributions described in the Statement, $P_{0} > 0$ , and a fixed soft-attention predictor.

[F1]

Predictions on inputs differing at one nonfinal token differ in $ℓ^{1}$ by at most $C / n$ (A nonfinal token has inverse-length influence under bounded soft attention).

[F2]

If two target laws on a five-symbol alphabet have predictions within $ϵ$ in $ℓ^{1}$ , their mean cross-entropy is at least the entropy of the mean target law minus $\log (1 + 5 ϵ)$ (Close paired predictions incur mixture entropy).

Proof

1.1givenalgebra

For one pair, write $r$ for the target law at $x$ and $r^{'}$ for the law at $x^{'}$ . Both assign $p / 2$ to each opening token; $r$ assigns $1 - p$ to one closing type and $r^{'}$ assigns $1 - p$ to the other. Thus $H (r) = H (r^{'})$ , while $\overset{ˉ}{r} = (r + r^{'}) / 2$ splits the close mass evenly between the two closing types, giving $H (\overset{ˉ}{r}) - H (r) = (1 - p) \log 2$ .

2.1step 1.1F1F2algebra

Let $q = q_{n} (x)$ and $q^{'} = q_{n} (x^{'})$ . Because the changed opening position is nonfinal, [F1] gives $∥ q - q^{'} ∥_{1} \leq C / n$ . Applying [F2] yields pair-mean loss at least $H (\overset{ˉ}{r}) - \log (1 + 5 C / n)$ . Subtracting the pair's optimal mean loss $H (r)$ gives excess at least $(1 - p) \log 2 - \log (1 + 5 C / n)$ .

3.1step 2.1givenF2algebra

At every context outside $E_{n}$ , cross-entropy is at least its conditional entropy by the finite-distribution inequality proved in [F2]. The pair-mass condition and step 2.1 therefore give $L_{n} - L_{n}^{*} \geq P_{0} ((1 - p) \log 2 - \log (1 + 5 C / n))$ for all sufficiently large $n$ .

4.1step 3.1algebra∎

Since $\log (1 + 5 C / n) \to 0$ , taking the lower limit in step 3.1 proves the stated gap.

Depends on

Used by

Hard and soft attention limits for formal-language prediction Theorem

Dependency tree · two levels

5 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

Hahn, Theoretical Limitations of Self-Attention in Neural Sequence Models, §6, Theorem 6 proof (standard reference, not scraped)