diff --git a/OrdvecFormalization/FiniteProductQuotient.lean b/OrdvecFormalization/FiniteProductQuotient.lean
index 1fffd64..452016a 100644
--- a/OrdvecFormalization/FiniteProductQuotient.lean
+++ b/OrdvecFormalization/FiniteProductQuotient.lean
@@ -252,6 +252,106 @@ theorem card_productQuotientRules {Z₁ Z₂ A : Type}
       Fintype.card A ^ (Fintype.card Z₁ * Fintype.card Z₂) := by
   rw [Fintype.card_fun, Fintype.card_prod]
 
+/--
+The reachable image of a product map is contained in the product of the two
+reachable component images.
+-/
+theorem productMap_image_subset_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (productMap Q₁ Q₂) ⊆
+      (QuotientImageFinset Q₁).product (QuotientImageFinset Q₂) := by
+  intro z hz
+  rcases Finset.mem_image.mp hz with ⟨p, _hp, hp⟩
+  rw [← hp]
+  exact Finset.mem_product.mpr
+    ⟨Finset.mem_image.mpr ⟨p.1, Finset.mem_univ p.1, rfl⟩,
+      Finset.mem_image.mpr ⟨p.2, Finset.mem_univ p.2, rfl⟩⟩
+
+/--
+The reachable image of a product map is exactly the product of the reachable
+component images.
+-/
+theorem productMap_image_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (productMap Q₁ Q₂) =
+      (QuotientImageFinset Q₁).product (QuotientImageFinset Q₂) := by
+  apply Finset.Subset.antisymm
+  · exact productMap_image_subset_product_images Q₁ Q₂
+  · intro z hz
+    rcases Finset.mem_product.mp hz with ⟨hz₁, hz₂⟩
+    rcases Finset.mem_image.mp hz₁ with ⟨x, _hx, hx⟩
+    rcases Finset.mem_image.mp hz₂ with ⟨y, _hy, hy⟩
+    exact Finset.mem_image.mpr
+      ⟨(x, y), Finset.mem_univ (x, y), Prod.ext hx hy⟩
+
+/--
+The number of reachable product codes is exactly the product of the numbers of
+reachable component codes.
+-/
+theorem productMap_image_card_eq_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (productMap Q₁ Q₂)).card =
+      (QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card := by
+  rw [productMap_image_eq_product_images Q₁ Q₂]
+  simp
+
+/--
+The number of reachable product codes is bounded by the product of the numbers
+of reachable component codes.
+-/
+theorem productMap_image_card_le_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (productMap Q₁ Q₂)).card ≤
+      (QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card := by
+  rw [productMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Rules on the reachable product image have search-space size
+`|A| ^ |image(productMap Q₁ Q₂)|`.
+-/
+theorem card_productImageQuotientRules
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) =
+      Fintype.card A ^ (QuotientImageFinset (productMap Q₁ Q₂)).card := by
+  exact card_quotientImageRules (productMap Q₁ Q₂)
+
+/--
+Rules on the reachable product image have search-space size
+`|A| ^ (|image Q₁| * |image Q₂|)`.
+-/
+theorem card_productImageQuotientRules_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) =
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_productImageQuotientRules Q₁ Q₂,
+    productMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Product-image quotient rules are bounded by assigning labels to every
+component-image pair.
+-/
+theorem card_productImageQuotientRules_le_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (productMap Q₁ Q₂) → A) ≤
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_productImageQuotientRules_eq_product_images Q₁ Q₂]
+
 namespace RuleFactorsThrough
 
 /-- Pairing two product-factorized targets is equivalent to factoring both components. -/
@@ -299,6 +399,26 @@ structure ComparisonObs (Ω₁ Ω₂ : Type) where
   second : Ω₂
 deriving DecidableEq
 
+/-- Finite comparison observations are equivalent to left/right/right triples. -/
+def comparisonObsEquivProd (Ω₁ Ω₂ : Type) :
+    ComparisonObs Ω₁ Ω₂ ≃ Ω₁ × Ω₂ × Ω₂ where
+  toFun c := (c.left, c.first, c.second)
+  invFun x := {
+    left := x.1
+    first := x.2.1
+    second := x.2.2
+  }
+  left_inv c := by
+    cases c
+    rfl
+  right_inv x := by
+    cases x
+    rfl
+
+instance comparisonObsFintype {Ω₁ Ω₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] : Fintype (ComparisonObs Ω₁ Ω₂) :=
+  Fintype.ofEquiv (Ω₁ × Ω₂ × Ω₂) (comparisonObsEquivProd Ω₁ Ω₂).symm
+
 /-- Product quotient for a left item and two right items. -/
 def comparisonMap {Ω₁ Ω₂ Z₁ Z₂ : Type}
     (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
@@ -387,4 +507,142 @@ theorem rankByScore_factorsThrough_of_score_factorsThrough
   cases c
   simp [rankByScore, comparisonMap, hscoreQ]
 
+/-! ## Comparison image bounds -/
+
+/--
+The ambient box of reachable comparison codes induced by one left image and two
+right images.
+-/
+def ComparisonImageBox {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) : Finset (ComparisonObs Z₁ Z₂) :=
+  ((QuotientImageFinset Q₁).product
+      ((QuotientImageFinset Q₂).product (QuotientImageFinset Q₂))).image
+    (fun z => {
+      left := z.1
+      first := z.2.1
+      second := z.2.2
+    })
+
+/--
+The reachable image of a comparison map is contained in the box of reachable
+left/right/right component codes.
+-/
+theorem comparisonMap_image_subset_imageBox
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (comparisonMap Q₁ Q₂) ⊆
+      ComparisonImageBox Q₁ Q₂ := by
+  intro z hz
+  rcases Finset.mem_image.mp hz with ⟨c, _hc, hc⟩
+  rw [← hc]
+  unfold ComparisonImageBox
+  apply Finset.mem_image.mpr
+  refine ⟨(Q₁ c.left, (Q₂ c.first, Q₂ c.second)), ?_, rfl⟩
+  exact Finset.mem_product.mpr
+    ⟨Finset.mem_image.mpr ⟨c.left, Finset.mem_univ c.left, rfl⟩,
+      Finset.mem_product.mpr
+        ⟨Finset.mem_image.mpr ⟨c.first, Finset.mem_univ c.first, rfl⟩,
+          Finset.mem_image.mpr ⟨c.second, Finset.mem_univ c.second, rfl⟩⟩⟩
+
+/--
+The reachable image of a comparison map is exactly the box of reachable
+left/right/right component codes.
+-/
+theorem comparisonMap_image_eq_imageBox
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    QuotientImageFinset (comparisonMap Q₁ Q₂) =
+      ComparisonImageBox Q₁ Q₂ := by
+  apply Finset.Subset.antisymm
+  · exact comparisonMap_image_subset_imageBox Q₁ Q₂
+  · intro z hz
+    unfold ComparisonImageBox at hz
+    rcases Finset.mem_image.mp hz with ⟨p, hp, hpz⟩
+    rcases Finset.mem_product.mp hp with ⟨hzleft, hzrights⟩
+    rcases Finset.mem_product.mp hzrights with ⟨hzfirst, hzsecond⟩
+    rcases Finset.mem_image.mp hzleft with ⟨x, _hxmem, hx⟩
+    rcases Finset.mem_image.mp hzfirst with ⟨y₁, _hy₁mem, hy₁⟩
+    rcases Finset.mem_image.mp hzsecond with ⟨y₂, _hy₂mem, hy₂⟩
+    apply Finset.mem_image.mpr
+    refine ⟨{ left := x, first := y₁, second := y₂ }, Finset.mem_univ _, ?_⟩
+    rw [← hpz]
+    simp [comparisonMap, hx, hy₁, hy₂]
+
+/--
+The number of reachable comparison codes is exactly
+`|image Q₁| * |image Q₂| * |image Q₂|`.
+-/
+theorem comparisonMap_image_card_eq_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (comparisonMap Q₁ Q₂)).card =
+      (QuotientImageFinset Q₁).card *
+        (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card := by
+  rw [comparisonMap_image_eq_imageBox Q₁ Q₂]
+  unfold ComparisonImageBox
+  rw [Finset.card_image_of_injective]
+  · simp [mul_assoc]
+  · intro p₁ p₂ h
+    exact Prod.ext (congrArg ComparisonObs.left h)
+      (Prod.ext (congrArg ComparisonObs.first h)
+        (congrArg ComparisonObs.second h))
+
+/--
+The number of reachable comparison codes is bounded by
+`|image Q₁| * |image Q₂| * |image Q₂|`.
+-/
+theorem comparisonMap_image_card_le_product_images_card
+    {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    (QuotientImageFinset (comparisonMap Q₁ Q₂)).card ≤
+      (QuotientImageFinset Q₁).card *
+        (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card := by
+  rw [comparisonMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Rules on the reachable comparison image have search-space size
+`|A| ^ |image(comparisonMap Q₁ Q₂)|`.
+-/
+theorem card_comparisonImageQuotientRules
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) =
+      Fintype.card A ^ (QuotientImageFinset (comparisonMap Q₁ Q₂)).card := by
+  exact card_quotientImageRules (comparisonMap Q₁ Q₂)
+
+/--
+Rules on the reachable comparison image have search-space size
+`|A| ^ (|image Q₁| * |image Q₂| * |image Q₂|)`.
+-/
+theorem card_comparisonImageQuotientRules_eq_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) =
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card *
+          (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_comparisonImageQuotientRules Q₁ Q₂,
+    comparisonMap_image_card_eq_product_images_card Q₁ Q₂]
+
+/--
+Comparison-image quotient rules are bounded by assigning labels to every
+left/right/right component-image triple.
+-/
+theorem card_comparisonImageQuotientRules_le_product_images
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂] [Fintype A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Fintype.card (QuotientImageBucket (comparisonMap Q₁ Q₂) → A) ≤
+      Fintype.card A ^
+        ((QuotientImageFinset Q₁).card *
+          (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card) := by
+  rw [card_comparisonImageQuotientRules_eq_product_images Q₁ Q₂]
+
 end OrdvecFormalization
diff --git a/OrdvecFormalization/FiniteQuotientSearch.lean b/OrdvecFormalization/FiniteQuotientSearch.lean
index 00655a5..0857202 100644
--- a/OrdvecFormalization/FiniteQuotientSearch.lean
+++ b/OrdvecFormalization/FiniteQuotientSearch.lean
@@ -174,6 +174,23 @@ abbrev QuotientImageBucket {Ω Ωq : Type} [Fintype Ω] [DecidableEq Ωq]
     (Q : Ω → Ωq) : Type :=
   {z : Ωq // z ∈ QuotientImageFinset Q}
 
+/--
+Rules on a finite reachable image have search-space size
+`|A| ^ |image Q|`.
+-/
+theorem card_quotientImageRules {Ω Ωq A : Type}
+    [Fintype Ω] [DecidableEq Ωq] [Fintype A] (Q : Ω → Ωq) :
+    Fintype.card (QuotientImageBucket Q → A) =
+      Fintype.card A ^ (QuotientImageFinset Q).card := by
+  classical
+  letI : Fintype (QuotientImageBucket Q) :=
+    Fintype.ofFinset (QuotientImageFinset Q) (by
+      intro z
+      constructor <;> intro hz <;> exact hz)
+  rw [Fintype.card_fun]
+  congr
+  simp [QuotientImageBucket]
+
 /-- Reachable quotient buckets that have not appeared in a finite sample. -/
 abbrev UnobservedReachableQuotients {Ω Ωq : Type}
     [Fintype Ω] [DecidableEq Ωq]
diff --git a/OrdvecFormalization/Verify.lean b/OrdvecFormalization/Verify.lean
index 151d4f5..b6637ae 100644
--- a/OrdvecFormalization/Verify.lean
+++ b/OrdvecFormalization/Verify.lean
@@ -119,6 +119,7 @@ namespace OrdvecFormalization
 #check @sampleConsistent_iff_exists_quotientRuleFitsSample
 #check @QuotientImageFinset
 #check @QuotientImageBucket
+#check @card_quotientImageRules
 #check @UnobservedReachableQuotients
 #check @restrictRuleToImage
 #check @imageRuleToFullTarget
@@ -198,9 +199,17 @@ namespace OrdvecFormalization
 #check @ObservedProductQuotients
 #check @UnobservedReachableProductQuotients
 #check @card_productQuotientRules
+#check @productMap_image_subset_product_images
+#check @productMap_image_eq_product_images
+#check @productMap_image_card_eq_product_images_card
+#check @productMap_image_card_le_product_images_card
+#check @card_productImageQuotientRules
+#check @card_productImageQuotientRules_eq_product_images
+#check @card_productImageQuotientRules_le_product_images
 #check @RuleFactorsThrough.product_pair_iff
 #check @ProductSampleConsistent.prod_iff
 #check @ComparisonObs
+#check @comparisonObsEquivProd
 #check @comparisonMap
 #check @comparisonMap_left
 #check @comparisonMap_first
@@ -210,6 +219,14 @@ namespace OrdvecFormalization
 #check @ruleFactorsThrough_comparison_fiberInvariant
 #check @rankByScore
 #check @rankByScore_factorsThrough_of_score_factorsThrough
+#check @ComparisonImageBox
+#check @comparisonMap_image_subset_imageBox
+#check @comparisonMap_image_eq_imageBox
+#check @comparisonMap_image_card_eq_product_images_card
+#check @comparisonMap_image_card_le_product_images_card
+#check @card_comparisonImageQuotientRules
+#check @card_comparisonImageQuotientRules_eq_product_images
+#check @card_comparisonImageQuotientRules_le_product_images
 #check @pairQuotient
 #check @pairQuotient_apply
 #check @pairQuotient_eq_iff
@@ -437,6 +454,7 @@ namespace OrdvecFormalization
 #print axioms extendWithUnobserved_fits_sample
 #print axioms card_fullTargets
 #print axioms card_quotientRules
+#print axioms card_quotientImageRules
 #print axioms quotientCompatible_search_space_bound
 #print axioms card_unobserved_assignments
 #print axioms card_unobserved_bool_assignments
@@ -482,11 +500,25 @@ namespace OrdvecFormalization
 #print axioms productSampleConsistent_iff_exists_productRuleFitsSample
 #print axioms no_productQuotientTarget_of_sample_collision
 #print axioms card_productQuotientRules
+#print axioms productMap_image_subset_product_images
+#print axioms productMap_image_eq_product_images
+#print axioms productMap_image_card_eq_product_images_card
+#print axioms productMap_image_card_le_product_images_card
+#print axioms card_productImageQuotientRules
+#print axioms card_productImageQuotientRules_eq_product_images
+#print axioms card_productImageQuotientRules_le_product_images
 #print axioms RuleFactorsThrough.product_pair_iff
 #print axioms ProductSampleConsistent.prod_iff
 #print axioms comparisonMap_eq_iff
 #print axioms ruleFactorsThrough_comparison_fiberInvariant
 #print axioms rankByScore_factorsThrough_of_score_factorsThrough
+#print axioms comparisonMap_image_subset_imageBox
+#print axioms comparisonMap_image_eq_imageBox
+#print axioms comparisonMap_image_card_eq_product_images_card
+#print axioms comparisonMap_image_card_le_product_images_card
+#print axioms card_comparisonImageQuotientRules
+#print axioms card_comparisonImageQuotientRules_eq_product_images
+#print axioms card_comparisonImageQuotientRules_le_product_images
 #print axioms pairQuotient_eq_iff
 #print axioms pairRuleFactorsThrough_same_on_quotient_fibers
 #print axioms no_pair_compatible_target_of_sample_collision
diff --git a/docs/paper/README.md b/docs/paper/README.md
index 8ae7902..7803417 100644
--- a/docs/paper/README.md
+++ b/docs/paper/README.md
@@ -13,7 +13,8 @@ Rebuild from this directory with:
 
 ```sh
 latexmk -pdf -interaction=nonstopmode -halt-on-error ordvec_formalization_paper.tex
-pdftotext ordvec_formalization_paper.pdf ordvec_formalization_paper.txt
+pdftotext -nopgbrk ordvec_formalization_paper.pdf ordvec_formalization_paper.txt
+perl -0pi -e 's/^\d+\n//mg' ordvec_formalization_paper.txt
 ```
 
 LaTeX intermediate files are ignored locally.
diff --git a/docs/paper/ordvec_formalization_paper.pdf b/docs/paper/ordvec_formalization_paper.pdf
index 1413c53..f8f80d7 100644
Binary files a/docs/paper/ordvec_formalization_paper.pdf and b/docs/paper/ordvec_formalization_paper.pdf differ
diff --git a/docs/paper/ordvec_formalization_paper.tex b/docs/paper/ordvec_formalization_paper.tex
index 45787e3..e98f07d 100644
--- a/docs/paper/ordvec_formalization_paper.tex
+++ b/docs/paper/ordvec_formalization_paper.tex
@@ -612,6 +612,29 @@ \subsection{Product quotients, ranking, and kernel refinements}
 constant on product fibers.  The surjective and image-restricted converses are
 the clean formal versions of working on the actually reached product image
 rather than pretending that the full ambient code space is populated.
+The finite search space is then exactly controlled by the component images:
+\begin{leanblock}
+\lean{productMap_image_subset_product_images}\\
+\lean{productMap_image_eq_product_images}\\
+\lean{productMap_image_card_eq_product_images_card}\\
+\lean{productMap_image_card_le_product_images_card}\\
+\lean{card_productImageQuotientRules}\\
+\lean{card_productImageQuotientRules_eq_product_images}\\
+\lean{card_productImageQuotientRules_le_product_images}
+\end{leanblock}
+In symbols, reachable product codes sit inside
+\(\im(C_q)\times\im(C_d)\), and because the product domain lets the two
+components vary independently, Lean proves equality:
+\[
+  \card{\im(C_q,C_d)}
+  =
+  \card{\im(C_q)}\card{\im(C_d)}.
+\]
+Image-level pair rules therefore have size
+\[
+  \card{A}^{\card{\im(C_q)}\card{\im(C_d)}}
+\]
+for finite label type \(A\).
 
 Finite pair samples get the corresponding falsifier:
 \begin{leanblock}
@@ -655,6 +678,23 @@ \subsection{Product quotients, ranking, and kernel refinements}
 query/document/document comparison quotient.  This proves a conditional bridge
 from preserved pairwise scores to preserved pairwise ranking decisions; it does
 not prove top-\(k\) equality without separate tie or margin assumptions.
+The reachable comparison-code haystack is exactly one left image and two right
+images:
+\begin{leanblock}
+\lean{ComparisonImageBox}\quad
+\lean{comparisonMap_image_subset_imageBox}\\
+\lean{comparisonMap_image_eq_imageBox}\\
+\lean{comparisonMap_image_card_eq_product_images_card}\\
+\lean{comparisonMap_image_card_le_product_images_card}\\
+\lean{card_comparisonImageQuotientRules}\\
+\lean{card_comparisonImageQuotientRules_eq_product_images}\\
+\lean{card_comparisonImageQuotientRules_le_product_images}
+\end{leanblock}
+Thus comparison-level rules have size
+\[
+  \card{A}^{\card{\im(C_q)}\card{\im(C_d)}^2},
+\]
+again for finite \(A\).
 
 \lean{FinitePairQuotient.lean} remains as a retrieval-facing wrapper around the
 generic product API:
diff --git a/docs/paper/ordvec_formalization_paper.txt b/docs/paper/ordvec_formalization_paper.txt
index 93b8da5..87740db 100644
--- a/docs/paper/ordvec_formalization_paper.txt
+++ b/docs/paper/ordvec_formalization_paper.txt
@@ -31,7 +31,6 @@ the search space is reduced once the contract is assumed. The profile layer simi
 supplied finite score certificates; it does not estimate encoder distortion or prove that contrastive
 training implies quotient invariance.
 
-1
 
 Purpose and Scope
 
@@ -41,9 +40,8 @@ comparison of experiments [1, 2, 3, 4]. A full observation space may contain ric
 or residual information. A quotient map
 Q:Ω→Z
 
-1
 
-throws away all distinctions inside each fiber Q−1 (z). The central question is not whether Q
+throws away all distinctions inside each fiber Q−1 (z). The central question is not whether Q
 preserves the whole representation. The central question is whether a specific admission decision
 can be made with no loss after passing from Ω to Z.
 The Lean repository answers this question in a finite setting. It proves that under exact
@@ -67,7 +65,6 @@ the reachable haystack is its image im(C), not all of Z. The later image-quotien
 this distinction: C is always surjective onto im(C), while no claim is made that it reaches every
 theoretically available quotient code.
 
-2
 
 Proof Roadmap
 
@@ -89,14 +86,12 @@ code preserves the target. The profile-stability layer packages supplied finite
 composes their errors.
 The final band specializes the quotient machinery. Ordered quotient evidence and monotone
 likelihood ratios give threshold-form Bayes rules. A supplied calibration equality can be attached to
-2
 
-the same cutoff. Canonical finite overlap tilts instantiate the ordered-evidence assumptions. Bitmap
+the same cutoff. Canonical finite overlap tilts instantiate the ordered-evidence assumptions. Bitmap
 symmetry explains why literal overlap is the canonical invariant under query-preserving coordinate
 relabelings, and the constant-weight bitmap null supplies the exact hypergeometric tail for the
 resulting overlap event.
 
-3
 
 Finite Experiments and Bayes Admission
 
@@ -144,9 +139,8 @@ Definition 3.2 (Factorization through a quotient). A rule or target δ : Ω →
 Q : Ω → Z if there exists a function δZ : Z → A such that
 δ(ω) = δZ (Q(ω))
 for every ω ∈ Ω.
-3
 
-This is the formal predicate RuleFactorsThrough.
+This is the formal predicate RuleFactorsThrough.
 Theorem 3.3 (Quotient-form Bayes optimality). If the pointwise Bayes admission predicate is
 constant on every quotient fiber, then there is a quotient-level set RZ ⊆ Z whose pullback has
 weighted risk no larger than every deterministic full-space rule R ⊆ Ω.
@@ -160,7 +154,6 @@ finiteWeightedBayesAdmit_iff_cutoff_le_likelihoodRatio
 finiteBayesAdmitFactorsThrough_of_likelihoodRatioFactorsThrough
 exists_quotientPullback_finiteWeightedRisk_le_of_likelihoodRatioFactorsThrough
 
-4
 
 What the Quotient Contract Forces Globally
 
@@ -205,9 +198,8 @@ fiber invariant + surjective Q
 factors through Q.
 
 This is fiberInvariant_ruleFactorsThrough_of_surjective. Thus, in the surjective finite setting, factorization and fiber invariance are the same structural condition.
-4
 
-The important qualification is the codomain. For an ambient compression C : Ω → Z, Lean
+The important qualification is the codomain. For an ambient compression C : Ω → Z, Lean
 does not require surjectivity onto all of Z. The right codomain is the reachable image im(C), where
 surjectivity holds by construction. This is the bridge from global quotient algebra to finite empirical
 search.
@@ -231,7 +223,6 @@ full-space distinction. Therefore it narrows the admission-decision search space
 certify that all semantic, geometric, margin, uncertainty, or downstream-task information has
 survived.
 
-5
 
 Finite Quotient Search
 
@@ -260,9 +251,8 @@ quotientRuleFitsSample.
 The negative form is the most useful empirical falsifier. If two sampled points have the same
 quotient value but different labels, then no quotient-compatible full target can fit the sample. This
 is no_compatible_target_of_sample_collision.
-5
 
-5.2
+5.2
 
 Observed buckets and unobserved freedom
 
@@ -314,13 +304,11 @@ quotient rules out factorization through any coarser one.
 The product theorem RuleFactorsThrough.prod_iff proves that a paired target factors
 through a quotient exactly when both components factor through it. The sample-level analogue
 SampleConsistent.prod_iff gives the same componentwise criterion for finite samples.
-6
 
-Interpretation 5.3. These theorems are useful for probe design. A refined quotient gives more
+Interpretation 5.3. These theorems are useful for probe design. A refined quotient gives more
 buckets and can only make factorization easier. Pairing multiple labels or probe tasks makes the
 quotient contract stricter: the pair factors only if each component does.
 
-6
 
 Reachable Images, Kernels, and Fiber Topology
 
@@ -386,9 +374,8 @@ KernelContainedInTarget(C, y),
 
 meaning that every compression collision is also a target indistinguishability.
 
-7
 
-Theorem 6.2 (Image quotient factorization equals kernel containment). For finite Ω, a target
+Theorem 6.2 (Image quotient factorization equals kernel containment). For finite Ω, a target
 y : Ω → A factors through the reachable image quotient of C if and only if
 Kernel(C) ⊆ TargetKernel(y).
 The checked names are:
@@ -449,20 +436,33 @@ Cq (q1 ) = Cq (q2 ),
 Cd (d1 ) = Cd (d2 )
 
 Lean exposes this through
-8
 
 =⇒
 
 y(q1 , d1 ) = y(q2 , d2 ).
 
-productMap ProductFiberInvariant ruleFactorsThrough_product_fiberInvariant
+productMap ProductFiberInvariant ruleFactorsThrough_product_fiberInvariant
 productFiberInvariant_ruleFactorsThrough_of_surjective
 ruleFactorsThrough_productMap_image_iff_productFiberInvariant
 
 The first direction is the retrieval contract: any product-factorized target is constant on product
 fibers. The surjective and image-restricted converses are the clean formal versions of working on
 the actually reached product image rather than pretending that the full ambient code space is
-populated.
+populated. The finite search space is then exactly controlled by the component images:
+productMap_image_subset_product_images
+productMap_image_eq_product_images
+productMap_image_card_eq_product_images_card
+productMap_image_card_le_product_images_card
+card_productImageQuotientRules
+card_productImageQuotientRules_eq_product_images
+card_productImageQuotientRules_le_product_images
+
+In symbols, reachable product codes sit inside im(Cq ) × im(Cd ), and because the product domain
+lets the two components vary independently, Lean proves equality:
+|im(Cq , Cd )| = |im(Cq )||im(Cd )|.
+Image-level pair rules therefore have size
+|A||im(Cq )||im(Cd )|
+for finite label type A.
 Finite pair samples get the corresponding falsifier:
 ProductSampleConsistent productSampleConsistent_of_ruleFactorsThrough
 productSampleConsistent_iff_exists_productRuleFitsSample
@@ -493,7 +493,21 @@ If a pairwise score factors through the query/document product quotient, then th
 comparison “document d1 ranks no higher than document d2 for query q” factors through the
 corresponding query/document/document comparison quotient. This proves a conditional bridge
 from preserved pairwise scores to preserved pairwise ranking decisions; it does not prove top-k
-equality without separate tie or margin assumptions.
+equality without separate tie or margin assumptions. The reachable comparison-code haystack is
+exactly one left image and two right images:
+
+ComparisonImageBox comparisonMap_image_subset_imageBox
+comparisonMap_image_eq_imageBox
+comparisonMap_image_card_eq_product_images_card
+comparisonMap_image_card_le_product_images_card
+card_comparisonImageQuotientRules
+card_comparisonImageQuotientRules_eq_product_images
+card_comparisonImageQuotientRules_le_product_images
+
+Thus comparison-level rules have size
+
+|A||im(Cq )||im(Cd )| ,
+again for finite A.
 FinitePairQuotient.lean remains as a retrieval-facing wrapper around the generic product
 API:
 pairQuotient_eq_iff pairRuleFactorsThrough_same_on_quotient_fibers
@@ -511,9 +525,7 @@ imageQuotient_refines_of_kernel_subset
 Interpretation 6.4. This is the formal bit/dimension tradeoff language. Finer quotients force
 fewer identifications and are easier to satisfy. Coarser quotients merge more points, make stronger
 compression claims, and are easier to falsify.
-9
 
-7
 
 Windowed Quotients and Probe Families
 
@@ -543,12 +555,13 @@ windowMap
 
 ObservationFamilyAgreement
 
-WindowAgreement
-
 with kernel characterizations
 kernel_observationFamilyMap_iff
 kernel_windowMap_iff
 
+
+WindowAgreement
+
 Theorem 7.1 (Window target factorization). For finite Ω, a target y : Ω → A factors through the
 reachable image quotient of Wk if and only if agreement on every coordinate in the window implies
 equal target behavior:
@@ -580,9 +593,7 @@ The finite sample falsifier lifts directly from the single-quotient case:
 no_window_compatible_target_of_same_code_label_disagreement
 no_window_image_compatible_target_of_same_code_label_disagreement
 
-10
-
-If two sampled points have the same whole window code and different labels, no window-factorized
+If two sampled points have the same whole window code and different labels, no window-factorized
 target can fit that sample.
 Finally, the module includes a generic finite analogue of the coincidence-length criterion. It
 defines the first coordinate where a pair disagrees, observationCoincidenceLength, and proves:
@@ -596,13 +607,13 @@ Interpretation 7.2. This changes the empirical burden. One quotient view may col
 a small finite bundle of quotient views can still be target-sufficient. The formal object to audit is
 the joint-code fiber, not any individual lossy probe in isolation.
 
-8
 
 Score Margins and Profile Stability
 
 The formalization does not try to prove that contrastive training or any particular encoder architecture automatically implies ordinal or bitmap invariance. Instead, ScoreMarginQuotient.lean
 proves a sufficient condition for threshold decisions to survive quotient approximation.
 
+
 8.1
 
 Margin-stable threshold admission
@@ -637,9 +648,7 @@ Thus, if the approximate score factors through the reachable image quotient, and
 is smaller than every full-score decision margin, then the full-score threshold rule factors through
 that same image quotient.
 
-11
-
-8.2
+8.2
 
 Finite profile certificates
 
@@ -663,7 +672,7 @@ the resulting threshold decision equality, image-quotient factorization, and ker
 does not define how to estimate those certificates, does not introduce a manifest schema, and does
 not claim that any real encoder satisfies them globally.
 
-9
+
 
 Ordered Evidence and Threshold Rules
 
@@ -692,9 +701,6 @@ weighted_threshold_bayesRisk_optimal
 threshold_bayesRisk_optimal
 costed_threshold_bayesRisk_optimal
 
-12
-
-10
 
 Calibrated Evidence
 
@@ -714,7 +720,6 @@ exists_calibratedOrderedThreshold_finiteCostedBayesRisk_le_of_orderedEvidenceFac
 This layer is intentionally graph-neutral. It is a packaging theorem, not a proof that a real
 corpus null distribution is correct.
 
-11
 
 Canonical Tilts and Overlap Sufficiency
 
@@ -743,9 +748,7 @@ finite canonical tilt model.
 The later bitmap-symmetry section explains why literal overlap is the canonical quotient statistic
 when the fixed-cardinality bitmap problem is invariant under coordinate relabelings that preserve
 the query.
-13
 
-12
 
 Bitmap Symmetry
 
@@ -762,13 +765,13 @@ The content is:
 • Query-stabilizer permutations preserve literal overlap with the query.
 • Among bitmaps of the same cardinality, equal query overlap is equivalent to being in the same
 query-stabilizer orbit.
+
 • Any statistic on the constant-weight bitmap space that is invariant under those query-stabilizer
 symmetries factors through literal overlap.
 This is a symmetry theorem, not an encoder theorem. It says that if the bitmap problem is
 treated as invariant under coordinate relabelings that preserve the query, then overlap is the orbit
 classifier on the fixed-cardinality space.
 
-13
 
 The Exact Constant-Weight Bitmap Null
 
@@ -795,9 +798,6 @@ BitmapIncidence.lean then bridges the abstract overlap threshold set to literal
 events:
 overlapQuotientThresholdSet_constantWeightBitmapOverlapEvidence_eq
 
-14
-
-14
 
 Main Bitmap Theorem
 
@@ -811,6 +811,7 @@ the signal law be the finite exponential tilt of that uniform law by literal que
 1. the literal overlap-tail rule
 {d ∈ BD,K : |q ∩ d| ≥ t}
 has Bayes risk no larger than any deterministic admission rule R ⊆ BD,K ;
+
 2. the uniform bitmap null mass of that same tail event is exactly the checked hypergeometric
 upper-tail value.
 The cost-sensitive version is
@@ -823,7 +824,6 @@ It keeps two facts separate: Bayes optimality is proved for the positive-base ca
 while the reported hypergeometric tail value is the separate uniform constant-weight null mass at
 the selected cutoff.
 
-15
 
 FNCH and Overlap-Null Wrappers
 
@@ -851,15 +851,14 @@ fnch_overlap_costed_threshold_bayes_optimal
 These theorems are part of the full proof surface, but the main constant-weight bitmap theorem
 is the clearest end-to-end statement because it joins Bayes optimality, literal bitmap incidence, and
 exact uniform-null tail calibration.
-15
 
-16
 
 How This Narrows Empirical Search
 
 The formalization does not measure real embedding coordinates. It does, however, give a precise
 checklist for what empirical probes are trying to refute or constrain.
 
+
 16.1
 
 What must hold if the contract is true
@@ -910,18 +909,16 @@ For small bitmap probes, the constant-weight theorem gives an idealized target s
 • if the relevant signal model is a positive overlap tilt;
 • if the admission target is the Bayes decision for that model;
 • and if the uniform constant-weight bitmap null is the calibration null;
-16
-
-then some overlap-tail cutoff is Bayes-optimal and has a hypergeometric null tail mass. Empirical
+then some overlap-tail cutoff is Bayes-optimal and has a hypergeometric null tail mass. Empirical
 work can look for formal violations of the quotient, monotonicity, margin, and calibration contracts,
 or collect finite sample evidence consistent with them. Lean proves the consequences of the contracts,
 not that real encoders satisfy them.
+
 The observation-window layer lets these probes be combined. Several bitmap, ordinal, lexical,
 query-transform, or context-window views can be treated as a single joint code. Production-style
 falsification then checks whether same-joint-code examples ever disagree on the target, rather than
 requiring each individual probe to be injective.
 
-17
 
 Non-Claims
 
@@ -945,7 +942,6 @@ These exclusions are not weaknesses in the formal theorem. They are the boundary
 the theorem exact: finite observations, deterministic rules, explicit quotient contracts, explicit
 monotonicity, and exact constant-weight bitmap null calibration.
 
-18
 
 Lean Verification Surface
 
@@ -955,9 +951,9 @@ make verify
 make check-doc-names
 make audit
 make lint
-17
 
-The expected axiom baseline printed by the verification surface is:
+
+The expected axiom baseline printed by the verification surface is:
 [propext, Classical.choice, Quot.sound].
 The root import file and public verification dashboard cover these main modules and support
 layers:
@@ -971,7 +967,6 @@ OverlapBayesOptimal BitmapIncidence BitmapCalibration BitmapNull
 BitmapSymmetry OverlapNull FiniteDecision MLR
 BayesThreshold ExponentialTilt FNCH
 
-19
 
 Conclusion
 
@@ -1001,16 +996,11 @@ DOI: https://doi.org/10.1214/aoms/1177728259.
 [6] Luc Devroye, László Györfi, and Gábor Lugosi. A Probabilistic Theory of Pattern Recognition.
 Stochastic Modelling and Applied Probability, volume 31. Springer New York, 1996. DOI:
 https://doi.org/10.1007/978-1-4612-0711-5.
-18
 
-[7] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming
+[7] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming
 Language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28,
 Lecture Notes in Computer Science, volume 12699, pages 625–635. Springer, Cham, 2021. DOI:
 https://doi.org/10.1007/978-3-030-79876-5_37.
 [8] The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM
 SIGPLAN International Conference on Certified Programs and Proofs (CPP ’20), pages 367–381.
 ACM, New York, 2020. DOI: https://doi.org/10.1145/3372885.3373824.
-
-19
-
-
\ No newline at end of file
diff --git a/docs/proof-spine.md b/docs/proof-spine.md
index eb563cc..5629200 100644
--- a/docs/proof-spine.md
+++ b/docs/proof-spine.md
@@ -145,10 +145,12 @@ imports bitmap definitions from `BitmapNull`, but it does not depend on
    that a product-factorized target specializes to fixed-left and fixed-right
    quotient rules; that finite same-product-code label disagreements are
    falsifiers; that product quotient rule spaces have the expected finite
-   cardinality; that product targets and sample consistency split componentwise;
+   cardinality; that reachable product images are exactly component-image
+   products; that product targets and sample consistency split componentwise;
    and that a score factoring through the query/document product quotient
    induces ranking comparisons factoring through the corresponding
-   query/document/document comparison quotient.
+   query/document/document comparison quotient, whose reachable image is exactly
+   the one-left/two-right component-image box.
 
 8. `FinitePairQuotient.lean`
    Packages the generic product quotient under query/document names for
diff --git a/docs/reviewer-brief.md b/docs/reviewer-brief.md
index fa0b03a..d849bcd 100644
--- a/docs/reviewer-brief.md
+++ b/docs/reviewer-brief.md
@@ -121,7 +121,9 @@ The proof is intentionally decomposed:
   factorization.
 - `FiniteProductQuotient.lean`: generic product quotients for pairwise targets,
   product-sample falsifiers, fixed-left/fixed-right specializations,
-  componentwise multi-target signatures, and score-induced ranking comparisons.
+  componentwise multi-target signatures, score-induced ranking comparisons, and
+  reachable image/cardinality equalities for product and comparison quotient
+  rule spaces.
 - `FinitePairQuotient.lean`: retrieval-facing query/document wrapper around the
   generic product quotient API.
 - `FiniteObservationWindow.lean`: finite families/windows of lossy probes,
diff --git a/docs/theorem-map.md b/docs/theorem-map.md
index 0be58c7..3f8240a 100644
--- a/docs/theorem-map.md
+++ b/docs/theorem-map.md
@@ -94,6 +94,7 @@ OrdvecFormalization.exists_quotientRuleFitsSample_of_sampleConsistent
 OrdvecFormalization.sampleConsistent_iff_exists_quotientRuleFitsSample
 OrdvecFormalization.QuotientImageFinset
 OrdvecFormalization.QuotientImageBucket
+OrdvecFormalization.card_quotientImageRules
 OrdvecFormalization.UnobservedReachableQuotients
 OrdvecFormalization.restrictRuleToImage
 OrdvecFormalization.imageRuleToFullTarget
@@ -181,15 +182,31 @@ OrdvecFormalization.no_productQuotientTarget_of_sample_collision
 OrdvecFormalization.ObservedProductQuotients
 OrdvecFormalization.UnobservedReachableProductQuotients
 OrdvecFormalization.card_productQuotientRules
+OrdvecFormalization.productMap_image_subset_product_images
+OrdvecFormalization.productMap_image_eq_product_images
+OrdvecFormalization.productMap_image_card_eq_product_images_card
+OrdvecFormalization.productMap_image_card_le_product_images_card
+OrdvecFormalization.card_productImageQuotientRules
+OrdvecFormalization.card_productImageQuotientRules_eq_product_images
+OrdvecFormalization.card_productImageQuotientRules_le_product_images
 OrdvecFormalization.RuleFactorsThrough.product_pair_iff
 OrdvecFormalization.ProductSampleConsistent.prod_iff
 OrdvecFormalization.ComparisonObs
+OrdvecFormalization.comparisonObsEquivProd
 OrdvecFormalization.comparisonMap
 OrdvecFormalization.comparisonMap_eq_iff
 OrdvecFormalization.ComparisonFiberInvariant
 OrdvecFormalization.ruleFactorsThrough_comparison_fiberInvariant
 OrdvecFormalization.rankByScore
 OrdvecFormalization.rankByScore_factorsThrough_of_score_factorsThrough
+OrdvecFormalization.ComparisonImageBox
+OrdvecFormalization.comparisonMap_image_subset_imageBox
+OrdvecFormalization.comparisonMap_image_eq_imageBox
+OrdvecFormalization.comparisonMap_image_card_eq_product_images_card
+OrdvecFormalization.comparisonMap_image_card_le_product_images_card
+OrdvecFormalization.card_comparisonImageQuotientRules
+OrdvecFormalization.card_comparisonImageQuotientRules_eq_product_images
+OrdvecFormalization.card_comparisonImageQuotientRules_le_product_images
 OrdvecFormalization.pairQuotient
 OrdvecFormalization.pairQuotient_eq_iff
 OrdvecFormalization.pairRuleFactorsThrough_same_on_quotient_fibers
@@ -308,6 +325,7 @@ Public Lean names:
 - `sampleConsistent_iff_exists_quotientRuleFitsSample`
 - `QuotientImageFinset`
 - `QuotientImageBucket`
+- `card_quotientImageRules`
 - `UnobservedReachableQuotients`
 - `restrictRuleToImage`
 - `imageRuleToFullTarget`
@@ -387,9 +405,17 @@ Public Lean names:
 - `ObservedProductQuotients`
 - `UnobservedReachableProductQuotients`
 - `card_productQuotientRules`
+- `productMap_image_subset_product_images`
+- `productMap_image_eq_product_images`
+- `productMap_image_card_eq_product_images_card`
+- `productMap_image_card_le_product_images_card`
+- `card_productImageQuotientRules`
+- `card_productImageQuotientRules_eq_product_images`
+- `card_productImageQuotientRules_le_product_images`
 - `RuleFactorsThrough.product_pair_iff`
 - `ProductSampleConsistent.prod_iff`
 - `ComparisonObs`
+- `comparisonObsEquivProd`
 - `comparisonMap`
 - `comparisonMap_left`
 - `comparisonMap_first`
@@ -399,6 +425,14 @@ Public Lean names:
 - `ruleFactorsThrough_comparison_fiberInvariant`
 - `rankByScore`
 - `rankByScore_factorsThrough_of_score_factorsThrough`
+- `ComparisonImageBox`
+- `comparisonMap_image_subset_imageBox`
+- `comparisonMap_image_eq_imageBox`
+- `comparisonMap_image_card_eq_product_images_card`
+- `comparisonMap_image_card_le_product_images_card`
+- `card_comparisonImageQuotientRules`
+- `card_comparisonImageQuotientRules_eq_product_images`
+- `card_comparisonImageQuotientRules_le_product_images`
 - `pairQuotient`
 - `pairQuotient_apply`
 - `pairQuotient_eq_iff`