{0ⁿ1ⁿ2ᵐ3ᵐ} is not linear

The linear pumping lemma confines the pumped pieces to the two ends of the witness {0ⁿ1ⁿ2ᵐ3ᵐ}, so pumping breaks one of the two independent aⁿbⁿ matchings (L4_not_is_Linear). The relabelled version Lwit_not_is_Linear follows because linearity reflects along injective terminal maps.

theorem L4_not_is_Linear : ¬is_Linear L4

{0ⁿ1ⁿ2ᵐ3ᵐ} is not linear.

theorem Lwit_not_is_Linear {T : Type} (e : Fin 4 ↪ T) : ¬is_Linear ((Language.map ⇑e) L4)

The relabelled witness is not linear: linearity would reflect back to L4.