Merge pull request #14 from Fieldnote-Echo/codex/finite-product-quotient

[codex] Add finite product quotient layer

Author: project-navi-bot

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

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