refactor(opening): extract family cardinality bound

ComplexityTheory/ProofComplexity/CanonicalOpening/AffineBinding/Cardinality.lean

@@ -20,10 +20,39 @@ supplies additional binding information.
 
 namespace ComplexityTheory
 namespace CanonicalOpening
-namespace AffineBinding
 
 open scoped BigOperators
 
+/--
+Any deterministic decoder covering an injectively indexed family of canonical
+words needs at least one distinct message per family member.
+
+Informally, two different family members cannot share a message: decoding that
+message would make their canonical words equal. Applying this theorem to a
+research-specific family requires separate proofs that its canonical words are
+distinct and that the decoder represents every member.
+-/
+theorem messageCardinality_ge_injectiveCanonicalFamily
+    {Family Message Word : Type} [Fintype Family] [Fintype Message]
+    (canonicalWord : Family → Word)
+    (hCanonicalWordInjective : Function.Injective canonicalWord)
+    (decode : Message → Word)
+    (hCovers : ∀ family, ∃ message, decode message = canonicalWord family) :
+    Fintype.card Family ≤ Fintype.card Message := by
+  classical
+  let encode : Family → Message := fun family => Classical.choose (hCovers family)
+  have hEncode : ∀ family, decode (encode family) = canonicalWord family := fun family =>
+    Classical.choose_spec (hCovers family)
+  apply Fintype.card_le_of_injective encode
+  intro first second hEqual
+  apply hCanonicalWordInjective
+  calc
+    canonicalWord first = decode (encode first) := (hEncode first).symm
+    _ = decode (encode second) := congrArg decode hEqual
+    _ = canonicalWord second := hEncode second
+
+namespace AffineBinding
+
 /--
 Complete `n` free coordinates to one solution of a binary affine equation by
 solving for the omitted pivot coordinate.
@@ -56,21 +85,9 @@ theorem messageCardinality_ge_twoPow_freeCoordinates
     (hCovers : ∀ free, ∃ message,
       decode message = completeWord pivot coefficient affineValue free) :
     2 ^ n ≤ Fintype.card Message := by
-  classical
-  let encode : (Fin n → BinaryField) → Message := fun free =>
-    Classical.choose (hCovers free)
-  have hEncode : ∀ free,
-      decode (encode free) = completeWord pivot coefficient affineValue free := fun free =>
-    Classical.choose_spec (hCovers free)
-  have hInjective : Function.Injective encode := by
-    intro first second hEqual
-    apply completeWord_injective pivot coefficient affineValue
-    calc
-      completeWord pivot coefficient affineValue first = decode (encode first) :=
-        (hEncode first).symm
-      _ = decode (encode second) := congrArg decode hEqual
-      _ = completeWord pivot coefficient affineValue second := hEncode second
-  have hCard := Fintype.card_le_of_injective encode hInjective
+  have hCard := messageCardinality_ge_injectiveCanonicalFamily
+    (completeWord pivot coefficient affineValue)
+    (completeWord_injective pivot coefficient affineValue) decode hCovers
   simpa using hCard
 
 /--

docs/research/canonical-opening-experiments.md

@@ -221,6 +221,10 @@ parent tensor.
 
 ## Why the positive primitive does not scale
 
+The generic theorem `messageCardinality_ge_injectiveCanonicalFamily` makes the
+remaining burden explicit: exhibit a large injectively indexed family of
+canonical words and prove that the proposed decoder covers it.
+
 An affine equation on `n + 1` binary coordinates leaves `n` free coordinates.
 Lean proves that a deterministic no-response decoder representing every
 solution needs at least `2^n` messages. When the messages are `r`-bit strings,

docs/research/canonical-opening-theorem-index.md

@@ -233,6 +233,11 @@ parent tensor.
 
 ## Affine-binding cardinality barrier
 
+`messageCardinality_ge_injectiveCanonicalFamily` isolates the underlying
+pigeonhole argument: any decoder covering an injectively indexed canonical
+family needs at least one message per family member. Applying it to a proposed
+structured family still requires explicit proofs of injectivity and coverage.
+
 `messageCardinality_ge_twoPow_freeCoordinates` assumes a deterministic decoder
 represents every solution of one binary affine equation on `n + 1`
 coordinates. Lean proves that its message space has at least `2^n` elements.