diff --git a/OrdvecFormalization.lean b/OrdvecFormalization.lean
index e4f950a..92fcb53 100644
--- a/OrdvecFormalization.lean
+++ b/OrdvecFormalization.lean
@@ -5,6 +5,7 @@ import OrdvecFormalization.QuotientConstraints
 import OrdvecFormalization.FiniteQuotientImage
 import OrdvecFormalization.QuotientKernel
 import OrdvecFormalization.FiniteFiberTopology
+import OrdvecFormalization.FiniteProductQuotient
 import OrdvecFormalization.FinitePairQuotient
 import OrdvecFormalization.QuotientRefinementKernel
 import OrdvecFormalization.FiniteObservationWindow
diff --git a/OrdvecFormalization/FinitePairQuotient.lean b/OrdvecFormalization/FinitePairQuotient.lean
index 3ee5d02..a346ee3 100644
--- a/OrdvecFormalization/FinitePairQuotient.lean
+++ b/OrdvecFormalization/FinitePairQuotient.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nelson Spence
 -/
 
-import OrdvecFormalization.FiniteQuotientSearch
+import OrdvecFormalization.FiniteProductQuotient
 
 namespace OrdvecFormalization
 
@@ -17,9 +17,9 @@ same-compressed-pair invariance/falsifier theorems.
 -/
 
 /-- Product quotient for query/document pairs. -/
-def pairQuotient {Ωq Ωd Zq Zd : Type}
+abbrev pairQuotient {Ωq Ωd Zq Zd : Type}
     (Cq : Ωq → Zq) (Cd : Ωd → Zd) : Ωq × Ωd → Zq × Zd :=
-  fun pair => (Cq pair.1, Cd pair.2)
+  productMap Cq Cd
 
 @[simp]
 theorem pairQuotient_apply {Ωq Ωd Zq Zd : Type}
@@ -30,12 +30,8 @@ theorem pairQuotient_eq_iff {Ωq Ωd Zq Zd : Type}
     (Cq : Ωq → Zq) (Cd : Ωd → Zd)
     (pair₁ pair₂ : Ωq × Ωd) :
     pairQuotient Cq Cd pair₁ = pairQuotient Cq Cd pair₂ ↔
-      Cq pair₁.1 = Cq pair₂.1 ∧ Cd pair₁.2 = Cd pair₂.2 := by
-  constructor
-  · intro h
-    exact ⟨congrArg Prod.fst h, congrArg Prod.snd h⟩
-  · rintro ⟨hq, hd⟩
-    exact Prod.ext hq hd
+      Cq pair₁.1 = Cq pair₂.1 ∧ Cd pair₁.2 = Cd pair₂.2 :=
+  productMap_eq_iff Cq Cd pair₁ pair₂
 
 /--
 A pairwise target that factors through the product quotient is invariant under
@@ -48,9 +44,9 @@ theorem pairRuleFactorsThrough_same_on_quotient_fibers {Ωq Ωd Zq Zd A : Type}
     (hq : Cq pair₁.1 = Cq pair₂.1)
     (hd : Cd pair₁.2 = Cd pair₂.2) :
     target pair₁ = target pair₂ := by
-  rcases hfac with ⟨targetq, htarget⟩
-  rw [htarget pair₁, htarget pair₂]
-  exact congrArg targetq (Prod.ext hq hd)
+  rcases pair₁ with ⟨q₁, d₁⟩
+  rcases pair₂ with ⟨q₂, d₂⟩
+  exact ruleFactorsThrough_product_fiberInvariant Cq Cd target hfac hq hd
 
 /--
 If two sampled query/document pairs have the same product quotient but
diff --git a/OrdvecFormalization/FiniteProductQuotient.lean b/OrdvecFormalization/FiniteProductQuotient.lean
new file mode 100644
index 0000000..1fffd64
--- /dev/null
+++ b/OrdvecFormalization/FiniteProductQuotient.lean
@@ -0,0 +1,390 @@
+/-
+Copyright (c) 2026 Nelson Spence. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nelson Spence
+-/
+
+import OrdvecFormalization.QuotientKernel
+
+namespace OrdvecFormalization
+
+/-!
+# Finite product quotients
+
+This file lifts the quotient/fiber contract from one observation space to
+product-space targets.  This is the generic shape behind retrieval-style
+targets: a target may depend on a left object and a right object, while the
+compressed observation is the product of independently compressed codes.
+
+The ranking section adds a comparison observation with one left item and two
+right items.  It proves that a score factoring through a pair product quotient
+induces a pairwise ordering rule factoring through the corresponding comparison
+quotient.
+-/
+
+/-! ## Product quotients -/
+
+/-- Product map induced by two quotient maps. -/
+def productMap {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    Ω₁ × Ω₂ → Z₁ × Z₂ :=
+  Prod.map Q₁ Q₂
+
+@[simp]
+theorem productMap_apply {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) (x : Ω₁ × Ω₂) :
+    productMap Q₁ Q₂ x = (Q₁ x.1, Q₂ x.2) :=
+  rfl
+
+theorem productMap_eq_iff {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (x₁ x₂ : Ω₁ × Ω₂) :
+    productMap Q₁ Q₂ x₁ = productMap Q₁ Q₂ x₂ ↔
+      Q₁ x₁.1 = Q₁ x₂.1 ∧ Q₂ x₁.2 = Q₂ x₂.2 := by
+  cases x₁
+  cases x₂
+  simp [productMap, Prod.map]
+
+/--
+A product target is invariant on product quotient fibers when same left code
+and same right code force the same target value.
+-/
+def ProductFiberInvariant {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A) : Prop :=
+  ∀ ⦃x₁ x₂ : Ω₁⦄ ⦃y₁ y₂ : Ω₂⦄,
+    Q₁ x₁ = Q₁ x₂ →
+    Q₂ y₁ = Q₂ y₂ →
+    target (x₁, y₁) = target (x₂, y₂)
+
+/-- Product fiber invariance is exactly kernel containment for `productMap`. -/
+theorem kernelContainedInTarget_productMap_iff_productFiberInvariant
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A) :
+    KernelContainedInTarget (productMap Q₁ Q₂) target ↔
+      ProductFiberInvariant Q₁ Q₂ target := by
+  constructor
+  · intro hker x₁ x₂ y₁ y₂ h₁ h₂
+    exact hker (Prod.ext h₁ h₂)
+  · intro hinv p₁ p₂ hker
+    rcases p₁ with ⟨x₁, y₁⟩
+    rcases p₂ with ⟨x₂, y₂⟩
+    exact hinv (congrArg Prod.fst hker) (congrArg Prod.snd hker)
+
+/-- A target factoring through a product quotient is invariant on product fibers. -/
+theorem ruleFactorsThrough_product_fiberInvariant
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A)
+    (h : RuleFactorsThrough (productMap Q₁ Q₂) target) :
+    ProductFiberInvariant Q₁ Q₂ target := by
+  exact (kernelContainedInTarget_productMap_iff_productFiberInvariant
+    Q₁ Q₂ target).mp (ruleFactorsThrough_fiberInvariant
+      (productMap Q₁ Q₂) target h)
+
+/-- Under surjectivity, product fiber invariance builds a product quotient rule. -/
+theorem productFiberInvariant_ruleFactorsThrough_of_surjective
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A)
+    (h₁ : Function.Surjective Q₁)
+    (h₂ : Function.Surjective Q₂)
+    (hinv : ProductFiberInvariant Q₁ Q₂ target) :
+    RuleFactorsThrough (productMap Q₁ Q₂) target := by
+  refine ⟨fun z =>
+    target (Classical.choose (h₁ z.1), Classical.choose (h₂ z.2)), ?_⟩
+  intro p
+  rcases p with ⟨x, y⟩
+  have hx : Q₁ (Classical.choose (h₁ (Q₁ x))) = Q₁ x :=
+    Classical.choose_spec (h₁ (Q₁ x))
+  have hy : Q₂ (Classical.choose (h₂ (Q₂ y))) = Q₂ y :=
+    Classical.choose_spec (h₂ (Q₂ y))
+  exact (hinv hx hy).symm
+
+/--
+Factoring through the reachable image of a product map is exactly product fiber
+invariance.  This avoids any surjectivity claim about the full ambient product
+codomain.
+-/
+theorem ruleFactorsThrough_productMap_image_iff_productFiberInvariant
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A) :
+    RuleFactorsThrough (imageQuotient (productMap Q₁ Q₂)) target ↔
+      ProductFiberInvariant Q₁ Q₂ target := by
+  rw [ruleFactorsThrough_image_iff_kernelContainedInTarget,
+    kernelContainedInTarget_productMap_iff_productFiberInvariant]
+
+/--
+A product-factorized target gives a right-space quotient rule at every fixed
+left input.
+-/
+theorem ruleFactorsThrough_product_fixedLeft
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A)
+    (h : RuleFactorsThrough (productMap Q₁ Q₂) target)
+    (x : Ω₁) :
+    RuleFactorsThrough Q₂ (fun y : Ω₂ => target (x, y)) := by
+  rcases h with ⟨targetQ, htarget⟩
+  refine ⟨fun z₂ => targetQ (Q₁ x, z₂), ?_⟩
+  intro y
+  exact htarget (x, y)
+
+/--
+A product-factorized target gives a left-space quotient rule at every fixed
+right input.
+-/
+theorem ruleFactorsThrough_product_fixedRight
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A)
+    (h : RuleFactorsThrough (productMap Q₁ Q₂) target)
+    (y : Ω₂) :
+    RuleFactorsThrough Q₁ (fun x : Ω₁ => target (x, y)) := by
+  rcases h with ⟨targetQ, htarget⟩
+  refine ⟨fun z₁ => targetQ (z₁, Q₂ y), ?_⟩
+  intro x
+  exact htarget (x, y)
+
+/-! ## Product samples and finite falsifiers -/
+
+/-- A finite product sample has no same-product-code label contradictions. -/
+def ProductSampleConsistent {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (label : Ω₁ × Ω₂ → A) (sample : Finset (Ω₁ × Ω₂)) : Prop :=
+  ∀ ⦃p₁ p₂ : Ω₁ × Ω₂⦄,
+    p₁ ∈ sample →
+    p₂ ∈ sample →
+    Q₁ p₁.1 = Q₁ p₂.1 →
+    Q₂ p₁.2 = Q₂ p₂.2 →
+    label p₁ = label p₂
+
+/-- Product sample consistency is the usual sample consistency for `productMap`. -/
+theorem productSampleConsistent_iff_sampleConsistent_productMap
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (label : Ω₁ × Ω₂ → A) (sample : Finset (Ω₁ × Ω₂)) :
+    ProductSampleConsistent Q₁ Q₂ label sample ↔
+      SampleConsistent (productMap Q₁ Q₂) label sample := by
+  constructor
+  · intro hprod p₁ p₂ hp₁ hp₂ hcode
+    exact hprod hp₁ hp₂ (congrArg Prod.fst hcode) (congrArg Prod.snd hcode)
+  · intro hsample p₁ p₂ hp₁ hp₂ h₁ h₂
+    exact hsample hp₁ hp₂ (Prod.ext h₁ h₂)
+
+/-- A product-factorized target cannot contradict itself on a finite product sample. -/
+theorem productSampleConsistent_of_ruleFactorsThrough
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : Ω₁ × Ω₂ → A) (sample : Finset (Ω₁ × Ω₂))
+    (h : RuleFactorsThrough (productMap Q₁ Q₂) target) :
+    ProductSampleConsistent Q₁ Q₂ target sample := by
+  intro p₁ p₂ _hp₁ _hp₂ h₁ h₂
+  rcases p₁ with ⟨x₁, y₁⟩
+  rcases p₂ with ⟨x₂, y₂⟩
+  exact ruleFactorsThrough_product_fiberInvariant Q₁ Q₂ target h h₁ h₂
+
+/--
+A finite product sample is product-consistent iff some product-quotient rule
+fits it.
+-/
+theorem productSampleConsistent_iff_exists_productRuleFitsSample
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type} [Inhabited A]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (label : Ω₁ × Ω₂ → A) (sample : Finset (Ω₁ × Ω₂)) :
+    ProductSampleConsistent Q₁ Q₂ label sample ↔
+      ∃ ruleZ : Z₁ × Z₂ → A,
+        QuotientRuleFitsSample (productMap Q₁ Q₂) label sample ruleZ := by
+  rw [productSampleConsistent_iff_sampleConsistent_productMap,
+    sampleConsistent_iff_exists_quotientRuleFitsSample]
+
+/--
+If two sampled product observations have the same product quotient code but
+different labels, no product-quotient rule can fit the sample.
+-/
+theorem no_productQuotientTarget_of_sample_collision
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (label : Ω₁ × Ω₂ → A) (sample : Finset (Ω₁ × Ω₂))
+    {p₁ p₂ : Ω₁ × Ω₂}
+    (hp₁ : p₁ ∈ sample) (hp₂ : p₂ ∈ sample)
+    (h₁ : Q₁ p₁.1 = Q₁ p₂.1)
+    (h₂ : Q₂ p₁.2 = Q₂ p₂.2)
+    (hlabel : label p₁ ≠ label p₂) :
+    ¬ ∃ target : Ω₁ × Ω₂ → A,
+      RuleFactorsThrough (productMap Q₁ Q₂) target ∧
+        (∀ ⦃p : Ω₁ × Ω₂⦄, p ∈ sample → target p = label p) := by
+  rintro ⟨target, hfac, hfit⟩
+  have hsame : target p₁ = target p₂ := by
+    rcases p₁ with ⟨x₁, y₁⟩
+    rcases p₂ with ⟨x₂, y₂⟩
+    exact ruleFactorsThrough_product_fiberInvariant Q₁ Q₂ target hfac h₁ h₂
+  exact hlabel (by
+    rw [← hfit hp₁, ← hfit hp₂]
+    exact hsame)
+
+/-! ## Product-rule and multi-target search spaces -/
+
+/-- Observed product quotient buckets in a finite product sample. -/
+abbrev ObservedProductQuotients {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (sample : Finset (Ω₁ × Ω₂)) : Finset (Z₁ × Z₂) :=
+  ObservedQuotients (productMap Q₁ Q₂) sample
+
+/-- Reachable product quotient buckets that have not appeared in a finite sample. -/
+abbrev UnobservedReachableProductQuotients {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    [Fintype Ω₁] [Fintype Ω₂] [DecidableEq Z₁] [DecidableEq Z₂]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (sample : Finset (Ω₁ × Ω₂)) : Type :=
+  UnobservedReachableQuotients (productMap Q₁ Q₂) sample
+
+/--
+The full product-quotient rule space over ambient product codomain has size
+`|A| ^ (|Z₁| * |Z₂|)`.
+-/
+theorem card_productQuotientRules {Z₁ Z₂ A : Type}
+    [DecidableEq Z₁] [DecidableEq Z₂] [Fintype Z₁] [Fintype Z₂] [Fintype A] :
+    Fintype.card (Z₁ × Z₂ → A) =
+      Fintype.card A ^ (Fintype.card Z₁ * Fintype.card Z₂) := by
+  rw [Fintype.card_fun, Fintype.card_prod]
+
+namespace RuleFactorsThrough
+
+/-- Pairing two product-factorized targets is equivalent to factoring both components. -/
+theorem product_pair_iff {Ω₁ Ω₂ Z₁ Z₂ A B : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (targetA : Ω₁ × Ω₂ → A) (targetB : Ω₁ × Ω₂ → B) :
+    RuleFactorsThrough (productMap Q₁ Q₂) (fun p => (targetA p, targetB p)) ↔
+      RuleFactorsThrough (productMap Q₁ Q₂) targetA ∧
+        RuleFactorsThrough (productMap Q₁ Q₂) targetB :=
+  RuleFactorsThrough.prod_iff (productMap Q₁ Q₂) targetA targetB
+
+end RuleFactorsThrough
+
+namespace ProductSampleConsistent
+
+/-- Product-sample consistency for a paired label is componentwise consistency. -/
+theorem prod_iff {Ω₁ Ω₂ Z₁ Z₂ A B : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (labelA : Ω₁ × Ω₂ → A) (labelB : Ω₁ × Ω₂ → B)
+    (sample : Finset (Ω₁ × Ω₂)) :
+    ProductSampleConsistent Q₁ Q₂ (fun p => (labelA p, labelB p)) sample ↔
+      ProductSampleConsistent Q₁ Q₂ labelA sample ∧
+        ProductSampleConsistent Q₁ Q₂ labelB sample := by
+  constructor
+  · intro hpair
+    constructor
+    · intro p₁ p₂ hp₁ hp₂ h₁ h₂
+      exact congrArg Prod.fst (hpair hp₁ hp₂ h₁ h₂)
+    · intro p₁ p₂ hp₁ hp₂ h₁ h₂
+      exact congrArg Prod.snd (hpair hp₁ hp₂ h₁ h₂)
+  · rintro ⟨hA, hB⟩ p₁ p₂ hp₁ hp₂ h₁ h₂
+    exact Prod.ext (hA hp₁ hp₂ h₁ h₂) (hB hp₁ hp₂ h₁ h₂)
+
+end ProductSampleConsistent
+
+/-! ## Comparison quotients and score-induced ranking -/
+
+/-- A left item together with two right items, used for pairwise comparisons. -/
+structure ComparisonObs (Ω₁ Ω₂ : Type) where
+  /-- The left-side item, such as a query. -/
+  left : Ω₁
+  /-- The first right-side item in the comparison. -/
+  first : Ω₂
+  /-- The second right-side item in the comparison. -/
+  second : Ω₂
+deriving DecidableEq
+
+/-- Product quotient for a left item and two right items. -/
+def comparisonMap {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) :
+    ComparisonObs Ω₁ Ω₂ → ComparisonObs Z₁ Z₂ :=
+  fun c => {
+    left := Q₁ c.left
+    first := Q₂ c.first
+    second := Q₂ c.second
+  }
+
+@[simp]
+theorem comparisonMap_left {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) (c : ComparisonObs Ω₁ Ω₂) :
+    (comparisonMap Q₁ Q₂ c).left = Q₁ c.left :=
+  rfl
+
+@[simp]
+theorem comparisonMap_first {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) (c : ComparisonObs Ω₁ Ω₂) :
+    (comparisonMap Q₁ Q₂ c).first = Q₂ c.first :=
+  rfl
+
+@[simp]
+theorem comparisonMap_second {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂) (c : ComparisonObs Ω₁ Ω₂) :
+    (comparisonMap Q₁ Q₂ c).second = Q₂ c.second :=
+  rfl
+
+theorem comparisonMap_eq_iff {Ω₁ Ω₂ Z₁ Z₂ : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (c₁ c₂ : ComparisonObs Ω₁ Ω₂) :
+    comparisonMap Q₁ Q₂ c₁ = comparisonMap Q₁ Q₂ c₂ ↔
+      Q₁ c₁.left = Q₁ c₂.left ∧
+        Q₂ c₁.first = Q₂ c₂.first ∧
+          Q₂ c₁.second = Q₂ c₂.second := by
+  cases c₁
+  cases c₂
+  simp [comparisonMap]
+
+/-- A comparison target is invariant under compressed left/right/right codes. -/
+def ComparisonFiberInvariant {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : ComparisonObs Ω₁ Ω₂ → A) : Prop :=
+  ∀ ⦃c₁ c₂ : ComparisonObs Ω₁ Ω₂⦄,
+    Q₁ c₁.left = Q₁ c₂.left →
+    Q₂ c₁.first = Q₂ c₂.first →
+    Q₂ c₁.second = Q₂ c₂.second →
+    target c₁ = target c₂
+
+/-- A comparison-factorized target is invariant on comparison quotient fibers. -/
+theorem ruleFactorsThrough_comparison_fiberInvariant
+    {Ω₁ Ω₂ Z₁ Z₂ A : Type}
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (target : ComparisonObs Ω₁ Ω₂ → A)
+    (h : RuleFactorsThrough (comparisonMap Q₁ Q₂) target) :
+    ComparisonFiberInvariant Q₁ Q₂ target := by
+  rcases h with ⟨targetQ, htarget⟩
+  intro c₁ c₂ hleft hfirst hsecond
+  have hcode : comparisonMap Q₁ Q₂ c₁ = comparisonMap Q₁ Q₂ c₂ :=
+    (comparisonMap_eq_iff Q₁ Q₂ c₁ c₂).mpr ⟨hleft, hfirst, hsecond⟩
+  rw [htarget c₁, htarget c₂, hcode]
+
+/-- Score-induced pairwise ordering comparison. -/
+def rankByScore {Ω₁ Ω₂ S : Type}
+    [LE S] [DecidableRel (fun a b : S => a ≤ b)]
+    (score : Ω₁ × Ω₂ → S) :
+    ComparisonObs Ω₁ Ω₂ → Bool :=
+  fun c => decide (score (c.left, c.first) ≤ score (c.left, c.second))
+
+/--
+If a pair score factors through compressed left/right codes, then the
+score-induced ordering comparison factors through compressed left/right/right
+codes.
+-/
+theorem rankByScore_factorsThrough_of_score_factorsThrough
+    {Ω₁ Ω₂ Z₁ Z₂ S : Type}
+    [LE S] [DecidableRel (fun a b : S => a ≤ b)]
+    (Q₁ : Ω₁ → Z₁) (Q₂ : Ω₂ → Z₂)
+    (score : Ω₁ × Ω₂ → S)
+    (hscore : RuleFactorsThrough (productMap Q₁ Q₂) score) :
+    RuleFactorsThrough (comparisonMap Q₁ Q₂) (rankByScore score) := by
+  rcases hscore with ⟨scoreQ, hscoreQ⟩
+  refine ⟨fun zc =>
+    decide (scoreQ (zc.left, zc.first) ≤ scoreQ (zc.left, zc.second)), ?_⟩
+  intro c
+  cases c
+  simp [rankByScore, comparisonMap, hscoreQ]
+
+end OrdvecFormalization
diff --git a/OrdvecFormalization/Verify.lean b/OrdvecFormalization/Verify.lean
index 8da53ce..151d4f5 100644
--- a/OrdvecFormalization/Verify.lean
+++ b/OrdvecFormalization/Verify.lean
@@ -180,6 +180,36 @@ namespace OrdvecFormalization
 #check @hasCollision_iff_not_injectiveOnSample
 #check @hasCollision_of_card_gt_observedBuckets_card
 #check @no_compatible_target_of_same_bucket_label_disagreement
+#check @productMap
+#check @productMap_apply
+#check @productMap_eq_iff
+#check @ProductFiberInvariant
+#check @kernelContainedInTarget_productMap_iff_productFiberInvariant
+#check @ruleFactorsThrough_product_fiberInvariant
+#check @productFiberInvariant_ruleFactorsThrough_of_surjective
+#check @ruleFactorsThrough_productMap_image_iff_productFiberInvariant
+#check @ruleFactorsThrough_product_fixedLeft
+#check @ruleFactorsThrough_product_fixedRight
+#check @ProductSampleConsistent
+#check @productSampleConsistent_iff_sampleConsistent_productMap
+#check @productSampleConsistent_of_ruleFactorsThrough
+#check @productSampleConsistent_iff_exists_productRuleFitsSample
+#check @no_productQuotientTarget_of_sample_collision
+#check @ObservedProductQuotients
+#check @UnobservedReachableProductQuotients
+#check @card_productQuotientRules
+#check @RuleFactorsThrough.product_pair_iff
+#check @ProductSampleConsistent.prod_iff
+#check @ComparisonObs
+#check @comparisonMap
+#check @comparisonMap_left
+#check @comparisonMap_first
+#check @comparisonMap_second
+#check @comparisonMap_eq_iff
+#check @ComparisonFiberInvariant
+#check @ruleFactorsThrough_comparison_fiberInvariant
+#check @rankByScore
+#check @rankByScore_factorsThrough_of_score_factorsThrough
 #check @pairQuotient
 #check @pairQuotient_apply
 #check @pairQuotient_eq_iff
@@ -440,6 +470,23 @@ namespace OrdvecFormalization
 #print axioms hasCollision_iff_not_injectiveOnSample
 #print axioms hasCollision_of_card_gt_observedBuckets_card
 #print axioms no_compatible_target_of_same_bucket_label_disagreement
+#print axioms productMap_eq_iff
+#print axioms kernelContainedInTarget_productMap_iff_productFiberInvariant
+#print axioms ruleFactorsThrough_product_fiberInvariant
+#print axioms productFiberInvariant_ruleFactorsThrough_of_surjective
+#print axioms ruleFactorsThrough_productMap_image_iff_productFiberInvariant
+#print axioms ruleFactorsThrough_product_fixedLeft
+#print axioms ruleFactorsThrough_product_fixedRight
+#print axioms productSampleConsistent_iff_sampleConsistent_productMap
+#print axioms productSampleConsistent_of_ruleFactorsThrough
+#print axioms productSampleConsistent_iff_exists_productRuleFitsSample
+#print axioms no_productQuotientTarget_of_sample_collision
+#print axioms card_productQuotientRules
+#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 pairQuotient_eq_iff
 #print axioms pairRuleFactorsThrough_same_on_quotient_fibers
 #print axioms no_pair_compatible_target_of_sample_collision
diff --git a/README.md b/README.md
index a40f49e..8128d92 100644
--- a/README.md
+++ b/README.md
@@ -44,10 +44,12 @@ calibrated popcount threshold rather than an arbitrary accept/reject rule.
 
 The quotient-search layers also make the empirical burden explicit. A single
 lossy quotient need not be injective; what matters is whether its fibers, or
-the joint fibers of a finite family of lossy probes, preserve the target
-behavior being claimed. The windowed-observation layer formalizes this as a
-target-separation condition on joint codes, with same-joint-code label
-disagreements as finite falsifiers.
+the joint fibers of product quotients and finite families of lossy probes,
+preserve the target behavior being claimed. The product layer handles pairwise
+query/document decisions, multi-target signatures, and score-induced ranking
+comparisons; the windowed-observation layer formalizes target separation by
+joint probe codes, with same-joint-code label disagreements as finite
+falsifiers.
 
 ## Main Checked Result
 
@@ -76,6 +78,8 @@ This repository proves:
   and monotonicity assumptions;
 - finite quotient-search constraints, reachable-image/kernel containment, and
   sample-level same-bucket falsifiers;
+- finite product-quotient contracts for pairwise targets, componentwise
+  multi-target signatures, and score-induced ranking comparisons;
 - finite observation-window theorems showing that a family of lossy probes is
   target-sufficient exactly when joint-code agreement preserves the target;
 - a group-theoretic maximal-invariant theorem explaining why bitmap overlap is
diff --git a/docs/paper/ordvec_formalization_paper.pdf b/docs/paper/ordvec_formalization_paper.pdf
index 5c3d4fc..1413c53 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 66874f9..45787e3 100644
--- a/docs/paper/ordvec_formalization_paper.tex
+++ b/docs/paper/ordvec_formalization_paper.tex
@@ -60,8 +60,9 @@
 falsifiers; observed finite samples determine observed buckets but leave
 reachable unobserved image buckets freely assignable; the reachable image quotient is
 surjective by construction; kernel containment exactly characterizes safe
-compression; finite samples decompose into observed fiber clumps; pair
-quotients and refinement kernels constrain retrieval-style hypotheses; finite
+compression; finite samples decompose into observed fiber clumps; product
+quotients constrain pairwise, multi-target, and ranking-style hypotheses;
+refinement kernels order quotient strength; finite
 observation windows turn families of lossy probes into joint quotient codes
 whose kernels shrink with added coordinates; and any non-injective quotient
 necessarily forgets some possible full-space distinction.
@@ -150,8 +151,9 @@ \section{Proof Roadmap}
 reasoning.  A compression map is treated as surjective onto its reachable
 image; factorization through that image is equivalent to containment of the
 compression kernel inside the target kernel.  Sample fibers are counted as
-observed clumps; retrieval-style query/document decisions are handled by
-product quotients; refinement is characterized by kernel inclusion; and score
+observed clumps; product quotients handle query/document decisions,
+multi-target signatures, and score-induced ranking comparisons; refinement is
+characterized by kernel inclusion; and score
 approximation plus margin separation gives a sufficient condition for
 threshold decisions to remain quotient-factorized.  Between refinement and
 score margins, the observation-window layer proves that a finite family of
@@ -579,27 +581,88 @@ \subsection{Observed fiber topology}
 nontrivial sampled fiber exists.  If that fiber carries a label disagreement,
 the exact quotient contract is falsified on the sample.
 
-\subsection{Pair quotients and kernel refinements}
+\subsection{Product quotients, ranking, and kernel refinements}
 
-Retrieval contracts are often pairwise.  The module
-\lean{FinitePairQuotient.lean} packages query and document compressions
+Retrieval contracts are naturally pairwise.  The module
+\lean{FiniteProductQuotient.lean} defines the generic product map for two
+compressions
 \[
   C_q:\Omega_q\to Z_q,\qquad C_d:\Omega_d\to Z_d
 \]
 into the product quotient
 \[
-  \operatorname{pairQuotient}(q,d)=(C_q(q),C_d(d)).
+  \operatorname{productMap}(q,d)=(C_q(q),C_d(d)).
 \]
-Theorems
+The product fiber-invariance contract says that same compressed query code and
+same compressed document code force the same pairwise target behavior:
+\[
+  C_q(q_1)=C_q(q_2),\quad C_d(d_1)=C_d(d_2)
+  \quad\Longrightarrow\quad
+  y(q_1,d_1)=y(q_2,d_2).
+\]
+Lean exposes this through
+\begin{leanblock}
+\lean{productMap}\quad
+\lean{ProductFiberInvariant}\quad
+\lean{ruleFactorsThrough_product_fiberInvariant}\\
+\lean{productFiberInvariant_ruleFactorsThrough_of_surjective}\\
+\lean{ruleFactorsThrough_productMap_image_iff_productFiberInvariant}
+\end{leanblock}
+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.
+
+Finite pair samples get the corresponding falsifier:
+\begin{leanblock}
+\lean{ProductSampleConsistent}\quad
+\lean{productSampleConsistent_of_ruleFactorsThrough}\\
+\lean{productSampleConsistent_iff_exists_productRuleFitsSample}\\
+\lean{no_productQuotientTarget_of_sample_collision}
+\end{leanblock}
+If two sampled query-document pairs have the same compressed query code and the
+same compressed document code but different labels, then no product-quotient
+rule fits that labeled sample.
+
+The same module records two useful production refinements.  First, a globally
+product-factorized target specializes to a document quotient rule at each fixed
+query, but fixed-query sufficiency alone is weaker than the global product
+contract because queries with the same compressed query code must induce the
+same quotient-level document rule:
+\begin{leanblock}
+\lean{ruleFactorsThrough_product_fixedLeft}\quad
+\lean{ruleFactorsThrough_product_fixedRight}
+\end{leanblock}
+Second, multi-target retrieval signatures are componentwise:
+\begin{leanblock}
+\lean{RuleFactorsThrough.product_pair_iff}\quad
+\lean{ProductSampleConsistent.prod_iff}
+\end{leanblock}
+Thus a combined pipeline target factors through the product quotient exactly
+when each component target does.
+
+Ranking comparisons are handled by a three-field comparison observation:
+\begin{leanblock}
+\lean{ComparisonObs}\quad
+\lean{comparisonMap}\quad
+\lean{ComparisonFiberInvariant}\\
+\lean{rankByScore}\quad
+\lean{rankByScore_factorsThrough_of_score_factorsThrough}
+\end{leanblock}
+If a pairwise score factors through the query/document product quotient, then
+the score-induced comparison ``document \(d_1\) ranks no higher than document
+\(d_2\) 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.
+
+\lean{FinitePairQuotient.lean} remains as a retrieval-facing wrapper around the
+generic product API:
 \begin{leanblock}
-\lean{pairQuotient_eq_iff}\\
-\lean{pairRuleFactorsThrough_same_on_quotient_fibers}\\
+\lean{pairQuotient_eq_iff}\quad
+\lean{pairRuleFactorsThrough_same_on_quotient_fibers}\quad
 \lean{no_pair_compatible_target_of_sample_collision}
 \end{leanblock}
-say that a pairwise target factoring through the product quotient must be
-constant on same compressed query bucket and same compressed document bucket,
-and that a same-product-bucket label disagreement is the corresponding finite
-falsifier.
 
 \lean{QuotientRefinementKernel.lean} gives the kernel view of refinement.
 Finer quotients have smaller kernels; coarser quotients have larger fibers.
@@ -1194,6 +1257,7 @@ \section{Lean Verification Surface}
 \lean{FiniteQuotientImage}\quad
 \lean{QuotientKernel}\\
 \lean{FiniteFiberTopology}\quad
+\lean{FiniteProductQuotient}\quad
 \lean{FinitePairQuotient}\quad
 \lean{QuotientRefinementKernel}\\
 \lean{FiniteObservationWindow}\quad
diff --git a/docs/paper/ordvec_formalization_paper.txt b/docs/paper/ordvec_formalization_paper.txt
index a56418b..93b8da5 100644
--- a/docs/paper/ordvec_formalization_paper.txt
+++ b/docs/paper/ordvec_formalization_paper.txt
@@ -2,19 +2,21 @@ Finite Quotient Sufficiency, Search Constraints, Profile Stability, and
 Bitmap Overlap Calibration
 A mathematical paper extracted from the OrdvecFormalization Lean development
 June 2026
+
 Abstract
-This paper summarizes a Lean 4 formalization [7, 8] of a finite decision-theoretic pipeline
-for quotient-based candidate admission. The development proves, in ordinary finite probability
-spaces, that if the Bayes-relevant evidence for a binary admission problem factors through a
-quotient, then an optimal deterministic rule can also factor through that quotient. It then
-formalizes the structural consequences of such a contract: quotient-compatible targets are constant
-on quotient fibers; same-fiber label disagreements are formal falsifiers; observed finite samples
-determine observed buckets but leave reachable unobserved image buckets freely assignable; the
-reachable image quotient is surjective by construction; kernel containment exactly characterizes
-safe compression; finite samples decompose into observed fiber clumps; pair quotients and
-refinement kernels constrain retrieval-style hypotheses; finite observation windows turn families
-of lossy probes into joint quotient codes whose kernels shrink with added coordinates; and any
-non-injective quotient necessarily forgets some possible full-space distinction.
+This paper summarizes a Lean 4 formalization [7, 8] of a finite decision-theoretic pipeline for
+quotient-based candidate admission. The development proves, in ordinary finite probability spaces,
+that if the Bayes-relevant evidence for a binary admission problem factors through a quotient,
+then an optimal deterministic rule can also factor through that quotient. It then formalizes the
+structural consequences of such a contract: quotient-compatible targets are constant on quotient
+fibers; same-fiber label disagreements are formal falsifiers; observed finite samples determine
+observed buckets but leave reachable unobserved image buckets freely assignable; the reachable
+image quotient is surjective by construction; kernel containment exactly characterizes safe
+compression; finite samples decompose into observed fiber clumps; product quotients constrain
+pairwise, multi-target, and ranking-style hypotheses; refinement kernels order quotient strength;
+finite observation windows turn families of lossy probes into joint quotient codes whose kernels
+shrink with added coordinates; and any non-injective quotient necessarily forgets some possible
+full-space distinction.
 The second half of the development specializes this abstract quotient story to score-margin
 stability, finite profile-stability certificates, ordered evidence, monotone likelihood ratios, canonical finite exponential tilts, literal bitmap overlap, query-stabilizer symmetry, and the exact
 hypergeometric tail under the idealized uniform constant-weight bitmap null. The main bitmap
@@ -38,12 +40,13 @@ Its statistical backdrop is the classical theory of sufficiency, statistical dec
 comparison of experiments [1, 2, 3, 4]. A full observation space may contain rich geometric, semantic,
 or residual information. A quotient map
 Q:Ω→Z
-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.
+
 1
 
-The Lean repository answers this question in a finite setting. It proves that under exact
+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
 factorization assumptions, quotient-form rules are sufficient for Bayes-optimal admission. It also
 proves the converse kind of structural pressure: if a rule, target, evidence statistic, or likelihood
 ratio factors through a quotient, then it must be constant on quotient fibers. Therefore a single
@@ -74,24 +77,26 @@ buckets, and proves the fiber-invariance constraints that any quotient-compatibl
 It then turns those constraints into a finite search calculus: observed same-bucket disagreements are
 falsifiers, observed buckets fix the fitted bucket labels, reachable unobserved image buckets remain
 free, and compatible targets form a finite bucket-level version space.
-The middle layer replaces ambient-codomain reasoning with image reasoning. A compression map
-is treated as surjective onto its reachable image; factorization through that image is equivalent to
-containment of the compression kernel inside the target kernel. Sample fibers are counted as observed
-clumps; retrieval-style query/document decisions are handled by product quotients; refinement is
-characterized by kernel inclusion; and score approximation plus margin separation gives a sufficient
-condition for threshold decisions to remain quotient-factorized. Between refinement and score
-margins, the observation-window layer proves that a finite family of lossy probes is target-sufficient
-exactly when agreement on the whole joint code preserves the target. The profile-stability layer
-packages supplied finite score certificates and composes their errors.
+The middle layer replaces ambient-codomain reasoning with image reasoning. A compression
+map is treated as surjective onto its reachable image; factorization through that image is equivalent
+to containment of the compression kernel inside the target kernel. Sample fibers are counted as
+observed clumps; product quotients handle query/document decisions, multi-target signatures,
+and score-induced ranking comparisons; refinement is characterized by kernel inclusion; and score
+approximation plus margin separation gives a sufficient condition for threshold decisions to remain
+quotient-factorized. Between refinement and score margins, the observation-window layer proves
+that a finite family of lossy probes is target-sufficient exactly when agreement on the whole joint
+code preserves the target. The profile-stability layer packages supplied finite score certificates and
+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
-the same cutoff. Canonical finite overlap tilts instantiate the ordered-evidence assumptions. Bitmap
+2
+
+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.
-2
 
-3
+3
 
 Finite Experiments and Bayes Admission
 
@@ -139,13 +144,13 @@ 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 ω ∈ Ω.
-This is the formal predicate RuleFactorsThrough.
+3
+
+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 ⊆ Ω.
-3
-
-This is checked by exists_quotientPullback_finiteWeightedRisk_le. A useful sufficient
+This is checked by exists_quotientPullback_finiteWeightedRisk_le. A useful sufficient
 condition is likelihood-ratio factorization, paralleling the classical sufficiency factorization viewpoint
 [1, 2]. With
 LR(ω) = p1 (ω)/p0 (ω),
@@ -200,13 +205,14 @@ 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.
-The important qualification is the codomain. For an ambient compression C : Ω → Z, Lean
+4
+
+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.
-4
 
-4.3
+4.3
 
 What should not be inferred
 
@@ -254,7 +260,6 @@ 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
@@ -426,26 +431,74 @@ sample.
 
 6.4
 
-Pair quotients and kernel refinements
+Product quotients, ranking, and kernel refinements
 
-Retrieval contracts are often pairwise. The module FinitePairQuotient.lean packages query and
-document compressions
+Retrieval contracts are naturally pairwise. The module FiniteProductQuotient.lean defines the
+generic product map for two compressions
 Cq : Ωq → Zq ,
-Cd : Ωd → Zd
 into the product quotient
 
-pairQuotient(q, d) = (Cq (q), Cd (d)).
+Cd : Ωd → Zd
 
-Theorems
-pairQuotient_eq_iff
-pairRuleFactorsThrough_same_on_quotient_fibers
-no_pair_compatible_target_of_sample_collision
+productMap(q, d) = (Cq (q), Cd (d)).
+
+The product fiber-invariance contract says that same compressed query code and same compressed
+document code force the same pairwise target behavior:
+Cq (q1 ) = Cq (q2 ),
 
+Cd (d1 ) = Cd (d2 )
+
+Lean exposes this through
 8
 
-say that a pairwise target factoring through the product quotient must be constant on same
-compressed query bucket and same compressed document bucket, and that a same-product-bucket
-label disagreement is the corresponding finite falsifier.
+=⇒
+
+y(q1 , d1 ) = y(q2 , d2 ).
+
+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.
+Finite pair samples get the corresponding falsifier:
+ProductSampleConsistent productSampleConsistent_of_ruleFactorsThrough
+productSampleConsistent_iff_exists_productRuleFitsSample
+no_productQuotientTarget_of_sample_collision
+
+If two sampled query-document pairs have the same compressed query code and the same compressed
+document code but different labels, then no product-quotient rule fits that labeled sample.
+The same module records two useful production refinements. First, a globally product-factorized
+target specializes to a document quotient rule at each fixed query, but fixed-query sufficiency alone
+is weaker than the global product contract because queries with the same compressed query code
+must induce the same quotient-level document rule:
+ruleFactorsThrough_product_fixedLeft
+
+ruleFactorsThrough_product_fixedRight
+
+Second, multi-target retrieval signatures are componentwise:
+RuleFactorsThrough.product_pair_iff
+
+ProductSampleConsistent.prod_iff
+
+Thus a combined pipeline target factors through the product quotient exactly when each component
+target does.
+Ranking comparisons are handled by a three-field comparison observation:
+ComparisonObs comparisonMap ComparisonFiberInvariant
+rankByScore rankByScore_factorsThrough_of_score_factorsThrough
+
+If a pairwise score factors through the query/document product quotient, then the score-induced
+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.
+FinitePairQuotient.lean remains as a retrieval-facing wrapper around the generic product
+API:
+pairQuotient_eq_iff pairRuleFactorsThrough_same_on_quotient_fibers
+no_pair_compatible_target_of_sample_collision
+
 QuotientRefinementKernel.lean gives the kernel view of refinement. Finer quotients have
 smaller kernels; coarser quotients have larger fibers. For a surjective fine quotient, refinement is
 equivalent to kernel inclusion:
@@ -458,8 +511,9 @@ 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
+7
 
 Windowed Quotients and Probe Families
 
@@ -510,9 +564,7 @@ WindowSeparates
 
 windowSeparates_iff
 
-9
-
-but the target-invariance theorem is the production-relevant one. OrdVec does not need a probe
+but the target-invariance theorem is the production-relevant one. OrdVec does not need a probe
 family to reconstruct every raw distinction. It needs the joint code to separate the distinctions used
 by the task target.
 Longer windows are monotone refinements of shorter windows. If m ≤ n, then Wn refines Wm ,
@@ -528,7 +580,9 @@ 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
 
-If two sampled points have the same whole window code and different labels, no window-factorized
+10
+
+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:
@@ -550,9 +604,11 @@ The formalization does not try to prove that contrastive training or any particu
 proves a sufficient condition for threshold decisions to survive quotient approximation.
 
 8.1
-Let
 
 Margin-stable threshold admission
+
+Let
+
 s:Ω→R
 
 and
@@ -568,9 +624,7 @@ for all ω.
 It defines ThresholdMargin to mean every full score is separated from a threshold τ by more than
 ε. The Boolean admission rule is
 thresholdAdmitBool(s, τ )(ω) = 1{τ ≤ s(ω)}.
-10
-
-Theorem 8.1 (Margin-stable threshold equality). If s̃ is within ε of s, and every full-score
+Theorem 8.1 (Margin-stable threshold equality). If s̃ is within ε of s, and every full-score
 decision margin around τ exceeds ε, then thresholding s̃ gives exactly the same Boolean decisions as
 thresholding s.
 The checked names are:
@@ -583,7 +637,9 @@ 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.
 
-8.2
+11
+
+8.2
 
 Finite profile certificates
 
@@ -623,9 +679,7 @@ FiniteLikelihoodRatioFactorsThroughOrderedEvidence
 Theorem 9.1 (Ordered quotient threshold sufficiency). If the likelihood ratio is a monotone function
 of ordered quotient evidence, then some pulled-back ordered threshold has weighted risk no larger
 than every deterministic full-space rule.
-11
-
-This is checked by:
+This is checked by:
 exists_orderedQuotientThreshold_finiteWeightedRisk_le_of_orderedEvidenceFactor
 
 It rests on two lower layers: MLR.lean, which proves that monotone likelihood ratio makes Bayes
@@ -638,7 +692,9 @@ weighted_threshold_bayesRisk_optimal
 threshold_bayesRisk_optimal
 costed_threshold_bayesRisk_optimal
 
-10
+12
+
+10
 
 Calibrated Evidence
 
@@ -673,9 +729,7 @@ finiteLikelihoodRatio_finiteExponentialTilt_eq_factor
 finiteExponentialTilt_likelihoodRatioFactorsThroughOrderedEvidence
 finiteExponentialTilt_likelihoodRatioFactorsThroughOverlapEvidence
 
-12
-
-OverlapSufficiency.lean specializes ordered threshold sets to actual overlap coordinates,
+OverlapSufficiency.lean specializes ordered threshold sets to actual overlap coordinates,
 with overlapQuotientThresholdSet_eq_orderedQuotientThresholdSet identifying the overlap
 threshold set with the ordered threshold set. The Bayes-risk wrappers in OverlapBayesOptimal.
 lean expose this as
@@ -689,8 +743,9 @@ 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
+12
 
 Bitmap Symmetry
 
@@ -722,10 +777,7 @@ literal overlap threshold events to a closed-form null mass.
 Fix dimension D, active count K ≤ D, and a query bitmap q with |q| = K. The constant-weight
 document space is
 BD,K = {d ⊆ {1, . . . , D} : |d| = K}.
-
-13
-
-The literal overlap is
+The literal overlap is
 |q ∩ d|.
 Under the uniform law on BD,K , the event
 {d : |q ∩ d| ≥ t}
@@ -745,6 +797,8 @@ overlapQuotientThresholdSet_constantWeightBitmapOverlapEvidence_eq
 
 14
 
+14
+
 Main Bitmap Theorem
 
 The main checked theorem is
@@ -769,9 +823,7 @@ 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.
 
-14
-
-15
+15
 
 FNCH and Overlap-Null Wrappers
 
@@ -799,8 +851,9 @@ 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
+16
 
 How This Narrows Empirical Search
 
@@ -822,9 +875,7 @@ assumed route to quotient sufficiency.
 These are global mathematical necessities. Finite probes can only sample them, but any sampled
 violation is a formal falsifier for the exact quotient contract.
 
-15
-
-16.2
+16.2
 
 What finite samples can and cannot prove
 
@@ -859,7 +910,9 @@ 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;
-then some overlap-tail cutoff is Bayes-optimal and has a hypergeometric null tail mass. Empirical
+16
+
+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.
@@ -878,9 +931,7 @@ or overlap quotient.
 • It does not prove that same quotient value means same full embedding geometry.
 • It does not prove representation completeness.
 • It does not prove empirical calibration or real-corpus null adequacy.
-16
-
-• It does not prove that the textbook hypergeometric distribution is the deployment null for
+• It does not prove that the textbook hypergeometric distribution is the deployment null for
 real embeddings.
 • It does not define a manifest schema, estimate encoder distortion, or prove that real encoders
 globally satisfy the supplied profile assumptions.
@@ -904,13 +955,16 @@ make verify
 make check-doc-names
 make audit
 make lint
-The expected axiom baseline printed by the verification surface is:
+17
+
+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:
 FiniteExperiment FiniteQuotientSearch QuotientConstraints FiniteQuotientImage
 QuotientKernel
-FiniteFiberTopology FinitePairQuotient QuotientRefinementKernel
+FiniteFiberTopology FiniteProductQuotient FinitePairQuotient
+QuotientRefinementKernel
 FiniteObservationWindow ScoreMarginQuotient ProfileStability FiniteBayesRisk
 OrdinalSufficiency CalibratedEvidence OverlapSufficiency CanonicalTilt
 OverlapBayesOptimal BitmapIncidence BitmapCalibration BitmapNull
@@ -924,9 +978,7 @@ Conclusion
 The Lean development proves a finite theorem stack with two complementary messages.
 First, if the Bayes-relevant evidence for a binary admission task factors through a quotient, then
 quotient-form admission can be globally optimal. In the bitmap specialization, under the canonical
-17
-
-overlap-tilt signal model and uniform constant-weight bitmap null, this optimal quotient-form rule
+overlap-tilt signal model and uniform constant-weight bitmap null, this optimal quotient-form rule
 is a literal overlap tail and its null mass is the checked hypergeometric tail.
 Second, the quotient contract is structurally strong. It forces fiber invariance, gives finite
 same-bucket falsifiers, bounds compatible target search by quotient-bucket assignments, and shows
@@ -949,7 +1001,9 @@ 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.
-[7] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming
+18
+
+[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.
@@ -957,6 +1011,6 @@ https://doi.org/10.1007/978-3-030-79876-5_37.
 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.
 
-18
+19
 
 
\ No newline at end of file
diff --git a/docs/proof-spine.md b/docs/proof-spine.md
index 5885c4f..eb563cc 100644
--- a/docs/proof-spine.md
+++ b/docs/proof-spine.md
@@ -11,7 +11,7 @@ Finite observations
   -> quotient search / version-space reduction
   -> generic quotient constraints / fiber equivalence
   -> reachable quotient image / kernel containment
-  -> finite fiber topology / pair quotients / refinement kernels
+  -> finite fiber topology / product and pair quotients / refinement kernels
   -> finite observation windows / target-separating probe families
   -> score-margin threshold stability
   -> finite profile-stability certificates
@@ -37,12 +37,13 @@ The algebraic and decision-theoretic layers do different jobs:
   `FiniteFiberTopology.lean` keep quotient reasoning on the reachable image,
   relate factorization to kernel containment, and count the observed fiber
   clumps induced by finite samples.
-- `FinitePairQuotient.lean`, `QuotientRefinementKernel.lean`, and
-  `FiniteObservationWindow.lean` add retrieval-style pair quotients,
-  refinement as kernel inclusion, and a generic windowed-observation bridge:
-  individual lossy probes may collide, while a finite family/window is
-  sufficient for a target exactly when joint-code agreement preserves that
-  target.
+- `FiniteProductQuotient.lean`, `FinitePairQuotient.lean`,
+  `QuotientRefinementKernel.lean`, and `FiniteObservationWindow.lean` add
+  generic product quotients for pairwise, multi-target, and ranking-comparison
+  targets; a retrieval-style pair wrapper; refinement as kernel inclusion; and
+  a generic windowed-observation bridge: individual lossy probes may collide,
+  while a finite family/window is sufficient for a target exactly when
+  joint-code agreement preserves that target.
 - `ScoreMarginQuotient.lean` adds a sufficient margin-stability theorem for
   threshold admission under score approximation.
 - `ProfileStability.lean` packages supplied encoder-distortion and
@@ -68,7 +69,8 @@ FiniteExperiment
   -> FiniteQuotientSearch
   -> QuotientConstraints
   -> FiniteQuotientImage / QuotientKernel / FiniteFiberTopology
-  -> FinitePairQuotient / QuotientRefinementKernel / FiniteObservationWindow
+  -> FiniteProductQuotient / FinitePairQuotient
+  -> QuotientRefinementKernel / FiniteObservationWindow
   -> ScoreMarginQuotient
   -> ProfileStability
   -> FiniteBayesRisk
@@ -135,19 +137,32 @@ imports bitmap definitions from `BitmapNull`, but it does not depend on
    observed fiber sizes, collisions are exactly failure of sample injectivity,
    and too many sampled points for the observed bucket count forces a collision.
 
-7. `FinitePairQuotient.lean`
-   Packages product quotients for query/document pairs. It proves that
-   pairwise targets factoring through the product quotient are invariant under
-   same compressed query and document buckets, and gives the corresponding
+7. `FiniteProductQuotient.lean`
+   Defines the generic product quotient `productMap Q₁ Q₂` and its fiber
+   invariance contract. It proves that product factorization implies invariance
+   under same left and right compressed buckets; that surjective and
+   image-restricted product quotients recover factorization from that invariance;
+   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;
+   and that a score factoring through the query/document product quotient
+   induces ranking comparisons factoring through the corresponding
+   query/document/document comparison quotient.
+
+8. `FinitePairQuotient.lean`
+   Packages the generic product quotient under query/document names for
+   retrieval-facing docs and compatibility. It keeps the small API for
+   `pairQuotient`, same compressed query/document bucket invariance, and the
    finite same-product-bucket label-disagreement falsifier.
 
-8. `QuotientRefinementKernel.lean`
+9. `QuotientRefinementKernel.lean`
    Relates quotient refinement to kernel inclusion. Refinement implies
    fine-kernel collisions are coarse-kernel collisions; conversely, kernel
    inclusion builds a refinement when the fine quotient is surjective, in
    particular for image quotients.
 
-9. `FiniteObservationWindow.lean`
+10. `FiniteObservationWindow.lean`
    Defines arbitrary observation-family maps and countable-prefix window maps.
    It proves that a window kernel is exactly coordinatewise agreement; that
    target factorization through the reachable image of a window is equivalent
@@ -159,14 +174,14 @@ imports bitmap definitions from `BitmapNull`, but it does not depend on
    window injectivity is recorded as the special case where the target is
    identity.
 
-10. `ScoreMarginQuotient.lean`
+11. `ScoreMarginQuotient.lean`
    Gives a sufficient-condition theorem for score-based admission: if an
    approximate quotient score is uniformly close to a full score and full-score
    threshold margins exceed the error, then Boolean threshold admission is
    unchanged and factors through the same image quotient when the approximate
    score does.
 
-11. `ProfileStability.lean`
+12. `ProfileStability.lean`
    Packages two supplied finite score certificates: an
    `EncoderDistortionProfile`, saying an encoder score is uniformly close to a
    source/task score, and a `QuotientGeometryProfile`, saying a quotient score
@@ -175,72 +190,72 @@ imports bitmap definitions from `BitmapNull`, but it does not depend on
    preservation, image-quotient factorization, and kernel containment under the
    composed margin condition.
 
-12. `FiniteBayesRisk.lean`
+13. `FiniteBayesRisk.lean`
    Gives Bayes-risk and cost-sensitive Bayes-risk names to the generic finite
    weighted-risk API.
 
-13. `OrdinalSufficiency.lean`
+14. `OrdinalSufficiency.lean`
    Adds ordered quotient evidence. If the full likelihood ratio is a monotone
    function of ordered quotient evidence, then some pulled-back ordinal
    threshold is Bayes-optimal among all deterministic full-space rules.
 
-14. `CalibratedEvidence.lean`
+15. `CalibratedEvidence.lean`
    Combines the ordered threshold theorem with an externally supplied
    `OrderedTailCalibration`, returning one cutoff that is both Bayes-optimal and
    calibrated by the supplied equality. This layer is graph-neutral and does
    not prove empirical null adequacy.
 
-15. `OverlapSufficiency.lean`
+16. `OverlapSufficiency.lean`
    Specializes the ordered quotient bridge to overlap coordinates, exposing the
    actual-overlap threshold set used by later theorems.
 
-16. `CanonicalTilt.lean`
+17. `CanonicalTilt.lean`
    Instantiates the factorization contract with a finite exponential family over
    arbitrary full observations. Tilting a positive base law by quotient-level
    overlap evidence makes the likelihood ratio a monotone function of that
    evidence.
 
-17. `OverlapBayesOptimal.lean`
+18. `OverlapBayesOptimal.lean`
    Uses the finite Bayes-risk and cost-sensitive wrappers to expose the
    canonical overlap-tilt theorem in Bayes-risk form.
 
-18. `BitmapIncidence.lean`
+19. `BitmapIncidence.lean`
    Defines the constant-weight bitmap subtype, the uniform finite law on that
    subtype, literal bitmap overlap evidence, and the bridge showing pulled-back
    actual-overlap thresholds are literal bitmap overlap tail events.
 
-19. `BitmapCalibration.lean`
+20. `BitmapCalibration.lean`
    Connects the canonical overlap-tilt theorem to constant-weight bitmap
    observations. It proves that the Bayes-optimal pulled-back cutoff is the
    literal bitmap overlap tail event and that the uniform bitmap null assigns
    that event the corresponding hypergeometric upper-tail probability.
 
-20. `BitmapSymmetry.lean`
+21. `BitmapSymmetry.lean`
    Defines coordinate permutations, the query stabilizer, and the induced action
    on bitmaps. It proves query-stabilizer permutations preserve overlap, that
    equal-cardinality bitmaps with equal query overlap lie in the same
    query-stabilizer orbit, and that every invariant constant-weight bitmap
    statistic factors through literal overlap.
 
-21. `FiniteDecision.lean`
+22. `FiniteDecision.lean`
    Proves that every monotone predicate on a finite ordered support is
    represented by a threshold cut, including accept-all and reject-all boundary
    cuts.
 
-22. `MLR.lean`
+23. `MLR.lean`
    States monotone likelihood ratio by cross multiplication and proves it makes
    weighted pointwise Bayes admission monotone. It also connects admission to
    the usual likelihood-ratio cutoff when denominators are positive.
 
-23. `BayesThreshold.lean`
+24. `BayesThreshold.lean`
     Proves Bayes and cost-sensitive Bayes thresholds minimize finite pointwise
     risk by summing pointwise inequalities.
 
-24. `ExponentialTilt.lean`
+25. `ExponentialTilt.lean`
     Proves positive finite exponential tilts have monotone likelihood ratio as
     the tilt parameter increases.
 
-25. `FNCH.lean`
+26. `FNCH.lean`
     Connects literal actual-overlap Fisher noncentral hypergeometric weights to
     the shifted exponential-tilt implementation after normalization.
 
diff --git a/docs/rag-pipeline-guide.md b/docs/rag-pipeline-guide.md
index 5a81e12..b8a0afe 100644
--- a/docs/rag-pipeline-guide.md
+++ b/docs/rag-pipeline-guide.md
@@ -115,6 +115,18 @@ same-joint-code examples preserve the target behavior. Same-joint-code
 relevance disagreements are the finite falsifiers to track before treating a
 probe bundle as a safe first-stage gate.
 
+For retrieval specifically, the natural code is often a product code:
+
+```text
+(compressed query code, compressed document code)
+```
+
+The corresponding audit asks whether same product-code pairs preserve the
+pairwise behavior being claimed: admission, relevance, rerank bucket, or a
+score-induced ordering comparison. A fixed query can look document-only, but the
+global contract is stronger because queries with the same compressed query code
+must induce the same quotient-level document behavior.
+
 ## Why This Matters In A Real RAG System
 
 The useful real-world reading is not "Lean proves my retrieval stack works."
diff --git a/docs/reviewer-brief.md b/docs/reviewer-brief.md
index 962d711..fa0b03a 100644
--- a/docs/reviewer-brief.md
+++ b/docs/reviewer-brief.md
@@ -119,6 +119,11 @@ The proof is intentionally decomposed:
 - `FiniteQuotientImage.lean` and `QuotientKernel.lean`: reachable image
   quotients and the kernel-containment characterization of target
   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.
+- `FinitePairQuotient.lean`: retrieval-facing query/document wrapper around the
+  generic product quotient API.
 - `FiniteObservationWindow.lean`: finite families/windows of lossy probes,
   target-invariance on joint-code fibers, longer-window refinement, and
   same-window-code falsifiers.
@@ -169,6 +174,9 @@ The expected axiom baseline is:
 - Real encoders are not proved to satisfy quotient/factorization assumptions.
 - Concrete production probe families are not proved globally
   target-sufficient without finite target-invariance evidence.
+- Pairwise retrieval, ranking, and multi-target pipeline decisions are not
+  proved preserved unless the corresponding product quotient contract is
+  empirically supported.
 - Real encoders are not proved to satisfy the query-stabilizer symmetry
   assumption; the symmetry theorem identifies the canonical invariant when that
   assumption is appropriate.
diff --git a/docs/theorem-map.md b/docs/theorem-map.md
index bf5948d..0be58c7 100644
--- a/docs/theorem-map.md
+++ b/docs/theorem-map.md
@@ -5,9 +5,10 @@ the formalization proves finite Bayes decision theorems, a quotient-form
 optimality theorem, a canonical overlap-tilt signal instantiation, a
 group-theoretic bitmap-overlap invariant theorem, a supplied calibrated-evidence
 wrapper, a finite quotient-search layer, a generic quotient-constraint layer,
-reachable-image/kernel/fiber layers, a finite observation-window layer for
-target-separating probe families, score-margin profile-stability layers, and
-an exact constant-weight bitmap null.
+reachable-image/kernel/fiber layers, a finite product-quotient layer for
+pairwise and ranking targets, a finite observation-window layer for
+target-separating probe families, score-margin profile-stability layers, and an
+exact constant-weight bitmap null.
 
 ## Main Claim
 
@@ -136,8 +137,8 @@ OrdvecFormalization.exists_pair_quotientTarget_factorsThrough_and_otherTarget_no
 OrdvecFormalization.boolRuleFactorsThrough_positiveSet_eq_quotientPullback
 ```
 
-Quotient image, kernel, fiber topology, pair quotient, refinement, margin, and
-profile-stability layer:
+Quotient image, kernel, fiber topology, product/pair quotient, refinement,
+margin, and profile-stability layer:
 
 ```lean
 OrdvecFormalization.QuotientImage
@@ -163,6 +164,32 @@ OrdvecFormalization.sample_card_eq_sum_fiberSize_observed
 OrdvecFormalization.hasCollision_iff_not_injectiveOnSample
 OrdvecFormalization.hasCollision_of_card_gt_observedBuckets_card
 OrdvecFormalization.no_compatible_target_of_same_bucket_label_disagreement
+OrdvecFormalization.productMap
+OrdvecFormalization.productMap_eq_iff
+OrdvecFormalization.ProductFiberInvariant
+OrdvecFormalization.kernelContainedInTarget_productMap_iff_productFiberInvariant
+OrdvecFormalization.ruleFactorsThrough_product_fiberInvariant
+OrdvecFormalization.productFiberInvariant_ruleFactorsThrough_of_surjective
+OrdvecFormalization.ruleFactorsThrough_productMap_image_iff_productFiberInvariant
+OrdvecFormalization.ruleFactorsThrough_product_fixedLeft
+OrdvecFormalization.ruleFactorsThrough_product_fixedRight
+OrdvecFormalization.ProductSampleConsistent
+OrdvecFormalization.productSampleConsistent_iff_sampleConsistent_productMap
+OrdvecFormalization.productSampleConsistent_of_ruleFactorsThrough
+OrdvecFormalization.productSampleConsistent_iff_exists_productRuleFitsSample
+OrdvecFormalization.no_productQuotientTarget_of_sample_collision
+OrdvecFormalization.ObservedProductQuotients
+OrdvecFormalization.UnobservedReachableProductQuotients
+OrdvecFormalization.card_productQuotientRules
+OrdvecFormalization.RuleFactorsThrough.product_pair_iff
+OrdvecFormalization.ProductSampleConsistent.prod_iff
+OrdvecFormalization.ComparisonObs
+OrdvecFormalization.comparisonMap
+OrdvecFormalization.comparisonMap_eq_iff
+OrdvecFormalization.ComparisonFiberInvariant
+OrdvecFormalization.ruleFactorsThrough_comparison_fiberInvariant
+OrdvecFormalization.rankByScore
+OrdvecFormalization.rankByScore_factorsThrough_of_score_factorsThrough
 OrdvecFormalization.pairQuotient
 OrdvecFormalization.pairQuotient_eq_iff
 OrdvecFormalization.pairRuleFactorsThrough_same_on_quotient_fibers
@@ -231,7 +258,8 @@ FiniteExperiment
   -> FiniteQuotientSearch
   -> QuotientConstraints
   -> FiniteQuotientImage / QuotientKernel / FiniteFiberTopology
-  -> FinitePairQuotient / QuotientRefinementKernel / FiniteObservationWindow
+  -> FiniteProductQuotient / FinitePairQuotient
+  -> QuotientRefinementKernel / FiniteObservationWindow
   -> ScoreMarginQuotient
   -> ProfileStability
   -> FiniteBayesRisk
@@ -341,6 +369,36 @@ Public Lean names:
 - `hasCollision_iff_not_injectiveOnSample`
 - `hasCollision_of_card_gt_observedBuckets_card`
 - `no_compatible_target_of_same_bucket_label_disagreement`
+- `productMap`
+- `productMap_apply`
+- `productMap_eq_iff`
+- `ProductFiberInvariant`
+- `kernelContainedInTarget_productMap_iff_productFiberInvariant`
+- `ruleFactorsThrough_product_fiberInvariant`
+- `productFiberInvariant_ruleFactorsThrough_of_surjective`
+- `ruleFactorsThrough_productMap_image_iff_productFiberInvariant`
+- `ruleFactorsThrough_product_fixedLeft`
+- `ruleFactorsThrough_product_fixedRight`
+- `ProductSampleConsistent`
+- `productSampleConsistent_iff_sampleConsistent_productMap`
+- `productSampleConsistent_of_ruleFactorsThrough`
+- `productSampleConsistent_iff_exists_productRuleFitsSample`
+- `no_productQuotientTarget_of_sample_collision`
+- `ObservedProductQuotients`
+- `UnobservedReachableProductQuotients`
+- `card_productQuotientRules`
+- `RuleFactorsThrough.product_pair_iff`
+- `ProductSampleConsistent.prod_iff`
+- `ComparisonObs`
+- `comparisonMap`
+- `comparisonMap_left`
+- `comparisonMap_first`
+- `comparisonMap_second`
+- `comparisonMap_eq_iff`
+- `ComparisonFiberInvariant`
+- `ruleFactorsThrough_comparison_fiberInvariant`
+- `rankByScore`
+- `rankByScore_factorsThrough_of_score_factorsThrough`
 - `pairQuotient`
 - `pairQuotient_apply`
 - `pairQuotient_eq_iff`