Skip to content

[codex] Add finite product quotient layer #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
project-navi-bot merged 2 commits into from
Jun 4, 2026
Merged

[codex] Add finite product quotient layer #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b165f84
Add finite product quotient layer
Fieldnote-Echo Jun 4, 2026
0a3b131
Address product quotient review suggestions
Fieldnote-Echo Jun 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions OrdvecFormalization.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 8 additions & 12 deletions OrdvecFormalization/FinitePairQuotient.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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}
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading