Add product image bound theorems

Author: Fieldnote-Echo

OrdvecFormalization/FiniteProductQuotient.lean

@@ -254,6 +254,75 @@ 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 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
+  calc
+    (QuotientImageFinset (productMap Q₁ Q₂)).card
+        ≤ ((QuotientImageFinset Q₁).product (QuotientImageFinset Q₂)).card :=
+      Finset.card_le_card (productMap_image_subset_product_images Q₁ Q₂)
+    _ = (QuotientImageFinset Q₁).card * (QuotientImageFinset Q₂).card := by
+      simp
+
+/--
+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
+  classical
+  letI : Fintype (QuotientImageBucket (productMap Q₁ Q₂)) :=
+    Fintype.ofFinset (QuotientImageFinset (productMap Q₁ Q₂)) (by
+      intro z
+      constructor <;> intro hz <;> exact hz)
+  rw [Fintype.card_fun]
+  congr
+  simp [QuotientImageBucket]
+
+/--
+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]
+    [Nonempty 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₂]
+  exact Nat.pow_le_pow_right (Fintype.card_pos)
+    (productMap_image_card_le_product_images_card Q₁ Q₂)
+
 namespace RuleFactorsThrough
 
 /-- Pairing two product-factorized targets is equivalent to factoring both components. -/
@@ -301,6 +370,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
+
+noncomputable 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₂) :
@@ -396,4 +485,102 @@ 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 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
+  calc
+    (QuotientImageFinset (comparisonMap Q₁ Q₂)).card
+        ≤ (ComparisonImageBox Q₁ Q₂).card :=
+      Finset.card_le_card (comparisonMap_image_subset_imageBox Q₁ Q₂)
+    _ ≤ ((QuotientImageFinset Q₁).product
+          ((QuotientImageFinset Q₂).product (QuotientImageFinset Q₂))).card := by
+      unfold ComparisonImageBox
+      exact Finset.card_image_le
+    _ = (QuotientImageFinset Q₁).card *
+        (QuotientImageFinset Q₂).card * (QuotientImageFinset Q₂).card := by
+      simp [mul_assoc]
+
+/--
+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
+  classical
+  letI : Fintype (QuotientImageBucket (comparisonMap Q₁ Q₂)) :=
+    Fintype.ofFinset (QuotientImageFinset (comparisonMap Q₁ Q₂)) (by
+      intro z
+      constructor <;> intro hz <;> exact hz)
+  rw [Fintype.card_fun]
+  congr
+  simp [QuotientImageBucket]
+
+/--
+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]
+    [Nonempty 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₂]
+  exact Nat.pow_le_pow_right (Fintype.card_pos)
+    (comparisonMap_image_card_le_product_images_card Q₁ Q₂)
+
 end OrdvecFormalization

OrdvecFormalization/Verify.lean

@@ -198,9 +198,14 @@ namespace OrdvecFormalization
 #check @ObservedProductQuotients
 #check @UnobservedReachableProductQuotients
 #check @card_productQuotientRules
+#check @productMap_image_subset_product_images
+#check @productMap_image_card_le_product_images_card
+#check @card_productImageQuotientRules
+#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 +215,11 @@ namespace OrdvecFormalization
 #check @ruleFactorsThrough_comparison_fiberInvariant
 #check @rankByScore
 #check @rankByScore_factorsThrough_of_score_factorsThrough
+#check @ComparisonImageBox
+#check @comparisonMap_image_subset_imageBox
+#check @comparisonMap_image_card_le_product_images_card
+#check @card_comparisonImageQuotientRules
+#check @card_comparisonImageQuotientRules_le_product_images
 #check @pairQuotient
 #check @pairQuotient_apply
 #check @pairQuotient_eq_iff
@@ -482,11 +492,19 @@ 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_card_le_product_images_card
+#print axioms card_productImageQuotientRules
+#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_card_le_product_images_card
+#print axioms card_comparisonImageQuotientRules
+#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

docs/paper/ordvec_formalization_paper.pdf

@@ -612,6 +612,21 @@ \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 bounded by the component images:
+\begin{leanblock}
+\lean{productMap_image_subset_product_images}\\
+\lean{productMap_image_card_le_product_images_card}\\
+\lean{card_productImageQuotientRules}\\
+\lean{card_productImageQuotientRules_le_product_images}
+\end{leanblock}
+In symbols, reachable product codes sit inside
+\(\im(C_q)\times\im(C_d)\), so image-level pair rules have size
+\[
+  \card{A}^{\card{\im(C_q,C_d)}}
+  \le
+  \card{A}^{\card{\im(C_q)}\card{\im(C_d)}}
+\]
+for nonempty finite label type \(A\).
 
 Finite pair samples get the corresponding falsifier:
 \begin{leanblock}
@@ -655,6 +670,20 @@ \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 bounded by one left image and two
+right images:
+\begin{leanblock}
+\lean{ComparisonImageBox}\quad
+\lean{comparisonMap_image_subset_imageBox}\\
+\lean{comparisonMap_image_card_le_product_images_card}\\
+\lean{card_comparisonImageQuotientRules}\\
+\lean{card_comparisonImageQuotientRules_le_product_images}
+\end{leanblock}
+Thus comparison-level rules are bounded by
+\[
+  \card{A}^{\card{\im(C_q)}\card{\im(C_d)}^2},
+\]
+again for nonempty finite \(A\).
 
 \lean{FinitePairQuotient.lean} remains as a retrieval-facing wrapper around the
 generic product API: