Finite-period inversion sums

This file supplies the finite counting normalization used in the proof of paper Lemma lem:invtau (Lemma 4.10). The public definition of kInversionCount normalizes the first coordinate of an inversion, whereas the paper sums over representatives whose second coordinate lies in a fundamental period. The first theorem proves that these two choices count the same period orbits. The second theorem decomposes that count into the northwest quadrants which are already identified with complementary divisor ranks in ThetaNonrecurrence.

def Bananas.affineResidueMap (k : ℕ) (tau : ℤ → ℤ) (hk : 0 < k) (b : Fin k) : Fin k

Reduction of an affine permutation's values to one fundamental period.

Equations

• Bananas.affineResidueMap k tau hk b = ⟨(tau ↑↑b % ↑k).toNat, ⋯⟩

theorem Bananas.affineResidueMap_injective {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) : Function.Injective (affineResidueMap k tau hk)

The value-residue map of a bijective affine permutation is injective. Thus a transmission permutation permutes the k torsion residue classes, which is the finite reindexing step in Lemma 4.10.

theorem Bananas.affineResidueMap_bijective {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hBij : Function.Bijective tau) (hAffine : IsKAffine k tau) : Function.Bijective (affineResidueMap k tau hk)

Consequently, an affine bijection permutes the finite residue type.

theorem Bananas.kInversions_ncard_eq_kInversionsBySecond {k : ℕ} {tau : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k tau) : (kInversions k tau).ncard = (kInversionsBySecond k tau).ncard

Normalizing either coordinate of every inversion gives the same number of affine-period inversion classes.

noncomputable def Bananas.kInversionsBySecondEquivNorthwestSigma (k : ℕ) (tau : ℤ → ℤ) : { p : ℤ × ℤ // p ∈ kInversionsBySecond k tau } ≃ (b : Fin k) × { m : ℤ // m ∈ northwestSet tau (tau ↑↑b + 1) ↑↑b }

In the second-coordinate normalization, the fiber over b is exactly the northwest quadrant at the graph of tau.

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.kInversionCount_eq_sum_northwest (M : TwiceMarked) (D : CFDiv M.graph) (hconn : _root_.graphConnected M.graph) (k : ℕ) (tau : ℤ → ℤ) (hk : 0 < k) (hTau : IsTransmissionPermutation M D tau) (hAffine : IsKAffine k tau) : kInversionCount k tau = ∑ b : Fin k, (northwestSet tau (tau ↑↑b + 1) ↑↑b).ncard

The k-inversion count is a finite sum of northwest quadrant sizes, with one summand for each value in a fundamental period.

theorem Bananas.intCast_kInversionCount_eq_sum_complement_rank (M : TwiceMarked) (D : CFDiv M.graph) (hconn : _root_.graphConnected M.graph) (k : ℕ) (tau : ℤ → ℤ) (hk : 0 < k) (hTau : IsTransmissionPermutation M D tau) (hAffine : IsKAffine k tau) : ↑(kInversionCount k tau) = ∑ b : Fin k, (rank M.graph (canonicalDivisor M.graph - D - tau ↑↑b • oneChip M.u + ↑↑b • oneChip M.v) + 1)

Rank-theoretic form of the finite inversion-row sum. Each northwest fiber is the complementary rank appearing in paper Lemma lem:tauChars. This is the finite, Lean-ready starting point for the inclusion--exclusion calculation in Lemma 4.10.