audit(erdos-162): realign stale section line ranges + tighten function-f summary

[rjwalters]

Summary

Gallery integrity audit of erdos-162 found:

• Section line ranges all stale: The six per-section ranges in meta.json (e.g. colouring 32-75, function-f 76-103, examples 150-186) no longer match where the content lives. The file was expanded to 237 lines but the section ranges were never updated, so they point into the middle of unrelated proofs.
• function-f section summary overclaimed: It said discrepancyF is axiomatized "with characterization spec, monotonicity in α, F(n,0)=n, and F(n,α) ≤ n", but only discrepancyF and discrepancyF_mono_alpha are axiomatized in that section. The "characterization spec", "F(n,0)=n", and "F(n,α) ≤ n" appear only as docstring comments at lines 147-156.

Core integrity confirmed

Counted directly from proofs/Proofs/Erdos162Problem.lean:

• 0 sorries ✓ matches sorries: 0
• 4 axioms ✓ matches axiomCount: 4 (discrepancyF, discrepancyF_mono_alpha, discrepancy_lower, discrepancy_upper)
• 4 theorems ✓ matches theoremCount: 4 (colourEdgeCount_total, balanced_requires_le_half, discrepancy_theta_log, half_is_extremal)
• 5 definitions ✓ matches definitionCount: 5 (1 structure + 1 noncomputable def + 3 defs)
• 237 lines ✓ matches lineCount: 237
• No True stubs, no Mathlib-wrapper masking — this is a properly axiomatized open conjecture with status: "axiomatized" and badge: "axiom", which is correct.

Changes

• src/data/proofs/erdos-162/meta.json: realigned all six section startLine/endLine fields and tightened the function-f section summary.
• src/data/proofs/audit-tracker.json: updated by claim-target.sh complete erdos-162 issues-fixed.

Test plan

• Re-counted sorries, axioms, theorems, defs, structures, and lines against current Lean file
• Verified each section's revised range covers the declarations its summary names
• Confirmed status/badge match assumption profile
• (No build needed — metadata-only change)

🤖 Generated with Claude Code