Lean Proof Explanation

Strategy: State the theorem — the number of orbits times the group size equals the sum of fixed point counts over all group elements.

Explanation: Given a group action A : G → (X → X), Burnside's Lemma claims |Orbits| · |G| = Σ_{g∈G} |{x : g·x = x}|. This is a powerful counting tool: instead of enumerating orbits directly, we count fixed points for each group element and average. We work in ℚ to handle division cleanly throughout the proof.

Strategy: Claim the key equality in division form — if we prove this, multiplying by |G| gives the theorem.

Explanation: We state h_burnside : |Orbits| = (Σ_g |Fix(g)|)/|G|. Once we establish this, the final goal follows by multiplying both sides by |G|. This reformulation breaks the proof into two phases: (1) prove h_burnside via double counting and orbit-stabilizer, (2) clear the denominator. Working in ℚ allows us to manipulate fractions freely.

Strategy: Double counting — interchange the order of summation to switch from summing over group elements to summing over set elements.

Explanation: Both sides count the same set of pairs {(g,x) : g·x = x}. The left side groups by g: for each g, count how many x satisfy g·x = x (the fixed points of g). The right side groups by x: for each x, count how many g satisfy g·x = x (the stabilizer of x). Since we're counting the same finite set two ways, the sums are equal. This is the classical "double counting" technique.

Strategy: Unfold the definition of fixed_points and express its cardinality.

Explanation: Expand fixed_points A g to the subtype {x : X | A.act g x = x}, and use Fintype.card_subtype to express its cardinality as the number of elements satisfying the predicate. This prepares the left side for the interchange step.

Strategy: Unfold the definition of stabilizer and express its cardinality.

Explanation: Expand stabilizer A x to the subset {g : G | A.act g x = x}, and use Finset.card_filter to express its cardinality as the number of group elements satisfying the predicate. Now both sides are sums over filtered sets with the same predicate g·x = x, just with the roles of g and x swapped.

Strategy: Apply the summation commutativity lemma to complete the interchange.

Explanation: Finset.sum_comm states that Σᵢ Σⱼ f(i,j) = Σⱼ Σᵢ f(i,j) — we can swap the order of nested summations. Here, f(g,x) = 1 if g·x = x, else 0. The left side computes Σ_g (Σ_x f(g,x)) and the right side computes Σ_x (Σ_g f(g,x)), which are equal. The mod_cast handles coercion from ℕ to ℚ. This completes h_interchange.

Strategy: Apply the orbit-stabilizer theorem to relate stabilizer size to orbit size for each element.

Explanation: For every x ∈ X, we claim |Stab(x)| = |G| / |Orb(x)|. This is derived from the orbit-stabilizer theorem: |Orb(x)| · |Stab(x)| = |G|. We'll prove this by invoking the multiplicative form, showing the orbit is non-empty, and then dividing. This is the key bridge from stabilizers (which appear after the interchange) to orbits (which we need for the final summation lemma).

Strategy: Fix an arbitrary element x to prove the universal statement.

Explanation: To prove ∀ x : X, P(x), we use the intro tactic to introduce an arbitrary x and then prove P(x). This is standard universal introduction in natural deduction.

Strategy: State the multiplicative form of the orbit-stabilizer theorem.

Explanation: We claim |Stab(x)| · |Orb(x)| = |G|. This is the fundamental orbit-stabilizer theorem: the size of the stabilizer times the size of the orbit equals the size of the group. We'll apply the library lemma card_orbit_mul_card_stabilizer (possibly after rearranging factors) to establish this.

Strategy: Swap factors and apply the orbit-stabilizer lemma from the library.

Explanation: We use mul_comm to rewrite |Stab(x)| · |Orb(x)| as |Orb(x)| · |Stab(x)|, then apply card_orbit_mul_card_stabilizer which states exactly this equality. (The library lemma may have the factors in a specific order, hence the commutativity step.) This closes the nested have, establishing the multiplicative form.

Strategy: Prove that orbits are non-empty to justify division.

Explanation: To derive |Stab(x)| = |G| / |Orb(x)| from |Stab(x)| · |Orb(x)| = |G|, we need |Orb(x)| ≠ 0. Every orbit contains at least one element: x itself, since 1 · x = x (the identity element acts as the identity function). Therefore, |Orb(x)| ≥ 1, so it's non-zero.

Strategy: Simplify the non-zero condition to an existence statement.

Explanation: We unfold the definition of orbit cardinality and simplify the statement "|Orb(x)| ≠ 0" to "there exists an element in Orb(x)". The simp only chain expands Fintype.card_ofFinset (cardinality of a finset), Finset.card_eq_zero (a set has cardinality 0 iff it's empty), Finset.filter_eq_empty_iff (a filtered set is empty iff no element satisfies the predicate), and various logical simplifications. This reduces the goal to proving ∃ y, y ∈ Orb(x), which is easy to witness.

Strategy: Witness that x is in its own orbit via the identity element.

Explanation: To prove ∃ y ∈ Orb(x), we provide the witness y := x along with a proof that x ∈ Orb(x). By definition, x ∈ Orb(x) iff ∃ g ∈ G, g·x = x. We witness g := 1 (the identity), and the proof that 1·x = x is rfl (reflexivity, since group actions preserve identity). The anonymous constructor ⟨_, ⟨1, rfl⟩⟩ packages this: the first _ is x, the inner ⟨1, rfl⟩ is the proof that 1·x = x. This completes h_nonzero.

Strategy: Convert the multiplicative equality to the divisional form.

Explanation: Apply eq_div_of_mul_eq, which states: if b ≠ 0 and a · b = c, then a = c / b. Here a := |Stab(x)|, b := |Orb(x)|, c := |G|. We have h_orbit_stabilizer : |Stab(x)| · |Orb(x)| = |G| and h_nonzero : |Orb(x)| ≠ 0. We cast |Orb(x)| ≠ 0 from ℕ to ℚ using Nat.cast_ne_zero.mpr, and cast the multiplicative equality using mod_cast. This derives |Stab(x)| = |G| / |Orb(x)| in ℚ, completing the h_orbit_stabilizer proof for the fixed x.

Strategy: Invoke the orbit counting lemma that sums reciprocals of orbit sizes.

Explanation: Apply sum_inv_orbit_eq_orbits, which states Σₓ∈X 1/|Orb(x)| = |Orbits|. This is a beautiful combinatorial identity: each orbit O of size k contributes 1/k exactly k times (once for each of its k elements), so the total contribution of O is k · (1/k) = 1. Summing over all elements thus counts each orbit exactly once, giving |Orbits|. This lemma is the key to converting the sum over elements (which we have after applying h_orbit_stabilizer) into the number of orbits.

Strategy: Algebraically combine all the pieces to prove h_burnside.

Explanation: This single simp_all tactic orchestrates the entire calculation:
1. Substitute h_orbit_stabilizer into h_interchange: Σ_g |Fix(g)| = Σₓ |Stab(x)| = Σₓ |G|/|Orb(x)|.
2. Rewrite division as multiplication by reciprocal: Σₓ |G|/|Orb(x)| = Σₓ |G| · (1/|Orb(x)|).
3. Factor out the constant |G| from the sum: Σₓ |G| · (1/|Orb(x)|) = |G| · Σₓ (1/|Orb(x)|) (using Finset.mul_sum).
4. Apply sum_inv_orbit_eq_orbits (hypothesis h): Σₓ (1/|Orb(x)|) = |Orbits|.
5. Conclude: Σ_g |Fix(g)| = |G| · |Orbits|, which rearranges to |Orbits| = (Σ_g |Fix(g)|)/|G|.
The simp_all tactic applies all these algebraic rewrites automatically, closing the proof of h_burnside.

Strategy: Clear the denominator by multiplying both sides by |G|.

Explanation: The goal is |Orbits| · |G| = Σ_g |Fix(g)|. We rewrite the left side using h_burnside: |Orbits| = (Σ_g |Fix(g)|)/|G|, giving ((Σ_g |Fix(g)|)/|G|) · |G| = Σ_g |Fix(g)|. Apply div_mul_cancel₀, which states (a/b) · b = a when b ≠ 0. We prove |G| ≠ 0 using Fintype.card_ne_zero (finite groups are non-empty, a foundational axiom in the library), then cast this to ℚ via Nat.cast_ne_zero.mpr. This simplifies the left side to Σ_g |Fix(g)|, matching the right side.

Strategy: Normalize type coercions to finish the proof.

Explanation: Throughout the proof, we worked in ℚ (rationals) to handle division cleanly. The final goal statement is in ℚ, but all our cardinalities are natural numbers coerced to ℚ. The norm_cast tactic normalizes all the ℕ → ℚ coercions, verifying that the equality holds as stated. This completes the proof of Burnside's Lemma. □