sage-check: test every lemma on small cases first

Why

Proving a false lemma wastes days, and formalising one in Lean wastes weeks. Most wrong statements fail on a toy instance: a small prime, a small ring dimension, a 2×2 case. Run a finite check before proving and before formalising.

Protocol

1. Transcribe the statement exactly as in THEORY.md. Include every quantifier and side condition. Each checked statement gets an ID matching THEORY.md / CLAIMS.md.
2. Choose a parameter grid.
   • Include every smallest case (p ∈ {2, 3, 5, 7, 11, 13}, n ∈ {1, 2, 4, 8}).
   • Cover both residue classes the statement distinguishes (for example p ≡ 1 and p ≡ 3 mod 4).
   • Include the boundary of any inequality hypothesis, on both sides.
   • Include at least one parameter as large as the experiments use, if it is feasible.
3. Test the hypotheses too. Check that the hypotheses are satisfiable on the grid, because a vacuous theorem "passes" every check. Then check the conclusion.
4. Search exhaustively wherever the space is finite and small (≤ 10⁷ cases). Otherwise use random sampling with a fixed seed, and report the seed and the sample size.
5. Also test the converse. If a condition is claimed to be necessary and sufficient, test both directions separately.
6. Use exact arithmetic: ZMod/GF, Integer, QQ, sympy.Rational. Use no floats unless the statement is about floats. For asymptotic claims, check the exact finite formula on a range and fit the trend; do not trust a plotted curve.
7. Output one JSON line per check: {"check": ID, "params": {...}, "cases": N, "passed": bool, "counterexample": {...} | null}. Save the script under checks/ and the output under results/checks/, then add an EVIDENCE row if any number from it reaches the paper.
8. If a check fails, give the minimal counterexample (smallest parameters) to falsifier and theorist. Do not patch the statement silently.

Script template

scripts/sanity_check_template.py is a runnable skeleton with a guarded Sage import, a check(...) helper that stops at the first counterexample, and a toy statement about roots of unity mod p. Copy it, then replace the STATEMENTS list.

python3 skills/sage-check/scripts/sanity_check_template.py          # pure Python
sage -python skills/sage-check/scripts/sanity_check_template.py     # uses Sage if present

Typical checks by area

Tooling notes

• In Sage, GF(p), Zmod(n), CyclotomicField(m) and cyclotomic_polynomial(m) cover most checks. Run with sage -python script.py so the same file stays importable as plain Python.
• In pure Python, sympy (cyclotomic_poly, factor_list(..., modulus=p), n_order, primitive_root) and pow(a, -1, p) are enough for most toy checks.
• Mathematica, if connected, is useful for closed forms and series. Treat its output as a hint, then recheck with exact finite computation.