8. Comparator review of the Challenge statements🔗

This chapter is generated by OperatorRidgeletBlueprint/scripts/gen-comparator-chapter.py from comparator/paper.json, comparator/config.json, and the Challenge sources of the OperatorRidgelet project; it is regenerated on every build of the site and is never edited by hand. It exists so that the formal statements can be reviewed against the manuscript without leaving the Blueprint: for every manuscript item it shows, in manuscript order, the statement of each of its Lean declarations exactly as it stands in Challenge, a link to the Blueprint node that carries the informal statement, the modelling note of the manuscript index, and the comparator status of each declaration.

The comparator scheme. Every theorem, proposition, lemma, corollary, and example of the manuscript is a theorem OperatorRidgelet.Paper.<kind>_<label>[_<part>] (multi-part results are split per part), stated twice with identical text: in the Challenge library with proof sorry, and in OperatorRidgelet.Paper, imported by Solution, with the real proof. Challenge imports only the sorry-free definition modules of the library, never OperatorRidgelet.Paper, so the same names can be proved in Solution. The file comparator/config.json lists under theorem_names the declarations whose proofs are complete, and scripts/comparator-check.sh runs comparator on the two libraries. A declaration in that list is verified: comparator has checked that the Solution statement is identical to the Challenge statement, that the proof contains no sorry, that it depends on no axioms other than propext, Quot.sound, and Classical.choice, and it has replayed the proof through the Lean kernel. Definitions are not verified by comparator; they are part of the trusted statement and are reviewed through the Lean panel of the Blueprint node.

How to review an item. Read the informal statement in the Blueprint node (the link at the top of each item), then the Lean statement in the code block, which is the Challenge declaration with its docstring, copied verbatim with only the sorry line removed, and check that the two say the same thing; the note records how the manuscript's objects are encoded. The Blueprint node's Lean panel shows the same declaration as elaborated in OperatorRidgelet.Paper, with hover information and the proof status read from the code. A declaration marked verified by comparator is settled; one marked statement only is formalized but its proof is pending.