Style: lemma for steps, theorem for main results #18

Context

Every statement in the library (and downstream) is declared with theorem: paper results, main results listed in module docs, and small steps of a proof alike. A reader scanning a file cannot tell the results that matter from the scaffolding.

Mathlib provides lemma (Mathlib.Tactic.Lemma), which elaborates exactly like theorem; the keyword is documentation only.

Proposal

• theorem for the results a reader comes for: statements of a source result (their docstring cites it, e.g. [1, Lemma 4.16]), and the few headline results of a module that have no source.
• lemma for everything else: steps, helpers, rewriting lemmas, typed corollaries, even when a module doc lists them.
• Apply it module by module as files are touched (for example along the PR stack of Upstream candidates from downstream projects: a layer-by-layer PR stack #14), and in the downstream projects.

No statement or proof changes; #print axioms and the build are unaffected.

Status

Applied to the proof ladders (2026-10-06): 66 declarations stay theorem (the cited source results plus four headline results), 736 become lemma; the build is unchanged.