Function proof_mode_issues 

pub fn proof_mode_issues(ctx: &CodegenContext) -> Vec<String>

Proof-mode diagnostics for Lean transpilation.

Returns human-readable notices for recursive shapes that still fall back to regular partial Lean defs instead of total proof-mode emission.