Theory Free_Action_Paradox

(*  Title:       Free_Action_Paradox.thy
    Author:      Arthur F. Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz, 2026

    Auxiliary definitions for free group actions.

    This is the principal reduction step in the Banach-Tarski proof:
    the paradoxical decomposition of F⇩₂ is transported to the
    sphere once the F⇩₂ action by rotations is free away from its
    countable fixed-point set.
*)

theory Free_Action_Paradox
  imports Paradoxical_Decomposition
begin

section ‹Free actions›

text ‹
  An action is ∗‹free› on a set @{term X} if non-identity
  group elements have no fixed points in @{term X}: ‹g ⋅ x = x›
  forces ‹g = unit›.
›

context group_action
begin

definition free_on :: "'a set ⇒ bool" where
  "free_on X ⟷
    (∀g ∈ carrier. ∀x ∈ X. act g x = x ⟶ g = unit)"

end


section ‹Choice of orbit representatives›

text ‹
  Given a free action of @{term G} on @{term X}, the orbits partition
  @{term X}, and for any subset of choice representatives ‹M ⊆ X›
  (one per orbit), every ‹x ∈ X› can be written uniquely as
  ‹act g m› for some ‹g ∈ carrier› and ‹m ∈ M›.

  This is where the axiom of choice enters: we pick one element from
  each orbit.
›

context group_action
begin

definition orbit_eq :: "'a ⇒ 'a ⇒ bool" where
  "orbit_eq x y ⟷ (∃g ∈ carrier. y = act g x)"

lemma orbit_eq_refl: "x ∈ ground ⟹ orbit_eq x x"
  unfolding orbit_eq_def using act_unit unit_carrier by metis

text ‹
  When the action is free on @{term X}, the orbit relation is symmetric
  on @{term X}, provided every element has a group inverse in the
  carrier. We do not require ‹group›-level inverses here, so we
  state symmetry conditionally.
›

end


section ‹Transport of paradoxical decompositions along free actions›

text ‹
  This is the abstract Banach-Tarski reduction: suppose @{term G} acts
  freely on @{term X}, and @{term G} itself admits a paradoxical
  decomposition under the regular action (left multiplication on
  itself). Choosing one representative per @{term G}-orbit in @{term X}
  via the axiom of choice transports the paradox: each piece
  ‹P⇩_i ⊆ G› in the decomposition lifts to the union
  ‹{act g m | g ∈ P⇩_i, m ∈ M}›, where ‹M› is the chosen
  set of representatives.

  The later Hausdorff theory carries out this lift explicitly for
  ‹S⇧² ∖ D›: it defines orbit representatives, proves the lifted
  pieces are disjoint, and proves the two translated covers directly.
  The predicate below only packages the freeness and closure hypotheses
  that such an argument needs.
›

context group_action
begin

text ‹
  A free action is suitable for orbit-by-orbit transport when the set is
  contained in the ground space, the action is free on it, and the set is
  closed under the action of every carrier element.
›

definition transports_paradox :: "'a set ⇒ bool" where
  "transports_paradox X ⟷
    (X ⊆ ground ∧
     free_on X ∧
     (∀x ∈ X. ∀g ∈ carrier. act g x ∈ X))"

text ‹
  Under the assumptions captured by @{const transports_paradox}, a
  paradoxical decomposition of the carrier transports to a paradoxical
  decomposition of @{term X}. The proof is the standard
  ``orbit-by-orbit'' argument and uses the axiom of choice to select
  one representative per orbit.
›

end

end