Import Parikh's theorem and certified semilinear grammar compiler

[Vilin97]

Parikh's theorem says that the letter-count image of a context-free language is semilinear. This import adds the theorem in Mathlib vocabulary, its regular-language converse, and an executable compiler from finite grammars to exact finite semilinear representations. The library also proves component, period, coordinate and numerical bit-budget bounds.

The reusable development includes production-labelled trees with explicit holes, equivalence with Mathlib derivations, reversible subtree replacement, bounded cycle decomposition, activation accounting, finite tree enumeration and word-block automata. The general language theorem permits an infinite ambient nonterminal type; only the grammar's active labels must be finite. Empty alphabets, epsilon/unit productions, duplicate rules, unreachable symbols, and equal or zero-weight contexts retain their intended semantics.

Source and eligibility:

• Public upstream: focs-lab/parikh-theorem, commit 9c1cde93f29bbaa91542e401e074ec3cd7646880.
• First public release: v0.1.0, 2026-10-12 01:40:05 UTC. The October 11 completion diff replaces the open forward theorem and exact-witness proofs with closed derivation-tree proofs. The acquisition interval is [2026-10-07 09:17:01 UTC, 2026-10-14 09:17:01 UTC); eligibility does not use reindexing or mirror timestamps.
• Apache-2.0 license verified in the pinned source. Attribution: Umang Mathur. Provenance: AI; upstream documents development with Codex and human review of statements and incremental PRs.
• Mathematical sources: Parikh, On Context-Free Languages, Sin'ya's derivation-tree proof, and Rubtsov's exposition. The quantitative executable compiler is the upstream development's constructive extension.

Scope and port:

• Imports all 25 mathematical/compiler source modules, the project entry point and generated public aggregate: 27 Lean files, 4,396 lines, plus one YAML card. The standalone JSON CLI, examples and audit tooling are omitted. Every mathematical/compiler declaration remains available. No external project source is vendored.
• Ports Lean 4.34.1 to the pool's exact Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Adds module headers, explicit definition exposure, precise direct imports, and the empty-period range simplification required by the new version.
• Removes duplicate productions before enumeration and bounds both compiler searches by the active-label count, so unused declared labels do not increase search depth. The general enumerator still includes all declared leaves, and its exact membership contract and all compiler bounds are unchanged. Repairs documentation and line length. The generated aggregate exposes the entire project; the fixed LeanPool.lean is unchanged. CI, review rules and gate configuration are unchanged.
• Public-repository searches, live cards/PRs/issues/history, pinned Mathlib and Tau Ceti searches found no matching Parikh development. Mathlib's grammar and semilinear-set primitives are reused. Yesterday's merged Hajnal–Szemerédi import is preserved and not repeated.

Pinned prior-art evidence for the five card headlines (added after review2105):

The configured search reported that its LeanExplore API key was unavailable. That API lookup has not been repaired or claimed to have run. Separate primary-source checks ran against the exact imported Mathlib commit c55e6e786f49471c72fbddbec5415808896aec1e. All 33 Lean paths under Mathlib/Computability and Mathlib/ModelTheory/Arithmetic/Presburger were enumerated from that Git tree; a content-addressed git grep -n -i -E 'parikh|contextfree.*semilinear|semilinear.*contextfree|compilegrammar' over those paths returned no matches (exit 1, empty stderr). This is a bounded lexical check, not a whole-Mathlib semantic absence claim.

The relevant primary declaration types were also read:

• Context-free grammar definitions: ContextFreeGrammar.language is the generated word language; Language.IsContextFree asserts existence of such a grammar. These definitions supply the input predicate, without a semilinear count-image conclusion.
• Semilinear definitions and image laws and their algebraic extensions: IsSemilinearSet.image preserves an already semilinear set under an additive map, and IsSemilinearSet.closure_of_finite starts from a finite generator set. These are reused algebraic ingredients; neither starts from arbitrary context-free derivations. Nat.isSemilinearSet_iff_ultimately_periodic characterizes one-dimensional sets.
• Regular-expression semantics: RegularExpression.matches' defines the word language of a supplied expression. It does not construct a regular language from a finite semilinear representation.

Headline comparisons at the actual imported interface:

Headline	Distinction from those inspected Mathlib candidates
Parikh.parikhImage_isSemilinear_of_isContextFree	Proves the grammar-to-semilinear count-image bridge for any context-free language over a finite alphabet.
Parikh.exists_regularLanguage_with_parikhImage	Constructs a regular-language realization of a supplied semilinear vector set.
Parikh.compileGrammar_correct	Computes a representation from an encoded finite grammar and proves exact denotation.
Parikh.compileGrammar_size_bounds	Bounds the compiler's components, periods and coordinates in terms of grammar parameters.
Parikh.compileGrammar_bit_bound	Bounds the numerical encoding of the compiled representation; it does not claim a practical runtime bound.

The closest pooled declaration, Language.IsContextFree.pumping, concludes a pumpable word decomposition rather than a semilinear image or compiler. The inspected Tau Ceti semilinear code equivalences are ring-automorphism-twisted monomial equivalences of code submodules, a different notion of semilinearity. These are named candidate comparisons, with the existing corpus limits retained.

The first-party proof-production disclosure is in the pinned maintenance README, under independent review.

Measured optimization:

• Command: lake build LeanPool.Parikh.Imports, removing only owned project library/IR artifacts before each sample; exact-pin external oleans warm, same Azure VM and default Lake parallelism.
• Alternating clean pairs: baseline 32.596 / 36.369 s, optimized 29.439 / 31.016 s. Means 34.483 → 30.227 s, 12.3% faster. An earlier optimization checkpoint measured 30.452 → 27.627 seconds (9.3%); that experiment had lighter VM load and is not compared directly with the final samples. Shared-VM load and the small sample count limit precision.
• Import analysis removes unnecessary activation/construction dependencies from tree counting and compiler support and allows independent modules to build concurrently. Recursive proofs use exported constructor equations instead of unfolding well-founded implementation details. A reducible DFA grammar adapter removes an expensive conversion without changing its body or theorem statements.
• Same-command synchronous profiles measured DFA tactic execution 2.26 s → 127 ms, and GrammarTrees tactic execution 306 → 260 ms. TreePlugging did not show a monotonic profile improvement; no improvement is claimed for it. No heartbeat/recursion overrides or proof suppressions are used.

Validation:

• Complete warning-free project/aggregate build; generated-index check; Mathlib declaration linters over 27 modules, including generated declarations; text style; production project-card, header, prohibited-text and size checks.
• Production axiom audit and compiled-environment backdoor audit pass across every owned module, including generated declarations. Allowed closure is only Classical.choice, propext, and Quot.sound; there is no sorry, custom axiom, unsafe/partial code, native decision mechanism, or option escape hatch.
• The upstream semantic/compilation regression suite is ported and run separately in scratch, using exported constructor equations and explicit meta imports required by the module system. Mathematical assertions are preserved; one concrete duplicate-enumeration count now reflects the intentional optimization (8/14 to 7/11). Added regressions check the four-component output of S → SS | ε with four unused labels and the five-tree height-two search with sixteen duplicate unit rules.
• No Python source changes. Required CI and configured Greptile/GPT reviews must complete on the exact head before native queue submission.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No blocking code defect was found, but the unverified external-source and dependency comparisons prevent an unconditional merge recommendation.

Summary

Imports Parikh’s theorem, its regular-language converse, and a certified compiler to finite semilinear representations.

• Context-free grammars now have semilinear letter-count images.
• Every semilinear set now has a regular-language realization.
• Finite grammars now compile into exact bounded semilinear witnesses.

_{Reviews (2) · Last reviewed commit: "Bound compiler searches by active labels..." · Reviewed by Greptile}

[Vilin97]

/review

[Vilin97]

Source review at c3bbcd23f07508abaedb6fb13dbe41b861afb930: favorable for integration once this head's protected CI and independent configured verdict pass.

All 27 Lean modules and the card were checked for mathematical fidelity and completeness. The forward theorem applies to every context-free language over a finite terminal alphabet, without assuming a finite ambient nonterminal type. Derivation-tree decomposition and activation establish exact image equality. The regular converse constructs an actual finite automaton, and the executable compiler supplies proved exact-denotation, component/period/norm and numerical bit-budget guarantees. Its entry budget concerns numerical data; it does not promise practical running time or an optimal representation. Empty alphabets, epsilon/unit rules, duplicate rules and zero/equal-weight contexts retain their intended semantics.

The current two-file optimization is sound: enumeration uses the proved active-label height bound and deduplicates structurally identical rules with exact membership proofs. The previous Greptile cost findings are addressed. The module graph is acyclic and the generated public aggregate covers the project. Targeted code-quality review found no concrete defect.

The pinned upstream maintenance README supports the AI-proof provenance and human statement review; the Apache-2.0 license and October 12 release were independently verified. The release tag and later imported commit are distinguished.

Supplementary novelty assessment, October 15: favorable on the independently inspected primary sources. I compared all five public contracts at this head, including their actual hypotheses and output semantics:

• parikhImage_isSemilinear_of_isContextFree proves semilinearity of the complete letter-count image of any finite-alphabet context-free language. Mathlib's grammar semantics and Presburger definability equivalence supply the endpoint notions, but neither compared type proves this derivation-to-count-image bridge.
• exists_regularLanguage_with_parikhImage realizes every semilinear count set as exactly the count image of a regular language. Mathlib's DFA recognition and closure results and multiset/count-vector equivalences are supporting infrastructure; they do not state this realization.
• compileGrammar_correct proves exact denotation for a concrete finite grammar-to-semilinear-data compiler. A classical existence result, pumping decomposition or grammar normalization alone does not supply this executable contract.
• compileGrammar_size_bounds bounds components, periods and base/period norms of that computed output. The compared pumping and generation-width results bound different objects.
• compileGrammar_bit_bound supplies a fixed-width numerical-entry budget, excluding length metadata. It largely follows from the preceding size bounds and should not be counted as a separate major advance or a runtime guarantee.

The Mathlib comparison is pinned to c55e6e786f49471c72fbddbec5415808896aec1e. Six lexical queries covered its 8,563 versioned Lean paths, followed by actual candidate-type comparisons; the previous 33-path limitation is no longer the search boundary. Positional List.toFinsupp, occurrence-count Multiset.toFinsupp, Sym.equivNatSumOfFintype, semilinear closure and Presburger definability have distinct contracts from these bridges and compiler.

I also checked 25 selected primary-source files at the Tau Ceti revision pinned by current main, after inspecting complete path metadata. Its semilinear code equivalence concerns ring-automorphism-twisted submodule codes; occCount_eq_of_transitionCount_eq concerns two fixed words with equal adjacent-pair counts. Neither compared contract describes all count vectors of a grammar language. In the pool, the 61 files across PumpingCfg, LanguageGeneration and Computability supply pumping, learning/generation and oracle-code results with different hypotheses and conclusions.

No duplicate of these headline contracts was identified in those inspected candidates. This is bounded source evidence: the whole-tree Mathlib searches are lexical, the Tau Ceti and pool source selections are limited, and I am not asserting universal semantic absence. No previously unavailable search API was run.

Hosted exact-head CI38547495715 passed. The published configured review2108 still says needs_discussion for novelty, with the other four rubrics passing and no duplicate declaration named. This supplement supplies independent primary-source inspection for the concrete evidence gap; it records my favorable novelty judgment without changing that configured result or any required status. No identical review request or worker restart is warranted.

Current-main qualification refreshed October 16: main 6464ab4d6dfa33b23c60824564e8fc59ab427dd3 is the generated-README-only successor of tested source parent 4bdfd1ea6f9e2ad5889be389576076a1e0095e06. Its applicable individual required contexts and normal protections are verified, with the retained successful source-parent push, five mandatory validation steps and canonical Build project. This uses unchanged-input coverage; it does not claim eight new Lean validations on the metadata-only commit. PR610, PR611 and PR659 are merged. Daily documentation publishing is asynchronous and excluded from the merge predicate; aggregate rollup and cancelled publisher stages do not supply a remaining infrastructure blocker. Integration still awaits resolution of the actual configured novelty judgment above. The favorable independent primary-source supplement does not rewrite review2108's computed verdict, and all source, configured-review, discussion, protection and native queue gates remain required.

[Vilin97]

{
"kind": "author_acquisition_audit",
"reviewed_head": "c3bbcd23f07508abaedb6fb13dbe41b861afb930",
"conclusion": "approve",
"findings": [],
"evidence": {
"faithfulness": "Counting.counts is literal List.count, image is its Set.image, and Component.denotation is an independently indexed natural linear combination. Api.parikhImage_isSemilinear_of_isContextFree quantifies over every Mathlib Language with its actual IsContextFree predicate and a finite terminal alphabet. GrammarTrees.derives_iff_tree proves both directions against Mathlib Derives; GrammarImage.treeRepresentation_correct proves exact equality, with no hard result bundled as an input. RegularRealization.converse supplies an actual Mathlib-regular language. The compiler implements the correctness/boundedness fields of the interface with closed proofs. Its vectorBits bound covers numerical coordinates and excludes representation-length metadata, as documented. Tests cover empty alphabets, epsilon/unit/duplicate productions, inactive labels and distinct zero-weight contexts.",
"novelty": "No Parikh development was found by public code/issue/PR searches, all current project cards and repository history, or pinned Mathlib/Tau Ceti lexical/source comparison. The existing Language.IsContextFree.pumping proves a pumping decomposition, not semilinearity; its ChomskyNormalFormGrammar.parseTree has restricted binary/terminal syntax, unlike arbitrary production-labelled open trees and epsilon/unit contexts here. Mathlib's Semilinear.Defs supplies the algebraic vocabulary and finite-union tools but no grammar/image bridge. Tau Ceti's semilinear hits concern coding-theory maps rather than language counts. Searches support a bounded novelty judgment, not a claim that every differently-named theorem was semantically enumerated.",
"significance": "A named formal-language theorem together with a reusable constructive grammar library and certified compiler, about 4.4K Lean lines. The imported scope consists of human-readable definitions and proofs, not generated certificate tables. Every mathematical/compiler source is retained; CLI, tests and audit tooling are excluded from content.",
"sources": "Apache-2.0 LICENSE verified at 9c1cde93f29bbaa91542e401e074ec3cd7646880; public release 2026-10-12T01:40:05Z in the eligible window. The October 11 forward completion diff was inspected through git after REST rate limiting. Git authors identify Umang Mathur; upstream maintenance documentation discloses Codex development and human statement/PR review. The card distinguishes the Parikh paper, Sin'ya/Rubtsov proof sources and the upstream compiler extension. Rubtsov Theorem 1 and its tree-decomposition argument were compared with the actual Lean endpoint and activation/decomposition implementation.",
"quality": "Every changed file and its imports, definitions/contracts, endpoints and representative proof slices inspected in bounded reads. Public APIs use Mathlib predicates, theorem generality preserved, interface fields implemented rather than postulated. Precise import visibility and dependencies, targeted definition exposure, reducible DFA adapter, constructor-equation proofs, documentation, and line length repaired. No gate changes, overrides, suppressions or unsafe/native proof mechanism. Production audits cover all 27 compiled modules, including generated auxiliaries; Mathlib linters pass for 789 declarations. Alternating clean-build means improve 30.452 to 27.627 seconds (9.3%); synchronous DFA tactic profile improves 2.26s to 127ms. TreePlugging profile variation is not presented as an improvement. No further material safe compile-time improvement is evident from the reviewed module/declaration profiles. Greptile identified two search-cost defects on the initial head. Both were repaired: bounded compiler searches use activeLabels.card + 1, and duplicate rules are removed before expansion. The general enumerator exact membership theorem, both family membership theorems and all compiler correctness/size statements are unchanged; their revised proofs are kernel-checked. Expanded regression tests verify the concrete unused-label and repeated-rule cases. Final alternating clean means 34.483 → 30.227 s (12.3%), measured under later, heavier VM load; the earlier 9.3% experiment is preserved separately rather than mixed with these samples.",
"local_checks": "Repaired head: warning-free complete project/aggregate build; 27 modules/789 declaration linters; text style; generated indexes; production header/text/size/card/axiom/compiled-backdoor audits; full upstream semantic/executable regression plus two targeted search regressions pass, zero errors/warnings. One concrete enumeration-size assertion changes 8/14 to 7/11 because duplicates are intentionally eliminated; all mathematical assertions are preserved. No Python changes.",
"ci": "Exact repaired-head Lean Action CI 38547495715 and every current check complete SUCCESS/SKIPPED under live scope. Build, generated indexes, declaration lint, style and repository quality/trust pass. Greptile current-head rerun reports no blocking code defect; both repaired threads resolved. Configured GPT job2105 completed: faithfulness/significance/sources/quality pass (4/5 quality), novelty discuss because its Mathlib search was not run without LEANEXPLORE_API_KEY, overall needs_discussion. The author audit approves the inspected content but does not override that configured assessment or authorize queue submission."
},
"merge_acceptance": "blocked by configured novelty assessment: Mathlib search unavailable without LEANEXPLORE_API_KEY"
}

[Vilin97]

🤖 LLM review (gpt-6.1-sol, 5 rubrics)

Reviewed head: c3bbcd23f07508abaedb6fb13dbe41b861afb930

Verdict: 🤔 needs_discussion — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	All five card headlines match the corresponding Lean declarations, including their exact equalities and quantitative bounds.
Novelty	🤔 discuss	No duplicate declaration is identified in the pool or the fetched Tau Ceti candidates, but the Mathlib prior-art search for all five headlines was not run, so novelty cannot be cleared.
Significance	✅ pass	This is a research-level theory-building formalization centered on a named theorem and a certified constructive compiler.
Sources	✅ pass	The derivation-tree paper supports the forward theorem, and the explicitly credited pinned upstream reference supports the converse, compiler construction, and quantitative bounds.
Code quality (advisory)	✅ pass	Shared tree-accounting lemmas, generic activation proofs, and explicit list-to-finset bridges keep the compiler development maintainable.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The theorems assume [Finite T] and [DecidableEq T] for language-level results, plus L.IsContextFree or IsSemilinearSet X as appropriate; compiler theorems take an EncodedGrammar. The card discloses the substantive finite-alphabet, context-free, and semilinear conditions.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	formal language theory
Mode	theory_building
Code quality	4 / 5

Statement check: The language results require finite T and decidable equality together with the stated context-free or semilinear hypotheses, while the compiler results quantify over every EncodedGrammar and prove exact denotation and bounds.

The PR formalizes Parikh's theorem, its regular-language converse, and exact bounded grammar compilation through Parikh.parikhImage_isSemilinear_of_isContextFree, Parikh.exists_regularLanguage_with_parikhImage, and Parikh.compileGrammar_correct.

Novelty findings (1)

• partial-overlap — PR-wide
  The five headline declarations are present in the diff, but the configured Mathlib search is explicitly recorded as not run (LEANEXPLORE_API_KEY is not set) for each one. Without that comparison, an existing Mathlib theorem cannot be ruled out; the Tau Ceti candidates and Language.IsContextFree.pumping concern different results.
  Evidence: theorem parikhImage_isSemilinear_of_isContextFree ... : IsSemilinearSet (parikhImage L), theorem exists_regularLanguage_with_parikhImage ... : ∃ R : Language T, R.IsRegular ∧ parikhImage R = X, and theorem compileGrammar_correct, theorem compileGrammar_size_bounds, and theorem compileGrammar_bit_bound are stated in LeanPool/Parikh/Api.lean (lines 70–116). The supplied prior-art entries for each of these five names say Not searched: LEANEXPLORE_API_KEY is not set; the fetched Tau Ceti declarations such as TauCeti.SymplecticForm.exists_compatible do not state any of these results.

---

Tokens: 7,665,772 in / 38,218 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $31.2364 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

The acquisition work is complete at c3bbcd23f07508abaedb6fb13dbe41b861afb930. Its exact-head CI passes build, generated indexes, declaration lint, text style and repository quality/trust. Both Greptile compiler-cost findings were repaired and resolved; its current-head rerun reports no blocking code defect. The separate acquisition audit and retained permanent source review are favorable.

The configured five-rubric review is needs_discussion: faithfulness, significance, sources and code quality pass (quality 4/5), while novelty is discuss because its supplied Mathlib search says LEANEXPLORE_API_KEY is not set. It identifies no duplicate in the pool or fetched Tau Ceti candidates. This is an unavailable configured search, not a demonstrated duplicate. The review's CI footer describes its earlier snapshot; current-head CI subsequently completed successfully.

Independent public GitHub and pinned-source checks found no Parikh match. The inspected Mathlib grammar and semilinear-set definitions provide the reused primitives, and the pool's existing pumping theorem has a different conclusion. These are bounded prior-art observations; they do not change the configured review's unchecked Mathlib-search state.

The PR remains open without auto-merge or queue submission. The remaining acceptance action is to make Mathlib prior-art evidence available to the configured reviewer and rerun/resolve its novelty assessment. The credential is unavailable in this acquisition process, and no reviewer configuration, rule, workflow or gate was changed. The valid source, CI, reviews and exact-head checkpoints are preserved; no branch update to chase main is needed.

Final controlled clean-build means are 34.483 → 30.227 seconds, a 12.3% reduction under comparable alternating runs on the shared VM. The complete upstream semantic/executable suite and the targeted unused-label/duplicate-rule regressions pass. No mathematical statement or compiler correctness/size contract was weakened.

[Vilin97]

/review