binding standards live in `AGENTS.md`

One document, read by agents and humans alike, replacing a separate conventions file: agent tooling reads that filename automatically, so every dispatched round inherits the standards without its prompt restating them. The reader-facing rules became the opening section of CONTRIBUTING.md rather than a separate document.

Twelve standards, of which six are machine-enforced by the CI gates and the rest are review matters; AGENTS.md §13 says which is which, so nobody mistakes a norm for a gate. The standards: exact arithmetic; what a theorem ships as; runners; frozen inputs immutable; citation integrity; naming reserved to the author; dispatch provenance; and the Lean discipline — sorry-free, #print axioms per file, results auditing to [propext, Classical.choice, Quot.sound], and external theory entering only as named hypotheses rather than as axioms.