lean-bridge: paper proposition ↔ Lean theorem

Scope: what to formalise

Formalise the finite algebraic core: identities, support and character arguments, counting bounds, injectivity and admissibility conditions, cost-ratio identities and limits. Do not try to formalise lattice hardness, concrete noise distributions or performance.

If a quantity is only modelled, say so in the table and in the paper. An example is a noise bound taken as a definition rather than derived from ciphertext semantics. The paper may then claim only "operation/level counts are machine-checked relative to the model". It may not claim "noise growth is machine-checked".

Procedure

1. Start from lib/lean-template/. Copy it and keep lean-toolchain and the Mathlib rev in sync.
2. Run a numeric check first (skills/sage-check). Never start formalising a statement that has not survived toy parameters.
3. For each proposition, write the Lean statement first, with the proof as a placeholder on a WIP branch. Get the statement reviewed against the paper text. Most mismatches are in the statement, not the proof. Common ones: the Lean version is weaker, uses ℕ where the paper needs ℤ, or adds a hypothesis the paper omits.
4. Prove it. Useful tactics: decide for tiny concrete finite facts; ring, field_simp, linear_combination for identities; omega for linear ℕ/ℤ arithmetic; norm_num, simp for evaluation. Avoid native_decide.

5. Fill in the table, which is kept in the Lean project README and mirrored in THEORY.md:

   paper statement	Lean name (fully qualified)	file	modelling notes
   Lemma 3.2 (support stability)	Proj.Support.stable	Support.lean	coefficient level

6. Gate (all must pass before the table is cited in the paper):
   • lake build is green on a clean checkout at the recorded commit;
   • scripts_check_no_sorry.sh reports no sorry/admit/axiom/native_decide;
   • an axiom audit of every headline theorem (#print axioms T or lean_verify) shows only propext, Classical.choice, Quot.sound;
   • the table rows match the paper numbering on the final PDF.
7. Record the Lean commit and the "green build" log in EVIDENCE.md, for example "N results, zero sorry" as the printed fact and the lake build log as its source.

Lessons

• Lean often finds redundant or insufficient hypotheses. Run lean_minimal_hypotheses on key theorems. Sometimes a hypothesis the paper states is not needed, which gives a stronger theorem. Sometimes the Lean proof needs one the paper forgot, which is a correctness fix. Report both to theorist and falsifier.
• Formalising the coefficient-level statement is usually much easier than the polynomial-ring statement. Prove a bridge lemma (for example, the coefficient of P.comp (C a * X)) once and reuse it.
• Keep each file under a few hundred lines, with one namespace per paper section.
• A cost-ratio "→ 2 as d → ∞" claim can be formalised with Filter.Tendsto. Pair it with an explicit finite bound, because reviewers care about concrete sizes.

Mathlib cache pitfalls

See lib/lean-template/README.md. In short: match the toolchain and the Mathlib rev; run lake exe cache get after every lake update; never import Mathlib in project files; allow minutes for the first cold import; look up renamed lemmas with search tools, not from memory.

lean-lsp MCP tools (if configured)