section 6 and 7

[Ferinko]

• refine probability notation
• abstract over shiftspan
• restate average_proximity_implies_proximity_of_linear_subspace

[github-actions]

🤖 Gemini PR Summary

Error generating summary:
No API_KEY or ADC found. Please either:
- Set the GOOGLE_API_KEY environment variable.
- Manually pass the key with genai.configure(api_key=my_api_key).
- Or set up Application Default Credentials, see https://ai.google.dev/gemini-api/docs/oauth for more information.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	18
❌ Lines Removed	18

---

sorry Tracking

• ✅ Removed: 1 sorry(s)
  • theorem average_proximity_implies_proximity_of_linear_subspace [DecidableEq ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap.lean

---

Last updated: 2025-11-17 12:09 UTC. See the main CI run for build status.