Group-theoretic helpers used with rotation normalization.

The finRotate arithmetic lemmas live in SemicircleCheck.FinRotateLemmas.

The group-theoretic layer

theorem inv_apply_of_apply {m : ℕ} {ρ : Equiv.Perm (Fin m)} {a b : Fin m} (h : ρ a = b) : ρ⁻¹ b = a

If ρ sends a to b, then ρ⁻¹ sends b back to a. Pure injectivity.

theorem involution_reverse {m : ℕ} {π : Equiv.Perm (Fin m)} {i γi : Fin m} (hsq : π ^ 2 = 1) (hadj : π i = γi) : π γi = i

The involution gives us the reverse map. If π² = 1 and π(i) = γi, then π(γi) = i.

theorem conjugate_sends {m : ℕ} {π ρ : Equiv.Perm (Fin m)} {i γi a b : Fin m} (hρi : ρ i = a) (hργi : ρ γi = b) (hadj : π i = γi) : (ρ * π * ρ⁻¹) a = b

Conjugation sends a to b when ρ, π, and the adjacency align.

calc: (ρ * π * ρ⁻¹)(a) = ρ(π(ρ⁻¹(a))) = ρ(π(i)) = ρ(γi) = b

theorem conjugate_sends_back {m : ℕ} {π ρ : Equiv.Perm (Fin m)} {i γi a b : Fin m} (hρi : ρ i = a) (hργi : ρ γi = b) (hsq : π ^ 2 = 1) (hadj : π i = γi) : (ρ * π * ρ⁻¹) b = a

Conjugation sends b to a (the reverse direction via involution).

calc: (ρ * π * ρ⁻¹)(b) = ρ(π(ρ⁻¹(b))) = ρ(π(γi)) = ρ(i) = a