Self-contained document for LLM agents to close the 6 remaining
bridge sorries. Covers:
- Theorem statement and definitions
- Proof architecture (3 verified kernels + 6 bridge sorries)
- What each sorry needs and the proof strategy
- The key insight (zero/non-zero pattern only)
- The blocker (simp can't reduce List operations on 8 elements)
- Possible solutions and file context
