Line-anchor the remaining proof escape-hatch findings (oops, Admitted, postulate, believe_me, …) #280

What

#278 makes Lean and Isabelle sorry findings one per occurrence with a line, so an inline panic-attack: accepted marker can suppress exactly one audited occurrence. Every other proof escape-hatch detector still emits a single finding per file with a count and line: None, for example:

• Isabelle oops;
• Coq/Rocq Admitted and admit;
• Agda postulate;
• Idris believe_me and assert_total;
• Lean unsafeNativeIO.

Those findings can't take an inline marker. The only remaining route is the retired A2ML classification registry, which matches a whole file and category.

How

#278 added the pieces:

• occurrence_lines(code, needle);
• position-preserving strip_proof_comments and strip_isabelle_prose;
• a proptest that stripping preserves every newline.

Each remaining detector needs its own check that the text it counts is still position-preserving. Some go through other strippers or the Rocq Section-aware counter, count_rocq_unverified_postulates.

Acceptance criteria

• Each proof escape-hatch detector emits one line-anchored finding per occurrence.
• Every stripper on those paths is covered by the newline-preservation property test.
• One end-to-end test per language: a marked occurrence is suppressed and an unmarked one in the same file is not.