Guidance at the claim's grain

Claim: a verdict, an error or a hint names the person's claim, not the checker's internal step.

• Grade: supported with caveat: messages at the checker's grain stopped students; convention, untested for the grain itself.
• Evidence: Guo 2026b, sections 7.2.2 and 8.3.1; Carl 2022, section 5; position, condition 3.
• Check: lean-link (exact): a failing declaration maps to one claim topic; topic (exact): each claim is listed by its parent; whether a message helps the person is judgment, measured on what the person does next.
• Reader styles: none.

What it asks

• Report each failure against the claim topic that names the declaration.
• Give the claim's title and link, not only the checker's goal.

Why

• A message in the checker's words sends the person to a place they did not write.
• One declaration per claim lets a program turn the checker's name into the person's claim.

Limits

• No study measured whether a proof assistant's messages help any user.
• Guidance from the loop is not built yet; this rule fixes where it will speak.