linter.fugue.comments

The mechanically-checkable half of INSTRUCTIONS.md §Comments, in one pass over each command's source span (leading trivia, doc comment, and inline -- notes included):

• commented-out code — a -- line that is really a pasted declaration / directive / proof;
• plan reference — PLAN.md, OPEN_QUESTIONS.md, .claude/, §N;
• paper citation — arXiv, reference/*.pdf, [HFP, Specifying Systems, Definition N.N;
• prior-art comparison — "prior art", "distpcal-compiler", "earlier design", "once already";
• line-numbered cross-reference — Foo.lean:123;
• bare separator — a comment that is only dashes;
• subjectless TODO — a TODO not written TODO(subject):;
• expiring URL — a signed githubusercontent.com link;
• long module doc — a /-! … -/ over 25 lines is a design essay;
• status prose — "still owed", "not yet", "for now": a docstring reads as if the current state always was the state.

The judgment half — proof narration, consumer notes, a weak docstring — stays a reader's call.