GCD factorization of the joint local weight

Proved

gpy_jointWeight_factor

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

number-theory

At squarefree D and E, the joint local weight (the product over primes dividing lcm D E of the local good-choice counts, divided by phi (lcm D E)) factors into a gcd part, a D-only part, and an E-only part, each a product over the corresponding prime divisors divided by the totient of that part. This is an unconditional algebraic factorization; it does not evaluate any sum.

Preamble

import Mathlib
open Classical

Formal statement

theorem gpy_jointWeight_factor {k : ℕ} {h : Fin k → ℕ} {i : Fin k} {D E : ℕ}
    (hsqD : Squarefree D) (hsqE : Squarefree E) :
    ((∏ p ∈ (Nat.lcm D E).primeFactors, ((((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
        (ab.1.isSome ↔ p ∣ D) ∧ (ab.2.isSome ↔ p ∣ E) ∧
        (∀ 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 : ℝ))
          / ((Nat.totient (Nat.lcm D E) : ℕ) : ℝ))
      = ((∏ p ∈ (Nat.gcd D E).primeFactors, ((((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
        (ab.1.isSome ↔ p ∣ D) ∧ (ab.2.isSome ↔ p ∣ E) ∧
        (∀ 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 : ℝ))
          / ((Nat.totient (Nat.gcd D E) : ℕ) : ℝ))
        * ((∏ p ∈ (D / Nat.gcd D E).primeFactors, ((((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
        (ab.1.isSome ↔ p ∣ D) ∧ (ab.2.isSome ↔ p ∣ E) ∧
        (∀ 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 : ℝ))
          / ((Nat.totient (D / Nat.gcd D E) : ℕ) : ℝ))
        * ((∏ p ∈ (E / Nat.gcd D E).primeFactors, ((((Finset.univ : Finset (Option (Fin k) × Option (Fin k))).filter (fun ab =>
        (ab.1.isSome ↔ p ∣ D) ∧ (ab.2.isSome ↔ p ∣ E) ∧
        (∀ 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 : ℝ))
          / ((Nat.totient (E / Nat.gcd D E) : ℕ) : ℝ)) := by sorry

Source

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

View graph