Severity: error blocks a clean ledger; warn is advisory; info is reported.
These checks are mechanical: they establish that labels resolve to declarations of a
compatible kind, not that a declaration states the theorem it is aligned to. For that
gap see skills/faithfulness-audit/, an adversarial audit run outside span.
| id | sev | rule |
|---|---|---|
| C1 | error | Every paper object resolves to exactly one id; ids are unique within each paper summand. |
| C2 | error | Every ledger Lean ref resolves to a Lean node id; otherwise the entry is mismatch (dangling ref). |
| C3 | warn | Paper kind is compatible with at least one referenced Lean node kind (compat table); else mismatch. |
| C4 | warn/info | A stated result SHOULD sit in an amsthm environment with a \label; inline labels are allowed for in-proof construction objects. If a labeled environment's label prefix names a different kind (for example thm: inside lemma), warn. |
| C5 | warn | No two paper objects should have near-identical statements. |
| C6 | info | Every Lean node SHOULD be referenced by some paper object; unreferenced means lean_half and is reported, not treated as an error. |
| C7 | info | For a coherent entry, if all referenced Lean nodes are leanok mark fully_formalized; surface stated-but-not-proved. |
| C8 | error | The paper compiles under pdflatex when --latex is requested. |
| C10 | info | If paper kind and lean kind differ but are compatible, record a note, not an incoherence. |
| C12 | warn/info | The paper's statement order is a linear extension of native Lean statement-dependency edges lifted through the ledger. A statement-level back-edge, or an unavailable Lean dependency query, is a warning; a proof-only LaTeX reference back-edge is informational. |
| C13 | error | With --decls, named Lean declarations exist in source and have compatible declaration forms. |
| C15 | error | Multi-source references are unambiguous, or explicitly qualified by source. |
theorem ~ {theorem, lemma, proposition, corollary, claim}
lemma ~ {lemma, theorem, proposition, corollary, claim}
proposition ~ {proposition, lemma, theorem, claim}
corollary ~ {corollary, lemma, theorem, claim}
definition ~ {definition, notation, convention}
constant ~ {definition}
remark ~ {remark, definition, convention, notation}
example ~ {example, definition, theorem, lemma, proposition}
notation ~ {notation, definition}
convention ~ {convention, definition, notation}
assumption ~ {assumption, axiom, definition}
axiom ~ {axiom, assumption}
claim ~ {claim, lemma, theorem, proposition, corollary}
conjecture ~ {conjecture, theorem, lemma, proposition}