locus: Blueprint

1.1. How to read the statements🔗

Every PROVED or REFUTED statement is attached to the Lean declaration that carries it; each statement has one of three verdicts.

  • PROVED: sorry-free in Lean with a pinned axiom set. By default the only axioms are propext and Quot.sound; a result that uses Classical.choice is marked CLASSICAL. PROVED is the default and is not written.

  • REFUTED: there is a kernel-checked countermodel, and the countermodel theorem is the declaration attached.

  • OPEN: neither. An open statement carries no Lean declaration.

Some results are marked TESTED: they are checked by compiled code, not by the kernel.

Each definition also carries the class of its notion (from its source, bridged to it, unbridged, or new): the classes are set out at the head of the Notation chapter.