Supplementary files for "Four diagonals suffice: completeness of Parikh matrices when letters
occur at most twice" by Christopher Yamba. Copyright (c) 2026 Christopher Yamba. All rights
reserved.

ParikhCompleteness.lean, lakefile.toml, lean-toolchain
    The Lean 4 formalisation (Lean 4.34.0, core library only). Build with "lake build" in a
    directory containing these three files. Main theorems: rectangle (Lemma 3.1),
    crossing_formula (Theorem 4.2(iii)), complete_two (Theorem A), determined_by_short
    (Corollary 1.1), sharp_fourth_diagonal (Example 4.5), family_three and family_four
    (Theorem B for n = 3, 4).

check_article3.py
    Standard-library Python 3 checks of every numerical statement (Section 7). Run
    "python3 check_article3.py" (about 4 minutes) or with "--full".

corner.c
    Exact test of corner independence for a window content, used for the larger entries of
    Table 1. Compile with "cc -O2 -o corner corner.c" and run "./corner c1 c2 ... cr".
