Audit: Grand Challenge prize resolution formalizes collapsed predicates, not external conjectures

[awidearray]

Summary

Production-readiness / LARP audit found that Grand Challenge "prize resolution" modules prove formalized collapsed predicates (notably F6 in GrandChallengeCollapse.lean), not the external million-dollar proximity-prize conjectures referenced in issues #138–#141.

Evidence

• GrandChallengePrizeResolution.lean and GrandChallengesLattice/PrizeResolution.lean chain through collapsed prize specs
• Open surfaces remain as named Props: mcaConjecture, epsMCAgsPrizeUniformConjecture (Coding theory basic proofs #141 disposition doc)
• sorry_census.py --fail-on-holes reports 0 live holes — the gap is mathematical scope honesty, not missing sorry

Risk

Consumers may interpret _proven / "prize resolved" naming as closure of external conjectures rather than internal predicate plumbing.

Partial remediation (PR linked separately)

• Module docs clarified in GrandChallengePrizeResolution.lean
• Lambda_reedSolomon_prizeRate_capacity_residual renamed to Lambda_reedSolomon_prizeRate_capacity_of with deprecated alias

Still open

Issues #138, #139, #140, #141 require research-grade mathematics or mathlib upstreaming — not closeable via formalization glue alone.

[awidearray]

Partial remediation in PR #554 (docs/naming) and PR #555 (PrizeResolution capacity lemma rename).

[awidearray]

Closing: audit tracking moved to awidearray/ArkLib fork only. See https://github.com/awidearray/ArkLib