refactor(opening): extract family cardinality bound

[windsornguyen]

Explain what this changes, why it is needed, and anything reviewers should
verify. Link an issue when one exists.

What does this change?

Extracts the affine proof's generic pigeonhole lemma: a decoder covering an injectively indexed canonical family needs at least one message per family member. The affine lower bound now composes this theorem, leaving future research to prove the concrete family's injectivity and coverage.

How was it tested?

• lake build --wfail passes on stacked tip 16b7318
• lake lint passes on stacked tip 16b7318
• No sorry or new axioms, or this PR does not change Lean proofs
• git diff --check passes
• The refactored affine theorem and strict documentation build pass