Function proof_mode_issues 

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

Strict proof-mode gate for Lean transpilation.

Returns human-readable blockers that would force generated Lean to rely on non-proof recursion fallback (partial).