2.1. Classes of definitions🔗

Each definition in this blueprint, and each row of the tables below, carries the class of the notion it defines, from an audit of the Lean definitions against their sources.

• FROM SOURCE: the Lean definition is the source's, clause by clause (or, where the audit says so, a standard textbook definition).

• BRIDGED: a different definition, with a proved theorem relating it to the source's or the library's notion.

• UNBRIDGED: it carries a source's or the library's name or symbol, and no theorem relates it to that notion.

• NEW: a notion of this project, with no source.

• Not audited: the audit has no entry for it.

A definition that gathers several declarations shows every class present and says which declaration has which; one declaration can carry two classes where the audit splits its verdict. Classes belong to notions: a theorem has a verdict (PROVED, REFUTED), not a class.

A theorem's statement is only as close to its source as the notions it is about. So a theorem ends with a line "Rests on", listing the notions its statement reaches that are UNBRIDGED, NEW or not audited. The line is computed from the Lean statement, never from the proof: starting from the constants in the types of the declarations attached to the theorem, each definition is opened in turn until a notion with a class is reached, and that notion is recorded and not opened further. One exception: when a theorem's statement is given by a named proposition that only abbreviates it (cocc_G1 : COccG1 …), that proposition is opened too, since it is the statement and not a notion; relations such as bisimilarity are notions and stay closed. A notion without a class is listed as not audited when the statement itself names it; long lists are cut at eight names. A theorem with no such line reaches only notions that are FROM SOURCE or BRIDGED.