From 16b73189470b676e738917db2524f03c8f53e4c8 Mon Sep 17 00:00:00 2001
From: windsornguyen <win@dedaluslabs.ai>
Date: Mon, 3 Aug 2026 21:14:23 -0700
Subject: [PATCH] refactor(opening): extract family cardinality bound

---
 .../AffineBinding/Cardinality.lean            | 49 +++++++++++++------
 .../research/canonical-opening-experiments.md |  4 ++
 .../canonical-opening-theorem-index.md        |  5 ++
 3 files changed, 42 insertions(+), 16 deletions(-)

diff --git a/ComplexityTheory/ProofComplexity/CanonicalOpening/AffineBinding/Cardinality.lean b/ComplexityTheory/ProofComplexity/CanonicalOpening/AffineBinding/Cardinality.lean
index 3dbe7e6..bbae6ae 100644
--- a/ComplexityTheory/ProofComplexity/CanonicalOpening/AffineBinding/Cardinality.lean
+++ b/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
 
 /--
diff --git a/docs/research/canonical-opening-experiments.md b/docs/research/canonical-opening-experiments.md
index 6e2a7bb..0fd9050 100644
--- a/docs/research/canonical-opening-experiments.md
+++ b/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,
diff --git a/docs/research/canonical-opening-theorem-index.md b/docs/research/canonical-opening-theorem-index.md
index a936e5a..822a7b2 100644
--- a/docs/research/canonical-opening-theorem-index.md
+++ b/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.