diff --git a/LeanPool/Parikh.lean b/LeanPool/Parikh.lean
new file mode 100644
index 0000000000..d7590b23ab
--- /dev/null
+++ b/LeanPool/Parikh.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Api
+public import LeanPool.Parikh.ActivationAlgorithm
+public import LeanPool.Parikh.BoundedEnumeration
+
+/-!
+# Parikh's theorem and a certified semilinear grammar compiler
+
+Source: doi:10.1145/321356.321364, url:https://github.com/focs-lab/parikh-theorem/tree/9c1cde93f29bbaa91542e401e074ec3cd7646880
+Authors: Umang Mathur
+Status: verified
+Main declarations: `Parikh.parikhImage_isSemilinear_of_isContextFree`
+Tags: formal-languages, context-free-grammars, semilinear-sets, verified-algorithms
+MSC: 68Q45, 68Q42, 03D05
+-/
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; the mathematical library and certified
+compiler are preserved. The standalone JSON CLI, examples and audit tooling are
+outside this import. -/
+
+/-! The derivation-tree proof follows Ryoma Sin'ya,
+*Simple proof of Parikh's theorem a la Takahashi* (arXiv:1909.09393), and
+Alexander Rubtsov, *The Simplest Proof of Parikh's Theorem via Derivation Trees*
+(arXiv:2301.00047). The quantitative grammar compiler is the upstream project's
+constructive extension, with bounds described in its mathematical reference. -/
diff --git a/LeanPool/Parikh/Activation.lean b/LeanPool/Parikh/Activation.lean
new file mode 100644
index 0000000000..e755fd8d83
--- /dev/null
+++ b/LeanPool/Parikh/Activation.lean
@@ -0,0 +1,387 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Decomposition
+import LeanPool.Parikh.InsertionSequences
+import Mathlib.Algebra.Group.Submonoid.Finsupp
+import Mathlib.Algebra.Order.Group.Nat
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# When can a family of cycles be used together?
+
+A context can be inserted only if its root label is already present. One
+insertion may introduce labels needed by another, so first uses require an
+order. Once a context is enabled, growing support keeps it enabled.
+
+We first study this without grammar syntax: each operation requires a label
+and adds a set of labels. `first_occurrences` reduces a valid sequence to an
+activation order, and `positive_multiplicities` permits arbitrary additional
+copies. The later results realize these operations by tree insertions.
+
+`one_linear` is the payoff: a chosen activatable family describes one linear
+set. Its base includes one copy of every chosen context; its periods describe
+extra copies. Context identities are retained throughout, because equal weights
+do not imply equal root requirements or equal added support.
+
+Source: `def:activation`, `lem:first-occurrence`, `lem:multiplicities`, `prop:one-linear`.
+-/
+namespace Parikh
+
+/-- Execute operations in an order that makes each required label available.
+Starting with support `U`, operation `c` requires `required c ∈ U` and enlarges
+support to `U ∪ added c` before the rest of the list is considered. Nothing is
+removed, so a label that has become available stays available (`eq:activation`). -/
+@[expose] def ActivationOrder {N C : Type*} (required : C → N) (added : C → Set N) :
+    Set N → List C → Prop
+  | _, [] => True
+  | U, c :: cs => required c ∈ U ∧ ActivationOrder required added (U ∪ added c) cs
+
+/-- A finite family admits an enabled order using each member exactly once.
+This describes the first-use phase. For cycle contexts, later repetitions are
+possible because support only grows; `positive_multiplicities` makes that
+consequence precise under its additional self-enabling hypothesis. -/
+@[expose] def Activatable {N C : Type*} (required : C → N) (added : C → Set N)
+    (U : Set N) (D : Finset C) : Prop :=
+  ∃ order : List C, order.Nodup ∧ (∀ c, c ∈ order ↔ c ∈ D) ∧
+    ActivationOrder required added U order
+
+namespace ActivationOrder
+variable {N C : Type*} {required : C → N} {added : C → Set N}
+
+/-- An operation may be omitted when everything it adds is already present. -/
+theorem filter_of_covered {U : Set N} {cs : List C}
+    (h : ActivationOrder required added U cs) (p : C → Bool)
+    (hcovered : ∀ c ∈ cs, p c = false → added c ⊆ U) :
+    ActivationOrder required added U (cs.filter p) := by
+  induction cs generalizing U with
+  | nil => simp [ActivationOrder]
+  | cons c cs ih =>
+    cases hp : p c with
+    | false =>
+      have hU : U ∪ added c = U :=
+        Set.union_eq_left.mpr (hcovered c (by simp) hp)
+      have htail : ActivationOrder required added U cs := by
+        simpa only [hU] using h.2
+      simpa only [List.filter_cons, hp, Bool.false_eq_true, ↓reduceIte] using
+        ih htail (fun d hd hpd => hcovered d (List.mem_cons_of_mem c hd) hpd)
+    | true =>
+      simp only [List.filter_cons, hp, ↓reduceIte, ActivationOrder]
+      refine ⟨h.1, ih h.2 ?_⟩
+      intro d hd hpd x hx
+      exact Or.inl (hcovered d (List.mem_cons_of_mem c hd) hpd hx)
+
+/-- If every requested root is already present, any finite order is enabled. -/
+theorem of_forall_mem {U : Set N} {cs : List C}
+    (h : ∀ c ∈ cs, required c ∈ U) : ActivationOrder required added U cs := by
+  induction cs generalizing U with
+  | nil => simp [ActivationOrder]
+  | cons c cs ih =>
+    refine ⟨h c (by simp), ih ?_⟩
+    intro d hd
+    exact Or.inl (h d (List.mem_cons_of_mem c hd))
+
+/-- After an activation pass, append any operations whose roots it supplies. -/
+theorem append_of_covered {U : Set N} {cs ds : List C}
+    (h : ActivationOrder required added U cs)
+    (hcovered : ∀ d ∈ ds, required d ∈ U ∨ ∃ c ∈ cs, required d ∈ added c) :
+    ActivationOrder required added U (cs ++ ds) := by
+  induction cs generalizing U with
+  | nil =>
+    apply of_forall_mem
+    intro d hd
+    simpa using hcovered d hd
+  | cons c cs ih =>
+    refine ⟨h.1, ih h.2 ?_⟩
+    intro d hd
+    rcases hcovered d hd with hU | ⟨b, hb, hadded⟩
+    · exact Or.inl (Or.inl hU)
+    · rcases List.mem_cons.mp hb with rfl | hb
+      · exact Or.inl (Or.inr hadded)
+      · exact Or.inr ⟨b, hb, hadded⟩
+end ActivationOrder
+
+/-- A valid sequence's distinct first occurrences activate the same set (`lem:first-occurrence`). -/
+theorem first_occurrences {N C : Type*} [DecidableEq C]
+    (required : C → N) (added : C → Set N) (U : Set N) (cs : List C)
+    (h : ActivationOrder required added U cs) :
+    Activatable required added U cs.toFinset := by
+  induction cs generalizing U with
+  | nil => exact ⟨[], by simp, by simp, by simp [ActivationOrder]⟩
+  | cons c cs ih =>
+    obtain ⟨order, hnd, hmem, horder⟩ := ih (U ∪ added c) h.2
+    have hfiltered := horder.filter_of_covered (fun d => decide (d ≠ c)) (by
+      intro d hd hp
+      have heq : d = c := by simpa using hp
+      subst d
+      exact Set.subset_union_right)
+    refine ⟨c :: order.filter (fun d => decide (d ≠ c)), ?_, ?_, h.1, hfiltered⟩
+    · exact List.nodup_cons.mpr ⟨by simp, List.Nodup.filter _ hnd⟩
+    · intro d
+      simp only [List.mem_cons, List.mem_filter, decide_eq_true_eq, hmem,
+        List.mem_toFinset]
+      tauto
+
+/-- After activation, every positive multiplicity is possible (`lem:multiplicities`). -/
+theorem positive_multiplicities {N C : Type*} [DecidableEq C]
+    (required : C → N) (added : C → Set N) (U : Set N) (D : Finset C)
+    (hself : ∀ c ∈ D, required c ∈ added c) (h : Activatable required added U D)
+    (m : C → ℕ) (hm : ∀ c ∈ D, 0 < m c) :
+    ∃ cs : List C, ActivationOrder required added U cs ∧
+      (∀ c, c ∈ cs ↔ c ∈ D) ∧ (∀ c ∈ D, cs.count c = m c) := by
+  obtain ⟨order, hnd, hmem, horder⟩ := h
+  -- Pay for every operation once, then append the requested extra copies.
+  let extra := order.flatMap (fun c => List.replicate (m c - 1) c)
+  have hextra : ∀ c ∈ extra, c ∈ D := by
+    intro c hc
+    obtain ⟨d, hd, hrep⟩ := List.mem_flatMap.mp hc
+    have hcd := List.eq_of_mem_replicate hrep
+    exact hcd ▸ (hmem d).mp hd
+  have hact : ActivationOrder required added U (order ++ extra) :=
+    horder.append_of_covered (by
+      intro c hc
+      have hD := hextra c hc
+      exact Or.inr ⟨c, (hmem c).mpr hD, hself c hD⟩)
+  refine ⟨order ++ extra, hact, ?_, ?_⟩
+  · intro c
+    constructor
+    · intro hc
+      rcases List.mem_append.mp hc with hc | hc
+      · exact (hmem c).mp hc
+      · exact hextra c hc
+    · intro hc
+      exact List.mem_append_left _ ((hmem c).mpr hc)
+  · intro c hc
+    have hone : order.count c = 1 := List.count_eq_one_of_mem hnd ((hmem c).mpr hc)
+    have hcount : extra.count c = m c - 1 := by
+      dsimp only [extra]
+      rw [List.count_flatMap]
+      have hzero : ∀ d, d ≠ c → d ∈ order →
+          (List.count c ∘ fun b => List.replicate (m b - 1) b) d = 0 := by
+        intro d hdc hd
+        simp [List.count_replicate, hdc]
+      rw [List.sum_map_eq_nsmul_single c _ hzero, hone]
+      simp
+    rw [List.count_append, hone, hcount]
+    have hpositive := hm c hc
+    omega
+
+/-- With matching cycles, enabled support transitions are exactly realizable
+tree insertion sequences (`lem:activation-realize`). Repeated cycles are allowed. -/
+theorem activationOrder_iff_insertionSequence {T : Type*} {g : ContextFreeGrammar T}
+    (roots : ParseTree T g.NT → g.NT) (B : ParseTree T g.NT)
+    (Cs : List (ParseTree T g.NT)) (hB : Complete g B)
+    (hCs : ∀ C ∈ Cs, Cycle g C (roots C)) :
+    ActivationOrder roots ParseTree.support B.support Cs ↔
+      ∃ t, InsertionSequence g B Cs t := by
+  classical
+  induction Cs generalizing B with
+  | nil => exact ⟨fun _ => ⟨B, .nil B⟩, fun _ => True.intro⟩
+  | cons C Cs ih =>
+    have hC := hCs C (by simp)
+    have htail : ∀ D ∈ Cs, Cycle g D (roots D) :=
+      fun D hD => hCs D (List.mem_cons_of_mem C hD)
+    constructor
+    · intro horder
+      obtain ⟨next, hstep⟩ := (insertion_enabled g B C (roots C) hB hC).mpr horder.1
+      have hsupport := (insertion_accounting g B C next hstep).2.2.2
+      have hnext : ActivationOrder roots ParseTree.support next.support Cs := by
+        simpa only [hsupport] using horder.2
+      obtain ⟨t, hseq⟩ := (ih next hstep.2.1 htail).mp hnext
+      exact ⟨t, .cons hstep hseq⟩
+    · rintro ⟨t, hseq⟩
+      cases hseq with
+      | @cons _ _ next _ _ hstep hrest =>
+        refine ⟨(insertion_enabled g B C (roots C) hB hC).mp ⟨next, hstep⟩, ?_⟩
+        have hsupport := (insertion_accounting g B C next hstep).2.2.2
+        rw [← hsupport]
+        exact (ih next hstep.2.1 htail).mpr ⟨t, hrest⟩
+
+/-- Exact finite-search interface, implemented by `activationTest` in `ActivationAlgorithm`.
+`lem:activation-test`: no choice of an enabled operation can cause a false rejection.
+-/
+structure ActivationTest (N C : Type*) [DecidableEq N] [DecidableEq C] where
+  /-- Decide whether all operations can be activated from the initial support. -/
+  run : (C → N) → (C → Finset N) → Finset N → Finset C → Bool
+  correct : ∀ required added U D,
+    run required added U D = true ↔
+      Activatable required (fun c => (added c : Set N)) (U : Set N) D
+
+/-- Concrete context subsets do not need a `DecidableEq g.NT` public hypothesis. -/
+@[expose] def ContextsActivatable {T : Type*} (g : ContextFreeGrammar T)
+    (B : ParseTree T g.NT) (D : Finset (ParseTree T g.NT)) : Prop :=
+  ∃ order : List (ParseTree T g.NT), order.Nodup ∧
+    (∀ C, C ∈ order ↔ C ∈ D) ∧
+    ∃ roots : ParseTree T g.NT → g.NT,
+      (∀ C ∈ D, Cycle g C (roots C)) ∧
+      ActivationOrder roots ParseTree.support B.support order
+
+/-- Introduce each selected context once, with exact accounting and every
+selected context enabled afterwards (`lem:activation-realize`, `eq:activated-wt/supp`). -/
+theorem ContextsActivatable.realize {T : Type*} [DecidableEq T]
+    {g : ContextFreeGrammar T} {B : ParseTree T g.NT} {D : Finset (ParseTree T g.NT)}
+    (hD : ContextsActivatable g B D) (hB : Complete g B) :
+    ∃ order t, order.Nodup ∧ (∀ C, C ∈ order ↔ C ∈ D) ∧
+      InsertionSequence g B order t ∧ Complete g t ∧ t.root = B.root ∧
+      t.weight = B.weight + ∑ C ∈ D, C.weight ∧
+      t.support = B.support ∪ ⋃ C ∈ D, C.support ∧
+      ∀ C ∈ D, ∃ t', Inserts g t C t' := by
+  classical
+  obtain ⟨order, hnd, hmem, roots, hcycles, horder⟩ := hD
+  obtain ⟨t, hseq⟩ := (activationOrder_iff_insertionSequence roots B order hB
+    (fun C hC => hcycles C ((hmem C).mp hC))).mp horder
+  obtain ⟨ht, hroot, hweight, _, hsupport⟩ := hseq.accounting hB
+  have hset : order.toFinset = D := by
+    ext C
+    simpa only [List.mem_toFinset] using hmem C
+  have hsum : (order.map ParseTree.weight).sum = ∑ C ∈ D, C.weight := by
+    rw [← hset]
+    exact (List.sum_toFinset ParseTree.weight hnd).symm
+  have hsupportD : t.support = B.support ∪ ⋃ C ∈ D, C.support := by
+    simpa only [hmem] using hsupport
+  refine ⟨order, t, hnd, hmem, hseq, ht, hroot, ?_, hsupportD, ?_⟩
+  · simpa only [hsum] using hweight
+  · intro C hC
+    apply (insertion_enabled g t C (roots C) ht (hcycles C hC)).mpr
+    rw [hsupportD]
+    apply Or.inr
+    simp only [Set.mem_iUnion]
+    exact ⟨C, hC, (hcycles C hC).root_mem_support⟩
+
+/-- Every selected context is paid once in the base (`eq:component-base`). -/
+@[expose] noncomputable def contextComponent {T : Type*} [DecidableEq T]
+    (B : ParseTree T N) (D : Finset (ParseTree T N)) : Component T := by
+  classical
+  exact ⟨B.weight + ∑ C ∈ D, C.weight, D.toList.map ParseTree.weight⟩
+
+/-- Reindex the period list by its context identities (`eq:component`).
+Equal or zero weights retain independent natural coefficients. -/
+theorem contextComponent.mem_denotation_iff {T N : Type*} [DecidableEq T]
+    (B : ParseTree T N) (D : Finset (ParseTree T N)) (v : Vector T) :
+    v ∈ (contextComponent B D).denotation ↔
+      ∃ k : ParseTree T N → ℕ,
+        v = (B.weight + ∑ C ∈ D, C.weight) + ∑ C ∈ D, k C • C.weight := by
+  classical
+  have hrange : Set.range (contextComponent B D).periods.get =
+      Set.range (fun C : D => C.val.weight) := by
+    ext w
+    simp [contextComponent]
+  rw [Component.denotation_eq_vadd_closure, hrange]
+  simp only [Set.mem_vadd_set, SetLike.mem_coe, vadd_eq_add,
+    AddSubmonoid.mem_closure_range_iff_of_fintype]
+  constructor
+  · rintro ⟨w, ⟨k, rfl⟩, rfl⟩
+    let coeff : ParseTree T N → ℕ := fun C => if hC : C ∈ D then k ⟨C, hC⟩ else 0
+    refine ⟨coeff, ?_⟩
+    change (B.weight + ∑ C ∈ D, C.weight) + (∑ C : D, k C • C.val.weight) = _
+    congr 1
+    rw [← Finset.sum_coe_sort D]
+    apply Finset.sum_congr rfl
+    intro C _
+    simp [coeff, C.property]
+  · rintro ⟨k, rfl⟩
+    refine ⟨∑ C : D, k C.val • C.val.weight, ⟨fun C => k C.val, rfl⟩, ?_⟩
+    change (B.weight + ∑ C ∈ D, C.weight) + (∑ C : D, k C.val • C.val.weight) = _
+    rw [Finset.sum_coe_sort D (fun C => k C • C.weight)]
+
+/-- The explicit finite-union formula, retaining context identities (`eq:main`). -/
+@[expose] def treeRepresentation {T : Type*} [DecidableEq T] (g : ContextFreeGrammar T) :
+    Set (Vector T) :=
+  {v | ∃ B D, IsBase g B ∧ (∀ C ∈ D, IsBoundedCycle g C) ∧
+    ContextsActivatable g B D ∧ v ∈ (contextComponent B D).denotation}
+
+/-- The weights obtained using exactly an activatable family of contexts form
+one linear component (`prop:one-linear`).
+Every selected context must occur at least once. These first copies are included
+in the component's base; its period coefficients count additional copies.
+The equality proves both that insertion yields only these vectors and that
+every choice of coefficients can be realized by an insertion sequence. -/
+theorem one_linear {T : Type*} [DecidableEq T] (g : ContextFreeGrammar T)
+    (B : ParseTree T g.NT) (D : Finset (ParseTree T g.NT))
+    (hB : Complete g B) (hD : ContextsActivatable g B D) :
+    {v | ∃ t Cs, InsertionSequence g B Cs t ∧
+      (∀ C, C ∈ Cs ↔ C ∈ D) ∧ t.weight = v} =
+      (contextComponent B D).denotation := by
+  classical
+  have sum_counts : ∀ (Cs : List (ParseTree T g.NT))
+      (hmem : ∀ C, C ∈ Cs ↔ C ∈ D),
+      (Cs.map ParseTree.weight).sum = ∑ C ∈ D, Cs.count C • C.weight := by
+    intro Cs hmem
+    have hset : Cs.toFinset = D := by
+      ext C
+      simpa only [List.mem_toFinset] using hmem C
+    rw [Finset.sum_list_map_count, hset]
+  ext v
+  rw [contextComponent.mem_denotation_iff]
+  constructor
+  · rintro ⟨t, Cs, hseq, hmem, rfl⟩
+    refine ⟨fun C => Cs.count C - 1, ?_⟩
+    rw [(hseq.accounting hB).2.2.1, sum_counts Cs hmem]
+    have hsplit : ∑ C ∈ D, Cs.count C • C.weight =
+        (∑ C ∈ D, C.weight) + ∑ C ∈ D, (Cs.count C - 1) • C.weight := by
+      rw [← Finset.sum_add_distrib]
+      apply Finset.sum_congr rfl
+      intro C hC
+      have hpositive : 0 < Cs.count C := List.count_pos_iff.mpr ((hmem C).mpr hC)
+      have hcount : Cs.count C = 1 + (Cs.count C - 1) := by omega
+      conv_lhs => rw [hcount]
+      rw [add_nsmul, one_nsmul]
+    rw [hsplit, add_assoc]
+  · rintro ⟨k, rfl⟩
+    obtain ⟨order, hnd, hmem, roots, hcycles, horder⟩ := hD
+    have hact : Activatable roots ParseTree.support B.support D := ⟨order, hnd, hmem, horder⟩
+    obtain ⟨Cs, hCs, hCs_mem, hcount⟩ := positive_multiplicities roots ParseTree.support
+      B.support D (fun C hC => (hcycles C hC).root_mem_support) hact
+      (fun C => k C + 1) (by simp)
+    obtain ⟨t, hseq⟩ := (activationOrder_iff_insertionSequence roots B Cs hB
+      (fun C hC => hcycles C ((hCs_mem C).mp hC))).mp hCs
+    refine ⟨t, Cs, hseq, hCs_mem, ?_⟩
+    rw [(hseq.accounting hB).2.2.1, sum_counts Cs hCs_mem]
+    have hsplit : ∑ C ∈ D, Cs.count C • C.weight =
+        (∑ C ∈ D, C.weight) + ∑ C ∈ D, k C • C.weight := by
+      rw [← Finset.sum_add_distrib]
+      apply Finset.sum_congr rfl
+      intro C hC
+      rw [hcount C hC, add_nsmul, one_nsmul, add_comm]
+    rw [hsplit, add_assoc]
+
+/-- The distinct contexts used by an insertion sequence are activatable from
+its complete base (`lem:first-occurrence`, `thm:main`). Context identities are retained. -/
+theorem InsertionSequence.contextsActivatable {T : Type*} {g : ContextFreeGrammar T}
+    {B t : ParseTree T g.NT} {Cs : List (ParseTree T g.NT)}
+    [DecidableEq (ParseTree T g.NT)]
+    (h : InsertionSequence g B Cs t) (hB : Complete g B) :
+    ContextsActivatable g B Cs.toFinset := by
+  classical
+  have hcycles : ∀ C ∈ Cs, ∃ A, Cycle g C A := by
+    clear hB
+    induction h with
+    | nil _ => simp
+    | cons step _ ih =>
+      intro C hC
+      rcases List.mem_cons.mp hC with rfl | hC
+      · obtain ⟨_, _, A, hcycle, _⟩ := step
+        exact ⟨A, hcycle⟩
+      · exact ih C hC
+  let roots : ParseTree T g.NT → g.NT := fun C =>
+    if hC : C ∈ Cs then Classical.choose (hcycles C hC) else g.initial
+  have hrootcycles : ∀ C ∈ Cs, Cycle g C (roots C) := by
+    intro C hC
+    simpa only [roots, dite_eq_left hC] using Classical.choose_spec (hcycles C hC)
+  have horder := (activationOrder_iff_insertionSequence roots B Cs hB hrootcycles).mpr ⟨t, h⟩
+  obtain ⟨order, hnodup, hmem, hfirst⟩ :=
+    first_occurrences roots ParseTree.support B.support Cs horder
+  exact ⟨order, hnodup, hmem, roots,
+    fun C hC => hrootcycles C (List.mem_toFinset.mp hC), hfirst⟩
+
+end Parikh
diff --git a/LeanPool/Parikh/ActivationAlgorithm.lean b/LeanPool/Parikh/ActivationAlgorithm.lean
new file mode 100644
index 0000000000..b19d1aa835
--- /dev/null
+++ b/LeanPool/Parikh/ActivationAlgorithm.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-! Executable activation testing (`lem:activation-test`). Each round processes
+all currently enabled operations. This uses finite-set operations, not a chosen
+ordering or a classical selection function. The proof stays independent of grammar syntax.
+-/
+namespace Parikh
+
+namespace ActivationOrder
+variable {N C : Type*} {required : C → N} {added : C → Set N}
+
+/-- More available labels preserve every enabled operation order. -/
+theorem mono {U V : Set N} {cs : List C} (h : ActivationOrder required added U cs)
+    (hUV : U ⊆ V) : ActivationOrder required added V cs := by
+  induction cs generalizing U V with
+  | nil => trivial
+  | cons c cs ih =>
+    refine ⟨hUV h.1, ih h.2 ?_⟩
+    exact Set.union_subset_union_left _ hUV
+end ActivationOrder
+
+namespace Activatable
+variable {N C : Type*} [DecidableEq C]
+
+/-- Any currently enabled operation may be processed first, without changing
+whether all operations can be activated (`lem:activation-test`). -/
+theorem erase_iff_of_enabled (required : C → N) (added : C → Set N) (U : Set N)
+    (D : Finset C) (c : C) (hc : c ∈ D) (henabled : required c ∈ U) :
+    Activatable required added U D ↔ Activatable required added (U ∪ added c) (D.erase c) := by
+  constructor
+  · rintro ⟨order, hnodup, hmem, horder⟩
+    -- Pay for `c` first, then omit it from the old order: its support is already available.
+    have hmore := horder.mono (V := U ∪ added c) Set.subset_union_left
+    have hfiltered := hmore.filter_of_covered (fun d => decide (d ≠ c)) (by
+      intro d _ hp
+      have : d = c := by simpa using hp
+      subst d
+      exact Set.subset_union_right)
+    refine ⟨order.filter (fun d => decide (d ≠ c)), hnodup.filter _, ?_, hfiltered⟩
+    intro d
+    simp only [List.mem_filter, decide_eq_true_eq, hmem, Finset.mem_erase]
+    tauto
+  · rintro ⟨order, hnodup, hmem, horder⟩
+    -- Conversely, prepend the enabled operation to an order for the remaining set.
+    refine ⟨c :: order, List.nodup_cons.mpr ⟨?_, hnodup⟩, ?_, henabled, horder⟩
+    · simpa using (hmem c).mp
+    · intro d
+      simp only [List.mem_cons, hmem, Finset.mem_erase]
+      by_cases hd : d = c
+      · subst d; simp [hc]
+      · tauto
+
+/-- A whole subset enabled at the start can be processed together. Each member
+still occurs exactly once; its added labels are accumulated by finite union. -/
+theorem batch_iff_of_enabled [DecidableEq N] (required : C → N) (added : C → Finset N)
+    (U : Finset N) (D E : Finset C) (hED : E ⊆ D)
+    (henabled : ∀ c ∈ E, required c ∈ U) :
+    Activatable required (fun c => (added c : Set N)) (U : Set N) D ↔
+      Activatable required (fun c => (added c : Set N))
+        ((U ∪ E.biUnion added : Finset N) : Set N) (D \ E) := by
+  induction E using Finset.induction_on generalizing U D with
+  | empty => simp
+  | @insert c E hc ih =>
+    have hcD : c ∈ D := hED (Finset.mem_insert_self _ _)
+    have hroot : required c ∈ U := henabled c (Finset.mem_insert_self _ _)
+    have hED' : E ⊆ D.erase c := by
+      intro d hd
+      exact Finset.mem_erase.mpr ⟨by intro h; subst d; exact hc hd,
+        hED (Finset.mem_insert_of_mem hd)⟩
+    have hroot' : ∀ d ∈ E, required d ∈ U ∪ added c := by
+      intro d hd
+      exact Finset.mem_union_left _ (henabled d (Finset.mem_insert_of_mem hd))
+    have hrem : D.erase c \ E = D \ insert c E := by
+      ext d
+      simp only [Finset.mem_sdiff, Finset.mem_erase, Finset.mem_insert]
+      tauto
+    -- Process one enabled member, then apply the induction hypothesis to the rest of the batch.
+    calc
+      _ ↔ Activatable required (fun d => (added d : Set N))
+          ((U ∪ added c : Finset N) : Set N) (D.erase c) := by
+        simpa only [Finset.coe_union] using
+          erase_iff_of_enabled required (fun d => (added d : Set N)) U D c hcD hroot
+      _ ↔ Activatable required (fun d => (added d : Set N))
+          (((U ∪ added c) ∪ E.biUnion added : Finset N) : Set N) (D.erase c \ E) :=
+        ih _ _ hED' hroot'
+      _ ↔ _ := by rw [Finset.biUnion_insert, ← Finset.union_assoc, hrem]
+end Activatable
+
+variable {N C : Type*} [DecidableEq N] [DecidableEq C]
+
+/-- Run at most `fuel` rounds. Reject if unprocessed operations remain with none
+enabled. No operation is processed more than once; neither type must be finite. -/
+@[expose] def activationRounds (required : C → N) (added : C → Finset N) (fuel : ℕ) :
+    Finset N → Finset C → Bool :=
+  Nat.rec (motive := fun _ => Finset N → Finset C → Bool)
+    (fun _ D => decide (D = ∅))
+    (fun _ next U D =>
+      if D = ∅ then true else
+        let enabled := D.filter (fun c => required c ∈ U)
+        if enabled = ∅ then false else
+          next (U ∪ enabled.biUnion added) (D \ enabled)) fuel
+
+/-- Sufficient fuel gives an exact decision of the accepted activation predicate,
+without assuming an operation adds its own required label (`lem:activation-test`). -/
+theorem activationRounds_correct (required : C → N) (added : C → Finset N)
+    (fuel : ℕ) (U : Finset N) (D : Finset C) (hfuel : D.card ≤ fuel) :
+    activationRounds required added fuel U D = true ↔
+      Activatable required (fun c => (added c : Set N)) (U : Set N) D := by
+  have hempty (V : Finset N) :
+      Activatable required (fun c => (added c : Set N)) (V : Set N) ∅ :=
+    ⟨[], by simp, by simp, trivial⟩
+  induction fuel generalizing U D with
+  | zero =>
+    have hD : D = ∅ := Finset.card_eq_zero.mp (Nat.eq_zero_of_le_zero hfuel)
+    subst D
+    exact ⟨fun _ => hempty U, fun _ => rfl⟩
+  | succ fuel ih =>
+    by_cases hD : D = ∅
+    · subst D
+      simp only [activationRounds, ↓reduceIte, true_iff]
+      exact hempty U
+    · let enabled := D.filter (fun c => required c ∈ U)
+      have hsub : enabled ⊆ D := Finset.filter_subset _ _
+      have hroot : ∀ c ∈ enabled, required c ∈ U :=
+        fun _ hc => (Finset.mem_filter.mp hc).2
+      by_cases hE : enabled = ∅
+      · have hnot : ¬ Activatable required (fun c => (added c : Set N)) (U : Set N) D := by
+          -- A nonempty successful order would have an enabled first operation.
+          rintro ⟨order, _, hmem, horder⟩
+          cases order with
+          | nil =>
+            apply hD
+            ext c
+            simpa using (hmem c).symm
+          | cons c cs =>
+            have hc : c ∈ enabled := Finset.mem_filter.mpr
+              ⟨(hmem c).mp (by simp), horder.1⟩
+            simp [hE] at hc
+        simp only [activationRounds, hD, ↓reduceIte]
+        change (if enabled = ∅ then false else _) = true ↔ _
+        simp [hE, hnot]
+      · have hprogress : 0 < enabled.card := Finset.card_pos.mpr
+          (Finset.nonempty_iff_ne_empty.mpr hE)
+        have hcard := Finset.card_sdiff_of_subset hsub
+        -- A nonempty batch removes at least one operation, preserving the fuel invariant.
+        have hremaining : (D \ enabled).card ≤ fuel := by omega
+        simp only [activationRounds, hD, ↓reduceIte]
+        change (if enabled = ∅ then false else _) = true ↔ _
+        simp only [hE, ↓reduceIte]
+        exact (ih (U ∪ enabled.biUnion added) (D \ enabled) hremaining).trans
+          (Activatable.batch_iff_of_enabled required added U D enabled hsub hroot).symm
+
+/-- An executable value of the accepted interface. Its correctness
+field is proved above; its runtime uses only equality, finite sets and recursion. -/
+@[expose] def activationTest (N C : Type*) [DecidableEq N] [DecidableEq C] :
+    ActivationTest N C where
+  run required added U D := activationRounds required added D.card U D
+  correct required added U D := activationRounds_correct required added D.card U D le_rfl
+
+end Parikh
diff --git a/LeanPool/Parikh/Api.lean b/LeanPool/Parikh/Api.lean
new file mode 100644
index 0000000000..6de4e7a7e1
--- /dev/null
+++ b/LeanPool/Parikh/Api.lean
@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.ExecutableCompiler
+public import Mathlib.Computability.DFA
+import LeanPool.Parikh.RegularRealization
+import LeanPool.Parikh.Statements
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Public interface
+
+Count letters with `parikhVector` and take a language's `parikhImage`.
+The main theorems give semilinearity, finite representations, and regular
+languages with the same image. `compileGrammar` computes a representation
+from a finite encoded grammar.
+-/
+namespace Parikh
+
+/-- A natural-number count for each letter in the alphabet. -/
+abbrev CountVector (T : Type*) := Vector T
+
+/-- One base vector and a finite list of period vectors. -/
+abbrev LinearComponent (T : Type*) := Component T
+
+/-- A finite list of linear components. -/
+abbrev SemilinearRepresentation (T : Type*) := Witness T
+
+/-- The vector recording how often each letter occurs in a word. -/
+abbrev parikhVector {T : Type*} [DecidableEq T] (w : List T) : CountVector T := counts w
+
+/-- The set of count vectors of the words in a language. -/
+abbrev parikhImage {T : Type*} [DecidableEq T] (L : Language T) : Set (CountVector T) := image L
+
+/-- The base plus arbitrary natural multiples of the indexed periods. -/
+abbrev LinearComponent.denotation {T : Type*} (c : LinearComponent T) : Set (CountVector T) :=
+  Component.denotation c
+
+/-- The union of the represented linear sets. -/
+abbrev SemilinearRepresentation.denotation {T : Type*}
+    (W : SemilinearRepresentation T) : Set (CountVector T) := Witness.denotation W
+
+/-- Concatenating words adds their count vectors. -/
+theorem parikhVector_append {T : Type*} [DecidableEq T] (u v : List T) :
+    parikhVector (u ++ v) = parikhVector u + parikhVector v := counts_append u v
+
+/-- Each component denotes a linear set in Mathlib's sense. -/
+theorem LinearComponent.isLinearSet {T : Type*} (c : LinearComponent T) :
+    IsLinearSet c.denotation := component_isLinearSet c
+
+/-- Every finite representation denotes a semilinear set. -/
+theorem SemilinearRepresentation.isSemilinearSet {T : Type*}
+    (W : SemilinearRepresentation T) : IsSemilinearSet W.denotation := witness_isSemilinearSet W
+
+/-- The Parikh image of a context-free grammar is semilinear. -/
+theorem parikhImage_isSemilinear_of_grammar {T : Type*} [Finite T] [DecidableEq T]
+    (g : ContextFreeGrammar T) : IsSemilinearSet (parikhImage g.language) := grammar_image g
+
+/-- Parikh's theorem for a context-free language over a finite alphabet. -/
+theorem parikhImage_isSemilinear_of_isContextFree {T : Type*} [Finite T] [DecidableEq T]
+    (L : Language T) (hL : L.IsContextFree) : IsSemilinearSet (parikhImage L) :=
+  contextFree_image L hL
+
+/-- The Parikh image of a regular language is semilinear. -/
+theorem parikhImage_isSemilinear_of_isRegular {T : Type*} [Finite T] [DecidableEq T]
+    (L : Language T) (hL : L.IsRegular) : IsSemilinearSet (parikhImage L) := regular_image L hL
+
+/-- Every grammar has a finite representation of exactly its Parikh image. -/
+theorem exists_semilinearRepresentation_of_grammar {T : Type*} [Finite T] [DecidableEq T]
+    (g : ContextFreeGrammar T) :
+    ∃ W : SemilinearRepresentation T, W.denotation = parikhImage g.language := grammar_witness g
+
+/-- An exact representation also exists within the grammar's size bounds. -/
+theorem exists_boundedSemilinearRepresentation_of_grammar {T : Type*}
+    [Fintype T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    ∃ W : SemilinearRepresentation T,
+      W.denotation = parikhImage g.language ∧ WithinBounds (grammarSize g) W := bounded_witness g
+
+/-- Every semilinear set is the Parikh image of a regular language. -/
+theorem exists_regularLanguage_with_parikhImage {T : Type*} [Finite T] [DecidableEq T]
+    (X : Set (CountVector T)) (hX : IsSemilinearSet X) :
+    ∃ R : Language T, R.IsRegular ∧ parikhImage R = X := converse X hX
+
+/-- Every context-free grammar has a regular language with the same Parikh image. -/
+theorem exists_regularLanguage_with_grammar_parikhImage {T : Type*}
+    [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    ∃ R : Language T, R.IsRegular ∧ parikhImage R = parikhImage g.language := regular_realization g
+
+/-- Compute an exact finite representation from a grammar with numeric labels. -/
+abbrev compileGrammar (g : EncodedGrammar) : SemilinearRepresentation (Fin g.terminalCount) :=
+  compiler.compile g
+
+/-- The computed representation denotes exactly the grammar's Parikh image. -/
+theorem compileGrammar_correct (g : EncodedGrammar) :
+    (compileGrammar g).denotation = parikhImage g.decode.language := compiler.correct g
+
+/-- The computed representation satisfies the component, period, and norm bounds. -/
+theorem compileGrammar_size_bounds (g : EncodedGrammar) :
+    WithinBounds g.size (compileGrammar g) := compiler.bounded g
+
+/-- The computed coordinates fit the fixed-width numerical bit budget. -/
+theorem compileGrammar_bit_bound (g : EncodedGrammar) :
+    entryBits g.size (compileGrammar g) ≤ g.size.vectorBits ∧
+      (∀ c ∈ compileGrammar g, ∀ a, c.base a < 2 ^ g.size.coordinateBits) ∧
+      (∀ c ∈ compileGrammar g, ∀ p ∈ c.periods, ∀ a, p a < 2 ^ g.size.coordinateBits) :=
+  g.compile_bit_bound
+
+end Parikh
diff --git a/LeanPool/Parikh/BoundedCutSupport.lean b/LeanPool/Parikh/BoundedCutSupport.lean
new file mode 100644
index 0000000000..16906ad3fb
--- /dev/null
+++ b/LeanPool/Parikh/BoundedCutSupport.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+import LeanPool.Parikh.ParseTreePaths
+import Mathlib.Algebra.Order.Group.Nat
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Finding a small context inside a non-simple tree
+
+A repeated label on a path suggests a removable cycle, but an arbitrary
+choice could leave very large side branches in that cycle. We instead find
+a minimal non-simple subtree: all its children are simple, so their heights
+are bounded. A repeated occurrence of its root then determines a bounded cut.
+
+These lemmas justify the selection, bounds, and reversible replacement used
+by `bounded_cut`. Progress is measured by production nodes, because removing
+a cycle need not shorten the terminal word.
+
+Source: `lem:cut`.
+-/
+namespace Parikh
+variable {T N : Type*}
+
+namespace ParseTree
+
+/-- Filling holes cannot reduce production height. -/
+theorem height_le_height_plug (E t : ParseTree T N) : E.height ≤ (E.plug t).height := by
+  induction E using ParseTree.rec (motive_2 := fun cs =>
+    ∀ c ∈ cs, c.height ≤ (c.plug t).height) with
+  | terminal a => simp [height, plug]
+  | hole A => simp [height, plug]
+  | node r cs ih =>
+    simp only [plug, height, List.map_map, List.foldl_map]
+    apply Nat.add_le_add_left
+    exact List.foldl_rel (r := (· ≤ ·)) (Nat.le_refl 0)
+      (fun c hc a b hab => max_le_max hab (ih c hc))
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc
+    · exact hcs d hd
+
+/-- Replacement retains the selected position and can be undone exactly. -/
+theorem subtree_replacement (t : ParseTree T N) (q : List ℕ) (u v : ParseTree T N)
+    (hpos : t.subtree q = some u) :
+    ∃ t', t.replaceAt q v = some t' ∧ t'.subtree q = some v ∧
+      t'.replaceAt q u = some t := by
+  induction q generalizing t with
+  | nil =>
+    simp only [subtree, Option.some.injEq] at hpos
+    subst u
+    exact ⟨v, rfl, rfl, rfl⟩
+  | cons i q ih =>
+    cases t with
+    | terminal a => simp [subtree] at hpos
+    | hole A => simp [subtree] at hpos
+    | node r cs =>
+      obtain ⟨c, hi, hpos⟩ := Option.bind_eq_some_iff.mp hpos
+      obtain ⟨c', hreplace, hsub, hundo⟩ := ih c hpos
+      obtain ⟨hlt, helem⟩ := List.getElem?_eq_some_iff.mp hi
+      have hset : cs.set i c = cs := by
+        rw [← helem]
+        exact List.set_getElem_self hlt
+      refine ⟨.node r (cs.set i c'), ?_, ?_, ?_⟩
+      · simp [replaceAt, hi, hreplace]
+      · simp [subtree, List.getElem?_set_self hlt, hsub]
+      · simp [replaceAt, List.getElem?_set_self hlt, hundo, List.set_set, hset]
+
+/-- A proper subtree has strictly fewer production nodes than its parent tree. -/
+theorem productionSize_subtree_bound (t : ParseTree T N) (q : List ℕ)
+    (u : ParseTree T N) (hpos : t.subtree q = some u) :
+    u.productionSize ≤ t.productionSize ∧
+      (q ≠ [] → u.productionSize < t.productionSize) := by
+  induction q generalizing t with
+  | nil =>
+    simp only [subtree, Option.some.injEq] at hpos
+    subst u
+    exact ⟨le_rfl, by simp⟩
+  | cons i q ih =>
+    cases t with
+    | terminal a => simp [subtree] at hpos
+    | hole A => simp [subtree] at hpos
+    | node r cs =>
+      obtain ⟨c, hi, hpos⟩ := Option.bind_eq_some_iff.mp hpos
+      have huc := (ih c hpos).1
+      have hmem : c.productionSize ∈ cs.map productionSize :=
+        List.mem_map_of_mem (List.mem_of_getElem? hi)
+      have hsum := List.single_le_sum (fun n _ => Nat.zero_le n) _ hmem
+      simp only [productionSize]
+      constructor <;> omega
+
+/-- With simple children, a non-simple node repeats its root in a child. -/
+theorem exists_root_mem_child_support (r : ContextFreeRule T N)
+    (cs : List (ParseTree T N)) (hs : ¬ (node r cs).Simple)
+    (hc : ∀ c ∈ cs, c.Simple) : ∃ c ∈ cs, r.input ∈ c.support := by
+  by_contra h
+  apply hs
+  intro path hp
+  simp only [labelPaths, List.mem_cons, List.mem_map, ← List.flatMap_def,
+    List.mem_flatMap] at hp
+  rcases hp with rfl | ⟨tail, ⟨c, hcmem, htail⟩, rfl⟩
+  · simp
+  · apply List.nodup_cons.mpr
+    refine ⟨?_, hc c hcmem tail htail⟩
+    intro hA
+    exact h ⟨c, hcmem, c.labelPath_subset_support tail htail r.input hA⟩
+
+end ParseTree
+
+/-- Descend through non-simple children until every child is simple. This selects
+the source's minimal non-simple occurrence without a finite ambient alphabet. -/
+theorem Complete.exists_minimal_nonsimple_subtree {g : ContextFreeGrammar T}
+    {t : ParseTree T g.NT} (ht : Complete g t) (hs : ¬ t.Simple) :
+    ∃ q r cs, t.subtree q = some (.node r cs) ∧ Complete g (.node r cs) ∧
+      ¬ (ParseTree.node r cs).Simple ∧ ∀ c ∈ cs, c.Simple := by
+  obtain ⟨hv, hh⟩ := ht
+  induction hv with
+  | terminal a => simp [ParseTree.Simple, ParseTree.labelPaths] at hs
+  | hole A => simp [ParseTree.holes] at hh
+  | node r cs hr hc roots ih =>
+    have hholes : ∀ c ∈ cs, c.holes = [] := by
+      simpa only [ParseTree.holes, List.flatten_eq_nil_iff, List.forall_mem_map] using hh
+    by_cases hsimple : ∀ c ∈ cs, c.Simple
+    · exact ⟨[], r, cs, rfl, ⟨.node r cs hr hc roots, hh⟩, hs, hsimple⟩
+    · push Not at hsimple
+      obtain ⟨c, hcmem, hcs⟩ := hsimple
+      obtain ⟨q, r', cs', hq, ht', hs', hchildren⟩ :=
+        ih c hcmem hcs (hholes c hcmem)
+      obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp hcmem
+      exact ⟨i :: q, r', cs', by simp [ParseTree.subtree, hi, hq], ht', hs', hchildren⟩
+
+end Parikh
diff --git a/LeanPool/Parikh/BoundedEnumeration.lean b/LeanPool/Parikh/BoundedEnumeration.lean
new file mode 100644
index 0000000000..0211c87d86
--- /dev/null
+++ b/LeanPool/Parikh/BoundedEnumeration.lean
@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Construction
+import Mathlib.Algebra.Order.Group.Nat
+import Mathlib.Data.List.Sections
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Computing all valid trees up to a height bound
+
+At height zero, enumerate every terminal leaf and every declared nonterminal hole.
+At the next height, choose a production and a smaller tree for each right-hand-side
+symbol. Mathlib's `List.sections` enumerates these ordered Cartesian products;
+filtering the child families by root makes every generated node valid.
+
+The result includes open trees, unused declared symbols and empty productions.
+Duplicate input productions are removed before expansion. The accepted interface
+requires exact membership, without prescribing duplicate multiplicities.
+
+Source: `lem:finite`, `sec:effective`.
+-/
+namespace Parikh
+
+namespace ParseTree
+variable {T N : Type*}
+
+/-- The height of a production node in terms of its child heights. -/
+theorem height_node_eq (r : ContextFreeRule T N) (children : List (ParseTree T N)) :
+    (node r children).height = 1 + (children.map height).foldl max 0 := by
+  exact height.eq_3 r children
+
+/-- A node fits the next height bound exactly when every child fits the current bound. -/
+theorem height_node_le_iff (r : ContextFreeRule T N) (children : List (ParseTree T N))
+    (H : ℕ) : (node r children).height ≤ H + 1 ↔ ∀ c ∈ children, c.height ≤ H := by
+  rw [height_node_eq]
+  constructor
+  · intro hh c hc
+    have hm : c.height ∈ children.map height := List.mem_map_of_mem hc
+    have hmax := List.le_max_of_mem hm
+    rw [List.foldl_max_eq_max (List.ne_nil_of_mem hm), Nat.zero_max] at hh
+    omega
+  · intro hchildren
+    have hfold : (children.map height).foldl max 0 ≤ H := by
+      by_cases hnil : children = []
+      · simp [hnil]
+      · have hne : children.map height ≠ [] := fun h => hnil (List.map_eq_nil_iff.mp h)
+        rw [List.foldl_max_eq_max hne, Nat.zero_max]
+        apply (List.max_le_iff hne).mpr
+        intro n hn
+        obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hn
+        exact hchildren c hc
+    omega
+
+/-- Root-filtered Cartesian products preserve both child membership and child order. -/
+theorem mem_root_sections [DecidableEq T] [DecidableEq N]
+    (family : List (ParseTree T N)) (symbols : List (Symbol T N))
+    (children : List (ParseTree T N)) :
+    children ∈ (symbols.map (fun s => family.filter (fun t => decide (t.root = s)))).sections ↔
+      (∀ c ∈ children, c ∈ family) ∧ children.map root = symbols := by
+  rw [List.mem_sections, List.forall₂_map_right_iff]
+  simp only [List.mem_filter, decide_eq_true_eq]
+  rw [List.forall₂_and_left, ← List.forall₂_map_left_iff, List.forall₂_eq_eq_eq]
+end ParseTree
+
+/-- The three checks required at a production node, as a reusable elimination rule. -/
+theorem Valid.node_iff {T : Type*} (g : ContextFreeGrammar T)
+    (r : ContextFreeRule T g.NT) (children : List (ParseTree T g.NT)) :
+    Valid g (.node r children) ↔ r ∈ g.rules ∧
+      (∀ c ∈ children, Valid g c) ∧ children.map ParseTree.root = r.output := by
+  constructor
+  · intro hv
+    cases hv with
+    | node _ _ hr hc roots => exact ⟨hr, hc, roots⟩
+  · rintro ⟨hr, hc, roots⟩
+    exact Valid.node (g := g) r children hr hc roots
+
+namespace EncodedGrammar
+
+/-- Every declared leaf, including holes for nonterminals absent from productions. -/
+@[expose] def leaves (g : EncodedGrammar) :
+    List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :=
+  (List.finRange g.terminalCount).map ParseTree.terminal ++
+    (List.finRange (g.extraNonterminalCount + 1)).map ParseTree.hole
+
+/-- The height-zero family is exactly all valid leaves (`lem:finite`). -/
+theorem leaves_correct (g : EncodedGrammar)
+    (t : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :
+    t ∈ g.leaves ↔ Valid g.decode t ∧ t.height = 0 := by
+  constructor
+  · intro ht
+    simp only [leaves, List.mem_append, List.mem_map, List.mem_finRange, true_and] at ht
+    rcases ht with ⟨a, rfl⟩ | ⟨A, rfl⟩
+    · exact ⟨Valid.terminal (g := g.decode) a, by simp [ParseTree.height]⟩
+    · exact ⟨Valid.hole (g := g.decode) A, by simp [ParseTree.height]⟩
+  · rintro ⟨hv, hh⟩
+    cases t with
+    | terminal a => simp [leaves]
+    | hole A => simp [leaves]
+    | node r children =>
+      rw [ParseTree.height_node_eq] at hh
+      omega
+
+/-- Enumerate valid open trees by height, using finite ordered child products.
+Explicit natural-number recursion supplies a computable implementation. -/
+@[expose] def enumerateTrees (g : EncodedGrammar) (H : ℕ) :
+    List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :=
+  Nat.rec (motive := fun _ =>
+      List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))))
+    g.leaves
+    (fun _ smaller => g.leaves ++ g.rules.dedup.flatMap (fun r =>
+      ((r.output.map (fun s => smaller.filter (fun t => decide (t.root = s)))).sections).map
+        (ParseTree.node r))) H
+
+/-- Every generated tree is valid and within the bound, and every such tree is
+generated. This is the exact accepted enumeration contract (`lem:finite`). -/
+theorem enumerateTrees_correct (g : EncodedGrammar) (H : ℕ)
+    (t : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :
+    t ∈ g.enumerateTrees H ↔ Valid g.decode t ∧ t.height ≤ H := by
+  induction H generalizing t with
+  | zero =>
+    change t ∈ g.leaves ↔ _
+    simpa only [Nat.le_zero_eq] using g.leaves_correct t
+  | succ H ih =>
+    change t ∈ g.leaves ++ g.rules.dedup.flatMap (fun r =>
+      ((r.output.map (fun s => (g.enumerateTrees H).filter (fun c => decide (c.root =
+        s)))).sections).map
+        (ParseTree.node r)) ↔ _
+    constructor
+    · intro ht
+      rcases List.mem_append.mp ht with hleaf | hnode
+      · have h := (g.leaves_correct t).mp hleaf
+        exact ⟨h.1, by omega⟩
+      · obtain ⟨r, hr, hmap⟩ := List.mem_flatMap.mp hnode
+        obtain ⟨cs, hsection, rfl⟩ := List.mem_map.mp hmap
+        have h := (ParseTree.mem_root_sections _ _ _).mp hsection
+        have hchildren : ∀ c ∈ cs, Valid g.decode c ∧ c.height ≤ H :=
+          fun c hc => (ih c).mp (h.1 c hc)
+        refine ⟨Valid.node (g := g.decode) r cs ?_ (fun c hc => (hchildren c hc).1) h.2, ?_⟩
+        · change r ∈ g.rules.toFinset
+          exact List.mem_toFinset.mpr (List.mem_dedup.mp hr)
+        · exact (ParseTree.height_node_le_iff r cs H).mpr (fun c hc => (hchildren c hc).2)
+    · rintro ⟨hv, hh⟩
+      cases t with
+      | terminal a =>
+        exact List.mem_append_left _ ((g.leaves_correct _).mpr
+          ⟨Valid.terminal (g := g.decode) a, by simp [ParseTree.height]⟩)
+      | hole A =>
+        exact List.mem_append_left _ ((g.leaves_correct _).mpr
+          ⟨Valid.hole (g := g.decode) A, by simp [ParseTree.height]⟩)
+      | node r cs =>
+        obtain ⟨hr, hchildren, roots⟩ := (Valid.node_iff g.decode r cs).mp hv
+        change r ∈ g.rules.toFinset at hr
+        apply List.mem_append_right
+        apply List.mem_flatMap.mpr
+        refine ⟨r, List.mem_dedup.mpr (List.mem_toFinset.mp hr),
+          List.mem_map.mpr ⟨cs, ?_, rfl⟩⟩
+        apply (ParseTree.mem_root_sections _ _ _).mpr
+        refine ⟨?_, roots⟩
+        have hheight := (ParseTree.height_node_le_iff r cs H).mp hh
+        exact fun c hc => (ih c).mpr ⟨hchildren c hc, hheight c hc⟩
+end EncodedGrammar
+
+/-- An executable value of the accepted enumeration interface, with its complete
+correctness proof and no classical runtime selection (`lem:finite`). -/
+@[expose] def boundedEnumeration : BoundedEnumeration where
+  enumerate := EncodedGrammar.enumerateTrees
+  correct := EncodedGrammar.enumerateTrees_correct
+
+end Parikh
diff --git a/LeanPool/Parikh/BoundedFamilySupport.lean b/LeanPool/Parikh/BoundedFamilySupport.lean
new file mode 100644
index 0000000000..d8f55c3103
--- /dev/null
+++ b/LeanPool/Parikh/BoundedFamilySupport.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Data.Fintype.BigOperators
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Counting bounded tree syntax
+
+For counting, root compatibility may be discarded: every valid active open
+tree is covered by choosing a production and a child tuple of its fixed arity.
+Mathlib's finite function spaces count the tuples, and finite unions bound
+each height layer. This is a classical overcount, not an executable enumerator.
+The existing executable enumerator retains the root checks.
+
+Source: `lem:count-trees`.
+-/
+namespace Parikh
+
+/-- The number of positions in a full `b`-ary tree through depth `H`. -/
+@[expose] def heightPositions (b H : ℕ) : ℕ := ∑ i ∈ Finset.range (H + 1), b ^ i
+
+theorem heightPositions_zero (b : ℕ) : heightPositions b 0 = 1 := by
+  simp [heightPositions]
+
+theorem heightPositions_succ (b H : ℕ) :
+    heightPositions b (H + 1) = 1 + b * heightPositions b H := by
+  unfold heightPositions
+  rw [Finset.sum_range_succ']
+  simp only [pow_succ', pow_zero]
+  rw [Finset.mul_sum]
+  omega
+
+theorem heightPositions_pos (b H : ℕ) : 1 ≤ heightPositions b H := by
+  cases H with
+  | zero => simp [heightPositions_zero]
+  | succ H => rw [heightPositions_succ]; omega
+
+namespace ParseTree
+variable {T N : Type*}
+
+/-- Every child's height is strictly smaller than its production node's height. -/
+theorem height_child_lt (r : ContextFreeRule T N) (children : List (ParseTree T N))
+    (c : ParseTree T N) (hc : c ∈ children) : c.height < (node r children).height := by
+  have hm : c.height ∈ children.map height := List.mem_map_of_mem hc
+  have hmax := List.le_max_of_mem hm
+  rw [height.eq_3, List.foldl_max_eq_max (List.ne_nil_of_mem hm), Nat.zero_max]
+  omega
+
+/-- All ordered child tuples from a finite family, at a production's fixed arity. -/
+@[expose] noncomputable def nodeFamily (r : ContextFreeRule T N) (family : Finset (ParseTree T N)) :
+    Finset (ParseTree T N) := by
+  classical
+  exact Finset.univ.image fun f : Fin r.output.length → family =>
+    node r (List.ofFn fun i => (f i).val)
+
+theorem mem_nodeFamily (r : ContextFreeRule T N) (family : Finset (ParseTree T N))
+    (children : List (ParseTree T N)) (hlen : children.length = r.output.length)
+    (hchildren : ∀ c ∈ children, c ∈ family) : node r children ∈ nodeFamily r family := by
+  classical
+  let f : Fin r.output.length → family := fun i =>
+    ⟨children[i.val]'(by omega), hchildren _ (List.getElem_mem (by omega))⟩
+  apply Finset.mem_image.mpr
+  refine ⟨f, Finset.mem_univ _, ?_⟩
+  congr 1
+  apply List.ext_getElem <;> simp [f, hlen]
+
+theorem card_nodeFamily_le (r : ContextFreeRule T N) (family : Finset (ParseTree T N)) :
+    (nodeFamily r family).card ≤ family.card ^ r.output.length := by
+  classical
+  exact (Finset.card_image_le).trans_eq (by simp)
+end ParseTree
+
+variable {T : Type*} [Fintype T]
+
+/-- Terminal leaves and active holes; the ambient nonterminal type may be infinite. -/
+@[expose] noncomputable def treeLeaves (g : ContextFreeGrammar T) : Finset (ParseTree T g.NT) := by
+  classical
+  exact Finset.univ.image ParseTree.terminal ∪ (activeNonterminals g).image ParseTree.hole
+
+/-- A finite overcount of active open trees, without child-root compatibility checks. -/
+@[expose] noncomputable def treeFamily (g : ContextFreeGrammar T) : ℕ → Finset (ParseTree T
+  g.NT) := by
+  classical
+  exact Nat.rec (treeLeaves g) fun _ previous =>
+    treeLeaves g ∪ g.rules.biUnion (fun r => ParseTree.nodeFamily r previous)
+
+theorem card_treeLeaves_le (g : ContextFreeGrammar T) :
+    (treeLeaves g).card ≤ Fintype.card T + (activeNonterminals g).card := by
+  classical
+  apply (Finset.card_union_le _ _).trans
+  exact Nat.add_le_add (by simpa using Finset.card_image_le (s := (Finset.univ : Finset T)))
+    Finset.card_image_le
+
+/-- Every bounded active open tree belongs to the counting family. -/
+theorem mem_treeFamily (g : ContextFreeGrammar T) (H : ℕ) (t : ParseTree T g.NT)
+    (ht : ActiveOpen g t) (hh : t.height ≤ H) : t ∈ treeFamily g H := by
+  classical
+  induction H generalizing t with
+  | zero =>
+    cases ht.1 with
+    | terminal a => simp [treeFamily, treeLeaves]
+    | hole A =>
+      have hA := ht.2 A (by simp only [ParseTree.holes.eq_2, List.mem_singleton])
+      simp [treeFamily, treeLeaves, hA]
+    | node r cs hr hv roots => rw [ParseTree.height.eq_3] at hh; omega
+  | succ H ih =>
+    cases ht.1 with
+    | terminal a => simp [treeFamily, treeLeaves]
+    | hole A =>
+      have hA := ht.2 A (by simp only [ParseTree.holes.eq_2, List.mem_singleton])
+      simp [treeFamily, treeLeaves, hA]
+    | node r cs hr hv roots =>
+      apply Finset.mem_union_right
+      apply Finset.mem_biUnion.mpr
+      refine ⟨r, hr, ParseTree.mem_nodeFamily r _ cs ?_ ?_⟩
+      · simpa using congrArg List.length roots
+      · intro c hc
+        have hchild := ParseTree.height_child_lt r cs c hc
+        apply ih c ⟨hv c hc, ?_⟩ (by omega)
+        intro A hA
+        apply ht.2 A
+        simp only [ParseTree.holes.eq_3, ← List.flatMap_def, List.mem_flatMap]
+        exact ⟨c, hc, hA⟩
+
+/-- Count each layer using finite union and function-space cardinalities. -/
+theorem card_treeFamily_le (g : ContextFreeGrammar T) (b q : ℕ)
+    (hq : 1 + Fintype.card T + (activeNonterminals g).card + g.rules.card ≤ q)
+    (hb : ∀ r ∈ g.rules, r.output.length ≤ b) (H : ℕ) :
+    (treeFamily g H).card ≤ q ^ heightPositions b H := by
+  classical
+  have hq1 : 1 ≤ q := by omega
+  induction H with
+  | zero => simpa [treeFamily, heightPositions_zero] using (card_treeLeaves_le g).trans (by omega)
+  | succ H ih =>
+    let A := q ^ heightPositions b H
+    have hA : 1 ≤ A ^ b := one_le_pow₀ (one_le_pow₀ hq1)
+    have hnodes : ∀ r ∈ g.rules,
+        (ParseTree.nodeFamily r (treeFamily g H)).card ≤ A ^ b := by
+      intro r hr
+      exact (ParseTree.card_nodeFamily_le r _).trans
+        ((Nat.pow_le_pow_left ih _).trans (pow_le_pow_right₀ (one_le_pow₀ hq1) (hb r hr)))
+    calc
+      (treeFamily g (H + 1)).card
+          ≤ (treeLeaves g).card + ∑ r ∈ g.rules,
+              (ParseTree.nodeFamily r (treeFamily g H)).card :=
+        (Finset.card_union_le _ _).trans (Nat.add_le_add_left Finset.card_biUnion_le _)
+      _ ≤ (Fintype.card T + (activeNonterminals g).card) + g.rules.card * A ^ b := by
+        exact Nat.add_le_add (card_treeLeaves_le g) (by
+          simpa using Finset.sum_le_sum hnodes)
+      _ ≤ q * A ^ b := by
+        have hl := Nat.mul_le_mul_left (Fintype.card T + (activeNonterminals g).card) hA
+        have hq' : Fintype.card T + (activeNonterminals g).card + g.rules.card ≤ q := by omega
+        calc
+          _ ≤ (Fintype.card T + (activeNonterminals g).card) * A ^ b +
+              g.rules.card * A ^ b := Nat.add_le_add_right (by simpa using hl) _
+          _ = (Fintype.card T + (activeNonterminals g).card + g.rules.card) * A ^ b :=
+            (Nat.add_mul _ _ _).symm
+          _ ≤ q * A ^ b := Nat.mul_le_mul_right _ hq'
+      _ = q ^ heightPositions b (H + 1) := by
+        dsimp [A]
+        rw [heightPositions_succ, pow_add, pow_one, Nat.mul_comm b, ← pow_mul]
+
+omit [Fintype T] in
+/-- Valid trees have at most the full branching-tree budget of terminal leaves. -/
+theorem yield_length_le_heightPositions (g : ContextFreeGrammar T) (b : ℕ)
+    (hb : ∀ r ∈ g.rules, r.output.length ≤ b) (H : ℕ) (t : ParseTree T g.NT)
+    (hv : Valid g t) (hh : t.height ≤ H) : t.yield.length ≤ heightPositions b H := by
+  induction H generalizing t with
+  | zero =>
+    cases hv with
+    | terminal a => simp [ParseTree.yield.eq_1, heightPositions_zero]
+    | hole A => simp only [ParseTree.yield.eq_2, List.length_nil, Nat.zero_le]
+    | node r cs hr hc roots => rw [ParseTree.height.eq_3] at hh; omega
+  | succ H ih =>
+    cases hv with
+    | terminal a => simpa only [ParseTree.yield.eq_1, List.length_singleton] using
+      heightPositions_pos b (H + 1)
+    | hole A => simp only [ParseTree.yield.eq_2, List.length_nil, Nat.zero_le]
+    | node r cs hr hc roots =>
+      have hlen : cs.length ≤ b := by
+        have := congrArg List.length roots
+        simpa using this.le.trans (hb r hr)
+      have hchildren : ∀ n ∈ cs.map (fun c => c.yield.length), n ≤ heightPositions b H := by
+        intro n hn
+        obtain ⟨c, hmem, rfl⟩ := List.mem_map.mp hn
+        have hchild := ParseTree.height_child_lt r cs c hmem
+        exact ih c (hc c hmem) (by omega)
+      calc
+        (ParseTree.node r cs).yield.length = (cs.map (fun c => c.yield.length)).sum := by
+          simp only [ParseTree.yield.eq_3, List.length_flatten, List.map_map, Function.comp_def]
+        _ ≤ cs.length * heightPositions b H := by
+          simpa [List.length_map, nsmul_eq_mul] using List.sum_le_length_nsmul _ _ hchildren
+        _ ≤ b * heightPositions b H := Nat.mul_le_mul_right _ hlen
+        _ ≤ heightPositions b (H + 1) := by rw [heightPositions_succ]; omega
+
+end Parikh
diff --git a/LeanPool/Parikh/CompilerBounds.lean b/LeanPool/Parikh/CompilerBounds.lean
new file mode 100644
index 0000000000..3888d128c1
--- /dev/null
+++ b/LeanPool/Parikh/CompilerBounds.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.CompilerTrees
+import LeanPool.Parikh.BoundedFamilySupport
+import LeanPool.Parikh.InsertionSequences
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Bounds for executable tree families
+
+Specialize the existing counting cover and leaf-norm results to the declared
+encoded alphabet. This covers unused symbols and duplicate input productions
+without changing the accepted grammar-size definitions.
+Source: `lem:count-trees`, `thm:size-bound`.
+-/
+namespace Parikh
+namespace EncodedGrammar
+
+/-- The executable exact families satisfy the declared syntax budgets. -/
+theorem tree_budgets (g : EncodedGrammar) :
+    g.baseTrees.length ≤ g.size.trees ∧ g.cycleTrees.length ≤ g.size.trees ∧
+      ∀ t, IsBase g.decode t ∨ IsBoundedCycle g.decode t → norm t.weight ≤ g.size.positions := by
+  classical
+  let s := g.size
+  have hb : ∀ r ∈ g.decode.rules, r.output.length ≤ s.branching := by
+    intro r hr
+    change r ∈ g.rules.toFinset at hr
+    have hm : r.output.length ∈ g.rules.map (fun r => r.output.length) :=
+      List.mem_map.mpr ⟨r, List.mem_toFinset.mp hr, rfl⟩
+    have hfold : r.output.length ≤ (g.rules.map fun r => r.output.length).foldl max 0 := by
+      rw [List.foldl_max_eq_max (List.ne_nil_of_mem hm), Nat.zero_max]
+      exact List.le_max_of_mem hm
+    exact hfold.trans (Nat.le_max_right _ _)
+  have hq : 1 + Fintype.card (Fin g.terminalCount) +
+      (activeNonterminals g.decode).card + g.decode.rules.card ≤ s.records := by
+    have hn := g.active_card_le
+    change (activeNonterminals g.decode).card ≤ g.extraNonterminalCount + 1 at hn
+    change 1 + Fintype.card (Fin g.terminalCount) + (activeNonterminals g.decode).card +
+      g.rules.toFinset.card ≤ 1 + g.terminalCount + (g.extraNonterminalCount + 1) +
+        g.rules.toFinset.card
+    simp only [Fintype.card_fin]
+    omega
+  have hbounded : ∀ t, IsBase g.decode t ∨ IsBoundedCycle g.decode t →
+      ActiveOpen g.decode t ∧ t.height ≤ s.nonterminals + 1 := by
+    intro t ht
+    rcases ht with hbase | hcycle
+    · refine ⟨⟨hbase.1.1, ?_⟩, ?_⟩
+      · simp [hbase.1.2]
+      · exact ((simple_height g.decode t hbase.1 hbase.2.2).trans g.active_card_le).trans
+          (Nat.le_succ _)
+    · obtain ⟨⟨A, hc⟩, hh⟩ := hcycle
+      refine ⟨⟨hc.1.1, ?_⟩, hh.trans (Nat.add_le_add_right g.active_card_le 1)⟩
+      intro B hB
+      have hBA : B = A := by simpa only [hc.1.2, List.mem_singleton] using hB
+      subst B
+      exact hc.1.1.support_active hc.root_mem_support
+  let family := treeFamily g.decode (s.nonterminals + 1)
+  have hmem : ∀ t, IsBase g.decode t ∨ IsBoundedCycle g.decode t → t ∈ family := by
+    intro t ht
+    obtain ⟨ho, hh⟩ := hbounded t ht
+    exact mem_treeFamily g.decode _ t ho hh
+  have hcard : family.card ≤ s.trees := by
+    simpa only [GrammarSize.trees, GrammarSize.positions, heightPositions, Nat.add_assoc] using
+      card_treeFamily_le g.decode s.branching s.records hq hb (s.nonterminals + 1)
+  refine ⟨?_, ?_, ?_⟩
+  · rw [← List.toFinset_card_of_nodup g.baseTrees_nodup]
+    exact (Finset.card_le_card (show g.baseTrees.toFinset ⊆ family from
+      fun B hB => hmem B (Or.inl ((g.mem_baseTrees B).mp (List.mem_toFinset.mp hB))))).trans hcard
+  · rw [← List.toFinset_card_of_nodup g.cycleTrees_nodup]
+    exact (Finset.card_le_card (show g.cycleTrees.toFinset ⊆ family from
+      fun C hC => hmem C (Or.inr ((g.mem_cycleTrees C).mp (List.mem_toFinset.mp hC))))).trans hcard
+  · intro t ht
+    obtain ⟨ho, hh⟩ := hbounded t ht
+    rw [ParseTree.norm_weight_eq_length]
+    simpa only [GrammarSize.positions, heightPositions, Nat.add_assoc] using
+      yield_length_le_heightPositions g.decode s.branching hb _ t ho.1 hh
+
+end EncodedGrammar
+end Parikh
diff --git a/LeanPool/Parikh/CompilerSupport.lean b/LeanPool/Parikh/CompilerSupport.lean
new file mode 100644
index 0000000000..8040fe62a0
--- /dev/null
+++ b/LeanPool/Parikh/CompilerSupport.lean
@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.ActivationAlgorithm
+import LeanPool.Parikh.BoundedFamilySupport
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Executable adapters for witness compilation
+
+Structural equality compares trees with an explicit height budget. List-based
+components preserve context identities and avoid classical finite-set listing.
+Source: `sec:effective`, `eq:component`, `lem:activation-test`.
+-/
+namespace Parikh
+namespace ParseTree
+variable {T N : Type*} [DecidableEq T] [DecidableEq N]
+
+/-- Compare tree syntax through a fixed production height, without recursive
+runtime helpers or a classical equality decision. -/
+@[expose] def equalAt (H : ℕ) : ParseTree T N → ParseTree T N → Bool :=
+  Nat.rec
+    (fun t u => match t, u with
+      | .terminal a, .terminal b => decide (a = b)
+      | .hole A, .hole B => decide (A = B)
+      | _, _ => false)
+    (fun _ next t u => match t, u with
+      | .terminal a, .terminal b => decide (a = b)
+      | .hole A, .hole B => decide (A = B)
+      | .node r cs, .node s ds => decide (r = s) && cs.isEqv ds next
+      | _, _ => false) H
+
+/-- Sufficient height makes the structural comparison exact. -/
+theorem equalAt_correct (H : ℕ) (t u : ParseTree T N)
+    (ht : t.height ≤ H) (hu : u.height ≤ H) : equalAt H t u = true ↔ t = u := by
+  induction H generalizing t u with
+  | zero =>
+    cases t <;> cases u <;> simp [equalAt]
+    all_goals rw [height.eq_3] at ht; omega
+  | succ H ih =>
+    have hlist : ∀ cs ds : List (ParseTree T N),
+        (∀ c ∈ cs, c.height ≤ H) → (∀ d ∈ ds, d.height ≤ H) →
+        (cs.isEqv ds (equalAt H) = true ↔ cs = ds) := by
+      intro cs ds hc hd
+      induction cs generalizing ds with
+      | nil => cases ds <;> simp [List.isEqv]
+      | cons c cs hcs =>
+        cases ds with
+        | nil => simp [List.isEqv]
+        | cons d ds =>
+          simp only [List.isEqv, Bool.and_eq_true]
+          rw [ih c d (hc c (by simp)) (hd d (by simp)),
+            hcs ds (fun x hx => hc x (by simp [hx]))
+              (fun x hx => hd x (by simp [hx]))]
+          simp only [List.cons.injEq]
+    cases t with
+    | terminal a => cases u <;> simp [equalAt]
+    | hole A => cases u <;> simp [equalAt]
+    | node r cs =>
+      cases u with
+      | terminal a => simp [equalAt]
+      | hole A => simp [equalAt]
+      | node s ds =>
+        have hc : ∀ c ∈ cs, c.height ≤ H := fun c hc => by
+          have := height_child_lt r cs c hc
+          omega
+        have hd : ∀ d ∈ ds, d.height ≤ H := fun d hd => by
+          have := height_child_lt s ds d hd
+          omega
+        change (decide (r = s) && cs.isEqv ds (equalAt H)) = true ↔ _
+        simp only [Bool.and_eq_true, decide_eq_true_eq, hlist cs ds hc hd, node.injEq]
+
+/-- A computable equality decision for the existing nested parse-tree syntax.
+It is supplied explicitly by the compiler, without a new global instance. -/
+@[expose] def decEq : DecidableEq (ParseTree T N) := fun t u =>
+  decidable_of_iff (equalAt (t.height + u.height) t u = true)
+    (equalAt_correct _ t u (by omega) (by omega))
+end ParseTree
+
+/-- Assemble in list order: each context pays once in the base and retains its
+own period position, even when weights coincide or vanish. -/
+@[expose] def listComponent {T N : Type*} [DecidableEq T]
+    (B : ParseTree T N) (D : List (ParseTree T N)) : Component T :=
+  ⟨B.weight + (D.map ParseTree.weight).sum, D.map ParseTree.weight⟩
+
+/-- Listing a context set in any duplicate-free order preserves its exact
+linear-set denotation. No equality or deduplication of weights is required. -/
+theorem listComponent_denotation {T N : Type*} [DecidableEq T]
+    [DecidableEq (ParseTree T N)]
+    (B : ParseTree T N) (D : List (ParseTree T N)) (hD : D.Nodup) :
+    (listComponent B D).denotation = (contextComponent B D.toFinset).denotation := by
+  classical
+  have hbase : (listComponent B D).base = (contextComponent B D.toFinset).base := by
+    change B.weight + (D.map ParseTree.weight).sum = B.weight + ∑ C ∈ D.toFinset, C.weight
+    rw [List.sum_toFinset ParseTree.weight hD]
+  have hrange : Set.range (listComponent B D).periods.get =
+      Set.range (contextComponent B D.toFinset).periods.get := by
+    ext w
+    simp [listComponent, contextComponent]
+  rw [Component.denotation_eq_vadd_closure, Component.denotation_eq_vadd_closure,
+    hbase, hrange]
+
+namespace ParseTree
+/-- Extract a nonterminal root; the default is irrelevant for certified cycles. -/
+@[expose] def rootLabel {T N : Type*} (default : N) (t : ParseTree T N) : N :=
+  match t.root with
+  | .terminal _ => default
+  | .nonterminal A => A
+end ParseTree
+
+/-- Run the existing activation algorithm on actual context identities and
+finite production-label supports. -/
+@[expose] def contextActivation {T : Type*} (g : ContextFreeGrammar T)
+    [DecidableEq g.NT] [DecidableEq (ParseTree T g.NT)]
+    (B : ParseTree T g.NT) (D : List (ParseTree T g.NT)) : Bool :=
+  (activationTest g.NT (ParseTree T g.NT)).run (ParseTree.rootLabel g.initial)
+    (fun C => C.productionLabels.toFinset) B.productionLabels.toFinset D.toFinset
+
+/-- For a family of cycles, the executable support test is exactly the accepted
+grammar activation predicate. -/
+theorem contextActivation_correct {T : Type*} (g : ContextFreeGrammar T)
+    [DecidableEq g.NT] [DecidableEq (ParseTree T g.NT)]
+    (B : ParseTree T g.NT) (D : List (ParseTree T g.NT))
+    (hD : ∀ C ∈ D, ∃ A, Cycle g C A) :
+    contextActivation g B D = true ↔ ContextsActivatable g B D.toFinset := by
+  have hroot (C : ParseTree T g.NT) (A : g.NT) (h : Cycle g C A) :
+      ParseTree.rootLabel g.initial C = A := by
+    unfold ParseTree.rootLabel
+    rw [h.2.1]
+  have hcycles : ∀ C ∈ D.toFinset, Cycle g C (ParseTree.rootLabel g.initial C) := by
+    intro C hC
+    obtain ⟨A, ha⟩ := hD C (List.mem_toFinset.mp hC)
+    simpa only [hroot C A ha] using ha
+  have hsupport (C : ParseTree T g.NT) :
+      (C.productionLabels.toFinset : Set g.NT) = C.support := by
+    ext A
+    simp [ParseTree.support]
+  rw [contextActivation, (activationTest g.NT (ParseTree T g.NT)).correct]
+  simp only [hsupport]
+  constructor
+  · rintro ⟨order, hn, hm, ho⟩
+    exact ⟨order, hn, hm, ParseTree.rootLabel g.initial, hcycles, ho⟩
+  · rintro ⟨order, hn, hm, roots, hc, ho⟩
+    refine ⟨order, hn, hm, ?_⟩
+    have heq : ∀ C ∈ order, ParseTree.rootLabel g.initial C = roots C :=
+      fun C hC => hroot C (roots C) (hc C ((hm C).mp hC))
+    have hcongr : ∀ (U : Set g.NT) (cs : List (ParseTree T g.NT)),
+        (∀ c ∈ cs, ParseTree.rootLabel g.initial c = roots c) →
+        (ActivationOrder roots ParseTree.support U cs ↔
+          ActivationOrder (ParseTree.rootLabel g.initial) ParseTree.support U cs) := by
+      intro U cs he
+      induction cs generalizing U with
+      | nil => rfl
+      | cons c cs ih =>
+        simp only [ActivationOrder, he c (by simp)]
+        rw [ih (U ∪ c.support) (fun d hd => he d (by simp [hd]))]
+    exact (hcongr _ order heq).mp ho
+end Parikh
diff --git a/LeanPool/Parikh/CompilerTrees.lean b/LeanPool/Parikh/CompilerTrees.lean
new file mode 100644
index 0000000000..1d0790039b
--- /dev/null
+++ b/LeanPool/Parikh/CompilerTrees.lean
@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.CompilerSupport
+public import LeanPool.Parikh.BoundedEnumeration
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Executable base and cycle families
+
+Enumerate declared finite syntax, filter the accepted predicates, and remove
+only duplicate trees. Unused symbols are allowed. Cycle heights use the exact
+active alphabet, matching the general grammar formula.
+Source: `lem:finite`, `sec:effective`.
+-/
+namespace Parikh
+namespace EncodedGrammar
+
+/-- The existing active alphabet computed from the finite input syntax. -/
+@[expose] def activeLabels (g : EncodedGrammar) : Finset (Fin (g.extraNonterminalCount + 1)) :=
+  {g.initial} ∪ g.rules.toFinset.biUnion (fun r =>
+    {r.input} ∪ (r.output.filterMap fun s => match s with
+      | .terminal _ => none
+      | .nonterminal A => some A).toFinset)
+
+theorem activeLabels_eq (g : EncodedGrammar) :
+    g.activeLabels = activeNonterminals g.decode := by
+  classical
+  unfold activeLabels activeNonterminals
+  have heq : (fun a b : g.decode.NT => Classical.propDecidable (a = b)) =
+      instDecidableEqFin (g.extraNonterminalCount + 1) := Subsingleton.elim _ _
+  rw [heq]
+  congr 3
+  funext r
+  congr 3
+  funext s
+  cases s <;> rfl
+
+/-- The active alphabet is bounded by the declared finite nonterminal count. -/
+theorem active_card_le (g : EncodedGrammar) :
+    (activeNonterminals g.decode).card ≤ g.size.nonterminals := by
+  classical
+  calc
+    (activeNonterminals g.decode).card = g.activeLabels.card :=
+      congrArg Finset.card g.activeLabels_eq.symm
+    _ ≤ Fintype.card (Fin (g.extraNonterminalCount + 1)) := Finset.card_le_univ _
+    _ = g.size.nonterminals := by simp [size]
+
+/-- Enumeration already guarantees validity; test completeness, start root and
+pathwise simplicity using finite lists. -/
+@[expose] def baseTest (g : EncodedGrammar)
+    (B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) : Bool :=
+  decide (B.holes = [] ∧ B.root = .nonterminal g.initial) &&
+    B.labelPaths.all (fun p => decide p.Nodup)
+
+theorem baseTest_correct (g : EncodedGrammar)
+    (B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))
+    (hv : Valid g.decode B) : g.baseTest B = true ↔ IsBase g.decode B := by
+  unfold baseTest
+  simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true]
+  constructor
+  · rintro ⟨⟨hh, hr⟩, hs⟩
+    exact ⟨⟨hv, hh⟩, hr, hs⟩
+  · rintro ⟨⟨_, hh⟩, hr, hs⟩
+    exact ⟨⟨hh, hr⟩, hs⟩
+
+/-- Test a nontrivial same-root/hole context and the exact active-height bound. -/
+@[expose] def cycleTest (g : EncodedGrammar)
+    (C : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) : Bool :=
+  decide (∃ A, C.holes = [A] ∧ C.root = .nonterminal A ∧ 0 < C.productionSize) &&
+    decide (C.height ≤ g.activeLabels.card + 1)
+
+theorem cycleTest_correct (g : EncodedGrammar)
+    (C : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))
+    (hv : Valid g.decode C) : g.cycleTest C = true ↔ IsBoundedCycle g.decode C := by
+  unfold cycleTest
+  rw [activeLabels_eq]
+  simp only [Bool.and_eq_true, decide_eq_true_eq]
+  constructor
+  · rintro ⟨⟨A, hh, hr, hp⟩, hheight⟩
+    exact ⟨⟨A, ⟨hv, hh⟩, hr, hp⟩, hheight⟩
+  · rintro ⟨⟨A, ⟨_, hh⟩, hr, hp⟩, hheight⟩
+    exact ⟨⟨A, hh, hr, hp⟩, hheight⟩
+
+/-- Duplicate-free base trees, searched only through the active-label height bound. -/
+@[expose] def baseTrees (g : EncodedGrammar) :
+    List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :=
+  letI := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  ((boundedEnumeration.enumerate g (g.activeLabels.card + 1)).filter g.baseTest).dedup
+
+/-- Enumerate bounded cycle contexts at the active-label height, retaining their identities. -/
+@[expose] def cycleTrees (g : EncodedGrammar) :
+    List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :=
+  letI := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  ((boundedEnumeration.enumerate g (g.activeLabels.card + 1)).filter g.cycleTest).dedup
+
+theorem baseTrees_nodup (g : EncodedGrammar) : g.baseTrees.Nodup := by
+  let _ := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  unfold baseTrees
+  exact List.nodup_dedup _
+
+theorem cycleTrees_nodup (g : EncodedGrammar) : g.cycleTrees.Nodup := by
+  let _ := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  unfold cycleTrees
+  exact List.nodup_dedup _
+
+/-- Every simple complete start tree is enumerated, including epsilon trees. -/
+theorem mem_baseTrees (g : EncodedGrammar)
+    (B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :
+    B ∈ g.baseTrees ↔ IsBase g.decode B := by
+  let _ := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  change B ∈ ((boundedEnumeration.enumerate g (g.activeLabels.card + 1)).filter
+    g.baseTest).dedup ↔ _
+  rw [List.mem_dedup, List.mem_filter]
+  constructor
+  · rintro ⟨hm, ht⟩
+    exact (g.baseTest_correct B ((boundedEnumeration.correct g _ B).mp hm).1).mp ht
+  · intro hb
+    have hh : B.height ≤ g.activeLabels.card := by
+      rw [g.activeLabels_eq]
+      exact simple_height g.decode B hb.1 hb.2.2
+    exact ⟨(boundedEnumeration.correct g _ B).mpr ⟨hb.1.1, hh.trans (Nat.le_succ _)⟩,
+      (g.baseTest_correct B hb.1.1).mpr hb⟩
+
+/-- Cycle enumeration uses precisely the frozen active-height predicate. -/
+theorem mem_cycleTrees (g : EncodedGrammar)
+    (C : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))) :
+    C ∈ g.cycleTrees ↔ IsBoundedCycle g.decode C := by
+  let _ := ParseTree.decEq (T := Fin g.terminalCount) (N := Fin (g.extraNonterminalCount + 1))
+  change C ∈ ((boundedEnumeration.enumerate g (g.activeLabels.card + 1)).filter
+    g.cycleTest).dedup ↔ _
+  rw [List.mem_dedup, List.mem_filter]
+  constructor
+  · rintro ⟨hm, ht⟩
+    exact (g.cycleTest_correct C ((boundedEnumeration.correct g _ C).mp hm).1).mp ht
+  · intro hc
+    obtain ⟨A, ha⟩ := hc.1
+    have hh : C.height ≤ g.activeLabels.card + 1 := by
+      rw [g.activeLabels_eq]
+      exact hc.2
+    exact ⟨(boundedEnumeration.correct g _ C).mpr ⟨ha.1.1, hh⟩,
+      (g.cycleTest_correct C ha.1.1).mpr hc⟩
+
+end EncodedGrammar
+end Parikh
diff --git a/LeanPool/Parikh/Construction.lean b/LeanPool/Parikh/Construction.lean
new file mode 100644
index 0000000000..d6c03cd1f2
--- /dev/null
+++ b/LeanPool/Parikh/Construction.lean
@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+public import Mathlib.Data.Nat.Log
+import LeanPool.Parikh.BoundedFamilySupport
+import LeanPool.Parikh.FiniteWitness
+import LeanPool.Parikh.InsertionSequences
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Finite grammar encoding and size bounds
+
+This file defines the finite input encoding, bounded-tree enumeration and
+compiler interfaces, and proves the representation's size and bit bounds.
+
+`EncodedGrammar` supplies finite syntax. `BoundedEnumeration` and `Compiler`
+package algorithms with their required correctness proofs. The former is
+implemented by `boundedEnumeration` in `Parikh/BoundedEnumeration.lean`; the
+latter by `compiler` in `Parikh/ExecutableCompiler.lean`.
+
+Source: `sec:effective`, `eq:bound-defs`, `thm:size-bound`, `eq:bit-bound`.
+-/
+namespace Parikh
+
+/-- The paper's grammar parameters; `branching ≥ 1` is supplied by the size definitions. -/
+structure GrammarSize where
+  /-- Number of available nonterminal labels. -/
+  nonterminals : ℕ
+  /-- Number of terminal letters. -/
+  terminals : ℕ
+  /-- Number of distinct production rules. -/
+  productions : ℕ
+  /-- Upper bound on the length of a production output. -/
+  branching : ℕ
+  deriving Repr
+
+/-- `M`, `q`, `K` in `eq:bound-defs`; production height at most `n+1`. -/
+@[expose] def GrammarSize.positions (s : GrammarSize) : ℕ :=
+  ∑ i ∈ Finset.range (s.nonterminals + 2), s.branching ^ i
+
+/-- Number of possible labels in the bounded syntax overcount. -/
+@[expose] def GrammarSize.records (s : GrammarSize) : ℕ :=
+  1 + s.terminals + s.nonterminals + s.productions
+
+/-- Upper bound on the number of bounded syntax trees. -/
+@[expose] def GrammarSize.trees (s : GrammarSize) : ℕ := s.records ^ s.positions
+
+/-- Size parameters using only the active nonterminal alphabet. -/
+@[expose] noncomputable def grammarSize {T : Type*} [Fintype T] (g : ContextFreeGrammar T) :
+  GrammarSize :=
+  ⟨(activeNonterminals g).card, Fintype.card T, g.rules.card,
+    max 1 (g.rules.sup fun r => r.output.length)⟩
+
+/-- Total number of letters represented by a count vector. -/
+@[expose] def norm {T : Type*} [Fintype T] (v : Vector T) : ℕ := ∑ a, v a
+
+/-- All four representation bounds, including duplicate/zero indexed periods (`thm:size-bound`). -/
+@[expose] def WithinBounds {T : Type*} [Fintype T] (s : GrammarSize) (W : Witness T) : Prop :=
+  W.length ≤ s.trees * 2 ^ s.trees ∧
+    ∀ c ∈ W, c.periods.length ≤ s.trees ∧
+      norm c.base ≤ (s.trees + 1) * s.positions ∧
+      ∀ p ∈ c.periods, norm p ≤ s.positions
+
+/-- Fixed coordinate width and vector-entry budget, excluding length metadata (`eq:bit-bound`). -/
+@[expose] def GrammarSize.coordinateBits (s : GrammarSize) : ℕ :=
+  max 1 (Nat.clog 2 ((s.trees + 1) * s.positions + 1))
+
+/-- Bit budget for all base and period coordinates, excluding length metadata. -/
+@[expose] def GrammarSize.vectorBits (s : GrammarSize) : ℕ :=
+  s.trees * 2 ^ s.trees * (s.trees + 1) * s.terminals * s.coordinateBits
+
+/-- Fixed-width bit count of the representation's numerical entries. -/
+@[expose] def entryBits {T : Type*} [Fintype T] (s : GrammarSize) (W : Witness T) : ℕ :=
+  (W.map fun c => (c.periods.length + 1) * Fintype.card T * s.coordinateBits).sum
+
+/-- Summing the terminal counts gives the length of a tree's terminal yield. -/
+theorem ParseTree.norm_weight_eq_length {T N : Type*} [Fintype T] [DecidableEq T]
+    (t : ParseTree T N) : norm t.weight = t.yield.length := by
+  classical
+  change (∑ a, t.yield.count a) = t.yield.length
+  rw [← List.sum_toFinset_count_eq_length t.yield]
+  symm
+  apply Finset.sum_subset (Finset.subset_univ _)
+  intro a _ ha
+  exact List.count_eq_zero.mpr (fun h => ha (List.mem_toFinset.mpr h))
+
+/-- Bounded families and leaf norms have the paper's coarse syntax bounds (`lem:count-trees`). -/
+theorem bounded_family_bounds {T : Type*} [Fintype T] [DecidableEq T]
+    (g : ContextFreeGrammar T) :
+    (∃ bases : Finset (ParseTree T g.NT),
+      (∀ B, B ∈ bases ↔ IsBase g B) ∧ bases.card ≤ (grammarSize g).trees) ∧
+    (∃ cycles : Finset (ParseTree T g.NT),
+      (∀ C, C ∈ cycles ↔ IsBoundedCycle g C) ∧ cycles.card ≤ (grammarSize g).trees) ∧
+    (∀ t, IsBase g t ∨ IsBoundedCycle g t → norm t.weight ≤ (grammarSize g).positions) := by
+  classical
+  let s := grammarSize g
+  have hb : ∀ r ∈ g.rules, r.output.length ≤ s.branching := by
+    intro r hr
+    exact (Finset.le_sup (f := fun r => r.output.length) hr).trans (Nat.le_max_right _ _)
+  have hbounded : ∀ t, IsBase g t ∨ IsBoundedCycle g t →
+      ActiveOpen g t ∧ t.height ≤ s.nonterminals + 1 := by
+    intro t ht
+    rcases ht with hbase | hcycle
+    · refine ⟨⟨hbase.1.1, ?_⟩, ?_⟩
+      · simp [hbase.1.2]
+      · exact (simple_height g t hbase.1 hbase.2.2).trans (Nat.le_succ _)
+    · obtain ⟨⟨A, hcycle⟩, hh⟩ := hcycle
+      refine ⟨⟨hcycle.1.1, ?_⟩, hh⟩
+      intro B hB
+      have hBA : B = A := by simpa only [hcycle.1.2, List.mem_singleton] using hB
+      subst B
+      exact hcycle.1.1.support_active hcycle.root_mem_support
+  let family := treeFamily g (s.nonterminals + 1)
+  have hmem : ∀ t, IsBase g t ∨ IsBoundedCycle g t → t ∈ family := by
+    intro t ht
+    obtain ⟨ho, hh⟩ := hbounded t ht
+    exact mem_treeFamily g _ t ho hh
+  have hcard : family.card ≤ s.trees := by
+    exact card_treeFamily_le g s.branching s.records (by rfl) hb _
+  refine ⟨⟨family.filter (IsBase g), ?_, ?_⟩,
+    ⟨family.filter (IsBoundedCycle g), ?_, ?_⟩, ?_⟩
+  · intro B
+    exact ⟨fun h => (Finset.mem_filter.mp h).2,
+      fun h => Finset.mem_filter.mpr ⟨hmem B (Or.inl h), h⟩⟩
+  · exact (Finset.card_filter_le _ _).trans hcard
+  · intro C
+    exact ⟨fun h => (Finset.mem_filter.mp h).2,
+      fun h => Finset.mem_filter.mpr ⟨hmem C (Or.inr h), h⟩⟩
+  · exact (Finset.card_filter_le _ _).trans hcard
+  · intro t ht
+    obtain ⟨ho, hh⟩ := hbounded t ht
+    rw [ParseTree.norm_weight_eq_length]
+    exact yield_length_le_heightPositions g s.branching hb _ t ho.1 hh
+
+/-- A component has one period per context and pays all first copies in its base. -/
+theorem contextComponent_size_bounds {T N : Type*} [Fintype T] [DecidableEq T]
+    (B : ParseTree T N) (D : Finset (ParseTree T N)) (M : ℕ)
+    (hB : norm B.weight ≤ M) (hD : ∀ C ∈ D, norm C.weight ≤ M) :
+    (contextComponent B D).periods.length = D.card ∧
+      norm (contextComponent B D).base ≤ (D.card + 1) * M ∧
+      ∀ p ∈ (contextComponent B D).periods, norm p ≤ M := by
+  classical
+  refine ⟨by simp [contextComponent], ?_, ?_⟩
+  · have hsum : norm (contextComponent B D).base =
+        norm B.weight + ∑ C ∈ D, norm C.weight := by
+      change (∑ a, (B.weight + ∑ C ∈ D, C.weight) a) = _
+      simp only [Pi.add_apply, Finset.sum_apply, Finset.sum_add_distrib, norm]
+      rw [Finset.sum_comm]
+    rw [hsum]
+    calc
+      norm B.weight + ∑ C ∈ D, norm C.weight ≤ M + D.card * M :=
+        Nat.add_le_add hB (by simpa using Finset.sum_le_sum hD)
+      _ = (D.card + 1) * M := by rw [Nat.add_mul, Nat.one_mul, Nat.add_comm]
+  · intro p hp
+    obtain ⟨C, hC, rfl⟩ := List.mem_map.mp hp
+    exact hD C (Finset.mem_toList.mp hC)
+
+/-- The guaranteed exact witness also satisfies all four bounds (`thm:size-bound`). -/
+theorem bounded_witness {T : Type*} [Fintype T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    ∃ W : Witness T, W.denotation = image g.language ∧ WithinBounds (grammarSize g) W := by
+  classical
+  obtain ⟨⟨bases, hb, hbcard⟩, ⟨cycles, hc, hccard⟩, hnorm⟩ := bounded_family_bounds g
+  refine ⟨familyWitness g bases cycles, familyWitness_denotation g bases cycles hb hc, ?_⟩
+  refine ⟨(familyWitness_length_le g bases cycles).trans ?_, ?_⟩
+  · exact Nat.mul_le_mul hbcard (Nat.pow_le_pow_right (by omega) hccard)
+  · intro c hmem
+    obtain ⟨B, hB, D, hD, _, rfl⟩ := (mem_familyWitness g bases cycles c).mp hmem
+    have hDcard : D.card ≤ (grammarSize g).trees := (Finset.card_le_card hD).trans hccard
+    obtain ⟨hlen, hbase, hperiod⟩ := contextComponent_size_bounds B D (grammarSize g).positions
+      (hnorm B (Or.inl ((hb B).mp hB)))
+      (fun C hC => hnorm C (Or.inr ((hc C).mp (hD hC))))
+    exact ⟨hlen.le.trans hDcard,
+      hbase.trans (Nat.mul_le_mul_right _ (Nat.add_le_add_right hDcard 1)), hperiod⟩
+
+/-- Numerical entries fit the stated fixed-width bit budget (`eq:bit-bound`). -/
+theorem witness_bit_bound {T : Type*} [Fintype T] (s : GrammarSize)
+    (hd : s.terminals = Fintype.card T) (W : Witness T) (h : WithinBounds s W) :
+    entryBits s W ≤ s.vectorBits ∧
+      (∀ c ∈ W, ∀ a, c.base a < 2 ^ s.coordinateBits) ∧
+      (∀ c ∈ W, ∀ p ∈ c.periods, ∀ a, p a < 2 ^ s.coordinateBits) := by
+  classical
+  have hwidth : (s.trees + 1) * s.positions < 2 ^ s.coordinateBits := by
+    apply lt_of_lt_of_le (Nat.lt_succ_self _)
+    exact (Nat.le_pow_clog (by omega) _).trans
+      (Nat.pow_le_pow_right (by omega) (Nat.le_max_right _ _))
+  have hcoordinate (v : Vector T) (a : T) : v a ≤ norm v :=
+    Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ a)
+  have hpositions : s.positions ≤ (s.trees + 1) * s.positions := by
+    simpa using Nat.mul_le_mul_right s.positions (Nat.le_add_left 1 s.trees)
+  refine ⟨?_, ?_, ?_⟩
+  · have hentries : entryBits s W ≤
+        W.length * ((s.trees + 1) * s.terminals * s.coordinateBits) := by
+      unfold entryBits
+      have hsum := List.sum_le_length_nsmul
+        (W.map fun c => (c.periods.length + 1) * Fintype.card T * s.coordinateBits)
+        ((s.trees + 1) * s.terminals * s.coordinateBits) (by
+          intro n hn
+          obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hn
+          rw [← hd]
+          exact Nat.mul_le_mul_right _
+            (Nat.mul_le_mul_right _ (Nat.add_le_add_right (h.2 c hc).1 1)))
+      simpa only [List.length_map, Nat.nsmul_eq_mul] using hsum
+    exact hentries.trans (by
+      simpa only [GrammarSize.vectorBits, Nat.mul_assoc] using
+        Nat.mul_le_mul_right ((s.trees + 1) * s.terminals * s.coordinateBits) h.1)
+  · intro c hc a
+    exact lt_of_le_of_lt ((hcoordinate c.base a).trans (h.2 c hc).2.1) hwidth
+  · intro c hc p hp a
+    exact lt_of_le_of_lt
+      ((hcoordinate p a).trans (((h.2 c hc).2.2 p hp).trans hpositions)) hwidth
+
+/-- Finite numeric syntax for the executable compiler; unused symbols are allowed. -/
+structure EncodedGrammar where
+  /-- Size of the declared terminal alphabet. -/
+  terminalCount : ℕ
+  /-- Number of nonterminal labels beyond the always-present initial label. -/
+  extraNonterminalCount : ℕ
+  /-- Starting nonterminal of the grammar. -/
+  initial : Fin (extraNonterminalCount + 1)
+  /-- Finite list of productions; duplicate rules are allowed. -/
+  rules : List (ContextFreeRule (Fin terminalCount) (Fin (extraNonterminalCount + 1)))
+
+/-- Interpret numeric grammar syntax as a Mathlib context-free grammar. -/
+@[expose] def EncodedGrammar.decode (g : EncodedGrammar) : ContextFreeGrammar (Fin
+  g.terminalCount) :=
+  ⟨Fin (g.extraNonterminalCount + 1), g.initial, g.rules.toFinset⟩
+
+/-- Numeric bounds count the declared finite alphabet; duplicate productions are collapsed. -/
+@[expose] def EncodedGrammar.size (g : EncodedGrammar) : GrammarSize :=
+  ⟨g.extraNonterminalCount + 1, g.terminalCount, g.rules.toFinset.card,
+    max 1 ((g.rules.map fun r => r.output.length).foldl max 0)⟩
+
+/-- Complete enumeration contract for finite encoded grammars (`lem:finite`).
+Implemented by `boundedEnumeration`, which enumerates syntax by height.
+-/
+structure BoundedEnumeration where
+  /-- List every valid open tree within the requested height bound. -/
+  enumerate : (g : EncodedGrammar) → ℕ →
+    List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))
+  correct : ∀ g H t, t ∈ enumerate g H ↔ Valid g.decode t ∧ t.height ≤ H
+
+/-- Algorithm output contract: exact image, explicit finite data, and the four bounds.
+Implemented by `compiler` using bounded enumeration and the activation test.
+The implementing value supplies effectivity as well as both required proofs.
+-/
+structure Compiler where
+  /-- Compute a finite semilinear representation from numeric grammar syntax. -/
+  compile : (g : EncodedGrammar) → Witness (Fin g.terminalCount)
+  correct : ∀ g, (compile g).denotation = image g.decode.language
+  bounded : ∀ g, WithinBounds g.size (compile g)
+
+end Parikh
diff --git a/LeanPool/Parikh/Counting.lean b/LeanPool/Parikh/Counting.lean
new file mode 100644
index 0000000000..2bd4bbfcf4
--- /dev/null
+++ b/LeanPool/Parikh/Counting.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import Mathlib.Computability.Language
+public import Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
+import Mathlib.Algebra.Group.Submonoid.Finsupp
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# From words to semilinear sets
+
+The Parikh map forgets letter order and remembers how often each letter occurs.
+Its central law is `counts_append`: concatenating words adds their vectors.
+
+A `Component` describes one linear set by a base and a finite list of periods;
+a `Witness` describes a finite union of such sets. The denotations give these
+finite descriptions their mathematical meaning. The final lemmas connect them
+to Mathlib's `IsLinearSet` and `IsSemilinearSet` in both directions, so later
+proofs can use explicit witnesses without replacing Mathlib's notions.
+
+Source: `sec:statement`, `eq:word-add`.
+-/
+open scoped Pointwise
+
+namespace Parikh
+
+/-- A natural-number coordinate for each terminal letter. -/
+abbrev Vector (T : Type*) := T → ℕ
+
+/-- Count occurrences with Mathlib's `List.count`; no order on the alphabet is needed. -/
+@[expose] def counts {T : Type*} [DecidableEq T] (w : List T) : Vector T := fun a => w.count a
+
+/-- The exact image of a Mathlib language under terminal counting. -/
+@[expose] def image {T : Type*} [DecidableEq T] (L : Language T) : Set (Vector T) := counts '' L
+
+/-- A finite description of one linear set (`sec:statement`).
+Start at `base` and add any natural number of copies of each period.
+A Lean `List` always has finite length; no separate finiteness proof is needed.
+Duplicate and zero periods are allowed, and an empty period list describes
+just the base vector. -/
+structure Component (T : Type*) where
+  /-- Initial count vector of the linear component. -/
+  base : Vector T
+  /-- Independently repeatable period vectors, retaining duplicates and zero vectors. -/
+  periods : List (Vector T)
+
+/-- A finite representation, independent of grammars and trace theory. -/
+abbrev Witness (T : Type*) := List (Component T)
+
+/-- The vectors represented by a component.
+A coefficient function assigns a natural number to each position in the period
+list. Each coefficient is chosen independently and may be zero. Thus membership
+means exactly that the vector is the base plus a finite nonnegative combination
+of the listed periods. -/
+@[expose] def Component.denotation {T : Type*} (c : Component T) : Set (Vector T) :=
+  {v | ∃ k : Fin c.periods.length → ℕ,
+    v = c.base + ∑ i : Fin c.periods.length, k i • c.periods[i]}
+
+/-- Empty list denotes the empty set; this is an exact union, not an approximation. -/
+@[expose] def Witness.denotation {T : Type*} (W : Witness T) : Set (Vector T) :=
+  {v | ∃ c ∈ W, v ∈ c.denotation}
+
+/-- Concatenation adds count vectors (`eq:word-add`). -/
+theorem counts_append {T : Type*} [DecidableEq T] (u v : List T) :
+    counts (u ++ v) = counts u + counts v := by
+  funext a
+  exact List.count_append
+
+/-- Indexed period sums are exactly the additive closure of the period values.
+This reuses Mathlib's finite-range closure theorem, including repeated and zero periods. -/
+theorem Component.denotation_eq_vadd_closure {T : Type*} (c : Component T) :
+    c.denotation = c.base +ᵥ
+      (AddSubmonoid.closure (Set.range c.periods.get) : Set (Vector T)) := by
+  ext x
+  simp only [Component.denotation, Set.mem_ofPred_eq, Set.mem_vadd_set,
+    SetLike.mem_coe, vadd_eq_add, AddSubmonoid.mem_closure_range_iff_of_fintype]
+  constructor
+  · rintro ⟨k, rfl⟩
+    exact ⟨_, ⟨k, rfl⟩, rfl⟩
+  · rintro ⟨_, ⟨k, rfl⟩, rfl⟩
+    exact ⟨k, rfl⟩
+
+/-- Bridge indexed coefficient sums to Mathlib's finitely generated additive closure. -/
+theorem component_isLinearSet {T : Type*} (c : Component T) :
+    IsLinearSet c.denotation := by
+  exact ⟨c.base, Set.range c.periods.get, Set.finite_range _,
+    c.denotation_eq_vadd_closure⟩
+
+/-- Every explicit witness denotes a Mathlib semilinear set (`sec:statement`). -/
+theorem witness_isSemilinearSet {T : Type*} (W : Witness T) :
+    IsSemilinearSet W.denotation := by
+  classical
+  have h : W.denotation = ⋃ c ∈ W.toFinset, c.denotation := by
+    ext v
+    simp [Witness.denotation]
+  rw [h]
+  exact IsSemilinearSet.biUnion_finset fun c _ =>
+    (component_isLinearSet c).isSemilinearSet
+
+/-- Mathlib's abstract semilinearity has an exact finite witness as well. -/
+theorem exists_witness {T : Type*} (X : Set (Vector T)) (hX : IsSemilinearSet X) :
+    ∃ W : Witness T, W.denotation = X := by
+  classical
+  have linear_witness : ∀ X : Set (Vector T), IsLinearSet X →
+      ∃ c : Component T, c.denotation = X := by
+    rintro X ⟨b, periods, hperiods, rfl⟩
+    refine ⟨⟨b, hperiods.toFinset.toList⟩, ?_⟩
+    rw [Component.denotation_eq_vadd_closure]
+    have hrange : Set.range hperiods.toFinset.toList.get = periods := by
+      ext p
+      simp only [Set.mem_range, ← List.mem_iff_get, Finset.mem_toList,
+        Set.Finite.mem_toFinset]
+    simp only [hrange]
+  rcases hX with ⟨S, hS, hlinear, rfl⟩
+  induction S, hS using Set.Finite.induction_on with
+  | empty =>
+    exact ⟨[], by ext v; simp [Witness.denotation]⟩
+  | @insert X S hnot hS ih =>
+    obtain ⟨c, hc⟩ := linear_witness X (hlinear X (by simp))
+    obtain ⟨W, hW⟩ := ih (fun Y hY => hlinear Y (by simp [hY]))
+    refine ⟨c :: W, ?_⟩
+    have hcons : Witness.denotation (c :: W) = c.denotation ∪ W.denotation := by
+      ext v
+      simp [Witness.denotation]
+    rw [hcons, hc, hW, Set.sUnion_insert]
+
+end Parikh
diff --git a/LeanPool/Parikh/DFAGrammar.lean b/LeanPool/Parikh/DFAGrammar.lean
new file mode 100644
index 0000000000..0593f2ed8b
--- /dev/null
+++ b/LeanPool/Parikh/DFAGrammar.lean
@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import Mathlib.Computability.ContextFreeGrammar
+public import Mathlib.Computability.DFA
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Reading a finite automaton as a grammar
+
+A DFA state describes what remains to be read. Use states as nonterminals:
+a transition from `q` to `q'` on `a` becomes the production `q → a q'`, and an
+accepting state may produce the empty word. Each derivation follows a run of
+the automaton and stops only at an accepting state.
+
+`dfaGrammar_derives_iff` proves this correspondence from any starting state;
+`dfaGrammar_language` gives equality of the complete word languages. Applying
+the forward Parikh theorem to this grammar establishes semilinearity for a
+regular language. This adapter uses Mathlib's existing DFA and grammar types;
+its finite production set is defined classically.
+-/
+namespace Parikh
+variable {T : Type*} {σ : Type} [Fintype T] [Fintype σ]
+
+/-- States are nonterminals. Transitions emit one letter and the next state;
+accepting states may emit the empty word. Classical finiteness suffices here;
+this adapter is not an executable compiler. -/
+noncomputable abbrev dfaGrammar (M : DFA T σ) : ContextFreeGrammar T := by
+  classical
+  exact {
+    NT := σ
+    initial := M.start
+    rules := (Finset.univ : Finset (σ × T)).image (fun (q, a) =>
+      ⟨q, [.terminal a, .nonterminal (M.step q a)]⟩) ∪
+      ((Finset.univ : Finset σ).filter (fun q => q ∈ M.accept)).image (fun q => ⟨q, []⟩)
+  }
+
+/-- From any DFA state, grammar derivation of a terminal word is exactly
+acceptance by the DFA started at that state. -/
+theorem dfaGrammar_derives_iff (M : DFA T σ) (q : σ) (w : List T) :
+    (dfaGrammar M).Derives [.nonterminal q] (w.map .terminal) ↔
+      M.evalFrom q w ∈ M.accept := by
+  classical
+  have hrules (r : ContextFreeRule T σ) : r ∈ (dfaGrammar M).rules ↔
+      (∃ s a, r = ⟨s, [.terminal a, .nonterminal (M.step s a)]⟩) ∨
+      (∃ s, s ∈ M.accept ∧ r = ⟨s, []⟩) := by
+    dsimp only [dfaGrammar]
+    simp only [Finset.mem_union, Finset.mem_image, Finset.mem_univ,
+      Finset.mem_filter, true_and]
+    constructor
+    · rintro (⟨⟨s, a⟩, hr⟩ | ⟨s, hs, hr⟩)
+      · exact Or.inl ⟨s, a, hr.symm⟩
+      · exact Or.inr ⟨s, hs, hr.symm⟩
+    · rintro (⟨s, a, rfl⟩ | ⟨s, hs, rfl⟩)
+      · exact Or.inl ⟨(s, a), rfl⟩
+      · exact Or.inr ⟨s, hs, rfl⟩
+  have hrewrite (r : ContextFreeRule T σ) (u : List T) (s : σ)
+      (v : List (Symbol T σ))
+      (h : r.Rewrites (u.map .terminal ++ [.nonterminal s]) v) :
+      r.input = s ∧ v = u.map .terminal ++ r.output := by
+    induction u generalizing v with
+    | nil =>
+      cases h with
+      | head => simp
+      | cons _ h => cases h
+    | cons a u ih =>
+      cases h with
+      | cons _ h =>
+        obtain ⟨hs, hv⟩ := ih _ h
+        exact ⟨hs, by simp [hv]⟩
+  have hterminal (u : List T) (v : List (Symbol T σ)) :
+      ¬ (dfaGrammar M).Produces (u.map .terminal) v := by
+    rintro ⟨r, _, hr⟩
+    have := hr.nonterminal_input_mem
+    simp at this
+  constructor
+  · intro h
+    have hinvariant {v : List (Symbol T σ)}
+        (hv : (dfaGrammar M).Derives [.nonterminal q] v) :
+        (∃ u, v = u.map .terminal ∧ M.evalFrom q u ∈ M.accept) ∨
+        (∃ u s, v = u.map .terminal ++ [.nonterminal s] ∧ M.evalFrom q u = s) := by
+      induction hv with
+      | refl => exact Or.inr ⟨[], q, rfl, rfl⟩
+      | tail _ hstep ih =>
+        rcases ih with ⟨u, rfl, _⟩ | ⟨u, s, rfl, hrun⟩
+        · exact (hterminal _ _ hstep).elim
+        · obtain ⟨r, hr, hrewriteStep⟩ := hstep
+          obtain ⟨hinput, rfl⟩ := hrewrite r u s _ hrewriteStep
+          rcases (hrules r).mp hr with ⟨s', a, rfl⟩ | ⟨s', hs', rfl⟩
+          · change s' = s at hinput
+            subst s'
+            right
+            refine ⟨u ++ [a], M.step s a, ?_, ?_⟩
+            · simp
+            · simp [DFA.evalFrom_of_append, hrun]
+          · change s' = s at hinput
+            subst s'
+            left
+            exact ⟨u, by simp, hrun ▸ hs'⟩
+    rcases hinvariant h with ⟨u, hu, haccept⟩ | ⟨u, s, hu, _⟩
+    · have : w = u := (List.map_inj_right (fun _ _ h => Symbol.terminal.inj h)).mp hu
+      simpa [this] using haccept
+    · have : (.nonterminal s : Symbol T σ) ∈ w.map .terminal := by
+        exact hu.symm ▸ (by simp)
+      simp at this
+  · intro h
+    induction w generalizing q with
+    | nil =>
+      apply ContextFreeGrammar.Produces.single
+      refine ⟨⟨q, []⟩, (hrules _).mpr (Or.inr ⟨q, h, rfl⟩), ?_⟩
+      exact ContextFreeRule.Rewrites.input_output
+    | cons a w ih =>
+      have hstep : (dfaGrammar M).Produces [.nonterminal q]
+          [.terminal a, .nonterminal (M.step q a)] :=
+        ⟨⟨q, [.terminal a, .nonterminal (M.step q a)]⟩,
+          (hrules _).mpr (Or.inl ⟨q, a, rfl⟩), ContextFreeRule.Rewrites.input_output⟩
+      exact hstep.trans_derives ((ih (M.step q a) h).append_left [.terminal a])
+
+/-- The finite right-linear grammar generates precisely the DFA's language,
+including empty words and empty terminal alphabets. -/
+theorem dfaGrammar_language (M : DFA T σ) : (dfaGrammar M).language = M.accepts := by
+  ext w
+  exact dfaGrammar_derives_iff M M.start w
+
+end Parikh
diff --git a/LeanPool/Parikh/Decomposition.lean b/LeanPool/Parikh/Decomposition.lean
new file mode 100644
index 0000000000..a8d0217c99
--- /dev/null
+++ b/LeanPool/Parikh/Decomposition.lean
@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+import LeanPool.Parikh.BoundedCutSupport
+import LeanPool.Parikh.ParseTreePaths
+import LeanPool.Parikh.TreePlugging
+import LeanPool.Parikh.TreeReplacement
+import Mathlib.Algebra.Order.Group.Nat
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Reconstructing trees from a base and bounded cycles
+
+Insertion wraps a matching subtree in a cycle context while retaining the
+original subtree in its hole. The first results show when insertion is possible
+and how it changes weight, size, and support.
+
+The main result, `decomposition`, reverses this process: cut a bounded cycle
+from a non-simple complete tree, repeat on the smaller tree, and stop at a
+simple base. Strong induction on production count ensures termination even
+when a removed cycle produces no terminals. The recorded insertion sequence
+reconstructs the exact original tree, not just its count vector.
+
+Source: `lem:plug`, `lem:cut`, `thm:decomposition`.
+-/
+namespace Parikh
+variable {T : Type*}
+
+/-- Insert around a selected occurrence, keeping the original subtree (`def:insertion`). -/
+@[expose] def Inserts (g : ContextFreeGrammar T) (t C t' : ParseTree T g.NT) : Prop :=
+  Complete g t ∧ Complete g t' ∧ ∃ A, Cycle g C A ∧
+    ∃ q u, t.subtree q = some u ∧ u.root = .nonterminal A ∧
+      t.replaceAt q (C.plug u) = some t'
+
+/-- An ordered sequence of cycle insertions reconstructing the final tree. -/
+inductive InsertionSequence (g : ContextFreeGrammar T) :
+    ParseTree T g.NT → List (ParseTree T g.NT) → ParseTree T g.NT → Prop where
+  | nil (t) : InsertionSequence g t [] t
+  | cons {t C next Cs final} (step : Inserts g t C next)
+      (rest : InsertionSequence g next Cs final) : InsertionSequence g t (C :: Cs) final
+
+/-- Base trees are simple complete start trees; context height uses the active alphabet. -/
+@[expose] def IsBase (g : ContextFreeGrammar T) (B : ParseTree T g.NT) : Prop :=
+  Complete g B ∧ B.root = .nonterminal g.initial ∧ B.Simple
+
+/-- A cycle context whose height is bounded by the active alphabet size plus one. -/
+@[expose] def IsBoundedCycle (g : ContextFreeGrammar T) (C : ParseTree T g.NT) : Prop :=
+  (∃ A, Cycle g C A) ∧ C.height ≤ (activeNonterminals g).card + 1
+
+/-- Plugging preserves validity/root and adds weight/size/support (`lem:plug`). -/
+theorem plugging [DecidableEq T] (g : ContextFreeGrammar T) (E t : ParseTree T g.NT)
+    (A : g.NT) (hE : OneHole g E A) (ht : Complete g t)
+    (hroot : t.root = .nonterminal A) :
+    Complete g (E.plug t) ∧ (E.plug t).root = E.root ∧
+      (E.plug t).weight = E.weight + t.weight ∧
+      (E.plug t).productionSize = E.productionSize + t.productionSize ∧
+      (E.plug t).support = E.support ∪ t.support := by
+  obtain ⟨hvalid, hholes⟩ := hE
+  have hsemantics := hvalid.plug_complete ht (by
+    intro B hB
+    have hBA : B = A := by simpa only [hholes, List.mem_singleton] using hB
+    simpa only [hBA] using hroot)
+  refine ⟨hsemantics.1, hsemantics.2, ?_, ?_, ?_⟩
+  · funext a
+    simpa only [ParseTree.weight, counts, Pi.add_apply, hholes,
+      List.length_singleton, Nat.one_mul] using E.count_yield_plug t a
+  · simpa only [hholes, List.length_singleton, Nat.one_mul]
+      using E.productionSize_plug t
+  · ext B
+    simp [E.mem_support_plug t B, hholes]
+
+/-- Support means an internal occurrence, including an empty-production node (`lem:enabled`). -/
+theorem insertion_enabled (g : ContextFreeGrammar T) (t C : ParseTree T g.NT)
+    (A : g.NT) (ht : Complete g t) (hC : Cycle g C A) :
+    (∃ t', Inserts g t C t') ↔ A ∈ t.support := by
+  classical
+  constructor
+  · rintro ⟨t', _, _, B, hCB, q, u, hpos, hu, _⟩
+    have hBA : B = A := Symbol.nonterminal.inj (hCB.2.1.symm.trans hC.2.1)
+    subst B
+    exact (ht.mem_support_iff_subtree A).mpr ⟨q, u, hpos, hu⟩
+  · intro hA
+    obtain ⟨q, u, hpos, hu⟩ := (ht.mem_support_iff_subtree A).mp hA
+    obtain ⟨huc, E, hE, _, _, hreplace⟩ := ht.subtree_context q u hpos A hu
+    have hCu := plugging g C u A hC.1 huc hu
+    have hCuRoot : (C.plug u).root = .nonterminal A := hCu.2.1.trans hC.2.1
+    have hwhole := plugging g E (C.plug u) A hE hCu.1 hCuRoot
+    exact ⟨E.plug (C.plug u), ht, hwhole.1, A, hC, q, u, hpos, hu,
+      hreplace (C.plug u)⟩
+
+/-- Exact accounting, including zero-weight cycles (`lem:insertion-laws`). -/
+theorem insertion_accounting [DecidableEq T] (g : ContextFreeGrammar T)
+    (t C t' : ParseTree T g.NT) (h : Inserts g t C t') :
+    t'.root = t.root ∧ t'.weight = t.weight + C.weight ∧
+      t'.productionSize = t.productionSize + C.productionSize ∧
+      t'.support = t.support ∪ C.support := by
+  obtain ⟨ht, _, A, hC, q, u, hpos, hu, hreplace⟩ := h
+  obtain ⟨huc, E, hE, hroot, hplug, houter⟩ := ht.subtree_context q u hpos A hu
+  have hCu := plugging g C u A hC.1 huc hu
+  have hCuRoot : (C.plug u).root = .nonterminal A := hCu.2.1.trans hC.2.1
+  have hbefore := plugging g E u A hE huc hu
+  have hafter := plugging g E (C.plug u) A hE hCu.1 hCuRoot
+  have hresult : E.plug (C.plug u) = t' :=
+    Option.some.inj ((houter (C.plug u)).symm.trans hreplace)
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · rw [← hresult, hafter.2.1, hroot]
+  · rw [← hresult, hafter.2.2.1, hCu.2.2.1, ← hplug, hbefore.2.2.1]
+    ac_rfl
+  · rw [← hresult, hafter.2.2.2.1, hCu.2.2.2.1, ← hplug, hbefore.2.2.2.1]
+    omega
+  · rw [← hresult, hafter.2.2.2.2, hCu.2.2.2.2, ← hplug, hbefore.2.2.2.2]
+    ext B
+    simp only [Set.mem_union]
+    tauto
+
+/-- Simple complete trees have bounded production height (`lem:simple-height`). -/
+theorem simple_height (g : ContextFreeGrammar T) (t : ParseTree T g.NT)
+    (ht : Complete g t) (hs : t.Simple) :
+    t.height ≤ (activeNonterminals g).card := by
+  classical
+  obtain ⟨path, hp, hlen⟩ := t.exists_labelPath_height
+  have hsubset : path.toFinset ⊆ activeNonterminals g := by
+    intro A hA
+    exact complete_support_active g t ht
+      (t.labelPath_subset_support path hp A (List.mem_toFinset.mp hA))
+  rw [← hlen, ← List.toFinset_card_of_nodup (hs path hp)]
+  exact Finset.card_le_card hsubset
+
+/-- Remove a bounded cycle from a non-simple complete tree (`lem:cut`).
+The smaller tree remains complete and has the same root. Inserting the returned
+context reconstructs the original tree, and production size strictly decreases.
+Choosing a minimal non-simple subtree bounds the context's side branches as
+well as the path between repeated labels. -/
+theorem bounded_cut (g : ContextFreeGrammar T) (t : ParseTree T g.NT)
+    (ht : Complete g t) (hs : ¬ t.Simple) :
+    ∃ smaller C, Complete g smaller ∧ smaller.root = t.root ∧
+      IsBoundedCycle g C ∧ Inserts g smaller C t ∧
+      smaller.productionSize < t.productionSize := by
+  classical
+  -- Descend to a non-simple occurrence whose side branches are all simple.
+  obtain ⟨q, r, cs, hpos, hU, hsU, hsimple⟩ :=
+    ht.exists_minimal_nonsimple_subtree hs
+  let U : ParseTree T g.NT := .node r cs
+  have hchildren : ∀ c ∈ cs, Complete g c := by
+    obtain ⟨hv, hh⟩ := hU
+    cases hv with
+    | node _ _ hr hc roots =>
+      have hholes : ∀ c ∈ cs, c.holes = [] := by
+        simpa only [ParseTree.holes, List.flatten_eq_nil_iff, List.forall_mem_map] using hh
+      exact fun c hc' => ⟨hc c hc', hholes c hc'⟩
+  have hheight : U.height ≤ (activeNonterminals g).card + 1 := by
+    have hchildheight : ∀ c ∈ cs, c.height ≤ (activeNonterminals g).card :=
+      fun c hc => simple_height g c (hchildren c hc) (hsimple c hc)
+    have hfold : (cs.map ParseTree.height).foldl max 0 ≤ (activeNonterminals g).card := by
+      by_cases hcs : cs = []
+      · simp [hcs]
+      · have hne : cs.map ParseTree.height ≠ [] := fun h => hcs (List.map_eq_nil_iff.mp h)
+        rw [List.foldl_max_eq_max hne, Nat.zero_max]
+        apply (List.max_le_iff hne).mpr
+        intro n hn
+        obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hn
+        exact hchildheight c hc
+    simpa only [U, ParseTree.height, Nat.add_comm] using Nat.add_le_add_left hfold 1
+  -- The repeated root gives a proper descendant with the same root symbol.
+  obtain ⟨c, hcmem, hrootmem⟩ :=
+    ParseTree.exists_root_mem_child_support r cs hsU hsimple
+  obtain ⟨p, v, hp, hvroot⟩ := ((hchildren c hcmem).mem_support_iff_subtree r.input).mp hrootmem
+  obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp hcmem
+  have hvpos : U.subtree (i :: p) = some v := by simp [U, ParseTree.subtree, hi, hp]
+  obtain ⟨hv, C, hC, hCroot, hCplug, _⟩ := hU.subtree_context (i :: p) v hvpos r.input hvroot
+  have hvsize : v.productionSize < U.productionSize :=
+    (U.productionSize_subtree_bound (i :: p) v hvpos).2 (by simp)
+  dsimp only [U] at hvsize
+  have hCsize : 0 < C.productionSize := by
+    have hsize := C.productionSize_plug v
+    rw [hC.2, List.length_singleton, Nat.one_mul, hCplug] at hsize
+    omega
+  have hcycle : Cycle g C r.input := ⟨hC, hCroot, hCsize⟩
+  have hCheight : C.height ≤ (activeNonterminals g).card + 1 := by
+    have hle := C.height_le_height_plug v
+    rw [hCplug] at hle
+    exact hle.trans hheight
+  -- Replace U by the descendant v; round-trip replacement certifies reconstruction.
+  obtain ⟨_, E, hE, hEroot, hEplug, hreplace⟩ :=
+    ht.subtree_context q U hpos r.input rfl
+  have hsmall := hE.1.plug_complete hv (by
+    intro A hA
+    have heq : A = r.input := by simpa only [hE.2, List.mem_singleton] using hA
+    simpa only [heq] using hvroot)
+  obtain ⟨smaller, hreplace', hsub, hundo⟩ := t.subtree_replacement q U v hpos
+  have heq : smaller = E.plug v := Option.some.inj (hreplace'.symm.trans (hreplace v))
+  subst smaller
+  refine ⟨E.plug v, C, hsmall.1, hsmall.2.trans hEroot, ⟨⟨r.input, hcycle⟩, hCheight⟩,
+    ⟨hsmall.1, ht, r.input, hcycle, q, v, hsub, hvroot, ?_⟩, ?_⟩
+  · rw [hCplug]
+    exact hundo
+  · have hbefore := E.productionSize_plug U
+    have hafter := E.productionSize_plug v
+    dsimp only [U] at hbefore
+    simp only [hE.2, List.length_singleton, Nat.one_mul] at hbefore hafter
+    rw [hEplug] at hbefore
+    omega
+
+/-- Concatenate insertion sequences, retaining the ordered list of contexts. -/
+theorem InsertionSequence.append {g : ContextFreeGrammar T}
+    {B middle t : ParseTree T g.NT} {Cs Ds : List (ParseTree T g.NT)}
+    (first : InsertionSequence g B Cs middle)
+    (second : InsertionSequence g middle Ds t) :
+    InsertionSequence g B (Cs ++ Ds) t := by
+  induction first with
+  | nil _ => simpa only [List.nil_append] using second
+  | cons step _ ih => exact .cons step (ih second)
+
+/-- Every complete tree can be rebuilt from a simple complete tree by inserting
+bounded cycle contexts (`thm:decomposition`).
+The insertion list retains actual contexts and their order, so reconstruction
+recovers the tree itself. The proof repeatedly applies `bounded_cut`, using
+production count for strong induction; zero-weight cycles still decrease this
+measure when removed. The simple tree has the same root as the original. -/
+theorem decomposition (g : ContextFreeGrammar T) (t : ParseTree T g.NT)
+    (ht : Complete g t) :
+    ∃ B Cs, Complete g B ∧ B.root = t.root ∧ B.Simple ∧
+      (∀ C ∈ Cs, IsBoundedCycle g C) ∧ InsertionSequence g B Cs t := by
+  classical
+  induction hn : t.productionSize using Nat.strong_induction_on generalizing t with
+  | h n ih =>
+    by_cases hs : t.Simple
+    · exact ⟨t, [], ht, rfl, hs, by simp, .nil t⟩
+    · obtain ⟨smaller, C, hsmaller, hroot, hbounded, hstep, hsize⟩ :=
+        bounded_cut g t ht hs
+      obtain ⟨B, Cs, hB, hBroot, hsimple, hCs, hseq⟩ :=
+        ih smaller.productionSize (hsize.trans_eq hn) smaller hsmaller rfl
+      refine ⟨B, Cs ++ [C], hB, hBroot.trans hroot, hsimple, ?_, ?_⟩
+      · intro D hD
+        rcases List.mem_append.mp hD with hD | hD
+        · exact hCs D hD
+        · exact (List.mem_singleton.mp hD) ▸ hbounded
+      · exact hseq.append (.cons hstep (.nil t))
+
+end Parikh
diff --git a/LeanPool/Parikh/ExecutableCompiler.lean b/LeanPool/Parikh/ExecutableCompiler.lean
new file mode 100644
index 0000000000..7c63371091
--- /dev/null
+++ b/LeanPool/Parikh/ExecutableCompiler.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.CompilerTrees
+import LeanPool.Parikh.CompilerBounds
+import LeanPool.Parikh.GrammarImage
+import Mathlib.Algebra.Order.Group.Nat
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# A certified executable grammar-to-witness compiler
+
+The finite input is enumerated by the proved bounded enumerator. Duplicate-free
+base/cycle lists are paired with all context sublists; the proved activation
+test selects exactly the compatible components. Context identities survive
+until activation and remain separately indexed periods afterwards.
+Source: `sec:effective`, `eq:main`, `thm:size-bound`, `eq:bit-bound`.
+-/
+namespace Parikh
+namespace EncodedGrammar
+
+/-- The certified activation test with computable equality for encoded syntax. -/
+@[expose] def activates (g : EncodedGrammar)
+    (B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))
+    (D : List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))) : Bool :=
+  letI : DecidableEq g.decode.NT := inferInstanceAs (DecidableEq (Fin
+    (g.extraNonterminalCount + 1)))
+  letI := ParseTree.decEq (T := Fin g.terminalCount) (N := g.decode.NT)
+  contextActivation g.decode B D
+
+theorem activates_correct (g : EncodedGrammar)
+    [de : DecidableEq (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))]
+    (B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)))
+    (D : List (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))))
+    (hD : ∀ C ∈ D, IsBoundedCycle g.decode C) :
+    g.activates B D = true ↔ ContextsActivatable g.decode B D.toFinset := by
+  classical
+  let dn := instDecidableEqFin (g.extraNonterminalCount + 1)
+  let dc := @ParseTree.decEq (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))
+    (inferInstance) dn
+  have h := @contextActivation_correct (Fin g.terminalCount) g.decode dn dc B D
+    (fun C hC => (hD C hC).1)
+  have hset : @List.toFinset _ dc D = @List.toFinset _ de D :=
+    congrArg (fun eqDecision => @List.toFinset _ eqDecision D) (Subsingleton.elim dc de)
+  exact h.trans (Iff.of_eq (congrArg (ContextsActivatable g.decode B) hset))
+
+/-- Compute the complete finite representation. Tree duplicates are removed;
+component/weight duplicates and zero periods are retained. -/
+@[expose] def compile (g : EncodedGrammar) : Witness (Fin g.terminalCount) :=
+  g.baseTrees.flatMap fun B =>
+    (g.cycleTrees.sublists.filter (g.activates B)).map (listComponent B)
+
+/-- Every output component retains a base and one ordered context subset. -/
+theorem mem_compile (g : EncodedGrammar) (c : Component (Fin g.terminalCount)) :
+    c ∈ g.compile ↔ ∃ B ∈ g.baseTrees,
+      ∃ D ∈ g.cycleTrees.sublists, g.activates B D = true ∧ listComponent B D = c := by
+  simp only [compile, List.mem_flatMap, List.mem_map, List.mem_filter]
+  tauto
+
+/-- The executable output denotes exactly the decoded grammar's Parikh image. -/
+theorem compile_correct (g : EncodedGrammar) :
+    g.compile.denotation = image g.decode.language := by
+  classical
+  rw [← (treeRepresentation_correct g.decode).1]
+  ext v
+  change (∃ c ∈ g.compile, v ∈ c.denotation) ↔
+    ∃ B : ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1)),
+      ∃ D : Finset (ParseTree (Fin g.terminalCount) (Fin (g.extraNonterminalCount + 1))),
+        IsBase g.decode B ∧ (∀ C ∈ D, IsBoundedCycle g.decode C) ∧
+          ContextsActivatable g.decode B D ∧ v ∈ (contextComponent B D).denotation
+  constructor
+  · rintro ⟨c, hc, hv⟩
+    obtain ⟨B, hb, D, hd, ha, rfl⟩ := (g.mem_compile c).mp hc
+    have hsub := List.mem_sublists.mp hd
+    have hcycles : ∀ C ∈ D, IsBoundedCycle g.decode C :=
+      fun C hC => (g.mem_cycleTrees C).mp (hsub.subset hC)
+    refine ⟨B, D.toFinset, (g.mem_baseTrees B).mp hb, ?_,
+      (g.activates_correct B D hcycles).mp ha, ?_⟩
+    · exact fun C hC => hcycles C (List.mem_toFinset.mp hC)
+    · rwa [← listComponent_denotation B D (hsub.nodup g.cycleTrees_nodup)]
+  · rintro ⟨B, D, hb, hd, ha, hv⟩
+    let cs := g.cycleTrees.filter (fun C => decide (C ∈ D))
+    have hsub : cs.Sublist g.cycleTrees := List.filter_sublist
+    have hset : cs.toFinset = D := by
+      ext C
+      simp only [List.mem_toFinset, cs, List.mem_filter, decide_eq_true_eq]
+      exact ⟨fun h => h.2, fun h => ⟨(g.mem_cycleTrees C).mpr (hd C h), h⟩⟩
+    have hcycles : ∀ C ∈ cs, IsBoundedCycle g.decode C :=
+      fun C hC => (g.mem_cycleTrees C).mp (hsub.subset hC)
+    have hact : g.activates B cs = true := (g.activates_correct B cs hcycles).mpr (by
+      rwa [hset])
+    refine ⟨listComponent B cs, (g.mem_compile _).mpr
+      ⟨B, (g.mem_baseTrees B).mpr hb, cs, List.mem_sublists.mpr hsub, hact, rfl⟩, ?_⟩
+    rw [listComponent_denotation B cs (hsub.nodup g.cycleTrees_nodup), hset]
+    exact hv
+
+/-- Activation filtering bounds output length by the base/subset candidate count. -/
+theorem compile_length_le (g : EncodedGrammar) :
+    g.compile.length ≤ g.baseTrees.length * 2 ^ g.cycleTrees.length := by
+  unfold compile
+  rw [List.length_flatMap]
+  have hsum := List.sum_le_length_nsmul
+    (g.baseTrees.map fun B =>
+      ((g.cycleTrees.sublists.filter (g.activates B)).map (listComponent B)).length)
+    (2 ^ g.cycleTrees.length) (by
+      intro n hn
+      obtain ⟨B, _, rfl⟩ := List.mem_map.mp hn
+      simpa only [List.length_map, List.length_sublists] using
+        List.length_filter_le (g.activates B) g.cycleTrees.sublists)
+  simpa only [List.length_map, Nat.nsmul_eq_mul] using hsum
+
+/-- Every computed witness satisfies all four accepted declared-size bounds. -/
+theorem compile_bounded (g : EncodedGrammar) : WithinBounds g.size g.compile := by
+  classical
+  obtain ⟨hb, hc, hnorm⟩ := g.tree_budgets
+  refine ⟨g.compile_length_le.trans
+    (Nat.mul_le_mul hb (Nat.pow_le_pow_right (by omega) hc)), ?_⟩
+  intro c hmem
+  obtain ⟨B, hB, D, hD, _, rfl⟩ := (g.mem_compile c).mp hmem
+  have hsub := List.mem_sublists.mp hD
+  have hDlen : D.length ≤ g.size.trees := hsub.length_le.trans hc
+  have hbase : norm B.weight ≤ g.size.positions :=
+    hnorm B (Or.inl ((g.mem_baseTrees B).mp hB))
+  have hperiod : ∀ C ∈ D, norm C.weight ≤ g.size.positions :=
+    fun C hC => hnorm C (Or.inr ((g.mem_cycleTrees C).mp (hsub.subset hC)))
+  have hnd := hsub.nodup g.cycleTrees_nodup
+  have hbnorm := (contextComponent_size_bounds B D.toFinset g.size.positions
+    hbase (fun C hC => hperiod C (List.mem_toFinset.mp hC))).2.1
+  have hcard : D.toFinset.card = D.length := List.toFinset_card_of_nodup hnd
+  have hbaseeq : (listComponent B D).base = (contextComponent B D.toFinset).base := by
+    change B.weight + (D.map ParseTree.weight).sum = B.weight + ∑ C ∈ D.toFinset, C.weight
+    rw [List.sum_toFinset ParseTree.weight hnd]
+  refine ⟨?_, ?_, ?_⟩
+  · simpa only [listComponent, List.length_map] using hDlen
+  · rw [hbaseeq]
+    exact hbnorm.trans (Nat.mul_le_mul_right _ (Nat.add_le_add_right (hcard.le.trans hDlen) 1))
+  · intro p hp
+    obtain ⟨C, hC, rfl⟩ := List.mem_map.mp hp
+    exact hperiod C hC
+
+/-- The compiled numerical entries satisfy the accepted fixed-width bit budget. -/
+theorem compile_bit_bound (g : EncodedGrammar) :
+    entryBits g.size g.compile ≤ g.size.vectorBits ∧
+      (∀ c ∈ g.compile, ∀ a, c.base a < 2 ^ g.size.coordinateBits) ∧
+      (∀ c ∈ g.compile, ∀ p ∈ c.periods, ∀ a, p a < 2 ^ g.size.coordinateBits) :=
+  witness_bit_bound g.size (by simp [size]) g.compile g.compile_bounded
+
+end EncodedGrammar
+
+/-- An executable implementing value of the accepted compiler interface,
+with kernel-checked exact-denotation and quantitative guarantees. -/
+@[expose] def compiler : Compiler where
+  compile := EncodedGrammar.compile
+  correct := EncodedGrammar.compile_correct
+  bounded := EncodedGrammar.compile_bounded
+
+end Parikh
diff --git a/LeanPool/Parikh/FiniteRepresentation.lean b/LeanPool/Parikh/FiniteRepresentation.lean
new file mode 100644
index 0000000000..e6db09aaad
--- /dev/null
+++ b/LeanPool/Parikh/FiniteRepresentation.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+import LeanPool.Parikh.InsertionSequences
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Turning the tree description into a finite union
+
+Decomposition and activation describe the grammar image using simple bases and
+bounded cycle contexts. To conclude semilinearity, we must show that only
+finitely many choices occur.
+
+`bases_finite` and `bounded_cycles_finite` specialize the bounded-tree theorem.
+There are then finitely many context subsets for each base, and each activatable
+choice contributes a linear set. `treeRepresentation_isSemilinearSet` combines
+these facts using Mathlib's finite-union results. This is semantic finiteness;
+an algorithm that enumerates the families is a separate task.
+
+Source: `lem:finite`, `thm:main`.
+-/
+namespace Parikh
+variable {T : Type*}
+
+/-- Simple complete start trees form a finite family over arbitrary nonterminals. -/
+theorem bases_finite [Finite T] (g : ContextFreeGrammar T) :
+    {B : ParseTree T g.NT | IsBase g B}.Finite := by
+  apply (bounded_open_finite g (activeNonterminals g).card).subset
+  rintro B ⟨hB, _, hsimple⟩
+  exact ⟨⟨hB.1, by simp [hB.2]⟩, simple_height g B hB hsimple⟩
+
+/-- A cycle's unique hole is active because its matching root is a production
+label. Thus the bounded-cycle family is finite even with infinite nonterminals. -/
+theorem bounded_cycles_finite [Finite T] (g : ContextFreeGrammar T) :
+    {C : ParseTree T g.NT | IsBoundedCycle g C}.Finite := by
+  apply (bounded_open_finite g ((activeNonterminals g).card + 1)).subset
+  rintro C ⟨⟨A, hcycle⟩, hheight⟩
+  refine ⟨⟨hcycle.1.1, ?_⟩, hheight⟩
+  intro B hB
+  have hBA : B = A := by
+    simpa only [hcycle.1.2, List.mem_singleton] using hB
+  subst B
+  exact hcycle.1.1.support_active hcycle.root_mem_support
+
+/-- The tree representation is a finite union of the existing linear components.
+Filtering the finite powerset keeps exactly the activatable context subsets. -/
+theorem treeRepresentation_isSemilinearSet [Finite T] [DecidableEq T]
+    (g : ContextFreeGrammar T) : IsSemilinearSet (treeRepresentation g) := by
+  classical
+  let bases := (bases_finite g).toFinset
+  let cycles := (bounded_cycles_finite g).toFinset
+  have hunion : treeRepresentation g =
+      ⋃ B ∈ bases, ⋃ D ∈ cycles.powerset.filter (ContextsActivatable g B),
+        (contextComponent B D).denotation := by
+    ext v
+    simp only [treeRepresentation, Set.mem_ofPred_eq, Set.mem_iUnion,
+      Finset.mem_filter, Finset.mem_powerset]
+    constructor
+    · rintro ⟨B, D, hB, hD, hactive, hv⟩
+      refine ⟨B, (bases_finite g).mem_toFinset.mpr hB, D, ⟨?_, hactive⟩, hv⟩
+      intro C hC
+      exact (bounded_cycles_finite g).mem_toFinset.mpr (hD C hC)
+    · rintro ⟨B, hB, D, ⟨hD, hactive⟩, hv⟩
+      exact ⟨B, D, (bases_finite g).mem_toFinset.mp hB,
+        fun C hC => (bounded_cycles_finite g).mem_toFinset.mp (hD hC), hactive, hv⟩
+  rw [hunion]
+  exact IsSemilinearSet.biUnion_finset fun B _ =>
+    IsSemilinearSet.biUnion_finset fun D _ =>
+      (component_isLinearSet (contextComponent B D)).isSemilinearSet
+
+end Parikh
diff --git a/LeanPool/Parikh/FiniteWitness.lean b/LeanPool/Parikh/FiniteWitness.lean
new file mode 100644
index 0000000000..fb6868e392
--- /dev/null
+++ b/LeanPool/Parikh/FiniteWitness.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+import LeanPool.Parikh.GrammarImage
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# A witness from finite tree families
+
+List one component for each base and activatable subset of bounded contexts.
+The periods keep context identities as separate list positions, even when
+their weights coincide or vanish. This classical assembly supports the
+quantitative existence theorem; executable compilation is a separate task.
+
+Source: `eq:main`, `thm:size-bound`.
+-/
+namespace Parikh
+variable {T : Type*} [DecidableEq T]
+
+/-- Assemble the exact tree formula from finite base and context families. -/
+@[expose] noncomputable def familyWitness (g : ContextFreeGrammar T)
+    (bases cycles : Finset (ParseTree T g.NT)) : Witness T := by
+  classical
+  exact ((bases ×ˢ cycles.powerset).filter fun pair =>
+    ContextsActivatable g pair.1 pair.2).toList.map fun pair => contextComponent pair.1 pair.2
+
+/-- Component membership retains both its base tree and its selected context subset. -/
+theorem mem_familyWitness (g : ContextFreeGrammar T)
+    (bases cycles : Finset (ParseTree T g.NT)) (c : Component T) :
+    c ∈ familyWitness g bases cycles ↔
+      ∃ B ∈ bases, ∃ D : Finset (ParseTree T g.NT),
+        D ⊆ cycles ∧ ContextsActivatable g B D ∧ contextComponent B D = c := by
+  classical
+  simp only [familyWitness, List.mem_map, Finset.mem_toList, Finset.mem_filter,
+    Finset.mem_product, Finset.mem_powerset, Prod.exists]
+  constructor
+  · rintro ⟨B, D, ⟨⟨hB, hD⟩, ha⟩, hc⟩
+    exact ⟨B, hB, D, hD, ha, hc⟩
+  · rintro ⟨B, hB, D, hD, ha, hc⟩
+    exact ⟨B, D, ⟨⟨hB, hD⟩, ha⟩, hc⟩
+
+/-- Activation filtering cannot exceed the number of base/subset pairs. -/
+theorem familyWitness_length_le (g : ContextFreeGrammar T)
+    (bases cycles : Finset (ParseTree T g.NT)) :
+    (familyWitness g bases cycles).length ≤ bases.card * 2 ^ cycles.card := by
+  classical
+  simpa only [familyWitness, List.length_map, Finset.length_toList,
+    Finset.card_product, Finset.card_powerset] using
+    Finset.card_filter_le (bases ×ˢ cycles.powerset)
+      (fun pair => ContextsActivatable g pair.1 pair.2)
+
+/-- Exact base and cycle families give exactly the grammar's Parikh image. -/
+theorem familyWitness_denotation [Finite T] (g : ContextFreeGrammar T)
+    (bases cycles : Finset (ParseTree T g.NT))
+    (hb : ∀ B, B ∈ bases ↔ IsBase g B)
+    (hc : ∀ C, C ∈ cycles ↔ IsBoundedCycle g C) :
+    (familyWitness g bases cycles).denotation = image g.language := by
+  classical
+  rw [← (treeRepresentation_correct g).1]
+  ext v
+  constructor
+  · rintro ⟨c, hmem, hv⟩
+    obtain ⟨B, hB, D, hD, ha, rfl⟩ := (mem_familyWitness g bases cycles c).mp hmem
+    exact ⟨B, D, (hb B).mp hB, fun C hC => (hc C).mp (hD hC), ha, hv⟩
+  · rintro ⟨B, D, hB, hD, ha, hv⟩
+    refine ⟨contextComponent B D, ?_, hv⟩
+    exact (mem_familyWitness g bases cycles _).mpr
+      ⟨B, (hb B).mpr hB, D, fun C hC => (hc C).mpr (hD C hC), ha, rfl⟩
+
+end Parikh
diff --git a/LeanPool/Parikh/GrammarImage.lean b/LeanPool/Parikh/GrammarImage.lean
new file mode 100644
index 0000000000..c047846f27
--- /dev/null
+++ b/LeanPool/Parikh/GrammarImage.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+import LeanPool.Parikh.FiniteRepresentation
+import LeanPool.Parikh.InsertionSequences
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Joining the tree description to the grammar language
+
+The earlier modules give a semilinear union of tree components. Here we prove
+that this union is exactly the grammar image: insertions turn component vectors
+into words, and decomposition puts each derived word into a component.
+
+`treeRepresentation_correct` packages this equality with semilinearity.
+The public theorems in `Statements.lean` project its two conclusions; the
+regular-language specialization reuses the same result. Keeping this argument
+in a shared module avoids an import cycle between the public statements and
+regular realization.
+
+Source: `thm:main`, `thm:parikh-statement`.
+-/
+namespace Parikh
+variable {T : Type*}
+
+/-- The exact tree formula and its semilinearity together give the grammar image
+(`thm:main`, `thm:parikh-statement`). No finite nonterminal assumption is needed. -/
+theorem treeRepresentation_correct [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    treeRepresentation g = image g.language ∧ IsSemilinearSet (image g.language) := by
+  have heq : treeRepresentation g = image g.language := by
+    classical
+    ext v
+    constructor
+    · -- Realize a component vector by insertions, then read the resulting word.
+      rintro ⟨B, D, hB, _, hD, hv⟩
+      rw [← one_linear g B D hB.1 hD] at hv
+      obtain ⟨t, Cs, hseq, _, hweight⟩ := hv
+      obtain ⟨ht, hroot, _, _, _⟩ := hseq.accounting hB.1
+      refine ⟨t.yield, ?_, hweight⟩
+      exact (g.mem_language_iff t.yield).mpr
+        ((derives_iff_tree g g.initial t.yield).mpr
+          ⟨t, ht, hroot.trans hB.2.1, rfl⟩)
+    · -- Decompose a word's derivation tree and collect the contexts it uses.
+      rintro ⟨w, hw, rfl⟩
+      obtain ⟨t, ht, hroot, hyield⟩ :=
+        (derives_iff_tree g g.initial w).mp ((g.mem_language_iff w).mp hw)
+      obtain ⟨B, Cs, hB, hBroot, hsimple, hbounded, hseq⟩ := decomposition g t ht
+      have hD := hseq.contextsActivatable hB
+      refine ⟨B, Cs.toFinset, ⟨hB, hBroot.trans hroot, hsimple⟩,
+        fun C hC => hbounded C (List.mem_toFinset.mp hC), hD, ?_⟩
+      rw [← one_linear g B Cs.toFinset hB hD]
+      exact ⟨t, Cs, hseq, fun C => List.mem_toFinset.symm,
+        by simp only [ParseTree.weight, hyield]⟩
+  refine ⟨heq, ?_⟩
+  rw [← heq]
+  exact treeRepresentation_isSemilinearSet g
+
+end Parikh
diff --git a/LeanPool/Parikh/GrammarTrees.lean b/LeanPool/Parikh/GrammarTrees.lean
new file mode 100644
index 0000000000..0b2a5aec0f
--- /dev/null
+++ b/LeanPool/Parikh/GrammarTrees.lean
@@ -0,0 +1,493 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Counting
+public import Mathlib.Computability.ContextFreeGrammar
+import Mathlib.Data.Set.Finite.List
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Parse trees, unfinished derivations, and their meaning
+
+To decompose a derivation, we need to retain its production nodes and child
+order. `ParseTree` provides this syntax. A hole represents an unexpanded
+nonterminal; `Valid` checks the grammar rules, and `Complete` rules out holes.
+An empty production is still a production node, even though its frontier is empty.
+
+The first part defines tree statistics and contexts. Later results show that
+complete trees describe exactly Mathlib's derivations (`derives_iff_tree`) and
+that trees of bounded height form a finite family when their labels are
+restricted appropriately (`bounded_open_finite`). These are the semantic and
+finiteness foundations for decomposition.
+
+Source: `def:tree`, `def:statistics`, `prop:tree-word`, `lem:finite`.
+-/
+namespace Parikh
+
+/-- Concrete parse-tree syntax (`def:tree`), including open trees with holes.
+Grammar validity and completeness are checked separately by `Valid` and `Complete`. -/
+inductive ParseTree (T N : Type*) where
+  | terminal (a : T)
+  | hole (A : N)
+  | node (rule : ContextFreeRule T N) (children : List (ParseTree T N))
+
+namespace ParseTree
+variable {T N : Type*}
+
+/-- Terminal or nonterminal symbol at the tree root. -/
+@[expose] def root : ParseTree T N → Symbol T N
+  | .terminal a => .terminal a
+  | .hole A => .nonterminal A
+  | .node r _ => .nonterminal r.input
+
+/-- Read the leaves from left to right, retaining holes as nonterminals.
+At a production node we concatenate the children's frontiers. In particular,
+an empty production has no children and contributes the empty list: its root
+label records a rule application, not a remaining symbol in the frontier. -/
+@[expose] def frontier : ParseTree T N → List (Symbol T N)
+  | .terminal a => [.terminal a]
+  | .hole A => [.nonterminal A]
+  | .node _ children => (children.map frontier).flatten
+
+/-- Terminal leaves in order; for a complete tree this is its yield. -/
+@[expose] def yield : ParseTree T N → List T
+  | .terminal a => [a]
+  | .hole _ => []
+  | .node _ children => (children.map yield).flatten
+
+/-- Unexpanded nonterminal leaves in frontier order. -/
+@[expose] def holes : ParseTree T N → List N
+  | .terminal _ => []
+  | .hole A => [A]
+  | .node _ children => (children.map holes).flatten
+
+/-- The termination measure counts productions, including silent/unit nodes. -/
+@[expose] def productionSize : ParseTree T N → ℕ
+  | .terminal _ | .hole _ => 0
+  | .node _ children => 1 + (children.map productionSize).sum
+
+/-- The maximum number of production nodes on a downward path.
+Terminal leaves and holes have height zero. A production node adds one to its
+largest child height; with no children, the maximum is zero, so an empty
+production has height one. -/
+@[expose] def height : ParseTree T N → ℕ
+  | .terminal _ | .hole _ => 0
+  | .node _ children => 1 + (children.map height).foldl max 0
+
+/-- Nonterminal labels at production nodes, including empty productions. -/
+@[expose] def productionLabels : ParseTree T N → List N
+  | .terminal _ | .hole _ => []
+  | .node r children => r.input :: (children.map productionLabels).flatten
+
+/-- Holes contribute no nonterminal to support (`def:statistics`). -/
+@[expose] def support (t : ParseTree T N) : Set N := {A | A ∈ t.productionLabels}
+
+/-- Letter-count vector of the terminal yield. -/
+@[expose] def weight [DecidableEq T] (t : ParseTree T N) : Vector T := counts t.yield
+
+/-- Production labels along downward paths, including nonempty prefixes at nodes.
+A terminal or hole contributes the empty label path. At a node, `[r.input]`
+records the path stopping there, and prepending `r.input` to each child path
+records paths continuing below it. The explicit singleton also handles an
+empty production. Labels repeated in different sibling branches are allowed;
+`Simple` excludes repetitions only within a single path. -/
+@[expose] def labelPaths : ParseTree T N → List (List N)
+  | .terminal _ | .hole _ => [[]]
+  | .node r children => [r.input] ::
+      ((children.map labelPaths).flatten.map (r.input :: ·))
+
+/-- No production label repeats along any downward path. -/
+@[expose] def Simple (t : ParseTree T N) : Prop := ∀ path ∈ t.labelPaths, path.Nodup
+
+/-- Plug all holes. The one-hole contract below makes this a single replacement. -/
+@[expose] def plug : ParseTree T N → ParseTree T N → ParseTree T N
+  | .terminal a, _ => .terminal a
+  | .hole _, t => t
+  | .node r children, t => .node r (children.map (fun c => plug c t))
+
+/-- Positions use zero-based child indices; invalid positions return `none`. -/
+@[expose] def subtree : ParseTree T N → List ℕ → Option (ParseTree T N)
+  | t, [] => some t
+  | .node _ children, i :: q => children[i]?.bind (fun t => subtree t q)
+  | _, _ :: _ => none
+
+/-- Replace the subtree at a child-index path, rejecting invalid positions. -/
+@[expose] def replaceAt : ParseTree T N → List ℕ → ParseTree T N → Option (ParseTree T N)
+  | _, [], replacement => some replacement
+  | .node r children, i :: q, replacement => do
+      let child ← children[i]?
+      let newChild ← replaceAt child q replacement
+      return .node r (children.set i newChild)
+  | _, _ :: _, _ => none
+
+end ParseTree
+
+variable {T : Type*}
+
+/-- A tree follows the grammar, although it may still contain holes.
+Terminal leaves and holes are valid on their own. A production node is valid
+when its rule belongs to the grammar, all children are valid, and their roots
+match the rule's right-hand side in order. For an empty right-hand side, this
+last condition forces the child list to be empty. -/
+inductive Valid (g : ContextFreeGrammar T) : ParseTree T g.NT → Prop where
+  | terminal (a) : Valid g (.terminal a)
+  | hole (A) : Valid g (.hole A)
+  | node (r children) (rule_mem : r ∈ g.rules)
+      (children_valid : ∀ t ∈ children, Valid g t)
+      (roots_match : children.map ParseTree.root = r.output) : Valid g (.node r children)
+
+/-- A valid tree with no unexpanded nonterminal leaves.
+Its terminal yield is therefore a fully derived word. The root condition for
+a grammar's start symbol is imposed separately where needed. -/
+@[expose] def Complete (g : ContextFreeGrammar T) (t : ParseTree T g.NT) : Prop :=
+  Valid g t ∧ t.holes = []
+
+/-- A valid context with exactly one hole, labelled `A`.
+A matching complete tree can be placed in that hole to finish the context. -/
+@[expose] def OneHole (g : ContextFreeGrammar T) (E : ParseTree T g.NT) (A : g.NT) : Prop :=
+  Valid g E ∧ E.holes = [A]
+
+/-- A derivation context that returns to its starting nonterminal (`def:cycle`).
+The unique hole and the root both have label `A`, so the context can wrap a
+subtree rooted at `A` and can be inserted repeatedly. Positive production size
+excludes the bare hole. A cycle may nevertheless produce no terminal letters;
+then insertion enlarges the tree without changing its Parikh vector. -/
+@[expose] def Cycle (g : ContextFreeGrammar T) (C : ParseTree T g.NT) (A : g.NT) : Prop :=
+  OneHole g C A ∧ C.root = .nonterminal A ∧ 0 < C.productionSize
+
+/-- The start and every nonterminal mentioned in a production: finite even if `g.NT` is infinite. -/
+@[expose] noncomputable def activeNonterminals (g : ContextFreeGrammar T) : Finset g.NT := by
+  classical
+  exact {g.initial} ∪ g.rules.biUnion (fun r =>
+    {r.input} ∪ (r.output.filterMap fun s => match s with
+      | .terminal _ => none
+      | .nonterminal A => some A).toFinset)
+
+/-- Arbitrary holes outside the active alphabet must be excluded from bounded enumeration. -/
+@[expose] def ActiveOpen (g : ContextFreeGrammar T) (t : ParseTree T g.NT) : Prop :=
+  Valid g t ∧ ∀ A ∈ t.holes, A ∈ activeNonterminals g
+
+/-- Production-node labels are active even in a valid open tree (`def:statistics`).
+Holes contribute no label to support. -/
+theorem Valid.support_active {g : ContextFreeGrammar T} {t : ParseTree T g.NT}
+    (ht : Valid g t) : t.support ⊆ (activeNonterminals g : Set g.NT) := by
+  classical
+  induction ht with
+  | terminal a =>
+    intro A hA
+    change A ∈ (ParseTree.terminal a : ParseTree T g.NT).productionLabels at hA
+    rw [ParseTree.productionLabels.eq_1] at hA
+    exact False.elim (List.not_mem_nil hA)
+  | hole A =>
+    intro B hB
+    change B ∈ (ParseTree.hole A : ParseTree T g.NT).productionLabels at hB
+    rw [ParseTree.productionLabels.eq_2] at hB
+    exact False.elim (List.not_mem_nil hB)
+  | node r children hr hc roots ih =>
+    intro A hA
+    change A ∈ (ParseTree.node r children).productionLabels at hA
+    rw [ParseTree.productionLabels.eq_3] at hA
+    rcases List.mem_cons.mp hA with rfl | hA
+    · unfold activeNonterminals
+      apply Finset.mem_union_right
+      apply Finset.mem_biUnion.mpr
+      exact ⟨r, hr, Finset.mem_union_left _ (Finset.mem_singleton_self _)⟩
+    · obtain ⟨labels, hlabels, hA⟩ := List.mem_flatten.mp hA
+      obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hlabels
+      exact ih c hc hA
+
+/-- Every production node in a complete tree belongs to the finite active alphabet. -/
+theorem complete_support_active (g : ContextFreeGrammar T) (t : ParseTree T g.NT)
+    (ht : Complete g t) : t.support ⊆ (activeNonterminals g : Set g.NT) := by
+  exact ht.1.support_active
+
+/-- Finite terminals and finite productions suffice; no `Fintype g.NT` (`lem:finite`). -/
+theorem bounded_open_finite [Finite T] (g : ContextFreeGrammar T) (H : ℕ) :
+    {t : ParseTree T g.NT | ActiveOpen g t ∧ t.height ≤ H}.Finite := by
+  classical
+  have nodeHeight (r : ContextFreeRule T g.NT) (cs : List (ParseTree T g.NT)) :
+      (ParseTree.node r cs).height = 1 + (cs.map ParseTree.height).foldl max 0 := by
+    exact ParseTree.height.eq_3 r cs
+  -- Fixed-length lists over a finite subtype cover every possible child list.
+  have finiteLists {s : Set (ParseTree T g.NT)} (hs : s.Finite) (n : ℕ) :
+      {cs : List (ParseTree T g.NT) | cs.length = n ∧ ∀ c ∈ cs, c ∈ s}.Finite := by
+    let : Finite s := hs
+    apply ((List.finite_length_eq s n).image (List.map Subtype.val)).subset
+    intro cs hcs
+    refine ⟨cs.attachWith (· ∈ s) hcs.2, ?_, ?_⟩
+    · simpa using hcs.1
+    · exact List.attachWith_map_subtype_val hcs.2
+  -- At height zero, only finite terminals and active holes are available.
+  have leaves :
+      (Set.range (ParseTree.terminal (N := g.NT)) ∪
+        ParseTree.hole '' (activeNonterminals g : Set g.NT)).Finite :=
+    (Set.finite_range (ParseTree.terminal (T := T) (N := g.NT))).union
+      ((activeNonterminals g).finite_toSet.image _)
+  induction H with
+  | zero =>
+    apply leaves.subset
+    rintro t ⟨⟨hv, ha⟩, hh⟩
+    cases hv with
+    | terminal a => exact Or.inl ⟨a, rfl⟩
+    | hole A =>
+      apply Or.inr
+      refine ⟨A, ?_, rfl⟩
+      apply ha A
+      simp [ParseTree.holes]
+    | node r cs hr hv roots =>
+      rw [nodeHeight] at hh
+      omega
+  | succ H ih =>
+    let family : Set (ParseTree T g.NT) :=
+      {t | ActiveOpen g t ∧ t.height ≤ H}
+    -- Each finite production fixes its arity; validity filters this finite superset.
+    have nodes : (⋃ r ∈ (g.rules : Set (ContextFreeRule T g.NT)),
+        ParseTree.node r '' {cs : List (ParseTree T g.NT) |
+          cs.length = r.output.length ∧ ∀ c ∈ cs, c ∈ family}).Finite :=
+      g.rules.finite_toSet.biUnion fun r _ => (finiteLists ih r.output.length).image _
+    apply (leaves.union nodes).subset
+    rintro t ⟨⟨hv, ha⟩, hh⟩
+    cases hv with
+    | terminal a => exact Or.inl (Or.inl ⟨a, rfl⟩)
+    | hole A =>
+      apply Or.inl ∘ Or.inr
+      refine ⟨A, ?_, rfl⟩
+      apply ha A
+      simp [ParseTree.holes]
+    | node r cs hr hv roots =>
+      apply Or.inr
+      apply Set.mem_iUnion₂.mpr
+      refine ⟨r, hr, cs, ⟨?_, ?_⟩, rfl⟩
+      · simpa using congrArg List.length roots
+      · intro c hc
+        refine ⟨⟨hv c hc, ?_⟩, ?_⟩
+        · intro A hA
+          apply ha A
+          simp only [ParseTree.holes, ← List.flatMap_def, List.mem_flatMap]
+          exact ⟨c, hc, hA⟩
+        · have hm : c.height ∈ cs.map ParseTree.height := List.mem_map_of_mem hc
+          have hmax := List.le_max_of_mem hm
+          have hne := List.ne_nil_of_mem hm
+          rw [nodeHeight, List.foldl_max_eq_max hne, Nat.zero_max] at hh
+          omega
+
+
+variable {N : Type*}
+
+/-- A context-free rewrite in a concatenation occurs in one of its two parts. -/
+theorem rewrites_append_cases (r : ContextFreeRule T N)
+    (u v w : List (Symbol T N)) (h : r.Rewrites (u ++ v) w) :
+    (∃ u', r.Rewrites u u' ∧ w = u' ++ v) ∨
+      (∃ v', r.Rewrites v v' ∧ w = u ++ v') := by
+  induction u generalizing w with
+  | nil => exact Or.inr ⟨w, h, rfl⟩
+  | cons x u ih =>
+    cases h with
+    | head =>
+      exact Or.inl ⟨r.output ++ u, .head u, (List.append_assoc _ _ _).symm⟩
+    | cons _ h =>
+      rcases ih _ h with ⟨u', hu', rfl⟩ | ⟨v', hv', rfl⟩
+      · exact Or.inl ⟨x :: u', .cons x hu', rfl⟩
+      · exact Or.inr ⟨v', hv', rfl⟩
+
+namespace ParseTree
+/-- The nonterminals on the frontier are exactly the holes. -/
+theorem frontier_holes (t : ParseTree T N) :
+    (t.frontier.filterMap fun (s : Symbol T N) => match s with
+      | .terminal _ => none | .nonterminal A => some A) = t.holes := by
+  induction t using ParseTree.rec (motive_2 := fun (ts : List (ParseTree T N)) =>
+    ∀ t ∈ ts, (t.frontier.filterMap fun (s : Symbol T N) => match s with
+      | .terminal _ => none | .nonterminal A => some A) = t.holes) with
+  | terminal a => simp [frontier, holes]
+  | hole A => simp [frontier, holes]
+  | node r children ih =>
+    simp only [frontier, holes, List.filterMap_flatten, List.map_map]
+    congr 1
+    exact List.map_congr_left ih
+  | nil c hc => simp at hc
+  | cons t ts ht hts c hc =>
+    rcases List.mem_cons.mp hc with rfl | hc
+    · exact ht
+    · exact hts c hc
+
+/-- The terminals on the frontier are exactly the yield. -/
+theorem frontier_yield (t : ParseTree T N) :
+    (t.frontier.filterMap fun (s : Symbol T N) => match s with
+      | .terminal a => some a | .nonterminal _ => none) = t.yield := by
+  induction t using ParseTree.rec (motive_2 := fun (ts : List (ParseTree T N)) =>
+    ∀ t ∈ ts, (t.frontier.filterMap fun (s : Symbol T N) => match s with
+      | .terminal a => some a | .nonterminal _ => none) = t.yield) with
+  | terminal a => simp [frontier, yield]
+  | hole A => simp [frontier, yield]
+  | node r children ih =>
+    simp only [frontier, yield, List.filterMap_flatten, List.map_map]
+    congr 1
+    exact List.map_congr_left ih
+  | nil c hc => simp at hc
+  | cons t ts ht hts c hc =>
+    rcases List.mem_cons.mp hc with rfl | hc
+    · exact ht
+    · exact hts c hc
+
+/-- A tree with no holes has a wholly terminal frontier. -/
+theorem frontier_of_holes_eq_nil (t : ParseTree T N) (h : t.holes = []) :
+    t.frontier = t.yield.map Symbol.terminal := by
+  have onlyTerminals : ∀ l : List (Symbol T N),
+      (l.filterMap fun s => match s with
+        | .terminal _ => none | .nonterminal A => some A) = [] →
+      l = (l.filterMap fun s => match s with
+        | .terminal a => some a | .nonterminal _ => none).map Symbol.terminal := by
+    intro l
+    induction l with
+    | nil => simp
+    | cons s l ih =>
+      cases s with
+      | terminal a =>
+        intro h
+        simp only [List.filterMap_cons_none] at h
+        simpa only [List.filterMap_cons, List.map_cons]
+          using congrArg (Symbol.terminal a :: ·) (ih h)
+      | nonterminal A => simp
+  rw [← frontier_yield]
+  exact onlyTerminals t.frontier (t.frontier_holes.trans h)
+
+end ParseTree
+
+/-- A valid tree gives a Mathlib derivation from its root to its frontier. -/
+theorem Valid.derives_frontier {g : ContextFreeGrammar T} {t : ParseTree T g.NT}
+    (ht : Valid g t) : g.Derives [t.root] t.frontier := by
+  induction ht with
+  | terminal a => simpa only [ParseTree.root, ParseTree.frontier] using
+      (ContextFreeGrammar.Derives.refl (g := g) [.terminal a])
+  | hole A => simpa only [ParseTree.root, ParseTree.frontier] using
+      (ContextFreeGrammar.Derives.refl (g := g) [.nonterminal A])
+  | node r children hr hc roots ih =>
+    have forest : g.Derives (children.map ParseTree.root)
+        (children.map ParseTree.frontier).flatten := by
+      clear hc roots
+      induction children with
+      | nil => exact .refl _
+      | cons c cs hcs =>
+        have hhead := ih c (by simp)
+        have htail := hcs (fun t ht => ih t (by simp [ht]))
+        exact (hhead.append_right (cs.map ParseTree.root)).trans
+          (htail.append_left c.frontier)
+    simpa only [ParseTree.root, ParseTree.frontier] using
+      (ContextFreeGrammar.Produces.single (g := g) ⟨r, hr,
+        ContextFreeRule.Rewrites.input_output⟩).trans (roots ▸ forest)
+
+/-- A rewrite expands one frontier hole, preserving validity and the tree root. -/
+theorem Valid.frontier_step {g : ContextFreeGrammar T} {t : ParseTree T g.NT}
+    (ht : Valid g t) {v : List (Symbol T g.NT)} (h : g.Produces t.frontier v) :
+    ∃ t', Valid g t' ∧ t'.root = t.root ∧ t'.frontier = v := by
+  induction ht generalizing v with
+  | terminal a =>
+    obtain ⟨r, hr, hs⟩ := h
+    have hm := hs.nonterminal_input_mem
+    simp [ParseTree.frontier] at hm
+  | hole A =>
+    obtain ⟨r, hr, hs⟩ := h
+    have hm := hs.nonterminal_input_mem
+    simp only [ParseTree.frontier, List.mem_singleton, Symbol.nonterminal.injEq] at hm
+    have hv : v = r.output := by
+      simp only [ParseTree.frontier] at hs
+      cases hs with
+      | head => simp
+      | cons _ hs => exact False.elim (by simpa using hs.nonterminal_input_mem)
+    let leaf : Symbol T g.NT → ParseTree T g.NT := fun s => match s with
+      | .terminal a => .terminal a
+      | .nonterminal B => .hole B
+    have hroot : ∀ s, (leaf s).root = s := by intro s; cases s <;> rfl
+    refine ⟨.node r (r.output.map leaf), .node _ _ hr ?_ ?_, ?_, ?_⟩
+    · intro c hc
+      obtain ⟨s, hs, rfl⟩ := List.mem_map.mp hc
+      cases s with
+      | terminal a => exact .terminal a
+      | nonterminal B => exact .hole B
+    · simp only [List.map_map]
+      simp only [Function.comp_def, hroot, List.map_id']
+    · simpa only [ParseTree.root] using congrArg Symbol.nonterminal hm
+    · have hf : ∀ s, (leaf s).frontier = [s] := by
+        intro s; cases s <;> simp [leaf, ParseTree.frontier]
+      simp only [ParseTree.frontier, List.map_map, Function.comp_def, hf]
+      simpa only [← List.flatMap_def, List.flatMap_singleton'] using hv.symm
+  | node r children hr hc roots ih =>
+    have forest : ∀ v, g.Produces (children.map ParseTree.frontier).flatten v →
+        ∃ children' : List (ParseTree T g.NT), (∀ c ∈ children', Valid g c) ∧
+          children'.map ParseTree.root = children.map ParseTree.root ∧
+          (children'.map ParseTree.frontier).flatten = v := by
+      clear hr roots h
+      induction children with
+      | nil =>
+        intro v hv
+        obtain ⟨s, hs, hrewrite⟩ := hv
+        exact False.elim (by simpa using hrewrite.nonterminal_input_mem)
+      | cons c cs hcs =>
+        intro v hv
+        obtain ⟨s, hs, hrewrite⟩ := hv
+        simp only [List.map_cons, List.flatten_cons] at hrewrite
+        rcases rewrites_append_cases s c.frontier (cs.map ParseTree.frontier).flatten v
+          hrewrite with ⟨u, hu, hv⟩ | ⟨u, hu, hv⟩
+        · obtain ⟨c', hc', hroot, hf⟩ := ih c (by simp) ⟨s, hs, hu⟩
+          refine ⟨c' :: cs, ?_, ?_, ?_⟩
+          · intro d hd
+            rcases List.mem_cons.mp hd with rfl | hd
+            · exact hc'
+            · exact hc d (by simp [hd])
+          · simp only [List.map_cons, hroot]
+          · simp only [List.map_cons, List.flatten_cons, hf, hv]
+        · obtain ⟨cs', hvalid, hroot, hf⟩ := hcs
+            (fun d hd => hc d (by simp [hd]))
+            (fun d hd => ih d (by simp [hd])) u ⟨s, hs, hu⟩
+          refine ⟨c :: cs', ?_, ?_, ?_⟩
+          · intro d hd
+            rcases List.mem_cons.mp hd with rfl | hd
+            · exact hc d (by simp)
+            · exact hvalid d hd
+          · simp only [List.map_cons, hroot]
+          · simp only [List.map_cons, List.flatten_cons, hf, hv]
+    obtain ⟨children', hvalid, hroots, hf⟩ := forest v (by
+      simpa only [ParseTree.frontier] using h)
+    exact ⟨.node r children', .node _ _ hr hvalid (hroots.trans roots),
+      rfl, by simpa only [ParseTree.frontier] using hf⟩
+
+/-- Any derivation from a nonterminal is the frontier of a valid open tree. -/
+theorem derives_tree_frontier (g : ContextFreeGrammar T) (A : g.NT)
+    {v : List (Symbol T g.NT)} (h : g.Derives [.nonterminal A] v) :
+    ∃ t, Valid g t ∧ t.root = .nonterminal A ∧ t.frontier = v := by
+  induction h with
+  | refl => exact ⟨.hole A, .hole A, rfl, by simp [ParseTree.frontier]⟩
+  | tail h step ih =>
+    obtain ⟨t, ht, hr, hf⟩ := ih
+    obtain ⟨t', ht', hr', hf'⟩ := ht.frontier_step (hf.symm ▸ step)
+    exact ⟨t', ht', hr'.trans hr, hf'⟩
+
+/-- Concrete bridge to Mathlib's derivation relation, for every root (`prop:tree-word`,
+appendix A). -/
+theorem derives_iff_tree (g : ContextFreeGrammar T) (A : g.NT) (w : List T) :
+    g.Derives [.nonterminal A] (w.map Symbol.terminal) ↔
+      ∃ t : ParseTree T g.NT,
+        Complete g t ∧ t.root = .nonterminal A ∧ t.yield = w := by
+  constructor
+  · intro h
+    obtain ⟨t, ht, hr, hf⟩ := derives_tree_frontier g A h
+    refine ⟨t, ⟨ht, ?_⟩, hr, ?_⟩
+    · rw [← t.frontier_holes, hf]
+      simp
+    · rw [← t.frontier_yield, hf]
+      simp
+  · rintro ⟨t, ⟨ht, hh⟩, hr, hw⟩
+    simpa only [hr, t.frontier_of_holes_eq_nil hh, hw] using ht.derives_frontier
+
+
+end Parikh
diff --git a/LeanPool/Parikh/Imports.lean b/LeanPool/Parikh/Imports.lean
new file mode 100644
index 0000000000..30afd41f94
--- /dev/null
+++ b/LeanPool/Parikh/Imports.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.Parikh
+public import LeanPool.Parikh.Activation
+public import LeanPool.Parikh.ActivationAlgorithm
+public import LeanPool.Parikh.Api
+public import LeanPool.Parikh.BoundedCutSupport
+public import LeanPool.Parikh.BoundedEnumeration
+public import LeanPool.Parikh.BoundedFamilySupport
+public import LeanPool.Parikh.CompilerBounds
+public import LeanPool.Parikh.CompilerSupport
+public import LeanPool.Parikh.CompilerTrees
+public import LeanPool.Parikh.Construction
+public import LeanPool.Parikh.Counting
+public import LeanPool.Parikh.DFAGrammar
+public import LeanPool.Parikh.Decomposition
+public import LeanPool.Parikh.ExecutableCompiler
+public import LeanPool.Parikh.FiniteRepresentation
+public import LeanPool.Parikh.FiniteWitness
+public import LeanPool.Parikh.GrammarImage
+public import LeanPool.Parikh.GrammarTrees
+public import LeanPool.Parikh.InsertionSequences
+public import LeanPool.Parikh.ParseTreePaths
+public import LeanPool.Parikh.RegularRealization
+public import LeanPool.Parikh.Statements
+public import LeanPool.Parikh.TreePlugging
+public import LeanPool.Parikh.TreeReplacement
+public import LeanPool.Parikh.WordBlockAutomata
diff --git a/LeanPool/Parikh/InsertionSequences.lean b/LeanPool/Parikh/InsertionSequences.lean
new file mode 100644
index 0000000000..283b66b310
--- /dev/null
+++ b/LeanPool/Parikh/InsertionSequences.lean
@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Decomposition
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Accounting for several insertions
+
+One insertion adds a context's terminal counts and production nodes while
+preserving existing support. Along a sequence, these contributions accumulate:
+weights and sizes add, and support is the union of the labels introduced.
+
+`InsertionSequence.accounting` packages these facts together with completeness
+and root preservation. Later activation proofs use it to move between an
+abstract list of operations and an actual reconstructed tree. Zero-weight
+cycles obey the same laws: they add productions even when they add no letters.
+
+Source: `cor:sequence`.
+-/
+namespace Parikh
+variable {T : Type*}
+
+/-- A nontrivial cycle has a production node at its root (`eq:cycle-root`). -/
+theorem Cycle.root_mem_support {g : ContextFreeGrammar T} {C : ParseTree T g.NT}
+    {A : g.NT} (hC : Cycle g C A) : A ∈ C.support := by
+  have hsize := hC.2.2
+  cases C with
+  | terminal a => simp [ParseTree.productionSize] at hsize
+  | hole B => simp [ParseTree.productionSize] at hsize
+  | node r cs =>
+    have hroot : r.input = A := by simpa only [ParseTree.root, Symbol.nonterminal.injEq]
+      using hC.2.1
+    simp [ParseTree.support, ParseTree.productionLabels, hroot]
+
+/-- Every insertion sequence preserves completeness/root and exactly adds the
+listed weights and production counts, while taking the union of supports. -/
+theorem InsertionSequence.accounting [DecidableEq T] {g : ContextFreeGrammar T}
+    {B t : ParseTree T g.NT} {Cs : List (ParseTree T g.NT)}
+    (h : InsertionSequence g B Cs t) (hB : Complete g B) :
+    Complete g t ∧ t.root = B.root ∧
+      t.weight = B.weight + (Cs.map ParseTree.weight).sum ∧
+      t.productionSize = B.productionSize + (Cs.map ParseTree.productionSize).sum ∧
+      t.support = B.support ∪ ⋃ C ∈ Cs, C.support := by
+  induction h with
+  | nil B => exact ⟨hB, rfl, by simp, by simp, by simp⟩
+  | @cons B C next Cs final step rest ih =>
+    have hs := insertion_accounting g B C next step
+    obtain ⟨hf, hr, hw, hn, hu⟩ := ih step.2.1
+    refine ⟨hf, hr.trans hs.1, ?_, ?_, ?_⟩
+    · simp only [List.map_cons, List.sum_cons]
+      rw [hw, hs.2.1]
+      ac_rfl
+    · simp only [List.map_cons, List.sum_cons]
+      rw [hn, hs.2.2.1]
+      omega
+    · rw [hu, hs.2.2.2]
+      ext A
+      simp only [Set.mem_union, Set.mem_iUnion, List.mem_cons]
+      aesop
+
+end Parikh
diff --git a/LeanPool/Parikh/ParseTreePaths.lean b/LeanPool/Parikh/ParseTreePaths.lean
new file mode 100644
index 0000000000..5ad25857d1
--- /dev/null
+++ b/LeanPool/Parikh/ParseTreePaths.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Why simple trees have bounded height
+
+A simple tree has no repeated production label along any downward path.
+To turn this condition into a height bound, we need two facts: every path
+label belongs to the tree's support, and some label path has length equal
+to the tree's height. Terminals and holes contribute no production label.
+
+This file proves those facts. `simple_height` in `Decomposition.lean` then
+compares the longest path with the finite set of active nonterminals.
+
+Source: `lem:simple-height`.
+-/
+namespace Parikh.ParseTree
+variable {T N : Type*}
+
+/-- Every production label on a path belongs to the tree's support. -/
+theorem labelPath_subset_support (t : ParseTree T N) (path : List N)
+    (hpath : path ∈ t.labelPaths) : ∀ A ∈ path, A ∈ t.support := by
+  induction t using ParseTree.rec (motive_2 := fun cs =>
+    ∀ c ∈ cs, ∀ path ∈ c.labelPaths, ∀ A ∈ path, A ∈ c.support) generalizing path with
+  | terminal a =>
+    simp only [labelPaths, List.mem_singleton] at hpath
+    subst path
+    simp
+  | hole A =>
+    simp only [labelPaths, List.mem_singleton] at hpath
+    subst path
+    simp
+  | node r cs ih =>
+    simp only [labelPaths, List.mem_cons, List.mem_map, ← List.flatMap_def,
+      List.mem_flatMap] at hpath
+    rcases hpath with rfl | ⟨tail, ⟨c, hc, htail⟩, rfl⟩
+    · intro A hA
+      have heq : A = r.input := by simpa using hA
+      simp [support, productionLabels, heq]
+    · intro A hA
+      simp only [List.mem_cons] at hA
+      rcases hA with rfl | hA
+      · simp [support, productionLabels]
+      · have hchild := ih c hc tail htail A hA
+        simp only [support, productionLabels, Set.mem_ofPred_eq, List.mem_cons,
+          ← List.flatMap_def, List.mem_flatMap]
+        exact Or.inr ⟨c, hc, hchild⟩
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rename_i path hp A hA
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc path hp A hA
+    · exact hcs d hd path hp A hA
+
+/-- A longest production-label path realizes production height (`def:statistics`).
+An empty-production node has the singleton root path; terminals and holes have the empty path. -/
+theorem exists_labelPath_height (t : ParseTree T N) :
+    ∃ path ∈ t.labelPaths, path.length = t.height := by
+  induction t using ParseTree.rec (motive_2 := fun cs =>
+    ∀ c ∈ cs, ∃ path ∈ c.labelPaths, path.length = c.height) with
+  | terminal a => exact ⟨[], by simp [labelPaths], by simp [height]⟩
+  | hole A => exact ⟨[], by simp [labelPaths], by simp [height]⟩
+  | node r cs ih =>
+    by_cases hcs : cs = []
+    · subst cs
+      exact ⟨[r.input], by simp [labelPaths], by simp [height]⟩
+    · have hheights : cs.map height ≠ [] := fun h => hcs (List.map_eq_nil_iff.mp h)
+      obtain ⟨c, hc, hmax⟩ := List.mem_map.mp (List.max_mem hheights)
+      obtain ⟨path, hp, hlen⟩ := ih c hc
+      refine ⟨r.input :: path, ?_, ?_⟩
+      · simp only [labelPaths, List.mem_cons, List.mem_map, ← List.flatMap_def,
+          List.mem_flatMap]
+        exact Or.inr ⟨path, ⟨c, hc, hp⟩, rfl⟩
+      · simp only [List.length_cons, height, List.foldl_max_eq_max hheights,
+          Nat.zero_max, hlen, hmax]
+        omega
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc
+    · exact hcs d hd
+
+end Parikh.ParseTree
diff --git a/LeanPool/Parikh/RegularRealization.lean b/LeanPool/Parikh/RegularRealization.lean
new file mode 100644
index 0000000000..27d2d38b7e
--- /dev/null
+++ b/LeanPool/Parikh/RegularRealization.lean
@@ -0,0 +1,278 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Counting
+public import Mathlib.Computability.RegularExpressions
+public import Mathlib.Computability.DFA
+import LeanPool.Parikh.DFAGrammar
+import LeanPool.Parikh.GrammarImage
+import LeanPool.Parikh.WordBlockAutomata
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Giving a semilinear set a regular language
+
+For a vector, choose a word containing exactly the prescribed letters. For a
+linear component, concatenate its base word with a starred word for each period.
+Taking the union of these expressions realizes a finite semilinear witness.
+
+There are two things to prove: the expression has exactly the requested Parikh
+image, and its language satisfies Mathlib's finite-state DFA predicate.
+The image proofs use counting laws; `WordBlockAutomata.lean` supplies the
+specialized automata constructions. Together they establish `converse`.
+The `regular_image` specialization goes in the other direction: it converts
+a DFA to a grammar with the same word language and applies the shared forward
+theorem.
+
+Source: `eq:representative`, `lem:linear-regular`, `thm:converse`.
+-/
+open scoped Computability Pointwise
+
+namespace Parikh
+section
+variable {T : Type*}
+
+/-- An explicit alphabet order, supplied as finite data for executable realization. -/
+structure AlphabetOrder (T : Type*) where
+  /-- Enumeration of the finite alphabet in the chosen order. -/
+  letters : List T
+  nodup : letters.Nodup
+  complete : ∀ a : T, a ∈ letters
+
+/-- Choose a word with count vector `v` by writing one block per letter.
+For alphabet order `[a, b]` and counts `v a = 2`, `v b = 1`, the blocks are
+`[a, a]` and `[b]`, giving `[a, a, b]` after flattening. A zero count contributes
+an empty block; an empty alphabet gives the empty word (`eq:representative`). -/
+@[expose] def representative (alphabet : AlphabetOrder T) (v : Vector T) : List T :=
+  (alphabet.letters.map fun a => List.replicate (v a) a).flatten
+
+/-- The regular expression accepting exactly the given word.
+The right fold concatenates each character with the expression for the remaining
+suffix. Its initial value is epsilon, so the empty list accepts just the empty
+word; `[a, b]` gives the expression `a · (b · ε)`. -/
+@[expose] def wordExpression (w : List T) : RegularExpression T :=
+  w.foldr (fun a rest => .comp (.char a) rest) .epsilon
+
+/-- Realize a linear component as `u_base · (u_p₁)* · ... · (u_pₖ)*`.
+The base word appears once. Each period word can appear any number of times,
+independently of the other periods. Concatenation adds their count vectors,
+so the resulting image is exactly the component's denotation. With no periods,
+the trailing expression is epsilon (`lem:linear-regular`). -/
+@[expose] def componentExpression (alphabet : AlphabetOrder T) (c : Component T) :
+  RegularExpression T :=
+  .comp (wordExpression (representative alphabet c.base))
+    (c.periods.foldr (fun p rest =>
+      .comp (.star (wordExpression (representative alphabet p))) rest) .epsilon)
+
+/-- Empty union is the zero expression (`eq:regular-construction`). -/
+@[expose] def witnessExpression (alphabet : AlphabetOrder T) (W : Witness T) :
+  RegularExpression T :=
+  W.foldr (fun c rest => .plus (componentExpression alphabet c) rest) .zero
+
+/-- Representative words have exactly the prescribed counts (`eq:representative`). -/
+theorem representative_counts [DecidableEq T] (alphabet : AlphabetOrder T) (v : Vector T) :
+    counts (representative alphabet v) = v := by
+  funext a
+  change List.count a ((alphabet.letters.map fun b => List.replicate (v b) b).flatten) = v a
+  rw [List.count_flatten, List.map_map]
+  have hzero : ∀ b, b ≠ a → b ∈ alphabet.letters →
+      (List.count a ∘ fun b => List.replicate (v b) b) b = 0 := by
+    intro b hba _
+    simp [List.count_replicate, hba]
+  rw [List.sum_map_eq_nsmul_single a _ hzero,
+    List.count_eq_one_of_mem alphabet.nodup (alphabet.complete a)]
+  simp
+
+/-- A literal-word expression accepts exactly that word. -/
+theorem wordExpression_matches (w : List T) :
+    (wordExpression w).matches' = {w} := by
+  induction w with
+  | nil => rfl
+  | cons a w ih =>
+    change ({[a]} : Language T) * (wordExpression w).matches' = {a :: w}
+    rw [ih]
+    change Set.image2 (fun u z : List T => u ++ z) {[a]} {w} = {a :: w}
+    exact Set.image2_singleton
+
+/-- Concatenation becomes pointwise addition under the Parikh map. -/
+theorem image_mul [DecidableEq T] (L M : Language T) :
+    image (L * M) = image L + image M := by
+  ext v
+  constructor
+  · rintro ⟨w, hw, rfl⟩
+    obtain ⟨u, hu, z, hz, rfl⟩ := Language.mem_mul.mp hw
+    exact Set.mem_add.mpr ⟨counts u, ⟨u, hu, rfl⟩, counts z,
+      ⟨z, hz, rfl⟩, (counts_append u z).symm⟩
+  · intro hv
+    obtain ⟨_, ⟨u, hu, rfl⟩, _, ⟨z, hz, rfl⟩, rfl⟩ := Set.mem_add.mp hv
+    exact ⟨u ++ z, Language.append_mem_mul hu hz, counts_append u z⟩
+
+/-- A starred word realizes exactly the additive closure of its count vector,
+including the empty word and zero repetitions. -/
+theorem wordExpression_star_image [DecidableEq T] (w : List T) :
+    image (wordExpression w).star.matches' =
+      (AddSubmonoid.closure ({counts w} : Set (Vector T)) : Set (Vector T)) := by
+  have hrep : ∀ n : ℕ, counts (List.replicate n w).flatten = n • counts w := by
+    intro n
+    induction n with
+    | zero => ext a; simp [counts]
+    | succ n ih =>
+      rw [List.replicate_succ, List.flatten_cons, counts_append, ih, succ_nsmul]
+      exact add_comm _ _
+  rw [RegularExpression.matches'_star, wordExpression_matches]
+  ext v
+  constructor
+  · rintro ⟨u, hu, rfl⟩
+    obtain ⟨ws, rfl, hws⟩ := Language.mem_kstar.mp hu
+    have hlist : ws = List.replicate ws.length w :=
+      List.eq_replicate_of_mem (fun z hz => Set.mem_singleton_iff.mp (hws z hz))
+    exact AddSubmonoid.mem_closure_singleton.mpr
+      ⟨ws.length, by rw [hlist]; simpa only [List.length_replicate] using (hrep _).symm⟩
+  · intro hv
+    obtain ⟨n, rfl⟩ := AddSubmonoid.mem_closure_singleton.mp hv
+    refine ⟨(List.replicate n w).flatten, Language.join_mem_kstar ?_, hrep n⟩
+    intro z hz
+    exact Set.mem_singleton_iff.mpr (List.eq_of_mem_replicate hz)
+
+end
+
+section
+variable {T : Type*}
+
+/-- The ordered product of starred period words realizes the existing additive
+closure of the period values; indexed coefficient semantics are reused unchanged. -/
+theorem periodExpressions_image [DecidableEq T] (alphabet : AlphabetOrder T)
+    (periods : List (Vector T)) :
+    image (periods.foldr (fun p (rest : RegularExpression T) =>
+      .comp (.star (wordExpression (representative alphabet p))) rest) .epsilon).matches' =
+      (AddSubmonoid.closure (Set.range periods.get) : Set (Vector T)) := by
+  induction periods with
+  | nil =>
+    have hnil : counts ([] : List T) = 0 := by ext a; simp [counts]
+    ext v
+    simp [image, RegularExpression.matches', Language.one_def,
+      Set.range_eq_empty, AddSubmonoid.closure_empty, hnil]
+  | cons p ps ih =>
+    have hrange : Set.range (p :: ps).get = {p} ∪ Set.range ps.get := by
+      rw [Set.range_list_get, Set.range_list_get]
+      ext q
+      simp only [Set.mem_ofPred_eq, Set.mem_union, Set.mem_singleton_iff, List.mem_cons]
+    rw [hrange, AddSubmonoid.closure_union]
+    change image ((wordExpression (representative alphabet p)).star.matches' *
+      (ps.foldr (fun q (rest : RegularExpression T) =>
+        .comp (.star (wordExpression (representative alphabet q))) rest) .epsilon).matches') = _
+    rw [image_mul, wordExpression_star_image, representative_counts, ih]
+    ext v
+    simp only [Set.mem_add, SetLike.mem_coe, AddSubmonoid.mem_sup]
+
+/-- The component expression has exactly the frozen indexed linear denotation
+(`lem:linear-regular`); DFA regularity is proved separately. -/
+theorem componentExpression_image [DecidableEq T] (alphabet : AlphabetOrder T)
+    (c : Component T) :
+    image (componentExpression alphabet c).matches' = c.denotation := by
+  have hliteral : image (wordExpression (representative alphabet c.base)).matches' =
+      {c.base} := by
+    rw [wordExpression_matches]
+    change counts '' ({representative alphabet c.base} : Set (List T)) = {c.base}
+    rw [Set.image_singleton, representative_counts]
+  change image ((wordExpression (representative alphabet c.base)).matches' *
+    (c.periods.foldr (fun p (rest : RegularExpression T) =>
+      .comp (.star (wordExpression (representative alphabet p))) rest) .epsilon).matches') = _
+  rw [image_mul, hliteral, periodExpressions_image,
+    Component.denotation_eq_vadd_closure]
+  ext v
+  simp only [Set.mem_add, Set.mem_singleton_iff, Set.mem_vadd_set,
+    vadd_eq_add, exists_eq_left]
+
+/-- Exact-image half of `witnessExpression_correct`, proved independently of the
+DFA clause (`eq:regular-construction`, `thm:converse`). -/
+theorem witnessExpression_image [DecidableEq T] (alphabet : AlphabetOrder T) (W : Witness T) :
+    image (witnessExpression alphabet W).matches' = W.denotation := by
+  induction W with
+  | nil => ext v; simp [witnessExpression, RegularExpression.matches', image,
+      Language.zero_def, Witness.denotation]
+  | cons c W ih =>
+    have hcons : Witness.denotation (c :: W) = c.denotation ∪ Witness.denotation W := by
+      ext v
+      simp [Witness.denotation]
+    have hunion : image ((componentExpression alphabet c).matches' +
+        (witnessExpression alphabet W).matches') =
+        image (componentExpression alphabet c).matches' ∪
+          image (witnessExpression alphabet W).matches' :=
+      Set.image_union counts _ _
+    change image ((componentExpression alphabet c).matches' +
+      (witnessExpression alphabet W).matches') = _
+    rw [hunion]
+    rw [componentExpression_image, ih, hcons]
+
+/-- Each ordered starred-period product is DFA-regular (`lem:linear-regular`). -/
+theorem periodExpressions_regular (alphabet : AlphabetOrder T) (periods : List (Vector T)) :
+    (periods.foldr (fun p (rest : RegularExpression T) =>
+      .comp (.star (wordExpression (representative alphabet p))) rest)
+        .epsilon).matches'.IsRegular := by
+  induction periods with
+  | nil => exact isRegular_one
+  | cons p ps ih =>
+    change ((wordExpression (representative alphabet p)).star.matches' *
+      (ps.foldr (fun q (rest : RegularExpression T) =>
+        .comp (.star (wordExpression (representative alphabet q))) rest)
+          .epsilon).matches').IsRegular
+    rw [RegularExpression.matches'_star, wordExpression_matches]
+    exact isRegular_word_star_mul _ _ ih
+
+/-- The base-word prefix preserves the regularity of the period product. -/
+theorem componentExpression_regular (alphabet : AlphabetOrder T) (c : Component T) :
+    (componentExpression alphabet c).matches'.IsRegular := by
+  change ((wordExpression (representative alphabet c.base)).matches' *
+    (c.periods.foldr (fun p (rest : RegularExpression T) =>
+      .comp (.star (wordExpression (representative alphabet p))) rest) .epsilon).matches').IsRegular
+  rw [wordExpression_matches]
+  exact isRegular_word_mul _ _ (periodExpressions_regular alphabet c.periods)
+
+/-- Mathlib's existing finite-union regularity combines the component automata. -/
+theorem witnessExpression_regular (alphabet : AlphabetOrder T) (W : Witness T) :
+    (witnessExpression alphabet W).matches'.IsRegular := by
+  induction W with
+  | nil => exact isRegular_zero
+  | cons c W ih =>
+    exact (componentExpression_regular alphabet c).add ih
+
+/-- The constructed expression realizes the exact witness and is DFA-regular (`thm:converse`). -/
+theorem witnessExpression_correct [DecidableEq T] (alphabet : AlphabetOrder T) (W : Witness T) :
+    image (witnessExpression alphabet W).matches' = W.denotation ∧
+      (witnessExpression alphabet W).matches'.IsRegular := by
+  exact ⟨witnessExpression_image alphabet W, witnessExpression_regular alphabet W⟩
+
+/-- Abstract semilinear sets are regular Parikh images (`thm:converse`). -/
+theorem converse [Finite T] [DecidableEq T] (X : Set (Vector T)) (hX : IsSemilinearSet X) :
+    ∃ R : Language T, R.IsRegular ∧ image R = X := by
+  classical
+  let : Fintype T := Fintype.ofFinite T
+  let alphabet : AlphabetOrder T :=
+    ⟨Finset.univ.toList, Finset.nodup_toList _, by intro a; simp⟩
+  obtain ⟨W, hW⟩ := exists_witness X hX
+  obtain ⟨himage, hregular⟩ := witnessExpression_correct alphabet W
+  exact ⟨(witnessExpression alphabet W).matches', hregular, himage.trans hW⟩
+
+/-- Regular-language specialization using Mathlib's DFA semantics (`thm:parikh-statement`). -/
+theorem regular_image [Finite T] [DecidableEq T] (R : Language T) (hR : R.IsRegular) :
+    IsSemilinearSet (image R) := by
+  classical
+  let : Fintype T := Fintype.ofFinite T
+  obtain ⟨σ, hσ, M, rfl⟩ := hR
+  let : Fintype σ := hσ
+  rw [← dfaGrammar_language M]
+  exact (treeRepresentation_correct (dfaGrammar M)).2
+
+end
+end Parikh
diff --git a/LeanPool/Parikh/Statements.lean b/LeanPool/Parikh/Statements.lean
new file mode 100644
index 0000000000..8c3027af64
--- /dev/null
+++ b/LeanPool/Parikh/Statements.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.Activation
+public import Mathlib.Computability.DFA
+import LeanPool.Parikh.GrammarImage
+import LeanPool.Parikh.RegularRealization
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Using Parikh's theorem
+
+This module proves semilinearity, exact finite representation, and the existence
+of a regular language with the same Parikh image. `Parikh/Api.lean` exposes
+descriptive public names for these results.
+
+The proof assembles earlier modules through `treeRepresentation_eq`: the union
+of activatable tree components is exactly the grammar image. Its proof and
+semilinearity are shared in `GrammarImage.lean`, so regular-language specialization
+can reuse them without an import cycle.
+The public results do not require a finite ambient nonterminal type.
+
+`Parikh/ExecutableCompiler.lean` computes a representation for finite encoded input.
+
+Source: `thm:main`, `thm:parikh-statement`.
+-/
+namespace Parikh
+variable {T : Type*}
+
+/-- The exact tree/context union equals the Mathlib grammar image (`thm:main`). -/
+theorem treeRepresentation_eq [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    treeRepresentation g = image g.language := by
+  exact (treeRepresentation_correct g).1
+
+/-- Forward Parikh theorem for Mathlib grammars (`thm:parikh-statement`).
+No finiteness or decidable-equality assumption is imposed on `g.NT`.
+-/
+theorem grammar_image [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    IsSemilinearSet (image g.language) := by
+  exact (treeRepresentation_correct g).2
+
+/-- A finite indexed witness with exact denotation, not merely containment (`thm:main`). -/
+theorem grammar_witness [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    ∃ W : Witness T, W.denotation = image g.language := by
+  exact exists_witness (image g.language) (grammar_image g)
+
+/-- Language-level specialization using Mathlib's context-free predicate. -/
+theorem contextFree_image [Finite T] [DecidableEq T] (L : Language T) (hL : L.IsContextFree) :
+    IsSemilinearSet (image L) := by
+  obtain ⟨g, rfl⟩ := hL
+  exact grammar_image g
+
+/-- Every CFL has a DFA-regular language with the same image (`thm:parikh-statement`). -/
+theorem regular_realization [Finite T] [DecidableEq T] (g : ContextFreeGrammar T) :
+    ∃ R : Language T, R.IsRegular ∧ image R = image g.language := by
+  exact converse (image g.language) (grammar_image g)
+
+end Parikh
diff --git a/LeanPool/Parikh/TreePlugging.lean b/LeanPool/Parikh/TreePlugging.lean
new file mode 100644
index 0000000000..7db98a3dfe
--- /dev/null
+++ b/LeanPool/Parikh/TreePlugging.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Filling a context with a tree
+
+Plugging replaces each hole of an open tree by a supplied tree. For the
+one-hole contexts used later, this joins two pieces of a derivation: their
+terminal counts and production counts add, and their supports are united.
+
+This file proves structural formulas for arbitrary numbers of holes and
+establishes validity and completeness when the inserted root matches the hole
+labels. The public theorem `Parikh.plugging` in `Decomposition.lean` packages the
+one-hole consequences used by insertion.
+
+Source: `lem:plug`.
+-/
+namespace Parikh
+variable {T N : Type*}
+
+/-- Filling matching holes with a complete tree preserves validity and the root. -/
+theorem Valid.plug_complete {g : ContextFreeGrammar T} {E t : ParseTree T g.NT}
+    (hE : Valid g E) (ht : Complete g t)
+    (hmatch : ∀ A ∈ E.holes, t.root = .nonterminal A) :
+    Complete g (E.plug t) ∧ (E.plug t).root = E.root := by
+  induction hE with
+  | terminal a =>
+    simp only [ParseTree.plug, Complete, ParseTree.holes]
+    exact ⟨⟨.terminal a, True.intro⟩, True.intro⟩
+  | hole A =>
+    simpa only [ParseTree.plug, ParseTree.root] using
+      And.intro ht (hmatch A (by simp [ParseTree.holes]))
+  | node r children hr hc roots ih =>
+    have children_plug : ∀ c ∈ children,
+        Complete g (c.plug t) ∧ (c.plug t).root = c.root := by
+      intro c hcmem
+      apply ih c hcmem
+      intro A hA
+      apply hmatch A
+      simp only [ParseTree.holes, ← List.flatMap_def, List.mem_flatMap]
+      exact ⟨c, hcmem, hA⟩
+    refine ⟨⟨?_, ?_⟩, by simp [ParseTree.plug, ParseTree.root]⟩
+    · simp only [ParseTree.plug]
+      refine Valid.node r _ hr ?_ ?_
+      · intro c hc
+        obtain ⟨d, hd, rfl⟩ := List.mem_map.mp hc
+        exact (children_plug d hd).1.1
+      · rw [List.map_map, ← roots]
+        exact List.map_congr_left fun c hc => (children_plug c hc).2
+    · simp only [ParseTree.plug, ParseTree.holes, List.flatten_eq_nil_iff,
+        List.forall_mem_map]
+      intro c hc
+      exact (children_plug c hc).1.2
+
+namespace ParseTree
+/-- Each hole contributes one copy of the inserted tree's production count. -/
+theorem productionSize_plug (E t : ParseTree T N) :
+    (E.plug t).productionSize = E.productionSize + E.holes.length * t.productionSize := by
+  induction E using ParseTree.rec (motive_2 := fun (cs : List (ParseTree T N)) =>
+    ∀ c ∈ cs, (c.plug t).productionSize =
+      c.productionSize + c.holes.length * t.productionSize) with
+  | terminal a => simp [plug.eq_1, productionSize.eq_1, holes.eq_1]
+  | hole A => simp [plug.eq_2, productionSize.eq_2, holes.eq_2]
+  | node r cs ih =>
+    simp only [plug.eq_3, productionSize.eq_3, holes.eq_3, List.length_flatten, List.map_map,
+      Function.comp_def]
+    have hs := List.map_congr_left ih
+    rw [hs, List.sum_map_add, List.sum_map_mul_right]
+    omega
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc
+    · exact hcs d hd
+
+/-- Terminal counts add once for each hole, regardless of its frontier position. -/
+theorem count_yield_plug [DecidableEq T] (E t : ParseTree T N) (a : T) :
+    (E.plug t).yield.count a = E.yield.count a + E.holes.length * t.yield.count a := by
+  induction E using ParseTree.rec (motive_2 := fun (cs : List (ParseTree T N)) =>
+    ∀ c ∈ cs, (c.plug t).yield.count a =
+      c.yield.count a + c.holes.length * t.yield.count a) with
+  | terminal b => simp [plug.eq_1, yield.eq_1, holes.eq_1]
+  | hole A => simp [plug.eq_2, yield.eq_2, holes.eq_2]
+  | node r cs ih =>
+    simp only [plug.eq_3, yield.eq_3, holes.eq_3, List.count_flatten, List.length_flatten,
+      List.map_map,
+      Function.comp_def]
+    have hs := List.map_congr_left ih
+    rw [hs, List.sum_map_add, List.sum_map_mul_right]
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc
+    · exact hcs d hd
+
+/-- Plugging adds the inserted support exactly when the context has a hole. -/
+theorem mem_support_plug (E t : ParseTree T N) (A : N) :
+    A ∈ (E.plug t).support ↔ A ∈ E.support ∨ (E.holes ≠ [] ∧ A ∈ t.support) := by
+  classical
+  induction E using ParseTree.rec (motive_2 := fun (cs : List (ParseTree T N)) =>
+    ∀ c ∈ cs, A ∈ (c.plug t).support ↔
+      A ∈ c.support ∨ (c.holes ≠ [] ∧ A ∈ t.support)) with
+  | terminal a => simp [plug.eq_1, support, productionLabels.eq_1, holes.eq_1]
+  | hole B => simp [plug.eq_2, support, productionLabels.eq_2, holes.eq_2]
+  | node r cs ih =>
+    have hholes : (node r cs).holes ≠ [] ↔ ∃ c ∈ cs, c.holes ≠ [] := by
+      simp only [holes.eq_3, ne_eq, List.flatten_eq_nil_iff, List.forall_mem_map]
+      push Not
+      rfl
+    have hlabels : ∀ c ∈ cs,
+        A ∈ (c.plug t).productionLabels ↔
+          A ∈ c.productionLabels ∨ (c.holes ≠ [] ∧ A ∈ t.productionLabels) := ih
+    simp only [plug.eq_3, support, productionLabels.eq_3, List.map_map, Set.mem_ofPred_eq,
+      List.mem_cons, ← List.flatMap_def, List.mem_flatMap, hholes]
+    aesop
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc
+    · exact hcs d hd
+end ParseTree
+
+end Parikh
diff --git a/LeanPool/Parikh/TreeReplacement.lean b/LeanPool/Parikh/TreeReplacement.lean
new file mode 100644
index 0000000000..6c32a963ac
--- /dev/null
+++ b/LeanPool/Parikh/TreeReplacement.lean
@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import LeanPool.Parikh.GrammarTrees
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Selecting and replacing a particular occurrence
+
+A nonterminal may occur many times in a tree. Support membership says that an
+occurrence exists; a position, given by child indices, selects which one.
+
+The results here connect these two views and extract the outer context around
+a selected subtree. Filling its hole recovers the original tree; filling it
+with a different matching subtree implements replacement. This lets later
+proofs reason about insertion locally while preserving the surrounding tree.
+
+Source: `lem:enabled`, `lem:insertion-laws`.
+-/
+namespace Parikh
+variable {T N : Type*}
+
+namespace ParseTree
+/-- A complete side branch is unchanged when another subtree fills holes. -/
+theorem plug_of_holes_eq_nil (E t : ParseTree T N) (hE : E.holes = []) :
+    E.plug t = E := by
+  induction E using ParseTree.rec (motive_2 := fun (cs : List (ParseTree T N)) =>
+    ∀ c ∈ cs, c.holes = [] → c.plug t = c) with
+  | terminal a => simp [plug]
+  | hole A => simp [holes] at hE
+  | node r cs ih =>
+    have hc : ∀ c ∈ cs, c.holes = [] := by
+      simpa only [holes, List.flatten_eq_nil_iff, List.forall_mem_map] using hE
+    simp only [plug]
+    congr 1
+    simpa using List.map_congr_left (fun c h => ih c h (hc c h))
+  | nil c hc => simp at hc
+  | cons c cs hc hcs d hd hh =>
+    rcases List.mem_cons.mp hd with rfl | hd
+    · exact hc hh
+    · exact hcs d hd hh
+end ParseTree
+
+/-- In a complete tree, support is exactly the labels of nonterminal-rooted subtrees. -/
+theorem Complete.mem_support_iff_subtree {g : ContextFreeGrammar T}
+    {t : ParseTree T g.NT} (ht : Complete g t) (A : g.NT) :
+    A ∈ t.support ↔ ∃ q u, t.subtree q = some u ∧ u.root = .nonterminal A := by
+  obtain ⟨hv, hh⟩ := ht
+  induction hv with
+  | terminal a =>
+    simp only [ParseTree.support, ParseTree.productionLabels, Set.mem_ofPred_eq,
+      List.not_mem_nil, false_iff]
+    rintro ⟨q, u, hq, hu⟩
+    cases q with
+    | nil => simp [ParseTree.subtree] at hq; subst u; simp [ParseTree.root] at hu
+    | cons i q => simp [ParseTree.subtree] at hq
+  | hole B => simp [ParseTree.holes] at hh
+  | node r cs hr hc roots ih =>
+    have hholes : ∀ c ∈ cs, c.holes = [] := by
+      simpa only [ParseTree.holes, List.flatten_eq_nil_iff, List.forall_mem_map] using hh
+    simp only [ParseTree.support, ParseTree.productionLabels, Set.mem_ofPred_eq,
+      List.mem_cons, ← List.flatMap_def, List.mem_flatMap]
+    constructor
+    · rintro (hA | ⟨c, hcmem, hA⟩)
+      · subst A
+        exact ⟨[], .node r cs, rfl, rfl⟩
+      · obtain ⟨q, u, hq, hu⟩ := (ih c hcmem (hholes c hcmem)).mp hA
+        obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp hcmem
+        exact ⟨i :: q, u, by simp [ParseTree.subtree, hi, hq], hu⟩
+    · rintro ⟨q, u, hq, hu⟩
+      cases q with
+      | nil =>
+        simp only [ParseTree.subtree, Option.some.injEq] at hq
+        subst u
+        exact Or.inl (by simpa only [ParseTree.root, Symbol.nonterminal.injEq] using hu.symm)
+      | cons i q =>
+        obtain ⟨c, hi, hq⟩ := Option.bind_eq_some_iff.mp hq
+        have hcmem := List.mem_of_getElem? hi
+        exact Or.inr ⟨c, hcmem, (ih c hcmem (hholes c hcmem)).mpr ⟨q, u, hq, hu⟩⟩
+
+/-- A selected nonterminal occurrence can be cut out and replaced through its
+outer one-hole context. The selected subtree and all side branches are complete. -/
+theorem Complete.subtree_context {g : ContextFreeGrammar T} {t : ParseTree T g.NT}
+    (ht : Complete g t) (q : List ℕ) (u : ParseTree T g.NT)
+    (hpos : t.subtree q = some u) (A : g.NT) (hu : u.root = .nonterminal A) :
+    Complete g u ∧ ∃ E, OneHole g E A ∧ E.root = t.root ∧ E.plug u = t ∧
+      ∀ v, t.replaceAt q v = some (E.plug v) := by
+  induction q generalizing t with
+  | nil =>
+    simp only [ParseTree.subtree, Option.some.injEq] at hpos
+    subst u
+    refine ⟨ht, .hole A, ⟨.hole A, by simp [ParseTree.holes]⟩, ?_, ?_, ?_⟩
+    · exact hu.symm
+    · simp [ParseTree.plug]
+    · intro v; simp [ParseTree.replaceAt, ParseTree.plug]
+  | cons i q ih =>
+    cases t with
+    | terminal a => simp [ParseTree.subtree] at hpos
+    | hole B => simp [ParseTree.subtree] at hpos
+    | node r cs =>
+      obtain ⟨c, hi, hpos⟩ := Option.bind_eq_some_iff.mp hpos
+      have hcmem := List.mem_of_getElem? hi
+      obtain ⟨hv, hh⟩ := ht
+      cases hv with
+      | node _ _ hr hc roots =>
+        have hholes : ∀ d ∈ cs, d.holes = [] := by
+          simpa only [ParseTree.holes, List.flatten_eq_nil_iff, List.forall_mem_map] using hh
+        obtain ⟨huc, E, hE, hroot, hplug, hreplace⟩ :=
+          ih ⟨hc c hcmem, hholes c hcmem⟩ hpos
+        obtain ⟨hlt, helem⟩ := List.getElem?_eq_some_iff.mp hi
+        have hset : cs.set i c = cs := by rw [← helem]; exact List.set_getElem_self hlt
+        have hmaps (v : ParseTree T g.NT) : cs.map (fun d => d.plug v) = cs := by
+          have hm : cs.map (fun d => d.plug v) = cs.map id :=
+            List.map_congr_left (fun d hd => d.plug_of_holes_eq_nil v (hholes d hd))
+          simpa using hm
+        refine ⟨huc, .node r (cs.set i E), ⟨?_, ?_⟩, rfl, ?_, ?_⟩
+        · refine Valid.node r _ hr ?_ ?_
+          · intro d hd
+            rcases List.mem_or_eq_of_mem_set hd with hd | rfl
+            · exact hc d hd
+            · exact hE.1
+          · rw [List.map_set, hroot, ← roots]
+            simpa only [List.map_set] using congrArg (List.map ParseTree.root) hset
+        · have hprefix : ((cs.take i).map ParseTree.holes).flatten = [] := by
+            simp only [List.flatten_eq_nil_iff, List.forall_mem_map]
+            intro d hd
+            exact hholes d (List.mem_of_mem_take hd)
+          have hsuffix : ((cs.drop (i + 1)).map ParseTree.holes).flatten = [] := by
+            simp only [List.flatten_eq_nil_iff, List.forall_mem_map]
+            intro d hd
+            exact hholes d (List.mem_of_mem_drop hd)
+          simp only [ParseTree.holes, List.set_eq_take_append_cons_drop, ite_eq_left hlt,
+            List.map_append, List.map_cons, List.flatten_append, List.flatten_cons,
+            hprefix, hsuffix, hE.2, List.nil_append, List.append_nil]
+        · simp only [ParseTree.plug, List.map_set, hmaps, hplug, hset]
+        · intro v
+          simp [ParseTree.replaceAt, hi, hreplace v, ParseTree.plug, List.map_set, hmaps]
+
+end Parikh
diff --git a/LeanPool/Parikh/WordBlockAutomata.lean b/LeanPool/Parikh/WordBlockAutomata.lean
new file mode 100644
index 0000000000..074b47e18a
--- /dev/null
+++ b/LeanPool/Parikh/WordBlockAutomata.lean
@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2026 Umang Mathur. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Umang Mathur
+-/
+
+module
+
+public import Mathlib.Computability.DFA
+import Mathlib.Computability.NFA
+import Mathlib.Data.Set.Finite.Range
+
+/-! Ported from focs-lab/parikh-theorem at
+`9c1cde93f29bbaa91542e401e074ec3cd7646880`; module headers and import paths
+adapted for Lean Pool. -/
+
+public section
+
+/-!
+# Automata for the words used in a linear component
+
+The converse construction needs languages consisting of fixed words followed
+by repetitions of other fixed words. We prove regularity of these particular
+operations using finite families of continuation languages.
+
+Think of a state as the language of suffixes still to be read. A finite family
+that covers every one-letter continuation supplies an NFA; its transition
+condition ensures soundness and the cover property ensures completeness.
+Mathlib's existing subset construction turns this NFA into a DFA.
+
+Fixed-word and starred-word prefixes are obtained by adding finitely many
+suffix states. These are classical existence proofs of automata, not an
+executable implementation of a grammar compiler.
+-/
+open scoped Computability
+
+namespace Parikh
+variable {T : Type*}
+
+/-- A finite family of languages covering every one-letter continuation gives
+a finite NFA. Transitions are sound language inclusions, and the cover hypothesis
+ensures completeness; determinization is Mathlib's existing construction. -/
+theorem isRegular_of_finite_language_cover (L : Language T)
+    (F : Set (Language T)) (hF : F.Finite) (hL : L ∈ F)
+    (hcover : ∀ K ∈ F, ∀ a w, a :: w ∈ K →
+      ∃ J ∈ F, w ∈ J ∧ ∀ v ∈ J, a :: v ∈ K) : L.IsRegular := by
+  classical
+  let : Fintype F := hF.fintype
+  let M : NFA T F :=
+    { step := fun K a => {J | ∀ v ∈ J.val, a :: v ∈ K.val}
+      start := {⟨L, hL⟩}
+      accept := {K | [] ∈ K.val} }
+  have hcons (K : F) (a : T) (w : List T) :
+      a :: w ∈ K.val ↔ ∃ J ∈ M.step K a, w ∈ J.val := by
+    constructor
+    · intro hw
+      obtain ⟨J, hJ, hw, hs⟩ := hcover K.val K.prop a w hw
+      exact ⟨⟨J, hJ⟩, hs, hw⟩
+    · rintro ⟨J, hs, hw⟩
+      exact hs w hw
+  have heval (w : List T) (S : Set F) :
+      (∃ K ∈ M.evalFrom S w, [] ∈ K.val) ↔ ∃ K ∈ S, w ∈ K.val := by
+    induction w generalizing S with
+    | nil => rfl
+    | cons a w ih =>
+      rw [NFA.evalFrom_cons, ih]
+      constructor
+      · rintro ⟨J, hJ, hw⟩
+        obtain ⟨K, hK, hs⟩ := NFA.mem_stepSet.mp hJ
+        exact ⟨K, hK, (hcons K a w).mpr ⟨J, hs, hw⟩⟩
+      · rintro ⟨K, hK, hw⟩
+        obtain ⟨J, hs, hw⟩ := (hcons K a w).mp hw
+        exact ⟨J, NFA.mem_stepSet.mpr ⟨K, hK, hs⟩, hw⟩
+  have hM : M.accepts = L := by
+    ext w
+    rw [NFA.mem_accepts]
+    change (∃ K, [] ∈ K.val ∧ K ∈ M.evalFrom {⟨L, hL⟩} w) ↔ w ∈ L
+    constructor
+    · rintro ⟨K, ha, hs⟩
+      obtain ⟨J, hJ, hw⟩ := (heval w {⟨L, hL⟩}).mp ⟨K, hs, ha⟩
+      have hJ : J = ⟨L, hL⟩ := Set.mem_singleton_iff.mp hJ
+      cases hJ
+      exact hw
+    · intro hw
+      obtain ⟨K, hs, ha⟩ := (heval w {⟨L, hL⟩}).mpr
+        ⟨⟨L, hL⟩, Set.mem_singleton _, hw⟩
+      exact ⟨K, ha, hs⟩
+  exact Language.isRegular_iff.mpr
+    ⟨Set F, inferInstance, M.toDFA, M.toDFA_correct.trans hM⟩
+
+/-- A one-state rejecting NFA suffices for the empty language. -/
+theorem isRegular_zero : (0 : Language T).IsRegular := by
+  apply isRegular_of_finite_language_cover _ {0} (Set.finite_singleton _) (by simp)
+  intro K hK a w hw
+  have hK : K = 0 := Set.mem_singleton_iff.mp hK
+  subst K
+  exact (Language.notMem_zero _ hw).elim
+
+/-- A one-state accepting NFA with no transitions recognizes epsilon. -/
+theorem isRegular_one : (1 : Language T).IsRegular := by
+  apply isRegular_of_finite_language_cover _ {1} (Set.finite_singleton _) (by simp)
+  intro K hK a w hw
+  have hK : K = 1 := Set.mem_singleton_iff.mp hK
+  subst K
+  simp only [Language.mem_one, List.cons_ne_nil] at hw
+
+/-- Reading the head of a literal prefix leaves its tail as the prefix. -/
+theorem mem_word_mul_cons (a b : T) (u x : List T) (L : Language T) :
+    a :: x ∈ ({b :: u} : Language T) * L ↔
+      a = b ∧ x ∈ ({u} : Language T) * L := by
+  simp only [Language.mem_mul]
+  change (∃ p, p = b :: u ∧ ∃ v ∈ L, p ++ v = a :: x) ↔
+    a = b ∧ ∃ p, p = u ∧ ∃ v ∈ L, p ++ v = x
+  simp only [exists_eq_left, List.cons_append, List.cons.injEq]
+  constructor
+  · rintro ⟨v, hv, hab, hx⟩
+    exact ⟨hab.symm, v, hv, hx⟩
+  · rintro ⟨hab, v, hv, hx⟩
+    exact ⟨v, hv, hab.symm, hx⟩
+
+/-- Prepending one fixed word preserves DFA regularity. The additional NFA
+states are the finitely many suffixes of that word. -/
+theorem isRegular_word_mul (w : List T) (R : Language T) (hR : R.IsRegular) :
+    (({w} : Language T) * R).IsRegular := by
+  classical
+  obtain ⟨σ, hσ, M, rfl⟩ := hR
+  let : Fintype σ := hσ
+  let F : Set (Language T) := Set.range M.acceptsFrom ∪
+    (fun u => ({u} : Language T) * M.accepts) '' (↑w.tails.toFinset : Set (List T))
+  have hF : F.Finite := (Set.finite_range M.acceptsFrom).union
+    (w.tails.toFinset.finite_toSet.image _)
+  have htail (u : List T) (hu : u <:+ w) : ({u} : Language T) * M.accepts ∈ F := by
+    exact Or.inr ⟨u, by simpa using (List.mem_tails u w).mpr hu, rfl⟩
+  have hdfa (s : σ) (a : T) (x : List T) (hx : a :: x ∈ M.acceptsFrom s) :
+      ∃ J ∈ F, x ∈ J ∧ ∀ v ∈ J, a :: v ∈ M.acceptsFrom s := by
+    refine ⟨M.acceptsFrom (M.step s a), Or.inl ⟨_, rfl⟩, ?_, ?_⟩
+    · simpa only [DFA.mem_acceptsFrom, DFA.evalFrom_cons] using hx
+    · intro v hv
+      simpa only [DFA.mem_acceptsFrom, DFA.evalFrom_cons] using hv
+  apply isRegular_of_finite_language_cover _ F hF (htail w (List.suffix_refl _))
+  intro K hK a x hx
+  rcases hK with hK | hK
+  · obtain ⟨s, rfl⟩ := hK
+    exact hdfa s a x hx
+  · obtain ⟨u, hu, rfl⟩ := hK
+    have hu : u <:+ w := (List.mem_tails u w).mp (by simpa using hu)
+    cases u with
+    | nil =>
+      change a :: x ∈ (1 : Language T) * M.accepts at hx
+      rw [one_mul] at hx
+      simpa only [show ({[]} : Language T) = 1 from rfl, one_mul, DFA.accepts] using
+        hdfa M.start a x hx
+    | cons b u =>
+      obtain ⟨hab, hrest⟩ := (mem_word_mul_cons a b u x M.accepts).mp hx
+      subst b
+      refine ⟨({u} : Language T) * M.accepts,
+        htail u ((List.suffix_cons a u).trans hu), hrest, ?_⟩
+      intro v hv
+      exact (mem_word_mul_cons a a u v M.accepts).mpr ⟨rfl, hv⟩
+
+/-- Prepending any number of copies of one fixed word preserves DFA regularity.
+Suffix states return to the same starred prefix; transitions may also enter the
+continuation DFA. The empty repeated word is handled without epsilon loops. -/
+theorem isRegular_word_star_mul (w : List T) (R : Language T) (hR : R.IsRegular) :
+    (({w} : Language T)∗ * R).IsRegular := by
+  classical
+  cases w with
+  | nil =>
+    simpa only [show ({[]} : Language T) = 1 from rfl, kstar_one, one_mul] using hR
+  | cons b bs =>
+    obtain ⟨σ, hσ, M, rfl⟩ := hR
+    let : Fintype σ := hσ
+    let S : Language T := ({b :: bs} : Language T)∗ * M.accepts
+    let F : Set (Language T) := Set.range M.acceptsFrom ∪
+      (fun u => ({u} : Language T) * S) '' (↑(b :: bs).tails.toFinset : Set (List T))
+    have hF : F.Finite := (Set.finite_range M.acceptsFrom).union
+      ((b :: bs).tails.toFinset.finite_toSet.image _)
+    have htail (u : List T) (hu : u <:+ b :: bs) : ({u} : Language T) * S ∈ F := by
+      exact Or.inr ⟨u, by simpa using (List.mem_tails u (b :: bs)).mpr hu, rfl⟩
+    have hdfa (s : σ) (a : T) (x : List T) (hx : a :: x ∈ M.acceptsFrom s) :
+        ∃ J ∈ F, x ∈ J ∧ ∀ v ∈ J, a :: v ∈ M.acceptsFrom s := by
+      refine ⟨M.acceptsFrom (M.step s a), Or.inl ⟨_, rfl⟩, ?_, ?_⟩
+      · simpa only [DFA.mem_acceptsFrom, DFA.evalFrom_cons] using hx
+      · intro v hv
+        simpa only [DFA.mem_acceptsFrom, DFA.evalFrom_cons] using hv
+    have hunfold : S = M.accepts + ({b :: bs} : Language T) * S := by
+      dsimp [S]
+      conv_lhs => rw [← Language.one_add_self_mul_kstar_eq_kstar ({b :: bs} : Language T)]
+      rw [add_mul, one_mul, mul_assoc]
+    have hstart : S ∈ F := by
+      simpa only [show ({[]} : Language T) = 1 from rfl, one_mul] using
+        htail [] List.nil_suffix
+    apply isRegular_of_finite_language_cover S F hF hstart
+    intro K hK a x hx
+    rcases hK with hK | hK
+    · obtain ⟨s, rfl⟩ := hK
+      exact hdfa s a x hx
+    · obtain ⟨u, hu, rfl⟩ := hK
+      have hu : u <:+ b :: bs := (List.mem_tails u (b :: bs)).mp (by simpa using hu)
+      cases u with
+      | nil =>
+        change a :: x ∈ (1 : Language T) * S at hx
+        rw [one_mul, hunfold, Language.mem_add] at hx
+        change ∃ J ∈ F, x ∈ J ∧ ∀ v ∈ J, a :: v ∈ (1 : Language T) * S
+        simp only [one_mul]
+        rcases hx with hx | hx
+        · obtain ⟨J, hJ, hx, hs⟩ := hdfa M.start a x hx
+          refine ⟨J, hJ, hx, ?_⟩
+          intro v hv
+          rw [hunfold, Language.mem_add]
+          exact Or.inl (hs v hv)
+        · obtain ⟨hab, hrest⟩ := (mem_word_mul_cons a b bs x S).mp hx
+          subst b
+          refine ⟨({bs} : Language T) * S, htail bs (List.suffix_cons a bs), hrest, ?_⟩
+          intro v hv
+          rw [hunfold, Language.mem_add]
+          exact Or.inr ((mem_word_mul_cons a a bs v S).mpr ⟨rfl, hv⟩)
+      | cons c u =>
+        obtain ⟨hac, hrest⟩ := (mem_word_mul_cons a c u x S).mp hx
+        subst c
+        refine ⟨({u} : Language T) * S,
+          htail u ((List.suffix_cons a u).trans hu), hrest, ?_⟩
+        intro v hv
+        exact (mem_word_mul_cons a a u v S).mpr ⟨rfl, hv⟩
+
+end Parikh
diff --git a/LeanPool/projects/parikh.yaml b/LeanPool/projects/parikh.yaml
new file mode 100644
index 0000000000..a4a01943ee
--- /dev/null
+++ b/LeanPool/projects/parikh.yaml
@@ -0,0 +1,68 @@
+slug: parikh
+title: Parikh's theorem and a certified semilinear grammar compiler
+summary: >-
+  Proves that the letter-count image of every context-free language over a finite
+  alphabet is semilinear, using Mathlib's language, grammar and semilinear-set
+  definitions. Proves the converse realization by a regular language and computes
+  exact finite semilinear representations for encoded finite grammars, with
+  component, period, coordinate and bit-budget bounds. Preserves production-labelled
+  derivation trees, bounded decomposition, context activation and word-block automata.
+  The language theorem does not require a finite ambient nonterminal type.
+branch: formal language theory
+entry_module: LeanPool.Parikh
+authors:
+- Umang Mathur
+source:
+  title: On Context-Free Languages
+  authors:
+  - Rohit J. Parikh
+  doi: 10.1145/321356.321364
+  url: https://github.com/focs-lab/parikh-theorem/tree/9c1cde93f29bbaa91542e401e074ec3cd7646880
+  github_repo: focs-lab/parikh-theorem
+  commit: 9c1cde93f29bbaa91542e401e074ec3cd7646880
+  announcement_url: https://github.com/focs-lab/parikh-theorem/releases/tag/v0.1.0
+  announcement_date: '2026-10-12'
+  proof_references:
+  - title: Simple proof of Parikh's theorem a la Takahashi
+    authors:
+    - Ryoma Sin'ya
+    arxiv: '1909.09393'
+  - title: The Simplest Proof of Parikh's Theorem via Derivation Trees
+    authors:
+    - Alexander Rubtsov
+    arxiv: '2301.00047'
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+- Parikh.parikhImage_isSemilinear_of_isContextFree
+main_results:
+- declaration: Parikh.parikhImage_isSemilinear_of_isContextFree
+  informal: >-
+    For every context-free language over a finite alphabet, its set of letter-count
+    vectors is semilinear in Mathlib's sense.
+- declaration: Parikh.exists_regularLanguage_with_parikhImage
+  informal: >-
+    Every semilinear set of natural-number vectors indexed by a finite alphabet is
+    exactly the letter-count image of some regular language.
+- declaration: Parikh.compileGrammar_correct
+  informal: >-
+    For every encoded finite grammar, the compiled finite representation denotes
+    exactly the letter-count image of its decoded Mathlib grammar language.
+- declaration: Parikh.compileGrammar_size_bounds
+  informal: >-
+    The compiled representation satisfies the explicit component-count, period-count,
+    base-norm and period-norm bounds determined by the encoded grammar's size.
+- declaration: Parikh.compileGrammar_bit_bound
+  informal: >-
+    The compiled representation's numerical entries satisfy the declared total bit
+    budget, and every base and period coordinate fits its coordinate bit width.
+tags:
+- formal-languages
+- context-free-grammars
+- semilinear-sets
+- verified-algorithms
+msc:
+- 68Q45
+- 68Q42
+- 03D05