Lean 4 lint: '#lint in Ns' can silently check 0 declarations

Running '#lint in Selberg' from a scratch file that imports the project modules reported 'Found 0 errors in 0 declarations' and 'All linting checks passed', even though the namespace had dozens of theorems. The '0 declarations' count is the signal that nothing was actually checked. Don't read 'passed' as success when the count is 0. A cheap fallback for missing docstrings is an awk pass over the source that flags theorem/lemma/def lines whose previous non-blank line does not end with '-/'. That found 7 undocumented helper lemmas the linter had skipped.