Address product image review findings

Author: Fieldnote-Echo

OrdvecFormalization/FiniteProductQuotient.lean

@@ -323,14 +323,7 @@ theorem card_productImageQuotientRules
     (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]
+  exact card_quotientImageRules (productMap Q₁ Q₂)
 
 /--
 Rules on the reachable product image have search-space size
@@ -422,7 +415,7 @@ def comparisonObsEquivProd (Ω₁ Ω₂ : Type) :
     cases x
     rfl
 
-noncomputable instance comparisonObsFintype {Ω₁ Ω₂ : Type}
+instance comparisonObsFintype {Ω₁ Ω₂ : Type}
     [Fintype Ω₁] [Fintype Ω₂] : Fintype (ComparisonObs Ω₁ Ω₂) :=
   Fintype.ofEquiv (Ω₁ × Ω₂ × Ω₂) (comparisonObsEquivProd Ω₁ Ω₂).symm
 
@@ -621,14 +614,7 @@ theorem card_comparisonImageQuotientRules
     (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]
+  exact card_quotientImageRules (comparisonMap Q₁ Q₂)
 
 /--
 Rules on the reachable comparison image have search-space size

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]

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
@@ -453,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

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.