Repository navigation
Import Parikh's theorem and certified semilinear grammar compiler - #653
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No actionable code defect was established, but the outstanding source and novelty checks prevent an unconditional merge approval. SummaryAdds Parikh's theorem, its regular-language converse, and an executable grammar compiler with exact-output and numerical size guarantees.
Reviews (4) · Last reviewed commit: "Integrate the landed build-watch race fi..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
|
/review |
There was a problem hiding this comment.
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_isContextFreeproves 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_parikhImagerealizes 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_correctproves 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_boundsbounds components, periods and base/period norms of that computed output. The compared pumping and generation-width results bound different objects.compileGrammar_bit_boundsupplies 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.
There was a problem hiding this comment.
{
"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"
}
🤖 LLM review (
|
| 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 andLanguage.IsContextFree.pumpingconcern different results.
Evidence:theorem parikhImage_isSemilinear_of_isContextFree ... : IsSemilinearSet (parikhImage L),theorem exists_regularLanguage_with_parikhImage ... : ∃ R : Language T, R.IsRegular ∧ parikhImage R = X, andtheorem compileGrammar_correct,theorem compileGrammar_size_bounds, andtheorem compileGrammar_bit_boundare stated inLeanPool/Parikh/Api.lean(lines 70–116). The supplied prior-art entries for each of these five names sayNot searched: LEANEXPLORE_API_KEY is not set; the fetched Tau Ceti declarations such asTauCeti.SymplecticForm.exists_compatibledo 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.
|
The acquisition work is complete at The configured five-rubric review is 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. |
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Approve at c3bbcd23f07508abaedb6fb13dbe41b861afb930.
The remaining novelty decision is resolved. My retained exact-head source review already completed the primary-source comparisons missing from configured review2108: the forward Parikh bridge, regular-language realization and certified finite-grammar compiler differ from the inspected Mathlib, Tau Ceti and pool results. The component/period/numeric-entry bounds are compiler-output guarantees, not runtime claims or five independent major advances.
I also refreshed the comparison against current main 5dd7126: Mathlib 56a0058 has 9,220 Lean paths and no Parikh-named path; five complete grammar/language/regular-expression/semilinear candidate files do not supply these contracts. Current pool content searches and the nearby pumping/grammar-normalization theorem types likewise identify no duplicate. Tau Ceti remains at the same inspected revision 5189e8a. This is bounded primary-source evidence, not universal semantic absence or a claim that the unavailable search API ran.
Faithfulness, significance, sources and the repaired compiler implementation retain their exact-head acceptance. I accept novelty and scope under the current reviewer assignment; there is no remaining maintainer decision or need to repeat the automated rubric. The historical configured report is preserved as history. Fresh integration and every applicable protected check remain required; no old-head validation is transferred to a queue candidate.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Approve — repaired the current integration failure at 991b52f364e39542103549fcc36a990ea878d3d5.
The protected queue build failed in Parikh.DFAGrammar because it could not synthesize Fintype (σ × T). Both finite-type hypotheses were already present. I added the explicit Mathlib.Data.Fintype.Prod import, whose pinned Mathlib source supplies that instance. The new commit changes exactly that import; all statements and proof bodies remain literal.
The source, significance and prior-art decision in my previous review stands. The old failed queue run is retired. Fresh checks on this repaired head must pass before another protected queue entry; this source repair does not claim a successful build.
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 286,125 maxHeartbeats units across 27 valid files (4,397 added LOC). Sum of Count-heartbeats wall-clock total: 65.76 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Parikh.DFAGrammar |
2.80 s |
LeanPool.Parikh.Counting |
2.70 s |
LeanPool.Parikh.WordBlockAutomata |
2.70 s |
LeanPool.Parikh.TreePlugging |
2.60 s |
LeanPool.Parikh.TreeReplacement |
1.80 s |
LeanPool.Parikh.BoundedFamilySupport |
1.80 s |
LeanPool.Parikh.ParseTreePaths |
1.50 s |
LeanPool.Parikh.CompilerSupport |
1.40 s |
LeanPool.Parikh.GrammarTrees |
1.30 s |
LeanPool.Parikh.InsertionSequences |
1.10 s |
LeanPool.Parikh.Activation |
1.10 s |
LeanPool.Parikh.FiniteWitness |
1.10 s |
Per-file `lean --profile` output
LeanPool/Parikh.lean
import took 1.18s
cumulative profiling times:
declTypeLinter 0.42ms
elaboration 0.194ms
import 1.18s
initialization 23.6ms
interpretation 88.9ms
linting 0.755ms
module linting 0.0085ms
parsing 0.0586ms
tacticAnalysis 1.23ms
real 1.81
user 0.59
sys 0.67
LeanPool/Parikh/Activation.lean
import took 536ms
cumulative profiling times:
attribute application 0.131ms
blocked (unaccounted) 83.6ms
compilation (IR) 0.0588ms
compilation (LCNF base) 0.4ms
compilation (LCNF impure) 0.306ms
compilation (LCNF mono) 0.389ms
congr simp thm 4.72ms
declTypeLinter 5.13ms
dsimp 0.349ms
elaboration 46.4ms
fix level params 2.7ms
import 536ms
initialization 23.2ms
instantiate metavars 3.15ms
interpretation 192ms
let-to-have transformation 0.134ms
linting 21.9ms
module linting 0.00926ms
parsing 13.4ms
process pre-definitions 10.4ms
share common exprs 5.58ms
simp 91.6ms
tactic execution 184ms
tacticAnalysis 4.75ms
type checking 40ms
typeclass inference 126ms
real 1.42
user 1.20
sys 0.66
LeanPool/Parikh/ActivationAlgorithm.lean
import took 537ms
cumulative profiling times:
attribute application 0.0516ms
compilation (IR) 0.158ms
compilation (LCNF base) 1.58ms
compilation (LCNF impure) 0.681ms
compilation (LCNF mono) 1.21ms
congr simp thm 1.27ms
declTypeLinter 3.23ms
elaboration 17.5ms
fix level params 0.745ms
import 537ms
initialization 23.5ms
instantiate metavars 0.882ms
interpretation 177ms
let-to-have transformation 0.214ms
linting 9.62ms
module linting 0.00973ms
parsing 5.71ms
process pre-definitions 3.19ms
share common exprs 1.54ms
simp 25ms
tactic execution 102ms
tacticAnalysis 2.06ms
type checking 15.6ms
typeclass inference 31.8ms
real 1.31
user 0.90
sys 0.63
LeanPool/Parikh/Api.lean
import took 547ms
cumulative profiling times:
attribute application 0.29ms
compilation (IR) 0.0533ms
compilation (LCNF base) 0.582ms
compilation (LCNF impure) 0.215ms
compilation (LCNF mono) 0.331ms
declTypeLinter 4.86ms
elaboration 30.9ms
fix level params 0.169ms
import 547ms
initialization 23.7ms
instantiate metavars 0.11ms
interpretation 114ms
let-to-have transformation 0.0896ms
linting 5.67ms
module linting 0.00847ms
parsing 4.4ms
process pre-definitions 1.9ms
share common exprs 0.387ms
tacticAnalysis 2.01ms
type checking 2.3ms
typeclass inference 8.29ms
real 1.22
user 0.67
sys 0.64
LeanPool/Parikh/BoundedCutSupport.lean
import took 538ms
cumulative profiling times:
attribute application 0.0397ms
blocked (unaccounted) 31.1ms
compilation (IR) 0.25ms
compilation (LCNF base) 1.3ms
compilation (LCNF impure) 1.19ms
compilation (LCNF mono) 1.39ms
congr simp thm 2.63ms
declTypeLinter 1.83ms
elaboration 13.6ms
fix level params 0.895ms
import 538ms
initialization 23.3ms
instantiate metavars 1.07ms
interpretation 110ms
let-to-have transformation 0.0567ms
linting 6.2ms
module linting 0.00946ms
parsing 3.44ms
process pre-definitions 2.66ms
share common exprs 1.61ms
simp 54.3ms
tactic execution 103ms
tacticAnalysis 1.67ms
type checking 18.6ms
typeclass inference 15.6ms
real 1.28
user 0.86
sys 0.63
LeanPool/Parikh/BoundedEnumeration.lean
import took 540ms
cumulative profiling times:
attribute application 0.0695ms
compilation (IR) 0.266ms
compilation (LCNF base) 3.63ms
compilation (LCNF impure) 1.26ms
compilation (LCNF mono) 2.3ms
congr simp thm 0.794ms
declTypeLinter 2.51ms
elaboration 20.8ms
fix level params 0.496ms
import 540ms
initialization 26ms
instantiate metavars 1.34ms
interpretation 114ms
let-to-have transformation 0.0818ms
linting 6.86ms
module linting 0.0105ms
parsing 5.47ms
process pre-definitions 3.28ms
share common exprs 1.83ms
simp 18.1ms
tactic execution 56.7ms
tacticAnalysis 2.32ms
type checking 23.3ms
typeclass inference 53.2ms
real 1.27
user 0.78
sys 0.66
LeanPool/Parikh/BoundedFamilySupport.lean
import took 547ms
cumulative profiling times:
attribute application 0.108ms
compilation (IR) 0.114ms
compilation (LCNF base) 1.3ms
compilation (LCNF impure) 0.437ms
compilation (LCNF mono) 0.693ms
congr simp thm 3.12ms
declTypeLinter 4.15ms
dsimp 0.242ms
elaboration 21.7ms
fix level params 1.2ms
import 547ms
initialization 28.4ms
instantiate metavars 1.78ms
interpretation 145ms
let-to-have transformation 0.101ms
linting 11.7ms
module linting 0.00937ms
parsing 7.2ms
process pre-definitions 4.53ms
share common exprs 2.82ms
simp 104ms
tactic execution 93ms
tacticAnalysis 3.61ms
type checking 57.2ms
typeclass inference 245ms
real 1.45
user 1.17
sys 0.70
LeanPool/Parikh/CompilerBounds.lean
import took 544ms
cumulative profiling times:
attribute application 0.00989ms
congr simp thm 0.507ms
declTypeLinter 0.985ms
elaboration 3.79ms
fix level params 0.0852ms
import 544ms
initialization 29.3ms
instantiate metavars 0.496ms
interpretation 91ms
let-to-have transformation 0.0151ms
linting 3.09ms
module linting 0.00853ms
parsing 2.41ms
process pre-definitions 0.805ms
share common exprs 0.566ms
simp 5.39ms
tactic execution 36.1ms
tacticAnalysis 1.29ms
type checking 6.93ms
typeclass inference 8ms
real 1.25
user 0.64
sys 0.66
LeanPool/Parikh/CompilerSupport.lean
import took 645ms
cumulative profiling times:
attribute application 0.15ms
compilation (IR) 0.593ms
compilation (LCNF base) 4.85ms
compilation (LCNF impure) 3.78ms
compilation (LCNF mono) 4.86ms
congr simp thm 5.02ms
declTypeLinter 7.66ms
elaboration 37ms
fix level params 0.984ms
import 645ms
initialization 24.2ms
instantiate metavars 1.42ms
interpretation 169ms
let-to-have transformation 0.0697ms
linting 10.9ms
module linting 0.00912ms
parsing 7.59ms
process pre-definitions 4.67ms
share common exprs 2.02ms
simp 320ms
tactic execution 72.7ms
tacticAnalysis 2.97ms
type checking 27.6ms
typeclass inference 89.1ms
real 1.75
user 1.33
sys 0.69
LeanPool/Parikh/CompilerTrees.lean
import took 544ms
cumulative profiling times:
attribute application 0.0943ms
compilation (IR) 0.738ms
compilation (LCNF base) 12ms
compilation (LCNF impure) 3.71ms
compilation (LCNF mono) 6.81ms
congr simp thm 0.979ms
declTypeLinter 2.48ms
elaboration 21.3ms
fix level params 0.285ms
import 544ms
initialization 23.3ms
instantiate metavars 0.671ms
interpretation 115ms
let-to-have transformation 0.0982ms
linting 6.73ms
module linting 0.00895ms
parsing 5.42ms
process pre-definitions 3.66ms
share common exprs 1.59ms
simp 14.8ms
tactic execution 42.4ms
tacticAnalysis 2.29ms
type checking 7.5ms
typeclass inference 27ms
real 1.25
user 0.77
sys 0.65
LeanPool/Parikh/Construction.lean
import took 561ms
cumulative profiling times:
attribute application 0.203ms
blocked (unaccounted) 74.6ms
compilation (IR) 0.557ms
compilation (LCNF base) 6.97ms
compilation (LCNF impure) 2.56ms
compilation (LCNF mono) 4.89ms
congr simp thm 1.96ms
declTypeLinter 4.57ms
elaboration 47ms
fix level params 0.834ms
import 561ms
initialization 25.4ms
instantiate metavars 0.931ms
interpretation 175ms
let-to-have transformation 0.0969ms
linting 12.7ms
module linting 0.00983ms
parsing 10.3ms
process pre-definitions 5.08ms
share common exprs 2.12ms
simp 28.3ms
tactic execution 77.3ms
tacticAnalysis 2.79ms
type checking 21.1ms
typeclass inference 81.5ms
real 1.39
user 0.98
sys 0.67
LeanPool/Parikh/Counting.lean
import took 543ms
cumulative profiling times:
attribute application 0.141ms
blocked (unaccounted) 0.262ms
compilation (IR) 0.0514ms
compilation (LCNF base) 0.604ms
compilation (LCNF impure) 0.211ms
compilation (LCNF mono) 0.301ms
congr simp thm 2.57ms
declTypeLinter 3.58ms
dsimp 0.214ms
elaboration 17.6ms
fix level params 0.58ms
import 543ms
initialization 26.5ms
instantiate metavars 0.596ms
interpretation 116ms
let-to-have transformation 0.0546ms
linting 6.51ms
module linting 0.00862ms
parsing 4.41ms
process pre-definitions 2.92ms
share common exprs 1.16ms
simp 58.7ms
tactic execution 40.6ms
tacticAnalysis 1.98ms
type checking 13.3ms
typeclass inference 47.4ms
real 1.29
user 0.79
sys 0.64
LeanPool/Parikh/DFAGrammar.lean
import took 503ms
cumulative profiling times:
attribute application 0.05ms
congr simp thm 0.611ms
declTypeLinter 1.91ms
dsimp 2.21ms
elaboration 7.41ms
fix level params 0.853ms
import 503ms
initialization 28.4ms
instantiate metavars 1.25ms
interpretation 99.6ms
let-to-have transformation 0.0247ms
linting 4.3ms
module linting 0.00895ms
parsing 3.22ms
process pre-definitions 3.23ms
share common exprs 1.64ms
simp 11.3ms
tactic execution 91.9ms
tacticAnalysis 1.19ms
type checking 9.11ms
typeclass inference 21.3ms
real 1.30
user 0.71
sys 0.64
LeanPool/Parikh/Decomposition.lean
import took 541ms
cumulative profiling times:
attribute application 0.075ms
blocked (unaccounted) 0.713ms
congr simp thm 2.51ms
declTypeLinter 3.57ms
dsimp 0.368ms
elaboration 25.4ms
fix level params 1.98ms
import 541ms
initialization 29.4ms
instantiate metavars 2.68ms
interpretation 224ms
let-to-have transformation 0.0757ms
linting 14.7ms
module linting 0.00884ms
parsing 6.03ms
process pre-definitions 5.48ms
share common exprs 3.42ms
simp 19.9ms
tactic execution 124ms
tacticAnalysis 2.81ms
type checking 36.4ms
typeclass inference 22.5ms
real 1.38
user 0.97
sys 0.64
LeanPool/Parikh/ExecutableCompiler.lean
import took 550ms
cumulative profiling times:
attribute application 0.0731ms
compilation (IR) 1ms
compilation (LCNF base) 11ms
compilation (LCNF impure) 5.15ms
compilation (LCNF mono) 7.45ms
congr simp thm 1.32ms
declTypeLinter 2.66ms
elaboration 17.8ms
fix level params 0.377ms
import 550ms
initialization 23.6ms
instantiate metavars 1.15ms
interpretation 131ms
let-to-have transformation 0.0739ms
linting 8.3ms
module linting 0.00912ms
parsing 5.68ms
process pre-definitions 3.68ms
share common exprs 2.2ms
simp 20.1ms
tactic execution 201ms
tacticAnalysis 2.14ms
type checking 11.5ms
typeclass inference 47.7ms
real 1.38
user 0.96
sys 0.65
LeanPool/Parikh/FiniteRepresentation.lean
import took 544ms
cumulative profiling times:
attribute application 0.0232ms
congr simp thm 0.488ms
declTypeLinter 2.24ms
elaboration 4.26ms
fix level params 0.405ms
import 544ms
initialization 23.5ms
instantiate metavars 0.407ms
interpretation 100ms
let-to-have transformation 0.0192ms
linting 2.97ms
module linting 0.00837ms
parsing 2ms
process pre-definitions 1.05ms
share common exprs 0.649ms
simp 8.65ms
tactic execution 19.6ms
tacticAnalysis 1.31ms
type checking 3.85ms
typeclass inference 3.94ms
real 1.21
user 0.63
sys 0.65
LeanPool/Parikh/FiniteWitness.lean
import took 542ms
cumulative profiling times:
attribute application 0.0341ms
blocked (unaccounted) 0.0679ms
congr simp thm 0.546ms
declTypeLinter 2.31ms
elaboration 9.86ms
fix level params 0.398ms
import 542ms
initialization 23.8ms
instantiate metavars 0.394ms
interpretation 102ms
let-to-have transformation 0.0384ms
linting 4.29ms
module linting 0.00876ms
parsing 2.32ms
process pre-definitions 1.33ms
share common exprs 0.874ms
simp 7.07ms
tactic execution 17.1ms
tacticAnalysis 1.72ms
type checking 4.26ms
typeclass inference 4.34ms
real 1.21
user 0.62
sys 0.67
LeanPool/Parikh/GrammarImage.lean
import took 552ms
cumulative profiling times:
attribute application 0.011ms
congr simp thm 0.0601ms
declTypeLinter 1.43ms
elaboration 3.75ms
fix level params 0.294ms
import 552ms
initialization 24ms
instantiate metavars 0.36ms
interpretation 86ms
let-to-have transformation 0.00925ms
linting 2.12ms
module linting 0.00891ms
parsing 1.3ms
process pre-definitions 0.789ms
share common exprs 0.62ms
simp 0.334ms
tactic execution 12.8ms
tacticAnalysis 1.19ms
type checking 2.61ms
typeclass inference 2.55ms
real 1.22
user 0.59
sys 0.67
LeanPool/Parikh/GrammarTrees.lean
import took 542ms
cumulative profiling times:
attribute application 0.264ms
blocked (unaccounted) 1.88ms
compilation (IR) 1.18ms
compilation (LCNF base) 13.6ms
compilation (LCNF impure) 5.6ms
compilation (LCNF mono) 8.55ms
congr simp thm 4.59ms
declTypeLinter 6.69ms
do element elaborator 0.642ms
elaboration 77.4ms
fix level params 2.86ms
import 542ms
initialization 29.5ms
instantiate metavars 3.81ms
interpretation 200ms
let-to-have transformation 0.234ms
linting 26.1ms
module linting 0.00959ms
parsing 17.2ms
process pre-definitions 56.9ms
share common exprs 5.54ms
simp 167ms
tactic execution 264ms
tacticAnalysis 5.51ms
type checking 79ms
typeclass inference 141ms
real 1.73
user 1.59
sys 0.66
LeanPool/Parikh/Imports.lean
import took 572ms
cumulative profiling times:
declTypeLinter 0.0816ms
elaboration 0.0972ms
import 572ms
initialization 23.6ms
interpretation 72.9ms
linting 0.198ms
module linting 0.00822ms
parsing 0.00254ms
tacticAnalysis 0.112ms
real 1.22
user 0.61
sys 0.64
LeanPool/Parikh/InsertionSequences.lean
import took 559ms
cumulative profiling times:
aesop 49.3ms
attribute application 0.0216ms
compilation (IR) 0.0828ms
compilation (LCNF base) 0.465ms
compilation (LCNF impure) 0.432ms
compilation (LCNF mono) 0.526ms
congr simp thm 2.71ms
declTypeLinter 1.92ms
elaboration 8.65ms
fix level params 0.468ms
import 559ms
initialization 28.8ms
instantiate metavars 0.594ms
interpretation 105ms
let-to-have transformation 0.0306ms
linting 3.73ms
module linting 0.0109ms
parsing 1.66ms
process pre-definitions 1.5ms
share common exprs 0.968ms
simp 170ms
tactic execution 18.9ms
tacticAnalysis 1.06ms
type checking 11.7ms
typeclass inference 97.8ms
real 1.55
user 1.00
sys 0.65
LeanPool/Parikh/ParseTreePaths.lean
import took 536ms
cumulative profiling times:
attribute application 0.0173ms
blocked (unaccounted) 1.68ms
compilation (IR) 0.0626ms
compilation (LCNF base) 0.449ms
compilation (LCNF impure) 0.328ms
compilation (LCNF mono) 0.478ms
congr simp thm 1.33ms
declTypeLinter 1.42ms
elaboration 4.98ms
fix level params 0.543ms
import 536ms
initialization 27.2ms
instantiate metavars 0.647ms
interpretation 97ms
let-to-have transformation 0.0162ms
linting 3.61ms
module linting 0.00867ms
parsing 1.87ms
process pre-definitions 1.57ms
share common exprs 0.974ms
simp 46.4ms
tactic execution 33.2ms
tacticAnalysis 1.27ms
type checking 8.81ms
typeclass inference 37.4ms
real 1.29
user 0.73
sys 0.64
LeanPool/Parikh/RegularRealization.lean
import took 562ms
cumulative profiling times:
attribute application 0.131ms
blocked (unaccounted) 5.16ms
compilation (IR) 0.472ms
compilation (LCNF base) 8.37ms
compilation (LCNF impure) 2.1ms
compilation (LCNF mono) 3.7ms
congr simp thm 9.5ms
declTypeLinter 4.96ms
elaboration 31.1ms
fix level params 1.22ms
import 562ms
initialization 23.4ms
instantiate metavars 1.35ms
interpretation 149ms
let-to-have transformation 0.0856ms
linting 11.7ms
module linting 0.0117ms
parsing 9.88ms
process pre-definitions 5.52ms
share common exprs 2.74ms
simp 55.6ms
tactic execution 95.2ms
tacticAnalysis 3.44ms
type checking 20.3ms
typeclass inference 72.4ms
real 1.32
user 0.99
sys 0.65
LeanPool/Parikh/Statements.lean
import took 570ms
cumulative profiling times:
attribute application 0.0352ms
declTypeLinter 3.02ms
elaboration 6.85ms
fix level params 0.0677ms
import 570ms
initialization 24ms
instantiate metavars 0.0523ms
interpretation 101ms
let-to-have transformation 0.0289ms
linting 2.29ms
module linting 0.00954ms
parsing 1.58ms
process pre-definitions 0.498ms
share common exprs 0.145ms
tactic execution 2.79ms
tacticAnalysis 1.56ms
type checking 0.836ms
typeclass inference 3.25ms
real 1.23
user 0.64
sys 0.64
LeanPool/Parikh/TreePlugging.lean
import took 559ms
aesop took 128ms
cumulative profiling times:
aesop 128ms
attribute application 0.0378ms
compilation (IR) 0.123ms
compilation (LCNF base) 0.896ms
compilation (LCNF impure) 0.651ms
compilation (LCNF mono) 0.724ms
congr simp thm 7.88ms
declTypeLinter 3.31ms
elaboration 11.7ms
fix level params 0.975ms
import 559ms
initialization 23.9ms
instantiate metavars 1.13ms
interpretation 150ms
let-to-have transformation 0.0416ms
linting 6.06ms
module linting 0.0102ms
parsing 3.88ms
process pre-definitions 3.3ms
share common exprs 2.08ms
simp 612ms
tactic execution 67.1ms
tacticAnalysis 2.33ms
type checking 15.8ms
typeclass inference 53.5ms
real 2.05
user 1.57
sys 0.66
LeanPool/Parikh/TreeReplacement.lean
import took 557ms
cumulative profiling times:
attribute application 0.0267ms
blocked (unaccounted) 25.3ms
compilation (IR) 0.166ms
compilation (LCNF base) 0.954ms
compilation (LCNF impure) 0.949ms
compilation (LCNF mono) 1.05ms
congr simp thm 2.57ms
declTypeLinter 1.5ms
elaboration 11.4ms
fix level params 0.852ms
import 557ms
initialization 29.1ms
instantiate metavars 1.2ms
interpretation 109ms
let-to-have transformation 0.0386ms
linting 6.83ms
module linting 0.00924ms
parsing 4.71ms
process pre-definitions 2.65ms
share common exprs 1.54ms
simp 49.2ms
tactic execution 105ms
tacticAnalysis 1.87ms
type checking 12.2ms
typeclass inference 4.12ms
real 1.34
user 0.86
sys 0.65
LeanPool/Parikh/WordBlockAutomata.lean
import took 525ms
cumulative profiling times:
attribute application 0.0483ms
congr simp thm 1.43ms
declTypeLinter 2.16ms
dsimp 0.771ms
elaboration 13.7ms
fix level params 1.27ms
import 525ms
initialization 27.8ms
instantiate metavars 2.08ms
interpretation 127ms
let-to-have transformation 0.0418ms
linting 11.1ms
module linting 0.00935ms
parsing 8.14ms
process pre-definitions 4.37ms
share common exprs 2.75ms
simp 31.5ms
tactic execution 98.5ms
tacticAnalysis 2.4ms
type checking 12ms
typeclass inference 29.4ms
real 1.28
user 0.81
sys 0.66
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Approve — source-preserving CI recovery at 6ef56fde705c3f802cd11a0436ea95d20fedadcc.
The repaired head 991b52f encountered the watcher’s vanished-process race in Python validation. PR819 has now landed through the protected queue. I integrated its main revision e5baf4d while preserving the entire Parikh proof subtree, facade and project card byte-for-byte, including the explicit finite-product import from my previous repair. All other files come from that main revision; this content PR adds no gate change.
The mathematical, provenance and bounded prior-art acceptance stands. Fresh validation on this new head is required; the earlier failed runs supply no passing credit. Main advanced again during readback, so its own applicable push checks must also qualify before a protected queue action.
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:
9c1cde93f29bbaa91542e401e074ec3cd7646880.Scope and port:
c55e6e786f49471c72fbddbec5415808896aec1e. Adds module headers, explicit definition exposure, precise direct imports, and the empty-period range simplification required by the new version.LeanPool.leanis unchanged. CI, review rules and gate configuration are unchanged.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 underMathlib/ComputabilityandMathlib/ModelTheory/Arithmetic/Presburgerwere enumerated from that Git tree; a content-addressedgit 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:
ContextFreeGrammar.languageis the generated word language;Language.IsContextFreeasserts existence of such a grammar. These definitions supply the input predicate, without a semilinear count-image conclusion.IsSemilinearSet.imagepreserves an already semilinear set under an additive map, andIsSemilinearSet.closure_of_finitestarts from a finite generator set. These are reused algebraic ingredients; neither starts from arbitrary context-free derivations.Nat.isSemilinearSet_iff_ultimately_periodiccharacterizes one-dimensional sets.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:
Parikh.parikhImage_isSemilinear_of_isContextFreeParikh.exists_regularLanguage_with_parikhImageParikh.compileGrammar_correctParikh.compileGrammar_size_boundsParikh.compileGrammar_bit_boundThe 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:
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.Validation:
Classical.choice,propext, andQuot.sound; there is nosorry, custom axiom, unsafe/partial code, native decision mechanism, or option escape hatch.S → SS | εwith four unused labels and the five-tree height-two search with sixteen duplicate unit rules.