Local good-choice count depends only on the membership pattern

Proved

gpy_localGoodChoiceFinset_card_congr

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

The cardinality of the local good-choice finset at a prime p depends only on the truth values of the two membership propositions, so replacing them by equivalent propositions leaves the count unchanged. This is an unconditional elementary lemma about the finite local count.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_localGoodChoiceFinset_card_congr {k : ℕ} {h : Fin k → ℕ} {i : Fin k}
    {p : ℕ} {hd he hd' he' : Prop} [Decidable hd] [Decidable he]
    [Decidable hd'] [Decidable he'] (h1 : hd ↔ hd') (h2 : he ↔ he') :
    ((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
      (ab.1.isSome ↔ hd) ∧ (ab.2.isSome ↔ he) ∧
      (∀ j j', (ab.1 = some j ∨ ab.2 = some j) →
        (ab.1 = some j' ∨ ab.2 = some j') → h j ≡ h j' [MOD p]) ∧
      (∀ j, (ab.1 = some j ∨ ab.2 = some j) → ¬ h i ≡ h j [MOD p]))).card
      = ((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
      (ab.1.isSome ↔ hd') ∧ (ab.2.isSome ↔ he') ∧
      (∀ j j', (ab.1 = some j ∨ ab.2 = some j) →
        (ab.1 = some j' ∨ ab.2 = some j') → h j ≡ h j' [MOD p]) ∧
      (∀ j, (ab.1 = some j ∨ ab.2 = some j) → ¬ h i ≡ h j [MOD p]))).card := by sorry

Source

GPY monomial joint (GPYMonomialJoint.lean), restated into Mathlib-only terms

View graph