[codex] Add product image bounds

[Fieldnote-Echo]

Summary

• add exact reachable product-image equality against component quotient images plus the cardinality equality
• keep the product-image <= theorem as a corollary and add exact product-image quotient-rule counts
• add exact comparison-image equality against the one-left/two-right image box plus the cardinality equality for ranking-style targets
• keep comparison-image <= bounds as corollaries and wire new names into Verify.lean, theorem map, proof spine, reviewer brief, and formalization paper artifacts

Stacking

This PR targets codex/finite-product-quotient and is intended as the remaining PR 5 layer on top of PR #14.

Validation

• lake env lean OrdvecFormalization/FiniteProductQuotient.lean
• make build
• make verify
• make check-doc-names
• make audit
• make lint
• git diff --check
• latexmk -pdf -interaction=nonstopmode -halt-on-error ordvec_formalization_paper.tex
• LaTeX log warning/error scan: clean

[qodo-code-review]

Review Summary by Qodo

Add product and comparison image bounds theorems

✨ Enhancement

Walkthroughs

Description

• Add product image cardinality bounds and reachable image subset theorems
• Add product-image quotient rule count upper bound theorems
• Add comparison image box definition and cardinality bound theorems
• Add comparison observation equivalence and fintype instance
• Wire new definitions and theorems into verification and documentation artifacts

Diagram

flowchart LR
  PM["productMap Q₁ Q₂"]
  PI1["Image Q₁"]
  PI2["Image Q₂"]
  PIP["Product of Images"]
  PIQR["Product Image<br/>Quotient Rules"]
  
  CM["comparisonMap Q₁ Q₂"]
  CIB["Comparison<br/>Image Box"]
  CIQR["Comparison Image<br/>Quotient Rules"]
  
  PM -->|"subset"| PIP
  PI1 -->|"product"| PIP
  PI2 -->|"product"| PIP
  PIP -->|"bounds"| PIQR
  
  CM -->|"subset"| CIB
  CIB -->|"bounds"| CIQR

Loading

File Changes

1. OrdvecFormalization/FiniteProductQuotient.lean ✨ Enhancement +187/-0

Add product and comparison image bound theorems

• Add productMap_image_subset_product_images theorem proving reachable product image is contained
 in product of component images
• Add productMap_image_card_le_product_images_card theorem bounding product image cardinality by
 component image cardinalities
• Add card_productImageQuotientRules theorem computing quotient rule space size on reachable
 product image
• Add card_productImageQuotientRules_le_product_images theorem bounding product image quotient
 rules by component images
• Add comparisonObsEquivProd equivalence between ComparisonObs and triple product type
• Add comparisonObsFintype fintype instance for ComparisonObs
• Add ComparisonImageBox definition for ambient box of reachable comparison codes
• Add comparisonMap_image_subset_imageBox theorem proving comparison image subset of image box
• Add comparisonMap_image_card_le_product_images_card theorem bounding comparison image
 cardinality
• Add card_comparisonImageQuotientRules theorem computing quotient rule space size on reachable
 comparison image
• Add card_comparisonImageQuotientRules_le_product_images theorem bounding comparison image
 quotient rules

OrdvecFormalization/FiniteProductQuotient.lean

---

2. OrdvecFormalization/Verify.lean 🧪 Tests +18/-0

Wire new theorems into verification surface

• Add #check directives for four new product image bound theorems
• Add #check directive for comparisonObsEquivProd equivalence
• Add #check directives for five new comparison image bound theorems
• Add #print axioms directives for all new theorems to verify axiom-free proofs

OrdvecFormalization/Verify.lean

---

3. docs/paper/ordvec_formalization_paper.tex 📝 Documentation +29/-0

Document product and comparison image bounds in paper

• Add section documenting product image bounds with four new theorem names and mathematical notation
• Add section documenting comparison image bounds with five new theorem names and mathematical
 bounds
• Include mathematical formulas for cardinality bounds: `|A|^|image(productMap)| ≤
 |A|^|image(Q₁)||image(Q₂)|` and comparison variant

docs/paper/ordvec_formalization_paper.tex

---

View more (4)

4. docs/paper/ordvec_formalization_paper.txt 📝 Documentation +59/-40

Update paper text with image bound documentation

• Add text documentation for product image bounds with theorem names and mathematical notation
• Add text documentation for comparison image bounds with theorem names and cardinality formulas
• Fix page numbering and formatting issues in text version

docs/paper/ordvec_formalization_paper.txt

---

5. docs/proof-spine.md 📝 Documentation +4/-2

Update proof spine documentation

• Update FiniteProductQuotient.lean description to mention reachable product image bounds
• Add mention of comparison image bounds by one left and two right images

docs/proof-spine.md

---

6. docs/reviewer-brief.md 📝 Documentation +3/-1

Update reviewer brief with image bounds

• Expand FiniteProductQuotient.lean description to include reachable image and cardinality bounds
• Add mention of bounds for both product and comparison quotient rule spaces

docs/reviewer-brief.md

---

7. docs/theorem-map.md 📝 Documentation +20/-0

Add new theorems to theorem map

• Add four new product image bound theorems to theorem map
• Add comparisonObsEquivProd equivalence to theorem map
• Add five new comparison image bound theorems to theorem map
• Update public Lean names section with all new definitions and theorems

docs/theorem-map.md

---

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (2) 📘 Rule violations (0) 🔗 Cross-repo conflicts (0)

1. Duplicated cardinality proof 🐞 Bug ⚙ Maintainability

Description

card_productImageQuotientRules and card_comparisonImageQuotientRules duplicate the same
Fintype.ofFinset + Fintype.card_fun proof pattern, which increases maintenance cost and the
chance the two bounds drift if the underlying library APIs change. This can be eliminated by
extracting a single generic lemma about QuotientImageBucket Q → A cardinality and reusing it for
both productMap and comparisonMap.

Code

OrdvecFormalization/FiniteProductQuotient.lean[R295-309]

+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]
+

Evidence

The two theorems use the same classical block, define the same local Fintype instance with
Fintype.ofFinset ... (by intro z; constructor; intro hz; exact hz), then finish with `rw
[Fintype.card_fun]; congr; simp [QuotientImageBucket], differing only in the map (productMap` vs
comparisonMap).

OrdvecFormalization/FiniteProductQuotient.lean[295-309]
OrdvecFormalization/FiniteProductQuotient.lean[554-568]

Agent prompt

The issue below was found during a code review. Follow the provided context and guidance below and implement a solution

## Issue description
Two theorems (`card_productImageQuotientRules` and `card_comparisonImageQuotientRules`) repeat identical boilerplate to (a) instantiate `Fintype (QuotientImageBucket Q)` via `Fintype.ofFinset` and (b) compute `Fintype.card (QuotientImageBucket Q → A)` via `Fintype.card_fun`. This duplication is easy to accidentally update in one place but not the other.

## Issue Context
Both proofs are the same up to substituting `Q := productMap Q₁ Q₂` vs `Q := comparisonMap Q₁ Q₂`.

## Fix Focus Areas
- OrdvecFormalization/FiniteProductQuotient.lean[295-309]
- OrdvecFormalization/FiniteProductQuotient.lean[554-568]

## Suggested approach
1. Add a generic lemma in an appropriate shared module (likely `OrdvecFormalization/FiniteQuotientSearch.lean` or `FiniteQuotientImage.lean`):
  - Input: `{Ω Ωq A : Type} [Fintype Ω] [DecidableEq Ωq] [Fintype A] (Q : Ω → Ωq)`
  - Output: `Fintype.card (QuotientImageBucket Q → A) = Fintype.card A ^ (QuotientImageFinset Q).card`
  - Proof: the exact existing pattern using `Fintype.ofFinset` + `Fintype.card_fun`.
2. Rewrite both theorems to `simpa`/`exact` the generic lemma applied to `productMap Q₁ Q₂` and `comparisonMap Q₁ Q₂`.
3. Keep the public theorem names intact (since they’re wired into `Verify.lean`/docs).

ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools

---

2. Noisy text extract 🐞 Bug ⚙ Maintainability

Description

The checked-in ordvec_formalization_paper.txt contains obvious pdftotext extraction artifacts
(standalone page numbers like 9 and math fragments like 2) that reduce its usefulness for
grep/review and will churn with pagination changes. Regenerating with pdftotext options (e.g.,
suppressing page breaks) or post-filtering isolated page-number lines would make the artifact stable
and readable.

Code

docs/paper/ordvec_formalization_paper.txt[R511-520]

+9
+
+
+2
+
+|A||im(Cq )||im(Cd )| ,
+again for nonempty finite A.
FinitePairQuotient.lean remains as a retrieval-facing wrapper around the generic product
API:
pairQuotient_eq_iff pairRuleFactorsThrough_same_on_quotient_fibers

Evidence

The .txt extract shows isolated numeric lines (9, 2) inserted between otherwise continuous
prose, consistent with PDF-to-text pagination/math extraction artifacts; the README confirms the
file is generated via pdftotext with default settings.

docs/paper/ordvec_formalization_paper.txt[508-526]
docs/paper/README.md[12-17]

Agent prompt

The issue below was found during a code review. Follow the provided context and guidance below and implement a solution

## Issue description
The tracked paper text extract includes noisy conversion artifacts (standalone page numbers and broken math lines). This makes the file harder to search/review and increases diff churn unrelated to content.

## Issue Context
`docs/paper/README.md` documents regenerating the `.txt` via `pdftotext ordvec_formalization_paper.pdf ordvec_formalization_paper.txt`, which by default preserves page numbers/breaks in a way that can inject these lines.

## Fix Focus Areas
- docs/paper/ordvec_formalization_paper.txt[508-526]
- docs/paper/README.md[12-17]

## Suggested approach
1. Update the documented regeneration command to use `pdftotext` flags that reduce page artifacts (e.g., `-nopgbrk`, optionally `-layout`).
2. Regenerate `ordvec_formalization_paper.txt` using the updated command.
3. (Optional) If page numbers still appear, add a small post-processing step to strip lines that are only an integer page number.

ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools

---

[gemini-code-assist]

Code Review

This pull request introduces theorems and definitions to bound the reachable images and search-space sizes of product and comparison quotient rule spaces, along with updating verification checks and documentation. The reviewer feedback suggests simplifying proofs for card_productImageQuotientRules and card_comparisonImageQuotientRules by removing redundant local Fintype instances, and removing the unnecessary noncomputable modifier from comparisonObsFintype.

Important

The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.

[Fieldnote-Echo]

Addressed Qodo/Gemini review findings in 0a718a1:

• added generic card_quotientImageRules in FiniteQuotientSearch.lean
• rewrote product/comparison reachable-image rule-count proofs through that generic lemma
• removed unnecessary noncomputable from comparisonObsFintype
• regenerated/postprocessed the paper .txt extract with pdftotext -nopgbrk plus standalone page-number stripping, and documented that command in docs/paper/README.md

Local validation:

• make build
• make verify
• make check-doc-names
• make audit
• make lint
• git diff --check
• latexmk -pdf -interaction=nonstopmode -halt-on-error ordvec_formalization_paper.tex

Inline review threads are resolved. I am intentionally leaving the broader paper-vs-full-Lean-stack audit for a separate follow-up PR.