Updated: 2026-09-09
Partially formalized. The compressed-sensing, incoherence, and upper-bound results are proved on the stated domains. The lower-bound branch uses the cited Alon rank theorem as an external assumption.
Garg, Kleinberg, and Peng, How Many Features Can a Language Model Store Under the Linear Representation Hypothesis?, arXiv v1 (2026). Scope includes the named main results and their cited rank-lemma support.
| Result | Comparison with the paper |
|---|---|
| Theorem 1 — Compressed sensing | Exact with source clarification. The finite construction covers the paper’s intended regime. |
| Theorem 2 — Upper bound | Exact. |
| Theorem 3 — Lower bound | Exact for , conditional on Lemma 7. |
| Lemma 5 — Incoherence of random matrices, and its dimension consequence | Exact. |
| Lemma 7 — Alon’s rank theorem | Cited external theorem; assumed in Lean. |
| Corollary 8 — Rank bound after row scaling | Exact conditional on Lemma 7. |
| Proposition 9 — Feature geometry construction | Exact. |
| Proposition 11 — Norm-constrained feature geometry | Exact after correcting a denominator typo. |
| Theorem 12 — Threshold lower bound | Exact conditional on Lemma 7. |
| Corollary 13 — Activation and bias | Exact conditional on Lemma 7. |
Theorem 3 retains its displayed lower restriction on ; the notes explain the nontrivial accuracy range and Proposition 11’s finite denominator change.
Lemma 7, the cited Alon rank theorem, has not been proved in this Lean development. Theorem 3, Corollary 8, Theorem 12, and Corollary 13 use it as an external assumption.
The source-compatible accuracy conventions are explained in the parameter-domain note.
Theorem 12 and Corollary 13: supplement the printed submatrix argument with from a trace/Frobenius bound on the intermediate range. This proves the full stated asymptotic regime conditional on Lemma 7.
None. The native proof of the cited rank theorem remains a formalization obligation, as recorded in Section 5.
Proposition 11’s denominator typo is explained in Section 10. The external proof boundary is listed in Section 5.
The source-facing interface presents each of the 11 selected paper claims once as a transparent semantic target. The exact cited Alon rank theorem is the sole nonstandard axiom in the relevant closure; its scaling corollary and the paper-local reductions from it are checked Lean derivations. The final closure receipt records the partial obligation graph.
The assumption ledger classifies the cited Alon normalized-rank theorem as a partial proof boundary, matching Section 5. The three paper-local semantic prerequisites match their source connections in the prerequisite ledger. No other standalone paper-facing assumption is listed.
The statement map routes the compressed sensing, incoherence, geometry, rank, threshold, and activation formulas. The two Proposition 11 denominator targets are recorded as corrected targets in the source-to-Spec ledger and explained in the denominator note. The threshold and activation calculations are documented in the asymptotic-scope memo.
Reusable components include finite Euclidean nets, concentration bounds, finite compressed-sensing recovery, rank normalization, and trace/Frobenius rank inequalities. The library ledger records 19 direct matches and two corrected-target matches. A native proof of the normalized Alon theorem remains future work.
The dependency DAG distinguishes native results from the partial branch through the cited rank theorem, places source definitions before their dependent results, and marks the lower, threshold, and activation/bias conclusions as conditional on that theorem. Its TeX source and rendered PDF were inspected for readability, arrow direction, and overlap.
The focused-build receipt records a passing paper build. The import-closure receipt and final closure receipt retain the checked dependency graph and its explicit Alon boundary.
The checked source definitions are linear compressed-sensing dimension, the linear recovery condition, and incoherence. Their paper-local and reusable mathematical prerequisites are recorded in the statement map, prerequisite ledger, and library ledger.
The 11 selected targets cover the compressed-sensing construction, random incoherence, the upper and lower bounds, Propositions 9 and 11, the threshold theorem, the activation/bias corollary, and the cited-rank reduction summarized in Section 4. The lower-bound branch remains conditional exactly as stated in Sections 1 and 5.
The source-to-Spec ledger contains 11 current judgments: nine matches and two corrected-target matches for Proposition 11. status.json separately records that human review remains 0 of 11 rows.
The coverage ledger contains 15 items: 11 covered, two support-only, and two covered as corrected targets. The statement map supplies the complete source inventory and route assignments.