Theory Free_Rotations_SO3

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

    SO(3) contains a free subgroup isomorphic to F⇩2.

    The classical witnesses are the rotations R⇩x and R⇩z by
    arccos(1/3) about orthogonal axes (e.g. the x- and z-axes). Showing
    that they generate a free F⇩2 is a substantial undertaking
    (see Wagon, "The Banach-Tarski Paradox", Theorem 2.1; de Rauglaudre,
    JFR 2017). It uses the AFP Free-Groups entry's PingPongLemma; the
    geometric content is to provide disjoint subsets of the sphere that
    R⇩x and R⇩z "ping-pong" between.

    This theory proves the concrete arithmetic freeness result used to
    embed the free group F⇩2 into SO(3).
*)

theory Free_Rotations_SO3
  imports
    "Banach_Tarski.F2_Paradox"
    "Banach_Tarski.Free_Action_Paradox"
    "HOL-Computational_Algebra.Primes"
    "Free-Groups.PingPongLemma"
begin

section ‹Rotations of three-space›

text ‹
  A rotation is an orthogonal transformation of determinant 1.
›

definition rotation :: "(real^3 ⇒ real^3) ⇒ bool" where
  "rotation f ⟷ orthogonal_transformation f ∧ det (matrix f) = 1"

definition SO3 :: "(real^3 ⇒ real^3) set" where
  "SO3 = {f. rotation f}"

text ‹SO(3) contains the identity and is closed under composition.›

lemma id_in_SO3: "id ∈ SO3"
proof -
  have "orthogonal_transformation (id::real^3 ⇒ real^3)"
    using orthogonal_transformation_id by (simp add: id_def)
  moreover have "det (matrix (id::real^3 ⇒ real^3)) = 1"
    by simp
  ultimately show ?thesis
    unfolding SO3_def rotation_def by simp
qed

lemma SO3_closed_compose:
  assumes "f ∈ SO3" and "g ∈ SO3"
  shows "f ∘ g ∈ SO3"
proof -
  from assms have f_orth: "orthogonal_transformation f"
    and g_orth: "orthogonal_transformation g"
    and f_det: "det (matrix f) = 1"
    and g_det: "det (matrix g) = 1"
    unfolding SO3_def rotation_def by auto
  have f_lin: "linear f" using f_orth by (rule orthogonal_transformation_linear)
  have g_lin: "linear g" using g_orth by (rule orthogonal_transformation_linear)

  have orth_comp: "orthogonal_transformation (f ∘ g)"
    using f_orth g_orth by (rule orthogonal_transformation_compose)

  have "matrix (f ∘ g) = matrix f ** matrix g"
    using g_lin f_lin by (rule matrix_compose)
  hence "det (matrix (f ∘ g)) = det (matrix f) * det (matrix g)"
    by (simp add: det_mul)
  also have "… = 1" using f_det g_det by simp
  finally have "det (matrix (f ∘ g)) = 1" .

  with orth_comp show ?thesis
    unfolding SO3_def rotation_def by simp
qed

text ‹SO(3) elements preserve the unit sphere.›

lemma rotation_preserves_sphere2:
  assumes "f ∈ SO3" and "x ∈ sphere2"
  shows "f x ∈ sphere2"
proof -
  from assms(1) have "orthogonal_transformation f"
    unfolding SO3_def rotation_def by auto
  hence "norm (f x) = norm x"
    by (rule orthogonal_transformation_norm)
  with assms(2) show ?thesis
    by (simp add: sphere2_def)
qed

lemma SO3_bij:
  assumes "f ∈ SO3"
  shows "bij f"
  using assms orthogonal_transformation_bij
  unfolding SO3_def rotation_def by auto


section ‹Two distinguished rotations›

text ‹
  We use the rotations ‹R⇩x› (about the x-axis) and
  ‹R⇩z› (about the z-axis) by the same angle ‹θ›
  with ‹cos θ = 1/3›. The exact-form witnesses are unimportant
  for the paradoxical decomposition; what matters is the abstract
  conclusion that these generate a free ‹F⇩2› inside SO(3).
›

definition rot_c :: real where
  "rot_c = 1 / 3"

definition rot_s :: real where
  "rot_s = sqrt 8 / 3"

lemma rot_c_sq_plus_rot_s_sq: "rot_c⇧2 + rot_s⇧2 = 1"
  unfolding rot_c_def rot_s_def
  by (simp add: power_divide)

lemma rot_c_mul_plus_rot_s_mul [simp]: "rot_c * rot_c + rot_s * rot_s = 1"
  using rot_c_sq_plus_rot_s_sq by (simp add: power2_eq_square)

definition Rx_mat :: "real^3^3" where
  "Rx_mat = vector [
     vector [1, 0, 0],
     vector [0, rot_c, - rot_s],
     vector [0, rot_s, rot_c]]"

definition Rz_mat :: "real^3^3" where
  "Rz_mat = vector [
     vector [rot_c, - rot_s, 0],
     vector [rot_s, rot_c, 0],
     vector [0, 0, 1]]"

definition Rx_inv_mat :: "real^3^3" where
  "Rx_inv_mat = vector [
     vector [1, 0, 0],
     vector [0, rot_c, rot_s],
     vector [0, - rot_s, rot_c]]"

definition Rz_inv_mat :: "real^3^3" where
  "Rz_inv_mat = vector [
     vector [rot_c, rot_s, 0],
     vector [- rot_s, rot_c, 0],
     vector [0, 0, 1]]"

definition Rx :: "real^3 ⇒ real^3" where
  "Rx v = Rx_mat *v v"

definition Rz :: "real^3 ⇒ real^3" where
  "Rz v = Rz_mat *v v"

definition Rx_inv :: "real^3 ⇒ real^3" where
  "Rx_inv v = Rx_inv_mat *v v"

definition Rz_inv :: "real^3 ⇒ real^3" where
  "Rz_inv v = Rz_inv_mat *v v"

lemma Rx_mat_orthogonal: "orthogonal_matrix Rx_mat"
  unfolding orthogonal_matrix Rx_mat_def
  by (simp add: matrix_matrix_mult_def transpose_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rz_mat_orthogonal: "orthogonal_matrix Rz_mat"
  unfolding orthogonal_matrix Rz_mat_def
  by (simp add: matrix_matrix_mult_def transpose_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rx_inv_mat_orthogonal: "orthogonal_matrix Rx_inv_mat"
  unfolding orthogonal_matrix Rx_inv_mat_def
  by (simp add: matrix_matrix_mult_def transpose_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rz_inv_mat_orthogonal: "orthogonal_matrix Rz_inv_mat"
  unfolding orthogonal_matrix Rz_inv_mat_def
  by (simp add: matrix_matrix_mult_def transpose_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma det_Rx_mat [simp]: "det Rx_mat = 1"
  unfolding Rx_mat_def
  by (simp add: det_3 vector_def rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma det_Rz_mat [simp]: "det Rz_mat = 1"
  unfolding Rz_mat_def
  by (simp add: det_3 vector_def rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma det_Rx_inv_mat [simp]: "det Rx_inv_mat = 1"
  unfolding Rx_inv_mat_def
  by (simp add: det_3 vector_def rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma det_Rz_inv_mat [simp]: "det Rz_inv_mat = 1"
  unfolding Rz_inv_mat_def
  by (simp add: det_3 vector_def rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rx_mat_inverse_left: "Rx_inv_mat ** Rx_mat = mat 1"
  unfolding Rx_inv_mat_def Rx_mat_def
  by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rx_mat_inverse_right: "Rx_mat ** Rx_inv_mat = mat 1"
  unfolding Rx_inv_mat_def Rx_mat_def
  by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rz_mat_inverse_left: "Rz_inv_mat ** Rz_mat = mat 1"
  unfolding Rz_inv_mat_def Rz_mat_def
  by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

lemma Rz_mat_inverse_right: "Rz_mat ** Rz_inv_mat = mat 1"
  unfolding Rz_inv_mat_def Rz_mat_def
  by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff vector_def sum_3 forall_3
      rot_c_sq_plus_rot_s_sq power2_eq_square algebra_simps)

text ‹The concrete generators and their inverses lie in ‹SO(3)›.›
lemma Rx_in_SO3: "Rx ∈ SO3"
  unfolding SO3_def rotation_def Rx_def
  by (simp add: orthogonal_transformation_matrix Rx_mat_orthogonal matrix_vector_mul_linear)

lemma Rz_in_SO3: "Rz ∈ SO3"
  unfolding SO3_def rotation_def Rz_def
  by (simp add: orthogonal_transformation_matrix Rz_mat_orthogonal matrix_vector_mul_linear)

lemma Rx_inv_in_SO3: "Rx_inv ∈ SO3"
  unfolding SO3_def rotation_def Rx_inv_def
  by (simp add: orthogonal_transformation_matrix Rx_inv_mat_orthogonal matrix_vector_mul_linear)

lemma Rz_inv_in_SO3: "Rz_inv ∈ SO3"
  unfolding SO3_def rotation_def Rz_inv_def
  by (simp add: orthogonal_transformation_matrix Rz_inv_mat_orthogonal matrix_vector_mul_linear)

text ‹The named inverse rotations are two-sided inverses of the generators.›
lemma Rx_inv_left: "Rx_inv ∘ Rx = id"
  by (rule ext) (simp add: Rx_inv_def Rx_def matrix_vector_mul_assoc Rx_mat_inverse_left)

lemma Rz_inv_left: "Rz_inv ∘ Rz = id"
  by (rule ext) (simp add: Rz_inv_def Rz_def matrix_vector_mul_assoc Rz_mat_inverse_left)

lemma Rx_inv_right: "Rx ∘ Rx_inv = id"
  by (rule ext) (simp add: Rx_inv_def Rx_def matrix_vector_mul_assoc Rx_mat_inverse_right)

lemma Rz_inv_right: "Rz ∘ Rz_inv = id"
  by (rule ext) (simp add: Rz_inv_def Rz_def matrix_vector_mul_assoc Rz_mat_inverse_right)


section ‹The rotations as bijections of the sphere›

definition sphere_perm :: "(real^3 ⇒ real^3) ⇒ (real^3 ⇒ real^3)" where
  "sphere_perm f = restrict f sphere2"

lemma SO3_bij_betw_sphere2:
  assumes "f ∈ SO3"
  shows "bij_betw f sphere2 sphere2"
proof -
  have "f ` sphere2 ⊆ sphere2"
    using rotation_preserves_sphere2[OF assms] by auto
  moreover have "sphere2 ⊆ f ` sphere2"
  proof
    fix y assume y: "y ∈ sphere2"
    from SO3_bij[OF assms] obtain x where x: "y = f x"
      by (meson bij_pointE)
    have "x ∈ sphere2"
    proof -
      from assms have orth: "orthogonal_transformation f"
        unfolding SO3_def rotation_def by auto
      from x y have "norm (f x) = 1"
        by (simp add: sphere2_def)
      moreover from orth have "norm (f x) = norm x"
        by (rule orthogonal_transformation_norm)
      ultimately show ?thesis
        by (simp add: sphere2_def)
    qed
    with x show "y ∈ f ` sphere2"
      by blast
  qed
  moreover have "inj_on f sphere2"
  proof -
    have "inj f"
      using SO3_bij[OF assms] by (rule bij_is_inj)
    thus ?thesis
      by (rule inj_on_subset) simp
  qed
  ultimately show ?thesis
    unfolding bij_betw_def by auto
qed

lemma sphere_perm_in_Bij:
  assumes "f ∈ SO3"
  shows "sphere_perm f ∈ Bij sphere2"
  using SO3_bij_betw_sphere2[OF assms]
  by (simp add: sphere_perm_def Bij_def)

lemma sphere_perm_mult:
  assumes "sphere_perm f ∈ Bij sphere2" "sphere_perm g ∈ Bij sphere2"
  shows "sphere_perm f ⊗⇘BijGroup sphere2⇙ sphere_perm g = sphere_perm (f ∘ g)"
proof (rule ext)
  fix x
  show "(sphere_perm f ⊗⇘BijGroup sphere2⇙ sphere_perm g) x = sphere_perm (f ∘ g) x"
  proof (cases "x ∈ sphere2")
    case True
    from assms True have "sphere_perm g x ∈ sphere2"
      by (auto simp: Bij_def bij_betw_def)
    with assms True show ?thesis
      by (simp add: sphere_perm_def BijGroup_def compose_def restrict_def)
  next
    case False
    with assms show ?thesis
      by (simp add: sphere_perm_def BijGroup_def compose_def restrict_def)
  qed
qed

lemma sphere_perm_id: "sphere_perm id = 𝟭⇘BijGroup sphere2⇙"
  by (simp add: sphere_perm_def BijGroup_def id_def)

lemma sphere_perm_Rx [simp]: "sphere_perm Rx ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule Rx_in_SO3)

lemma sphere_perm_Rx_inv [simp]: "sphere_perm Rx_inv ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule Rx_inv_in_SO3)

lemma sphere_perm_Rz [simp]: "sphere_perm Rz ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule Rz_in_SO3)

lemma sphere_perm_Rz_inv [simp]: "sphere_perm Rz_inv ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule Rz_inv_in_SO3)

lemma sphere_perm_Rx_inv_left:
  "sphere_perm Rx_inv ⊗⇘BijGroup sphere2⇙ sphere_perm Rx = 𝟭⇘BijGroup sphere2⇙"
  by (simp add: sphere_perm_mult Rx_inv_left sphere_perm_id)

lemma sphere_perm_Rx_inv_right:
  "sphere_perm Rx ⊗⇘BijGroup sphere2⇙ sphere_perm Rx_inv = 𝟭⇘BijGroup sphere2⇙"
  by (simp add: sphere_perm_mult Rx_inv_right sphere_perm_id)

lemma sphere_perm_Rz_inv_left:
  "sphere_perm Rz_inv ⊗⇘BijGroup sphere2⇙ sphere_perm Rz = 𝟭⇘BijGroup sphere2⇙"
  by (simp add: sphere_perm_mult Rz_inv_left sphere_perm_id)

lemma sphere_perm_Rz_inv_right:
  "sphere_perm Rz ⊗⇘BijGroup sphere2⇙ sphere_perm Rz_inv = 𝟭⇘BijGroup sphere2⇙"
  by (simp add: sphere_perm_mult Rz_inv_right sphere_perm_id)

lemma inv_sphere_perm_Rx:
  "inv⇘BijGroup sphere2⇙ (sphere_perm Rx) = sphere_perm Rx_inv"
proof -
  interpret B: group "BijGroup sphere2"
    by (rule group_BijGroup)
  show ?thesis
  proof (rule B.inv_equality)
    show "sphere_perm Rx_inv ⊗⇘BijGroup sphere2⇙ sphere_perm Rx = 𝟭⇘BijGroup sphere2⇙"
      by (rule sphere_perm_Rx_inv_left)
    show "sphere_perm Rx ∈ carrier (BijGroup sphere2)"
      by (simp add: BijGroup_def)
    show "sphere_perm Rx_inv ∈ carrier (BijGroup sphere2)"
      by (simp add: BijGroup_def)
  qed
qed

lemma inv_sphere_perm_Rz:
  "inv⇘BijGroup sphere2⇙ (sphere_perm Rz) = sphere_perm Rz_inv"
proof -
  interpret B: group "BijGroup sphere2"
    by (rule group_BijGroup)
  show ?thesis
  proof (rule B.inv_equality)
    show "sphere_perm Rz_inv ⊗⇘BijGroup sphere2⇙ sphere_perm Rz = 𝟭⇘BijGroup sphere2⇙"
      by (rule sphere_perm_Rz_inv_left)
    show "sphere_perm Rz ∈ carrier (BijGroup sphere2)"
      by (simp add: BijGroup_def)
    show "sphere_perm Rz_inv ∈ carrier (BijGroup sphere2)"
      by (simp add: BijGroup_def)
  qed
qed

interpretation sphere_Bij: group "BijGroup sphere2"
  by (rule group_BijGroup)


section ‹The map sigma: ‹F⇩2› to SO(3)›

text ‹
  The map ‹sigma› sends each reduced word in ‹F⇩2› to the
  corresponding composition of ‹R⇩x›, ‹R⇩z›, and
  their inverses.
›

definition letter_to_rot :: "bool × gen2 ⇒ (real^3 ⇒ real^3)" where
  "letter_to_rot p = (case p of
       (False, A) ⇒ Rx
     | (True,  A) ⇒ Rx_inv
     | (False, B) ⇒ Rz
     | (True,  B) ⇒ Rz_inv)"

definition rho :: "gen2 ⇒ (real^3 ⇒ real^3)" where
  "rho x = (case x of A ⇒ sphere_perm Rx | B ⇒ sphere_perm Rz)"

lemma rho_in_BijGroup:
  "rho ∈ Gen2 → carrier (BijGroup sphere2)"
  by (auto simp: rho_def BijGroup_def)

lemma rho_image_subset_BijGroup:
  "rho ` Gen2 ⊆ carrier (BijGroup sphere2)"
  using rho_in_BijGroup by auto

definition sphere_rot_group :: "(real^3 ⇒ real^3) monoid" where
  "sphere_rot_group =
    (BijGroup sphere2)⦇carrier := ⟨rho ` Gen2⟩⇘BijGroup sphere2⇙⦈"

lemma sphere_rot_subgroup:
  "subgroup (carrier sphere_rot_group) (BijGroup sphere2)"
  unfolding sphere_rot_group_def
  apply simp
  by (rule sphere_Bij.gen_subgroup_is_subgroup) (auto simp: rho_def BijGroup_def)

lemma sphere_rot_group_is_group: "group sphere_rot_group"
  unfolding sphere_rot_group_def
  by (rule sphere_Bij.subgroup_imp_group)
    (rule sphere_Bij.gen_subgroup_is_subgroup, rule rho_image_subset_BijGroup)

interpretation sphere_rot: group sphere_rot_group
  by (rule sphere_rot_group_is_group)

lemma rho_in_sphere_rot_group:
  "rho ∈ Gen2 → carrier sphere_rot_group"
  by (auto simp: sphere_rot_group_def intro: gen_span.gen_gens)

lemma sphere_rot_inclusion_hom:
  "id ∈ hom sphere_rot_group (BijGroup sphere2)"
  using sphere_Bij.gen_span_closed[OF rho_image_subset_BijGroup]
  by (auto simp: hom_def sphere_rot_group_def)

lemma sphere_rot_generated:
  "⟨rho ` Gen2⟩⇘sphere_rot_group⇙ = carrier sphere_rot_group"
proof -
  let ?H = "⟨rho ` Gen2⟩⇘BijGroup sphere2⇙"
  let ?G = "(BijGroup sphere2)⦇carrier := ?H⦈"
  have sub: "subgroup ?H (BijGroup sphere2)"
    by (rule sphere_Bij.gen_subgroup_is_subgroup) (rule rho_image_subset_BijGroup)
  have left: "⟨rho ` Gen2⟩⇘sphere_rot_group⇙ ⊆ carrier sphere_rot_group"
    by (rule sphere_rot.gen_span_closed) (use rho_in_sphere_rot_group in auto)
  have right: "?H ⊆ ⟨rho ` Gen2⟩⇘?G⇙"
  proof
    fix x
    assume "x ∈ ?H"
    thus "x ∈ ⟨rho ` Gen2⟩⇘?G⇙"
    proof (induct rule: gen_span.induct)
      case gen_one
      have "𝟭⇘?G⇙ ∈ ⟨rho ` Gen2⟩⇘?G⇙"
        by (rule gen_span.gen_one)
      thus ?case by simp
    next
      case (gen_gens x)
      thus ?case
        by (rule gen_span.gen_gens)
    next
      case (gen_inv x)
      have inv_eq: "inv⇘?G⇙ x = inv⇘BijGroup sphere2⇙ x"
        using sphere_Bij.m_inv_consistent[OF sub gen_inv.hyps(1)] .
      have "inv⇘?G⇙ x ∈ ⟨rho ` Gen2⟩⇘?G⇙"
        by (rule gen_span.gen_inv) (rule gen_inv.hyps(2))
      thus ?case
        using inv_eq by metis
    next
      case (gen_mult x y)
      have "x ⊗⇘?G⇙ y ∈ ⟨rho ` Gen2⟩⇘?G⇙"
        by (rule gen_span.gen_mult) (use gen_mult.hyps in auto)
      thus ?case by simp
    qed
  qed
  show ?thesis
    using left right by (auto simp: sphere_rot_group_def)
qed

lemma sphere_Bij_lift_gi_rho:
  assumes "snd p ∈ Gen2"
  shows "sphere_Bij.lift_gi rho p = sphere_perm (letter_to_rot p)"
  using assms
  by (cases p)
    (auto simp: rho_def letter_to_rot_def sphere_Bij.lift_gi_def
      inv_sphere_perm_Rx inv_sphere_perm_Rz split: bool.splits gen2.splits)

lemma sphere_rot_inv_rho_eq_sphere_Bij:
  assumes "i ∈ Gen2"
  shows "inv⇘sphere_rot_group⇙ (rho i) = inv⇘BijGroup sphere2⇙ (rho i)"
proof -
  have rho_i: "rho i ∈ carrier sphere_rot_group"
    using rho_in_sphere_rot_group assms by auto
  have "inv⇘(BijGroup sphere2)⦇carrier := carrier sphere_rot_group⦈⇙ (rho i) =
      inv⇘BijGroup sphere2⇙ (rho i)"
    using sphere_Bij.m_inv_consistent[OF sphere_rot_subgroup rho_i] .
  thus ?thesis
    by (simp add: sphere_rot_group_def)
qed

lemma sphere_rot_lift_gi_rho_eq_sphere_Bij:
  assumes "snd p ∈ Gen2"
  shows "sphere_rot.lift_gi rho p = sphere_Bij.lift_gi rho p"
  using assms
  by (cases p)
    (auto simp: sphere_rot.lift_gi_def sphere_Bij.lift_gi_def
      sphere_rot_inv_rho_eq_sphere_Bij)

lemma sphere_rot_lift_rho_eq_sphere_Bij:
  assumes "w ∈ lists (UNIV × Gen2)"
  shows "sphere_rot.lift rho w = sphere_Bij.lift rho w"
  using assms
proof (induct w)
  case Nil
  show ?case
  proof -
    have "sphere_rot.lift rho [] = 𝟭⇘sphere_rot_group⇙"
      by simp
    also have "… = 𝟭⇘BijGroup sphere2⇙"
      by (simp add: sphere_rot_group_def)
    also have "… = sphere_Bij.lift rho []"
      by simp
    finally show ?case .
  qed
next
  case (Cons p w)
  have p_gen: "snd p ∈ Gen2"
    by (simp add: Gen2_UNIV)
  have w_lists: "w ∈ lists (UNIV × Gen2)"
    using Cons.prems by (auto simp: Gen2_UNIV)
  have IH: "sphere_rot.lift rho w = sphere_Bij.lift rho w"
    using Cons.hyps w_lists by simp
  have gi_rot_closed: "sphere_rot.lift_gi rho p ∈ carrier sphere_rot_group"
    using rho_in_sphere_rot_group p_gen by (rule sphere_rot.lift_gi_closed)
  have tail_rot_closed: "sphere_rot.lift rho w ∈ carrier sphere_rot_group"
    using rho_in_sphere_rot_group w_lists by (rule sphere_rot.lift_closed)
  have gi_Bij_closed: "sphere_Bij.lift_gi rho p ∈ carrier (BijGroup sphere2)"
    using rho_in_BijGroup p_gen by (rule sphere_Bij.lift_gi_closed)
  have tail_Bij_closed: "sphere_Bij.lift rho w ∈ carrier (BijGroup sphere2)"
    using rho_in_BijGroup w_lists by (rule sphere_Bij.lift_closed)
  have "sphere_rot.lift rho (p # w) =
      sphere_rot.lift_gi rho p ⊗⇘sphere_rot_group⇙ sphere_rot.lift rho w"
    using gi_rot_closed tail_rot_closed
    by (simp add: sphere_rot.lift_def)
  also have "… =
      sphere_Bij.lift_gi rho p ⊗⇘BijGroup sphere2⇙ sphere_Bij.lift rho w"
    using IH sphere_rot_lift_gi_rho_eq_sphere_Bij[OF p_gen]
    by (simp add: sphere_rot_group_def)
  also have "… = sphere_Bij.lift rho (p # w)"
    using gi_Bij_closed tail_Bij_closed
    by (simp add: sphere_Bij.lift_def)
  finally show ?case .
qed

lemma sphere_Bij_lift_rho_injective_if_ping_pong:
  fixes Xin Xout :: "gen2 ⇒ (real^3) set"
  assumes sub_out: "∀i∈Gen2. Xout i ⊆ sphere2"
    and sub_in: "∀i∈Gen2. Xin i ⊆ sphere2"
    and disj_out: "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xout i ∩ Xout j = {}"
    and disj_in: "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xin i ∩ Xin j = {}"
    and disj_cross: "∀i∈Gen2. ∀j∈Gen2. Xin i ∩ Xout j = {}"
    and x_sphere: "x ∈ sphere2"
    and ping: "∀i∈Gen2. rho i ` (sphere2 - Xout i) ⊆ Xin i"
    and pong: "∀i∈Gen2. (inv⇘sphere_rot_group⇙ (rho i)) ` (sphere2 - Xin i) ⊆ Xout i"
  shows "inj_on (sphere_Bij.lift rho) (carrier F2)"
proof -
  have iso: "sphere_rot.lift rho ∈ iso F2 sphere_rot_group"
  proof (rule ping_pong_lemma[
      where X = sphere2 and I = Gen2 and act = id and g = rho
        and Xout = Xout and Xin = Xin and x = x])
    show "group sphere_rot_group"
      by (rule sphere_rot_group_is_group)
    show "id ∈ hom sphere_rot_group (BijGroup sphere2)"
      by (rule sphere_rot_inclusion_hom)
    show "rho ∈ Gen2 → carrier sphere_rot_group"
      by (rule rho_in_sphere_rot_group)
    show "⟨rho ` Gen2⟩⇘sphere_rot_group⇙ = carrier sphere_rot_group"
      by (rule sphere_rot_generated)
    show "∀i∈Gen2. Xout i ⊆ sphere2"
      by (rule sub_out)
    show "∀i∈Gen2. Xin i ⊆ sphere2"
      by (rule sub_in)
    show "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xout i ∩ Xout j = {}"
      by (rule disj_out)
    show "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xin i ∩ Xin j = {}"
      by (rule disj_in)
    show "∀i∈Gen2. ∀j∈Gen2. Xin i ∩ Xout j = {}"
      by (rule disj_cross)
    show "x ∈ sphere2"
      by (rule x_sphere)
    show "∀i. Gen2 = {i} ⟶ x ∉ Xout i ∧ x ∉ Xin i"
      by auto
    show "∀i∈Gen2. id (rho i) ` (sphere2 - Xout i) ⊆ Xin i"
      using ping by simp
    show "∀i∈Gen2. id (inv⇘sphere_rot_group⇙ (rho i)) ` (sphere2 - Xin i) ⊆ Xout i"
      using pong by simp
  qed
  have inj_rot: "inj_on (sphere_rot.lift rho) (carrier F2)"
    using iso by (auto simp: iso_def bij_betw_def)
  show ?thesis
  proof (rule inj_onI)
    fix w v
    assume w: "w ∈ carrier F2" and v: "v ∈ carrier F2"
      and eq: "sphere_Bij.lift rho w = sphere_Bij.lift rho v"
    have w_lists: "w ∈ lists (UNIV × Gen2)"
      using w by (simp add: F2_carrier_iff)
    have v_lists: "v ∈ lists (UNIV × Gen2)"
      using v by (simp add: F2_carrier_iff)
    have "sphere_rot.lift rho w = sphere_Bij.lift rho w"
      using w_lists by (rule sphere_rot_lift_rho_eq_sphere_Bij)
    also have "… = sphere_Bij.lift rho v"
      by (rule eq)
    also have "… = sphere_rot.lift rho v"
      using v_lists by (rule sphere_rot_lift_rho_eq_sphere_Bij[symmetric])
    finally have "sphere_rot.lift rho w = sphere_rot.lift rho v" .
    with inj_rot w v show "w = v"
      by (auto simp: inj_on_def)
  qed
qed

definition sigma :: "(bool × gen2) list ⇒ (real^3 ⇒ real^3)" where
  "sigma w = foldr (λp f. letter_to_rot p ∘ f) w id"

lemma letter_to_rot_cancel_left [simp]:
  "letter_to_rot (True, A) ∘ letter_to_rot (False, A) = id"
  "letter_to_rot (False, A) ∘ letter_to_rot (True, A) = id"
  "letter_to_rot (True, B) ∘ letter_to_rot (False, B) = id"
  "letter_to_rot (False, B) ∘ letter_to_rot (True, B) = id"
  by (simp_all add: letter_to_rot_def Rx_inv_left Rx_inv_right Rz_inv_left Rz_inv_right)

lemma letter_to_rot_canceling:
  assumes "canceling p q"
  shows "letter_to_rot p ∘ letter_to_rot q = id"
  using assms
  by (cases p; cases q)
    (auto split: bool.splits gen2.splits
      simp: canceling_def letter_to_rot_def Rx_inv_left Rx_inv_right Rz_inv_left Rz_inv_right)

lemma sigma_Nil [simp]: "sigma [] = id"
  by (simp add: sigma_def)

lemma sigma_Cons [simp]: "sigma (p # w) = letter_to_rot p ∘ sigma w"
  by (simp add: sigma_def)

lemma sigma_append [simp]: "sigma (u @ v) = sigma u ∘ sigma v"
  by (induct u) (simp_all add: o_assoc)

lemma sigma_singleton [simp]: "sigma [p] = letter_to_rot p"
  by (simp add: fun_eq_iff)

lemma sigma_doubleton_canceling:
  assumes "canceling p q"
  shows "sigma [p, q] = id"
  using letter_to_rot_canceling[OF assms]
  by (simp add: o_def fun_eq_iff)

lemma sigma_cancels_to_1:
  assumes "cancels_to_1 x y"
  shows "sigma x = sigma y"
proof -
  from assms obtain xs1 x1 x2 xs2
    where x_eq: "x = xs1 @ x1 # x2 # xs2"
      and y_eq: "y = xs1 @ xs2"
      and cancel: "canceling x1 x2"
    by (rule cancels_to_1_unfold)
  have "sigma x = sigma xs1 ∘ sigma [x1, x2] ∘ sigma xs2"
    by (simp add: x_eq o_assoc)
  also have "… = sigma xs1 ∘ sigma xs2"
    using letter_to_rot_canceling[OF cancel]
    by (auto simp: fun_eq_iff o_def)
  also have "… = sigma y"
    by (simp add: y_eq)
  finally show ?thesis .
qed

lemma sigma_cancels_to:
  assumes "cancels_to x y"
  shows "sigma x = sigma y"
  using assms unfolding cancels_to_def
proof (induct rule: rtranclp_induct)
  case base
  show ?case by simp
next
  case (step y z)
  then show ?case
    using sigma_cancels_to_1 by simp
qed

lemma sigma_normalize [simp]: "sigma (normalize w) = sigma w"
  using sigma_cancels_to[OF normalized_cancels_to] by simp

lemma letter_to_rot_in_SO3: "letter_to_rot p ∈ SO3"
  by (cases p)
    (auto split: bool.splits gen2.splits
      simp: letter_to_rot_def Rx_in_SO3 Rz_in_SO3 Rx_inv_in_SO3 Rz_inv_in_SO3)

lemma sphere_perm_letter_to_rot_in_Bij [simp]:
  "sphere_perm (letter_to_rot p) ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule letter_to_rot_in_SO3)

lemma sigma_in_SO3: "sigma w ∈ SO3"
proof (induct w)
  case Nil
  show ?case
    using id_in_SO3 by (simp add: id_def)
next
  case (Cons p w)
  have "letter_to_rot p ∘ sigma w ∈ SO3"
    using letter_to_rot_in_SO3 Cons.hyps by (rule SO3_closed_compose)
  then show ?case by (simp add: o_def)
qed

lemma sigma_preserves_sphere2:
  assumes "x ∈ sphere2"
  shows "sigma w x ∈ sphere2"
  using rotation_preserves_sphere2[OF sigma_in_SO3 assms] .

lemma sigma_bij: "bij (sigma w)"
  using SO3_bij sigma_in_SO3 by blast

lemma sphere_perm_sigma_in_Bij [simp]:
  "sphere_perm (sigma w) ∈ Bij sphere2"
  by (rule sphere_perm_in_Bij) (rule sigma_in_SO3)

lemma sphere_Bij_lift_rho_eq_sigma:
  assumes "w ∈ lists (UNIV × Gen2)"
  shows "sphere_Bij.lift rho w = sphere_perm (sigma w)"
  using assms
proof (induct w)
  case Nil
  show ?case
    by (simp add: sphere_perm_id[symmetric] id_def)
next
  case (Cons p w)
  have p_gen: "snd p ∈ Gen2"
    by (simp add: Gen2_UNIV)
  have w_lists: "w ∈ lists (UNIV × Gen2)"
    using Cons.prems by (auto simp: Gen2_UNIV)
  have IH: "sphere_Bij.lift rho w = sphere_perm (sigma w)"
    using Cons.hyps w_lists by simp
  have singleton_lists: "[p] ∈ lists (UNIV × Gen2)"
    by (simp add: Gen2_UNIV)
  have "sphere_Bij.lift rho (p # w) = sphere_Bij.lift rho ([p] @ w)"
    by simp
  also have "… = sphere_Bij.lift rho [p] ⊗⇘BijGroup sphere2⇙ sphere_Bij.lift rho w"
    using sphere_Bij.lift_append[OF rho_in_BijGroup singleton_lists w_lists] .
  also have "sphere_Bij.lift rho [p] = sphere_perm (letter_to_rot p)"
  proof -
    have gi_closed: "sphere_Bij.lift_gi rho p ∈ carrier (BijGroup sphere2)"
      using rho_in_BijGroup p_gen by (rule sphere_Bij.lift_gi_closed)
    have "sphere_Bij.lift rho [p] = sphere_Bij.lift_gi rho p"
      using rho_in_BijGroup p_gen
      by (simp add: sphere_Bij.lift_def gi_closed)
    also have "… = sphere_perm (letter_to_rot p)"
      using p_gen by (rule sphere_Bij_lift_gi_rho)
    finally show ?thesis .
  qed
  also have "sphere_perm (letter_to_rot p) ⊗⇘BijGroup sphere2⇙ sphere_Bij.lift rho w =
      sphere_perm (letter_to_rot p) ⊗⇘BijGroup sphere2⇙ sphere_perm (sigma w)"
    using IH by simp
  also have "… = sphere_perm (letter_to_rot p ∘ sigma w)"
    by (rule sphere_perm_mult) simp_all
  also have "… = sphere_perm (sigma (p # w))"
    by simp
  finally show ?case .
qed

lemma sigma_injective_if_sphere_lift_injective:
  assumes "inj_on (sphere_Bij.lift rho) (carrier F2)"
  shows "inj_on sigma (carrier F2)"
proof (rule inj_onI)
  fix w v
  assume w: "w ∈ carrier F2" and v: "v ∈ carrier F2" and eq: "sigma w = sigma v"
  have w_lists: "w ∈ lists (UNIV × Gen2)"
    using w by (simp add: F2_carrier_iff)
  have v_lists: "v ∈ lists (UNIV × Gen2)"
    using v by (simp add: F2_carrier_iff)
  have "sphere_Bij.lift rho w = sphere_perm (sigma w)"
    using w_lists by (rule sphere_Bij_lift_rho_eq_sigma)
  also have "… = sphere_perm (sigma v)"
    using eq by simp
  also have "… = sphere_Bij.lift rho v"
    using v_lists by (rule sphere_Bij_lift_rho_eq_sigma[symmetric])
  finally have lift_eq: "sphere_Bij.lift rho w = sphere_Bij.lift rho v" .
  show "w = v"
    using assms w v lift_eq by (auto simp: inj_on_def)
qed

lemma sigma_injective_if_ping_pong:
  fixes Xin Xout :: "gen2 ⇒ (real^3) set"
  assumes sub_out: "∀i∈Gen2. Xout i ⊆ sphere2"
    and sub_in: "∀i∈Gen2. Xin i ⊆ sphere2"
    and disj_out: "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xout i ∩ Xout j = {}"
    and disj_in: "∀i∈Gen2. ∀j∈Gen2. i ≠ j ⟶ Xin i ∩ Xin j = {}"
    and disj_cross: "∀i∈Gen2. ∀j∈Gen2. Xin i ∩ Xout j = {}"
    and x_sphere: "x ∈ sphere2"
    and ping: "∀i∈Gen2. rho i ` (sphere2 - Xout i) ⊆ Xin i"
    and pong: "∀i∈Gen2. (inv⇘sphere_rot_group⇙ (rho i)) ` (sphere2 - Xin i) ⊆ Xout i"
  shows "inj_on sigma (carrier F2)"
  by (rule sigma_injective_if_sphere_lift_injective)
    (rule sphere_Bij_lift_rho_injective_if_ping_pong[
      OF sub_out sub_in disj_out disj_in disj_cross x_sphere ping pong])

text ‹The ping-pong criterion gives a reusable injectivity criterion for ‹sigma›.›

section ‹Arithmetic freeness invariant›

text ‹
  The classical proof that the above rotations generate a free subgroup
  is arithmetic rather than geometric: scale each letter by ‹3›, so
  every word has entries in the integer quadratic ring generated by
  @{term "sqrt 2"}.  A nonempty reduced word
  leaves a coefficient nonzero modulo ‹3› after applying it to a
  suitable basis vector, whereas the identity matrix would have all
  scaled off-axis coefficients divisible by ‹3›.

  The following definitions make that invariant explicit.  They are
  deliberately separated from real-vector semantics so that the finite
  modulo-‹3› induction can be discharged by simplification and case
  analysis before being connected back to ‹sigma›.
›

type_synonym zsqrt2 = "int × int"
type_synonym zvec3 = "zsqrt2 × zsqrt2 × zsqrt2"

definition zsqrt2_val :: "zsqrt2 ⇒ real" where
  "zsqrt2_val q = of_int (fst q) + of_int (snd q) * sqrt 2"

definition zsqrt2_add :: "zsqrt2 ⇒ zsqrt2 ⇒ zsqrt2" where
  "zsqrt2_add p q = (fst p + fst q, snd p + snd q)"

definition zsqrt2_neg :: "zsqrt2 ⇒ zsqrt2" where
  "zsqrt2_neg p = (- fst p, - snd p)"

definition zsqrt2_sub :: "zsqrt2 ⇒ zsqrt2 ⇒ zsqrt2" where
  "zsqrt2_sub p q = zsqrt2_add p (zsqrt2_neg q)"

definition zsqrt2_scale :: "int ⇒ zsqrt2 ⇒ zsqrt2" where
  "zsqrt2_scale n p = (n * fst p, n * snd p)"

definition zsqrt2_mul_sqrt2 :: "zsqrt2 ⇒ zsqrt2" where
  "zsqrt2_mul_sqrt2 p = (2 * snd p, fst p)"

definition zsqrt2_div3 :: "zsqrt2 ⇒ bool" where
  "zsqrt2_div3 p ⟷ 3 dvd fst p ∧ 3 dvd snd p"

definition zvec3_div3 :: "zvec3 ⇒ bool" where
  "zvec3_div3 v ⟷
    (case v of (x, y, z) ⇒ zsqrt2_div3 x ∧ zsqrt2_div3 y ∧ zsqrt2_div3 z)"

definition zvec3_scale :: "int ⇒ zvec3 ⇒ zvec3" where
  "zvec3_scale n v = (case v of (x, y, z) ⇒
     (zsqrt2_scale n x, zsqrt2_scale n y, zsqrt2_scale n z))"

definition zvec3_val :: "zvec3 ⇒ real^3" where
  "zvec3_val v = (case v of (x, y, z) ⇒
     vector [zsqrt2_val x, zsqrt2_val y, zsqrt2_val z])"

definition ze_x :: zvec3 where
  "ze_x = ((1, 0), (0, 0), (0, 0))"

definition ze_y :: zvec3 where
  "ze_y = ((0, 0), (1, 0), (0, 0))"

definition ze_z :: zvec3 where
  "ze_z = ((0, 0), (0, 0), (1, 0))"

definition zRx_step :: "zvec3 ⇒ zvec3" where
  "zRx_step v = (case v of (x, y, z) ⇒
     (zsqrt2_scale 3 x,
      zsqrt2_sub y (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 z)),
      zsqrt2_add (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 y)) z))"

definition zRx_inv_step :: "zvec3 ⇒ zvec3" where
  "zRx_inv_step v = (case v of (x, y, z) ⇒
     (zsqrt2_scale 3 x,
      zsqrt2_add y (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 z)),
      zsqrt2_sub z (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 y))))"

definition zRz_step :: "zvec3 ⇒ zvec3" where
  "zRz_step v = (case v of (x, y, z) ⇒
     (zsqrt2_sub x (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 y)),
      zsqrt2_add (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 x)) y,
      zsqrt2_scale 3 z))"

definition zRz_inv_step :: "zvec3 ⇒ zvec3" where
  "zRz_inv_step v = (case v of (x, y, z) ⇒
     (zsqrt2_add x (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 y)),
      zsqrt2_sub y (zsqrt2_scale 2 (zsqrt2_mul_sqrt2 x)),
      zsqrt2_scale 3 z))"

definition zletter_step :: "bool × gen2 ⇒ zvec3 ⇒ zvec3" where
  "zletter_step p = (case p of
       (False, A) ⇒ zRx_step
     | (True,  A) ⇒ zRx_inv_step
     | (False, B) ⇒ zRz_step
     | (True,  B) ⇒ zRz_inv_step)"

definition zword_step :: "(bool × gen2) list ⇒ zvec3 ⇒ zvec3" where
  "zword_step w v = foldr (λp f. zletter_step p ∘ f) w id v"

definition zword_witness :: "(bool × gen2) list ⇒ zvec3" where
  "zword_witness w = (case snd (last w) of A ⇒ ze_y | B ⇒ ze_x)"

datatype r3 = R0 | R1 | R2

type_synonym rcoef = "r3 × r3"
type_synonym rvec3 = "rcoef × rcoef × rcoef"

fun r3_add :: "r3 ⇒ r3 ⇒ r3" where
  "r3_add R0 x = x"
| "r3_add x R0 = x"
| "r3_add R1 R1 = R2"
| "r3_add R1 R2 = R0"
| "r3_add R2 R1 = R0"
| "r3_add R2 R2 = R1"

fun r3_neg :: "r3 ⇒ r3" where
  "r3_neg R0 = R0"
| "r3_neg R1 = R2"
| "r3_neg R2 = R1"

definition r3_sub :: "r3 ⇒ r3 ⇒ r3" where
  "r3_sub x y = r3_add x (r3_neg y)"

fun r3_double :: "r3 ⇒ r3" where
  "r3_double R0 = R0"
| "r3_double R1 = R2"
| "r3_double R2 = R1"

definition rcoef_add :: "rcoef ⇒ rcoef ⇒ rcoef" where
  "rcoef_add p q = (r3_add (fst p) (fst q), r3_add (snd p) (snd q))"

definition rcoef_neg :: "rcoef ⇒ rcoef" where
  "rcoef_neg p = (r3_neg (fst p), r3_neg (snd p))"

definition rcoef_sub :: "rcoef ⇒ rcoef ⇒ rcoef" where
  "rcoef_sub p q = rcoef_add p (rcoef_neg q)"

definition rcoef_double :: "rcoef ⇒ rcoef" where
  "rcoef_double p = (r3_double (fst p), r3_double (snd p))"

definition rcoef_mul_sqrt2 :: "rcoef ⇒ rcoef" where
  "rcoef_mul_sqrt2 p = (r3_double (snd p), fst p)"

definition rRx_step :: "rvec3 ⇒ rvec3" where
  "rRx_step v = (case v of (x, y, z) ⇒
     ((R0, R0),
      rcoef_sub y (rcoef_double (rcoef_mul_sqrt2 z)),
      rcoef_add (rcoef_double (rcoef_mul_sqrt2 y)) z))"

definition rRx_inv_step :: "rvec3 ⇒ rvec3" where
  "rRx_inv_step v = (case v of (x, y, z) ⇒
     ((R0, R0),
      rcoef_add y (rcoef_double (rcoef_mul_sqrt2 z)),
      rcoef_sub z (rcoef_double (rcoef_mul_sqrt2 y))))"

definition rRz_step :: "rvec3 ⇒ rvec3" where
  "rRz_step v = (case v of (x, y, z) ⇒
     (rcoef_sub x (rcoef_double (rcoef_mul_sqrt2 y)),
      rcoef_add (rcoef_double (rcoef_mul_sqrt2 x)) y,
      (R0, R0)))"

definition rRz_inv_step :: "rvec3 ⇒ rvec3" where
  "rRz_inv_step v = (case v of (x, y, z) ⇒
     (rcoef_add x (rcoef_double (rcoef_mul_sqrt2 y)),
      rcoef_sub y (rcoef_double (rcoef_mul_sqrt2 x)),
      (R0, R0)))"

definition rletter_step :: "bool × gen2 ⇒ rvec3 ⇒ rvec3" where
  "rletter_step p = (case p of
       (False, A) ⇒ rRx_step
     | (True,  A) ⇒ rRx_inv_step
     | (False, B) ⇒ rRz_step
     | (True,  B) ⇒ rRz_inv_step)"

definition rword_step :: "(bool × gen2) list ⇒ rvec3 ⇒ rvec3" where
  "rword_step w v = foldr (λp f. rletter_step p ∘ f) w id v"

definition re_x :: rvec3 where
  "re_x = ((R1, R0), (R0, R0), (R0, R0))"

definition re_y :: rvec3 where
  "re_y = ((R0, R0), (R1, R0), (R0, R0))"

definition rword_witness :: "(bool × gen2) list ⇒ rvec3" where
  "rword_witness w = (case snd (last w) of A ⇒ re_y | B ⇒ re_x)"

definition rzero_vec :: rvec3 where
  "rzero_vec = ((R0, R0), (R0, R0), (R0, R0))"

definition rstate :: "bool × gen2 ⇒ rvec3 ⇒ bool" where
  "rstate p v ⟷
    v ∈ (case p of
       (False, A) ⇒ {
          ((R0, R0), (R0, R1), (R1, R0)),
          ((R0, R0), (R0, R2), (R2, R0)),
          ((R0, R0), (R1, R0), (R0, R2)),
          ((R0, R0), (R2, R0), (R0, R1))}
     | (True, A) ⇒ {
          ((R0, R0), (R0, R1), (R2, R0)),
          ((R0, R0), (R0, R2), (R1, R0)),
          ((R0, R0), (R1, R0), (R0, R1)),
          ((R0, R0), (R2, R0), (R0, R2))}
     | (False, B) ⇒ {
          ((R0, R1), (R1, R0), (R0, R0)),
          ((R0, R2), (R2, R0), (R0, R0)),
          ((R1, R0), (R0, R2), (R0, R0)),
          ((R2, R0), (R0, R1), (R0, R0))}
     | (True, B) ⇒ {
          ((R0, R1), (R2, R0), (R0, R0)),
          ((R0, R2), (R1, R0), (R0, R0)),
          ((R1, R0), (R0, R1), (R0, R0)),
          ((R2, R0), (R0, R2), (R0, R0))})"

lemma rstate_single:
  "rstate p (rletter_step p (case snd p of A ⇒ re_y | B ⇒ re_x))"
  by (cases p)
    (auto split: bool.splits gen2.splits
      simp: rstate_def rletter_step_def rRx_step_def rRx_inv_step_def
        rRz_step_def rRz_inv_step_def re_x_def re_y_def rcoef_add_def
        rcoef_sub_def rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def)

lemma rstate_step_FA_FA:
  "rstate (False, A) v ⟹ rstate (False, A) (rletter_step (False, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_FA_FB:
  "rstate (False, B) v ⟹ rstate (False, A) (rletter_step (False, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_FA_TB:
  "rstate (True, B) v ⟹ rstate (False, A) (rletter_step (False, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TA_TA:
  "rstate (True, A) v ⟹ rstate (True, A) (rletter_step (True, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TA_FB:
  "rstate (False, B) v ⟹ rstate (True, A) (rletter_step (True, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TA_TB:
  "rstate (True, B) v ⟹ rstate (True, A) (rletter_step (True, A) v)"
  by (simp add: rstate_def rletter_step_def rRx_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_FB_FB:
  "rstate (False, B) v ⟹ rstate (False, B) (rletter_step (False, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_FB_FA:
  "rstate (False, A) v ⟹ rstate (False, B) (rletter_step (False, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_FB_TA:
  "rstate (True, A) v ⟹ rstate (False, B) (rletter_step (False, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TB_TB:
  "rstate (True, B) v ⟹ rstate (True, B) (rletter_step (True, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TB_FA:
  "rstate (False, A) v ⟹ rstate (True, B) (rletter_step (True, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemma rstate_step_TB_TA:
  "rstate (True, A) v ⟹ rstate (True, B) (rletter_step (True, B) v)"
  by (simp add: rstate_def rletter_step_def rRz_inv_step_def rcoef_add_def rcoef_sub_def
      rcoef_neg_def rcoef_double_def rcoef_mul_sqrt2_def r3_sub_def; elim disjE; simp)

lemmas rstate_step_cases =
  rstate_step_FA_FA rstate_step_FA_FB rstate_step_FA_TB
  rstate_step_TA_TA rstate_step_TA_FB rstate_step_TA_TB
  rstate_step_FB_FB rstate_step_FB_FA rstate_step_FB_TA
  rstate_step_TB_TB rstate_step_TB_FA rstate_step_TB_TA

lemma rstate_step:
  assumes "rstate q v" and "¬ canceling p q"
  shows "rstate p (rletter_step p v)"
  using assms
  by (cases p; cases q; cases "fst p"; cases "snd p"; cases "fst q"; cases "snd q")
    (auto simp: canceling_def rstate_step_cases)

lemma rstate_nonzero:
  assumes "rstate p v"
  shows "v ≠ rzero_vec"
  using assms
  by (cases p)
    (auto split: bool.splits gen2.splits simp: rstate_def rzero_vec_def)

lemma rword_step_Cons [simp]:
  "rword_step (p # w) v = rletter_step p (rword_step w v)"
  by (simp add: rword_step_def)

lemma zword_step_Cons [simp]:
  "zword_step (p # w) v = zletter_step p (zword_step w v)"
  by (simp add: zword_step_def)

lemma rword_witness_Cons_nonempty [simp]:
  assumes "w ≠ []"
  shows "rword_witness (p # w) = rword_witness w"
  using assms by (cases w) (simp_all add: rword_witness_def)

lemma rword_step_witness_state:
  assumes "w ∈ carrier F2" and "w ≠ []"
  shows "rstate (hd w) (rword_step w (rword_witness w))"
  using assms
proof (induct w)
  case Nil
  then show ?case
    by simp
next
  case (Cons p w)
  have tail: "w ∈ carrier F2" and ncan_tail: "w = [] ∨ ¬ canceling p (hd w)"
    using Cons.prems(1) by (auto dest: F2_ConsD)
  show ?case
  proof (cases w)
    case Nil
    then show ?thesis
      using rstate_single[of p] by (simp add: rword_step_def rword_witness_def)
  next
    case (Cons q ws)
    have "rstate q (rword_step (q # ws) (rword_witness (q # ws)))"
      using Cons.hyps[OF tail] Cons by simp
    moreover have "¬ canceling p q"
      using ncan_tail Cons by simp
    ultimately have "rstate p (rletter_step p (rword_step (q # ws) (rword_witness (q # ws))))"
      by (rule rstate_step)
    then show ?thesis
      using Cons by simp
  qed
qed

definition r3_of_int :: "int ⇒ r3" where
  "r3_of_int n = (if n mod 3 = 0 then R0 else if n mod 3 = 1 then R1 else R2)"

definition rcoef_of_z :: "zsqrt2 ⇒ rcoef" where
  "rcoef_of_z p = (r3_of_int (fst p), r3_of_int (snd p))"

definition rvec3_of_z :: "zvec3 ⇒ rvec3" where
  "rvec3_of_z v = (case v of (x, y, z) ⇒ (rcoef_of_z x, rcoef_of_z y, rcoef_of_z z))"

lemma r3_of_int_add:
  "r3_of_int (a + b) = r3_add (r3_of_int a) (r3_of_int b)"
  by (auto simp: r3_of_int_def split: if_splits; presburger)

lemma r3_of_int_neg:
  "r3_of_int (- a) = r3_neg (r3_of_int a)"
  by (auto simp: r3_of_int_def split: if_splits; presburger)

lemma r3_of_int_sub:
  "r3_of_int (a - b) = r3_add (r3_of_int a) (r3_neg (r3_of_int b))"
  by (auto simp: r3_of_int_def split: if_splits; presburger)

lemma r3_of_int_double:
  "r3_of_int (2 * a) = r3_double (r3_of_int a)"
  by (auto simp: r3_of_int_def split: if_splits; presburger)

lemma r3_of_int_triple:
  "r3_of_int (3 * a) = R0"
  by (simp add: r3_of_int_def)

lemma rcoef_of_z_simps [simp]:
  "rcoef_of_z (zsqrt2_add p q) = rcoef_add (rcoef_of_z p) (rcoef_of_z q)"
  "rcoef_of_z (zsqrt2_neg p) = rcoef_neg (rcoef_of_z p)"
  "rcoef_of_z (zsqrt2_sub p q) = rcoef_sub (rcoef_of_z p) (rcoef_of_z q)"
  "rcoef_of_z (zsqrt2_scale 2 p) = rcoef_double (rcoef_of_z p)"
  "rcoef_of_z (zsqrt2_scale 3 p) = (R0, R0)"
  "rcoef_of_z (zsqrt2_mul_sqrt2 p) = rcoef_mul_sqrt2 (rcoef_of_z p)"
  by (simp_all add: rcoef_of_z_def zsqrt2_add_def zsqrt2_neg_def zsqrt2_sub_def
      zsqrt2_scale_def zsqrt2_mul_sqrt2_def rcoef_add_def rcoef_neg_def rcoef_sub_def
      rcoef_double_def rcoef_mul_sqrt2_def r3_of_int_add r3_of_int_neg
      r3_of_int_sub r3_of_int_double r3_of_int_triple)

lemma rvec3_of_z_basis [simp]:
  "rvec3_of_z ze_x = re_x"
  "rvec3_of_z ze_y = re_y"
  by (simp_all add: rvec3_of_z_def rcoef_of_z_def ze_x_def ze_y_def re_x_def re_y_def r3_of_int_def)

lemma rstep_of_z_simps [simp]:
  "rvec3_of_z (zRx_step v) = rRx_step (rvec3_of_z v)"
  "rvec3_of_z (zRx_inv_step v) = rRx_inv_step (rvec3_of_z v)"
  "rvec3_of_z (zRz_step v) = rRz_step (rvec3_of_z v)"
  "rvec3_of_z (zRz_inv_step v) = rRz_inv_step (rvec3_of_z v)"
  by (cases v; simp add: rvec3_of_z_def zRx_step_def zRx_inv_step_def zRz_step_def
        zRz_inv_step_def rRx_step_def rRx_inv_step_def rRz_step_def rRz_inv_step_def)+

lemma rletter_step_of_z [simp]:
  "rvec3_of_z (zletter_step p v) = rletter_step p (rvec3_of_z v)"
  by (cases p)
    (auto split: bool.splits gen2.splits simp: zletter_step_def rletter_step_def)

lemma rword_step_of_z [simp]:
  "rvec3_of_z (zword_step w v) = rword_step w (rvec3_of_z v)"
proof (induct w arbitrary: v)
  case Nil
  then show ?case
    by (simp add: zword_step_def rword_step_def)
next
  case (Cons p w)
  then show ?case
    by simp
qed

lemma rword_witness_of_z [simp]:
  "rvec3_of_z (zword_witness w) = rword_witness w"
  by (cases "snd (last w)")
    (simp_all add: zword_witness_def rword_witness_def)

lemma r3_of_int_eq_R0_iff:
  "r3_of_int n = R0 ⟷ 3 dvd n"
  by (simp add: r3_of_int_def dvd_eq_mod_eq_0)

lemma rcoef_of_z_zero_iff:
  "rcoef_of_z p = (R0, R0) ⟷ zsqrt2_div3 p"
  by (cases p) (simp add: rcoef_of_z_def zsqrt2_div3_def r3_of_int_eq_R0_iff)

lemma rvec3_of_z_zero_iff:
  "rvec3_of_z v = rzero_vec ⟷ zvec3_div3 v"
  by (cases v) (simp add: rvec3_of_z_def rzero_vec_def zvec3_div3_def rcoef_of_z_zero_iff)

lemma zsqrt2_val_simps [simp]:
  "zsqrt2_val (zsqrt2_add p q) = zsqrt2_val p + zsqrt2_val q"
  "zsqrt2_val (zsqrt2_neg p) = - zsqrt2_val p"
  "zsqrt2_val (zsqrt2_sub p q) = zsqrt2_val p - zsqrt2_val q"
  "zsqrt2_val (zsqrt2_scale n p) = of_int n * zsqrt2_val p"
  unfolding zsqrt2_val_def zsqrt2_add_def zsqrt2_neg_def zsqrt2_sub_def zsqrt2_scale_def
  by (simp_all add: algebra_simps)

lemma zsqrt2_mul_sqrt2_val [simp]:
  "zsqrt2_val (zsqrt2_mul_sqrt2 p) = sqrt 2 * zsqrt2_val p"
  unfolding zsqrt2_val_def zsqrt2_mul_sqrt2_def
  by (simp add: algebra_simps)

lemma sqrt_prime_irrational_dev:
  fixes p :: nat
  assumes "prime p"
  shows "sqrt p ∉ ℚ"
proof
  from assms have p: "p > 1"
    by (rule prime_gt_1_nat)
  assume "sqrt p ∈ ℚ"
  then obtain m n :: nat
    where n: "n ≠ 0"
      and sqrt_rat: "¦sqrt p¦ = m / n"
      and "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  have eq: "m⇧2 = p * n⇧2"
  proof -
    from n sqrt_rat have "m = ¦sqrt p¦ * n"
      by simp
    then have "m⇧2 = (sqrt p)⇧2 * n⇧2"
      by (simp add: power_mult_distrib)
    also have "(sqrt p)⇧2 = p"
      by simp
    also have "… * n⇧2 = p * n⇧2"
      by simp
    finally show ?thesis
      by linarith
  qed
  have "p dvd m ∧ p dvd n"
  proof
    from eq have "p dvd m⇧2" ..
    with assms show "p dvd m"
      by (rule prime_dvd_power)
    then obtain k where "m = p * k" ..
    with eq have "p * n⇧2 = p⇧2 * k⇧2"
      by algebra
    with p have "n⇧2 = p * k⇧2"
      by (simp add: power2_eq_square)
    then have "p dvd n⇧2" ..
    with assms show "p dvd n"
      by (rule prime_dvd_power)
  qed
  then have "p dvd gcd m n"
    by simp
  with ‹coprime m n› have "p = 1"
    by simp
  with p show False
    by simp
qed

lemma sqrt_2_not_rat_dev: "sqrt 2 ∉ ℚ"
  using sqrt_prime_irrational_dev[of 2] by simp

lemma zsqrt2_val_eq_iff:
  "zsqrt2_val p = zsqrt2_val q ⟷ p = q"
proof
  assume eq: "zsqrt2_val p = zsqrt2_val q"
  obtain a b c d where defs: "p = (a, b)" "q = (c, d)"
    by (cases p; cases q) auto
  let ?A = "a - c"
  let ?B = "b - d"
  from eq defs have eq0: "of_int ?A + of_int ?B * sqrt 2 = (0::real)"
    by (simp add: zsqrt2_val_def algebra_simps)
  have "?B = 0"
  proof (rule ccontr)
    assume "?B ≠ 0"
    hence "sqrt 2 = - of_int ?A / of_int ?B"
      using eq0 by (simp add: field_simps)
    moreover have "- of_int ?A / of_int ?B ∈ ℚ"
      by simp
    ultimately have "sqrt 2 ∈ ℚ"
      by simp
    with sqrt_2_not_rat_dev show False
      by simp
  qed
  moreover with eq0 have "?A = 0"
    by simp
  ultimately show "p = q"
    using defs by simp
qed simp

lemma zvec3_val_eq_iff:
  "zvec3_val u = zvec3_val v ⟷ u = v"
  by (cases u; cases v)
    (auto simp: zvec3_val_def vector_def vec_eq_iff forall_3 zsqrt2_val_eq_iff)

lemma zvec3_scale_val [simp]:
  "zvec3_val (zvec3_scale n v) = scaleR (of_int n) (zvec3_val v)"
  by (cases v)
    (simp add: zvec3_scale_def zvec3_val_def vector_def vec_eq_iff forall_3)

lemma sqrt8_eq_2_sqrt2: "sqrt 8 = 2 * sqrt 2"
  proof -
  have "sqrt (8::real) = sqrt ((4::real) * 2)"
    by simp
  also have "… = sqrt (4::real) * sqrt 2"
    by (subst real_sqrt_mult) simp
  also have "… = 2 * sqrt 2"
    by simp
  finally show ?thesis .
qed

lemma zletter_step_single_mod3:
  "¬ zvec3_div3 (zletter_step (False, A) ze_y)"
  "¬ zvec3_div3 (zletter_step (True, A) ze_y)"
  "¬ zvec3_div3 (zletter_step (False, B) ze_x)"
  "¬ zvec3_div3 (zletter_step (True, B) ze_x)"
  by (simp_all add: zletter_step_def zRx_step_def zRx_inv_step_def zRz_step_def zRz_inv_step_def
      ze_x_def ze_y_def zvec3_div3_def zsqrt2_div3_def zsqrt2_add_def zsqrt2_sub_def
      zsqrt2_neg_def zsqrt2_scale_def zsqrt2_mul_sqrt2_def)

lemma zRx_step_val:
  "zvec3_val (zRx_step v) = scaleR 3 (Rx (zvec3_val v))"
  by (cases v)
    (simp add: zvec3_val_def zRx_step_def Rx_def Rx_mat_def rot_c_def rot_s_def
      sqrt8_eq_2_sqrt2 matrix_vector_mult_def vector_def vec_eq_iff sum_3 forall_3 algebra_simps)

lemma zRx_inv_step_val:
  "zvec3_val (zRx_inv_step v) = scaleR 3 (Rx_inv (zvec3_val v))"
  by (cases v)
    (simp add: zvec3_val_def zRx_inv_step_def Rx_inv_def Rx_inv_mat_def rot_c_def rot_s_def
      sqrt8_eq_2_sqrt2 matrix_vector_mult_def vector_def vec_eq_iff sum_3 forall_3 algebra_simps)

lemma zRz_step_val:
  "zvec3_val (zRz_step v) = scaleR 3 (Rz (zvec3_val v))"
  by (cases v)
    (simp add: zvec3_val_def zRz_step_def Rz_def Rz_mat_def rot_c_def rot_s_def
      sqrt8_eq_2_sqrt2 matrix_vector_mult_def vector_def vec_eq_iff sum_3 forall_3 algebra_simps)

lemma zRz_inv_step_val:
  "zvec3_val (zRz_inv_step v) = scaleR 3 (Rz_inv (zvec3_val v))"
  by (cases v)
    (simp add: zvec3_val_def zRz_inv_step_def Rz_inv_def Rz_inv_mat_def rot_c_def rot_s_def
      sqrt8_eq_2_sqrt2 matrix_vector_mult_def vector_def vec_eq_iff sum_3 forall_3 algebra_simps)

lemma zletter_step_val:
  "zvec3_val (zletter_step p v) = scaleR 3 (letter_to_rot p (zvec3_val v))"
  by (cases p)
    (auto split: bool.splits gen2.splits
      simp: zletter_step_def letter_to_rot_def zRx_step_val zRx_inv_step_val
        zRz_step_val zRz_inv_step_val)

lemma letter_to_rot_linear: "linear (letter_to_rot p)"
  unfolding letter_to_rot_def Rx_def Rx_inv_def Rz_def Rz_inv_def
  by (cases p)
    (simp split: bool.splits gen2.splits add: matrix_vector_mul_linear)

lemma zword_step_val:
  "zvec3_val (zword_step w v) =
    scaleR ((3::real) ^ length w) (sigma w (zvec3_val v))"
proof (induct w arbitrary: v)
  case Nil
  show ?case
    by (simp add: zword_step_def)
next
  case (Cons p w)
  have lin: "linear (letter_to_rot p)"
    by (rule letter_to_rot_linear)
  have "zvec3_val (zword_step (p # w) v) =
      zvec3_val (zletter_step p (zword_step w v))"
    by (simp add: zword_step_def)
  also have "… = scaleR 3 (letter_to_rot p (zvec3_val (zword_step w v)))"
    by (rule zletter_step_val)
  also have "… =
      scaleR 3 (letter_to_rot p
        (scaleR ((3::real) ^ length w) (sigma w (zvec3_val v))))"
    using Cons.hyps by simp
  also have "… =
      scaleR ((3::real) ^ Suc (length w)) ((letter_to_rot p ∘ sigma w) (zvec3_val v))"
    using linear.scaleR[OF lin, of "((3::real) ^ length w)" "sigma w (zvec3_val v)"]
    by (simp add: scaleR_scaleR mult_ac)
  also have "… = scaleR ((3::real) ^ length (p # w)) (sigma (p # w) (zvec3_val v))"
    by simp
  finally show ?case .
qed

lemma zvec3_scale_power3_div3:
  assumes "n > 0"
  shows "zvec3_div3 (zvec3_scale ((3::int) ^ n) v)"
  using assms
  by (cases v)
    (auto simp: zvec3_div3_def zsqrt2_div3_def zvec3_scale_def zsqrt2_scale_def
      intro!: dvd_mult2)

lemma zword_step_identity_div3:
  assumes "w ≠ []" and "sigma w = id"
  shows "zvec3_div3 (zword_step w (zword_witness w))"
proof -
  have len_pos: "length w > 0"
    using assms(1) by (cases w) auto
  have "zvec3_val (zword_step w (zword_witness w)) =
      scaleR ((3::real) ^ length w) (zvec3_val (zword_witness w))"
    using zword_step_val[of w "zword_witness w"] assms(2) by simp
  also have "… = zvec3_val (zvec3_scale ((3::int) ^ length w) (zword_witness w))"
    by simp
  finally have "zword_step w (zword_witness w) =
      zvec3_scale ((3::int) ^ length w) (zword_witness w)"
    using zvec3_val_eq_iff by blast
  thus ?thesis
    using zvec3_scale_power3_div3[OF len_pos, of "zword_witness w"] by simp
qed

lemma zword_step_witness_not_div3_if_nonempty_F2:
  assumes "w ∈ carrier F2" and "w ≠ []"
  shows "¬ zvec3_div3 (zword_step w (zword_witness w))"
proof
  assume div3: "zvec3_div3 (zword_step w (zword_witness w))"
  have "rstate (hd w) (rword_step w (rword_witness w))"
    using assms by (rule rword_step_witness_state)
  hence "rword_step w (rword_witness w) ≠ rzero_vec"
    by (rule rstate_nonzero)
  moreover from div3 have "rword_step w (rword_witness w) = rzero_vec"
    by (simp add: rvec3_of_z_zero_iff[symmetric])
  ultimately show False
    by contradiction
qed

text ‹The word interpretation is an injective homomorphism into ‹SO(3)›.›
theorem sigma_homomorphism:
  assumes "w1 ∈ carrier F2" "w2 ∈ carrier F2"
  shows "sigma (w1 ⊗⇘F2⇙ w2) = sigma w1 ∘ sigma w2"
  by (simp add: F2_mult)

theorem sigma_nontrivial_word_not_id:
  assumes "w ∈ carrier F2" and "w ≠ []"
  shows "sigma w ≠ id"
proof
  assume "sigma w = id"
  hence "zvec3_div3 (zword_step w (zword_witness w))"
    using assms(2) by (intro zword_step_identity_div3)
  moreover have "¬ zvec3_div3 (zword_step w (zword_witness w))"
    using assms by (rule zword_step_witness_not_div3_if_nonempty_F2)
  ultimately show False
    by simp
qed

lemma sigma_injective_if_trivial_kernel:
  assumes kernel: "⋀w. w ∈ carrier F2 ⟹ w ≠ [] ⟹ sigma w ≠ id"
  shows "inj_on sigma (carrier F2)"
proof (rule inj_onI)
  interpret F: group F2
    by (rule F2_is_group)
  fix w v
  assume w: "w ∈ carrier F2" and v: "v ∈ carrier F2" and eq: "sigma w = sigma v"
  let ?iv = "inv⇘F2⇙ v"
  have iv: "?iv ∈ carrier F2"
    using v by (rule F.inv_closed)
  have prod: "w ⊗⇘F2⇙ ?iv ∈ carrier F2"
    using w iv by (rule F.m_closed)
  have "sigma (w ⊗⇘F2⇙ ?iv) = sigma w ∘ sigma ?iv"
    using w iv by (rule sigma_homomorphism)
  also have "… = sigma v ∘ sigma ?iv"
    using eq by simp
  also have "… = sigma (v ⊗⇘F2⇙ ?iv)"
    using v iv by (rule sigma_homomorphism[symmetric])
  also have "… = sigma []"
    using F.r_inv[OF v] by simp
  also have "… = id"
    by simp
  finally have prod_id: "sigma (w ⊗⇘F2⇙ ?iv) = id" .
  have prod_one: "w ⊗⇘F2⇙ ?iv = []"
  proof (rule ccontr)
    assume "w ⊗⇘F2⇙ ?iv ≠ []"
    with kernel[OF prod] prod_id show False
      by simp
  qed
  have "w = w ⊗⇘F2⇙ 𝟭⇘F2⇙"
    using w by simp
  moreover have "?iv ⊗⇘F2⇙ v = 𝟭⇘F2⇙"
    using v by (rule F.l_inv)
  ultimately have "w = w ⊗⇘F2⇙ (?iv ⊗⇘F2⇙ v)"
    by simp
  also have "… = (w ⊗⇘F2⇙ ?iv) ⊗⇘F2⇙ v"
    using w iv v by (simp add: F.m_assoc)
  also have "… = v"
    using prod_one v by simp
  finally show "w = v" .
qed

theorem sigma_injective_on_F2:
  "inj_on sigma (carrier F2)"
  by (rule sigma_injective_if_trivial_kernel) (rule sigma_nontrivial_word_not_id)

theorem sigma_image_in_SO3:
  assumes "w ∈ carrier F2"
  shows "sigma w ∈ SO3"
  by (rule sigma_in_SO3)

text ‹
  These three theorems together establish that ‹sigma› is a
  group monomorphism from ‹F⇩2› to SO(3) -- i.e., the image
  is a copy of ‹F⇩2› inside SO(3). This supplies the free subgroup
  used in the geometric part of the Banach-Tarski theorem.
›

end