Small-order trace counts after inversion pairing

The trace maps on both rotation tori identify an eigenvalue with its inverse. Applying this before the maximal-divisor union removes the factor two that is lost by counting eigenvalues instead of traces.

theorem BGS.Markoff.two_mul_card_image_le_card_add_two_of_inv_invariant {G : Type u_1} {T : Type u_2} [Group G] [DecidableEq T] [IsCyclic G] [Finite G] (s : Finset G) (f : G → T) (hsinv : ∀ x ∈ s, x⁻¹ ∈ s) (hfinv : ∀ (x : G), f x⁻¹ = f x) : 2 * (Finset.image f s).card ≤ s.card + 2

An inversion-invariant map has at most half as many values as inputs, apart from the at most two elements satisfying x² = 1.