audit(erdos-162): cycle 4 issues-found — section line ranges stale (#21485)

[rjwalters]

Summary

• Cycle 4 audit of erdos-162 (Discrepancy in 2-Coloured Complete Graphs)
• All numeric integrity checks pass (sorries=0, axioms=4, theorems=4, defs=5, lines=237)
• Section line ranges in meta.json are stale — filed as Gallery integrity: erdos-162 section line ranges stale (point inside theorem proofs) #21485 for fix

Audit findings

Pass:

• Sorries: 0 (matches meta.json)
• Axioms: 4 declared, matches axiomCount
• Theorems: 4, Definitions: 4 + 1 structure = 5 (matches definitionCount)
• lineCount: 237 matches actual file
• status: axiomatized + badge: axiom correct for the 4 open-conjecture axioms
• erdosProblemStatus: open accurate

Issue (filed):

• Per-section startLine/endLine ranges span 32-186 but the actual section content lives at 34-213. All six sections' boundaries land inside earlier theorem proof bodies. See Gallery integrity: erdos-162 section line ranges stale (point inside theorem proofs) #21485 for recommended realignment table.

Test plan

• grep -c "sorry" returns 0
• grep -c "^axiom " returns 4
• No True stub theorems
• Audit tracker updated to cycle 4 with issues-found result and Gallery integrity: erdos-162 section line ranges stale (point inside theorem proofs) #21485 reference

🤖 Generated with Claude Code