Theory Periodicity_Lemma
theory Periodicity_Lemma
imports CoWBasic
begin
chapter "The Periodicity Lemma"
text‹The Periodicity Lemma says that if a sufficiently long word has two periods p and q,
then the period can be refined to @{term "gcd p q"}.
The consequence is equivalent to the fact that the corresponding periodic roots commute.
``Sufficiently long'' here means at least @{term "p + q - gcd p q"}.
It is also known as the Fine and Wilf theorem due to its authors @{cite FineWilf}.›
text‹
If we relax the requirement to @{term "p + q"}, then the claim becomes easy, and it is proved in @{theory Combinatorics_Words.CoWBasic} as @{term two_pers_root}: @{thm[names_long] two_pers_root[no_vars]}.
›
theorem per_lemma_relaxed:
assumes "period w p" and "period w q" and "p + q ≤ ❙|w❙|"
shows "(take p w)⋅(take q w) = (take q w)⋅(take p w)"
using two_pers_root[OF
‹period w p›[unfolded period_def[of w p]]
‹period w q›[unfolded period_def[of w q]], unfolded
take_len[OF add_leD1[OF ‹p + q ≤ ❙|w❙|›]]
take_len[OF add_leD2[OF ‹p + q ≤ ❙|w❙|›]], OF ‹p + q ≤ ❙|w❙|›].
text‹Also in terms of the numeric period:›
thm two_periods
section ‹Main claim›
text‹We first formulate the claim of the Periodicity lemma in terms of commutation of two periodic roots.
For trivial reasons we can also drop the requirement that the roots are nonempty.
›
theorem per_lemma_comm:
assumes "w ≤p r ⋅ w" and "w ≤p s ⋅ w"
and len: "❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|"
shows "r ⋅ s = s ⋅ r"
using assms
proof (induction "❙|s❙| + ❙|s❙| + ❙|r❙|" arbitrary: w r s rule: less_induct)
case less
consider (empty) "s = ε" | (short) "❙|r❙| < ❙|s❙|" | (step) "s ≠ ε ∧ ❙|s❙| ≤ ❙|r❙|" by force
then show ?case
proof (cases)
case (empty)
thus "r ⋅ s = s ⋅ r" by fastforce
next
case (short)
thus "r ⋅ s = s ⋅ r"
using "less.hyps"[OF _ ‹ w ≤p s ⋅ w› ‹ w ≤p r ⋅ w›
‹❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|›[unfolded gcd.commute[of "❙|r❙|"] add.commute[of "❙|r❙|"]]] by fastforce
next
case (step)
hence "s ≠ ε" and "❙|s❙| ≤ ❙|r❙|" by blast+
from le_add_diff[OF gcd_le2_nat[OF ‹s ≠ ε›[folded length_0_conv], of "❙|r❙|"], unfolded gcd.commute[of "❙|r❙|"], of "❙|r❙|"]
have "❙|r❙| ≤ ❙|w❙|"
using ‹❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|›[unfolded gcd.commute[of "❙|r❙|"] add.commute[of "❙|r❙|"]] order.trans by blast
hence "❙|s❙| ≤ ❙|w❙|"
using ‹❙|s❙| ≤ ❙|r❙|› order.trans by blast
from pref_prod_long[OF ‹w ≤p s ⋅ w› this]
have "s ≤p w".
obtain w' where "s ⋅ w' = w" and "❙|w'❙| < ❙|w❙|"
using ‹s ≠ ε› ‹s ≤p w›[unfolded prefix_def]
by force
have "w' ≤p w"
using ‹w ≤p s ⋅ w› unfolding ‹s ⋅ w' = w›[symmetric] pref_cancel_conv.
from this[folded ‹s ⋅ w' = w›]
have "w' ≤p s⋅w'".
have "s ≤p r"
using pref_prod_le[OF prefix_order.trans[OF ‹s ≤p w› ‹w ≤p r ⋅ w›] ‹❙|s❙| ≤ ❙|r❙|›].
hence "w' ≤p (s¯⇧>r) ⋅ w'"
using ‹w ≤p r ⋅ w› ‹s ⋅ w' = w› pref_prod_pref[OF _ ‹w' ≤p w›, of "s¯⇧>r"]
unfolding prefix_def by fastforce
have ind_len: "❙|s¯⇧>r❙| + ❙|s❙| - (gcd ❙|s¯⇧>r❙| ❙|s❙|) ≤ ❙|w'❙|"
using ‹❙|r❙| + ❙|s❙| - (gcd ❙|r❙| ❙|s❙|) ≤ ❙|w❙|›[folded ‹s ⋅ w' = w›]
unfolding pref_gcd_lq[OF ‹s ≤p r›, unfolded gcd.commute[of "❙|s❙|"]] lenmorph lq_short_len[OF ‹s ≤p r›, unfolded add.commute[of "❙|s❙|"]] by force
have "s ⋅ s¯⇧>r = s¯⇧>r ⋅ s"
using "less.hyps"[OF _ ‹w' ≤p (s¯⇧>r) ⋅ w'› ‹w' ≤p s ⋅ w'› ind_len] ‹s ≤p r› ‹❙|w'❙| < ❙|w❙|›
unfolding prefix_def
by force
thus "r ⋅ s = s ⋅ r"
using ‹s ≤p r› by (fastforce simp add: prefix_def)
qed
qed
lemma per_lemma_comm_pref:
assumes "u ≤p r⇧@k" "u ≤p s⇧@l"
and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "r ⋅ s = s ⋅ r"
using pref_prod_root[OF assms(2)] pref_prod_root[OF assms(1)] per_lemma_comm[OF _ _ len] by blast
text‹We can now prove the numeric version.›
theorem per_lemma: assumes "period w p" and "period w q" and len: "p + q - gcd p q ≤ ❙|w❙|"
shows "period w (gcd p q)"
proof-
have takep: "w ≤p (take p w) ⋅ w" and takeq: "w ≤p (take q w) ⋅ w"
using ‹period w p› ‹period w q› per_pref by blast+
have "p ≤ ❙|w❙|"
using per_lemma_len_le[OF len] per_not_zero[OF ‹period w q›].
have lenp: "❙|take p w❙| = p"
using gcd_le2_pos[OF per_not_zero[OF ‹period w q›], of p] len take_len
by auto
have lenq: "❙|take q w❙| = q"
using gcd_le1_pos[OF per_not_zero[OF ‹period w p›], of q] len take_len
by simp
obtain t where "take p w ∈ t*" and "take q w ∈ t*"
using comm_rootE[OF per_lemma_comm[OF takep takeq, unfolded lenp lenq, OF len], of thesis] by blast
have "w <p t ⋅ w"
using ‹period w p›[unfolded period_def, THEN per_root_trans, OF ‹take p w ∈ t*›].
with per_nemp[OF ‹period w q›]
have "period w ❙|t❙|"
by (rule periodI)
have "❙|t❙| dvd (gcd p q)"
using common_root_len_gcd[OF ‹take p w ∈ t*› ‹take q w ∈ t*›] unfolding lenp lenq.
from dvd_div_mult_self[OF this]
have "gcd p q div ❙|t❙| * ❙|t❙| = gcd p q".
have "gcd p q ≠ 0"
using ‹period w p› by auto
from this[folded dvd_div_eq_0_iff[OF ‹❙|t❙| dvd (gcd p q)›]]
show "period w (gcd p q)"
using per_mult[OF ‹period w ❙|t❙|›, of "gcd p q div ❙|t❙|", unfolded dvd_div_mult_self[OF ‹❙|t❙| dvd (gcd p q)›]] by blast
qed
section ‹Optimality›
text‹@{term "FW_word"} (where FW stands for Fine and Wilf) yields a word which show the optimality of the bound in the Periodicity lemma.
Moreover, the obtained word has maximum possible letters (each equality of letters is forced by periods). The latter is not proved here.›
term "butlast ([0..<(gcd p q)]⇧@(p div (gcd p q)))⋅[gcd p q]⋅(butlast ([0..<(gcd p q)]⇧@(p div (gcd p q))))"
lemma ext_per_sum: assumes "period w p" and "period w q" and "p ≤ ❙|w❙|"
shows "period ((take p w) ⋅ w) (p+q)"
proof-
have nemp: "take p w ⋅ take q w ≠ ε"
using ‹period w p› by auto
have "take (p + q) (take p w ⋅ w) = take p (take p w ⋅ w) ⋅ take q (drop p (take p w ⋅ w))"
using take_add by blast
also have "... = take p w ⋅ take q w"
by (simp add: ‹p ≤ ❙|w❙|›)
ultimately have sum: "take (p + q) (take p w ⋅ w) = take p w ⋅ take q w"
by presburger
note assms[unfolded period_def]
show ?thesis
unfolding period_def sum rassoc
using pref_spref_prolong[OF self_pref spref_spref_prolong[OF ‹w <p take q w ⋅ w› ‹w <p take p w ⋅ w›]].
qed
definition "fw_p_per p q ≡ butlast ([0..<(gcd p q)]⇧@(p div (gcd p q)))"
definition "fw_base p q ≡ fw_p_per p q ⋅ [gcd p q]⋅ fw_p_per p q"
fun FW_word :: "nat ⇒ nat ⇒ nat list" where
FW_word_def: "FW_word p q =
(if q < p then FW_word q p else
if p = 0 then ε else
if p = q then ε else
if gcd p q = q - p then fw_base p q
else (take p (FW_word p (q-p))) ⋅ FW_word p (q-p))"
lemma FW_sym: "FW_word p q = FW_word q p"
by (cases rule: linorder_cases[of p q]) simp+
theorem fw_word': "¬ p dvd q ⟹ ¬ q dvd p ⟹
❙|FW_word p q❙| = p + q - gcd p q - 1 ∧ period (FW_word p q) p ∧ period (FW_word p q) q ∧ ¬ period (FW_word p q) (gcd p q)"
proof (induction "p + p + q" arbitrary: p q rule: less_induct)
case less
have "p ≠ 0"
using ‹¬ q dvd p› dvd_0_right[of q] by meson
have "p ≠ q"
using ‹¬ p dvd q› by auto
then consider "q < p" | "p < q"
by linarith
then show ?case
proof (cases)
assume "q < p"
have less: "q + q + p < p + p + q"
by (simp add: ‹q < p›)
thus ?case
using "less.hyps"[OF _ ‹¬ q dvd p› ‹¬ p dvd q›]
unfolding FW_sym[of p q] gcd.commute[of p q] add.commute[of p q] by blast
next
let ?d = "gcd p q"
let ?dw = "[0..<(gcd p q)]"
let ?pd = "p div (gcd p q)"
assume "p < q"
thus ?thesis
proof (cases "?d = q - p")
assume "?d = q - p" hence "p + ?d = q" using ‹p < q› by auto
hence "p ≠ q" and "¬ q < p" using ‹p ≠ 0› ‹p < q› by fastforce+
hence fw: "FW_word p q = fw_base p q"
unfolding FW_word_def[of p q] using ‹p ≠ 0› ‹gcd p q = q - p› by presburger
have "❙|[0..<gcd p q]❙| = gcd p q"
by simp
hence *: "p div gcd p q * ❙|[0..<gcd p q]❙| = p"
by fastforce
have ppref: "❙|butlast (?dw⇧@?pd)⋅[?d]❙| = p"
using ‹p ≠ 0› unfolding lenmorph pow_len length_butlast sing_len * by fastforce
note ppref' = this[unfolded lenmorph]
have qpref: "❙|butlast (?dw⇧@?pd)⋅[?d]⋅?dw❙| = q"
unfolding lassoc lenmorph ppref' using ‹p + gcd p q = q› by simp
have "butlast (?dw⇧@?pd)⋅[?d] ≤p FW_word p q"
unfolding fw fw_base_def fw_p_per_def lassoc using triv_pref.
from pref_take[OF this]
have takep: "take p (FW_word p q) = butlast (?dw⇧@?pd)⋅[?d]"
unfolding ppref.
have "?dw ≠ ε" and "❙|?dw❙| = ?d"
using ‹p ≠ 0› by auto
have "?pd ≠ 0"
by (simp add: ‹p ≠ 0› dvd_div_eq_0_iff)
from not0_implies_Suc[OF this]
obtain e where "?pd = Suc e" by blast
have "gcd p q ≠ p"
using ‹¬ p dvd q› gcd_dvd2[of p q] by force
hence "Suc e ≠ 1"
using dvd_mult_div_cancel[OF gcd_dvd1[of p q], unfolded ‹?pd = Suc e›] by force
hence "e ≠ 0" by simp
have "[0..<gcd p q] ⇧@ e ≠ ε"
using ‹[0..<gcd p q] ≠ ε› ‹e ≠ 0› nonzero_pow_emp by blast
hence but_dec: "butlast (?dw⇧@?pd) = ?dw ⋅ butlast (?dw⇧@e)"
unfolding ‹?pd = Suc e› pow_Suc butlast_append if_not_P[OF ‹[0..<gcd p q] ⇧@ e ≠ ε›] by blast
have but_dec_b: "butlast (?dw⇧@?pd) = ?dw⇧@e ⋅ butlast ?dw"
unfolding ‹?pd = Suc e› pow_Suc' butlast_append if_not_P[OF ‹?dw ≠ ε›] by blast
have "butlast (?dw⇧@?pd)⋅[?d]⋅?dw ≤p FW_word p q"
unfolding fw but_dec lassoc fw_base_def fw_p_per_def by blast
note takeq = pref_take[OF this, unfolded qpref]
have "❙|FW_word p q❙| = p + q - gcd p q - 1"
proof-
have "p + q - (q - p) = p + p"
using ‹p + gcd p q = q› by auto
hence "❙|?dw⇧@?pd❙| = p"
unfolding pow_len ‹❙|[0..<gcd p q]❙| = gcd p q› by force
hence "❙|butlast (?dw⇧@?pd)❙| = p - 1"
unfolding length_butlast by argo
hence "❙|FW_word p q❙| = (p - 1) + 1 + (p - 1)"
unfolding fw lenmorph sing_len fw_base_def fw_p_per_def by presburger
thus "❙|FW_word p q❙| = p + q - gcd p q - 1"
unfolding ‹gcd p q = q - p› ‹p + q - (q - p) = p + p› using ‹p ≠ 0› by fastforce
qed
have "period (FW_word p q) p"
unfolding period_def
proof (rule per_rootI)
show "take p (FW_word p q) ≠ ε"
using ‹p ≠ 0› unfolding length_0_conv[symmetric] ppref[folded takep].
have "fw_base p q ≤p fw_p_per p q ⋅ [gcd p q] ⋅ fw_base p q"
unfolding rassoc pref_cancel_conv fw_base_def fw_p_per_def by blast
thus "FW_word p q ≤p take p (FW_word p q) ⋅ FW_word p q"
unfolding fw rassoc fw_p_per_def takep[unfolded fw].
qed
have "period (FW_word p q) q"
unfolding period_def
proof (rule per_rootI)
show "take q (FW_word p q) ≠ ε"
unfolding length_0_conv[symmetric] qpref[folded takeq] using ‹p ≠ 0› ‹p < q› by linarith
have "butlast ([0..<gcd p q] ⇧@ (p div gcd p q)) ≤p [0..<gcd p q] ⋅ butlast ([0..<gcd p q] ⇧@ (p div gcd p q))"
using pref_prod_root[OF prefixeq_butlast[of "[0..<gcd p q] ⇧@ (p div gcd p q)"]].
from pref_ext[OF this, unfolded rassoc]
have "fw_base p q ≤p fw_p_per p q ⋅ [gcd p q] ⋅ [0..<gcd p q] ⋅ fw_base p q"
unfolding rassoc pref_cancel_conv fw_base_def fw_p_per_def.
thus "FW_word p q ≤p take q (FW_word p q) ⋅ FW_word p q"
unfolding fw rassoc fw_p_per_def takeq[unfolded fw].
qed
have "¬ period (FW_word p q) ?d"
proof-
have last_a: "last (take p (FW_word p q)) = ?d"
unfolding takep nth_append_length[of "butlast (?dw ⇧@ ?pd)" "?d" ε]
last_snoc by blast
have "?dw ≤p FW_word p q"
unfolding fw but_dec rassoc fw_base_def fw_p_per_def by blast
from pref_take[OF this, unfolded ‹❙|?dw❙| = ?d›]
have takegcd: "take (gcd p q) (FW_word p q) = [0..<gcd p q]".
have fw_dec_b: "FW_word p q = [0..<gcd p q]⇧@e ⋅ butlast ([0..<gcd p q]) ⋅ [?d] ⋅ (butlast ([0..<gcd p q]⇧@(p div gcd p q)))"
unfolding fw but_dec_b rassoc fw_base_def fw_p_per_def ..
have gcdepref: "[0..<gcd p q]⇧@ Suc e ≤p take (gcd p q) (FW_word p q) ⋅ FW_word p q"
unfolding takegcd pow_Suc pref_cancel_conv unfolding fw_dec_b by blast
have "❙|[0..<gcd p q]⇧@ Suc e❙| = p"
unfolding pow_len ‹❙|?dw❙| = ?d› ‹?pd = Suc e›[symmetric] using
dvd_div_mult_self[OF gcd_dvd1].
from pref_take[OF gcdepref, unfolded this]
have takegcdp: "take p (take (gcd p q) (FW_word p q) ⋅ (FW_word p q)) = [0..<gcd p q]⇧@e ⋅ [0..<gcd p q]"
unfolding pow_Suc'.
have "0 < gcd p q" by (simp add: ‹p ≠ 0›)
from last_upt[OF this]
have last_b: "last (take p (take (gcd p q) (FW_word p q) ⋅ (FW_word p q))) = gcd p q - 1"
unfolding takegcdp last_appendR[of "[0..<gcd p q]" "[0..<gcd p q]⇧@e", OF ‹[0..<gcd p q] ≠ ε›].
have "p ≤ ❙|FW_word p q❙|"
unfolding ‹❙|FW_word p q❙| = p + q - gcd p q - 1› ‹gcd p q = q - p› using ‹p < q› by auto
have "gcd p q ≠ gcd p q - 1"
using ‹gcd p q = q - p› ‹p < q› by linarith
hence "take p (FW_word p q) ≠ take p (take (gcd p q) (FW_word p q) ⋅ (FW_word p q))"
unfolding last_b[symmetric] unfolding last_a[symmetric] using arg_cong[of _ _ last] by blast
hence "¬ FW_word p q ≤p take (gcd p q) (FW_word p q) ⋅ FW_word p q "
using pref_share_take[OF _ ‹p ≤ ❙|FW_word p q❙|›, of "take (gcd p q) (FW_word p q) ⋅ FW_word p q"] by blast
thus "¬ period (FW_word p q) (gcd p q)"
unfolding period_def by blast
qed
show ?thesis
using ‹period (FW_word p q) p› ‹period (FW_word p q) q›
‹❙|FW_word p q❙| = p + q - gcd p q - 1› ‹¬ period (FW_word p q) (gcd p q)› by blast
next
let ?d' = "gcd p (q-p)"
assume "gcd p q ≠ q - p"
hence fw: "FW_word p q = (take p (FW_word p (q-p))) ⋅ FW_word p (q-p)"
using FW_word_def ‹p ≠ 0› ‹p ≠ q› ‹p < q› by (meson less_Suc_eq not_less_eq)
have divhyp1: "¬ p dvd q - p"
using ‹¬ p dvd q› ‹p < q› dvd_minus_self by auto
have divhyp2: "¬ q - p dvd p"
proof (rule notI)
assume "q - p dvd p"
have "q = p + (q - p)"
by (simp add: ‹p < q› less_or_eq_imp_le)
from gcd_add2[of p "q - p", folded this, unfolded gcd_nat.absorb2[of "q - p" p, OF ‹q - p dvd p›]]
show "False"
using ‹gcd p q ≠ q - p› by blast
qed
have lenhyp: "p + p + (q - p) < p + p + q"
using ‹p < q› ‹p ≠ 0› by linarith
have "❙|FW_word p (q - p)❙| = p + (q - p) - ?d' - 1" and "period (FW_word p (q-p)) p" and "period (FW_word p (q-p)) (q-p)" and
"¬ period (FW_word p (q-p)) (gcd p (q-p))"
using "less.hyps"[OF _ divhyp1 divhyp2] lenhyp
by blast+
have "p + (q - p) = q"
using divhyp1 dvd_minus_self by auto
have "?d = ?d'"
using gcd_add2[of p "q-p", unfolded le_add_diff_inverse[OF less_imp_le[OF ‹p < q›]]].
have "?d ≠ q"
using ‹¬ q dvd p› gcd_dvd2[of q p, unfolded gcd.commute[of q]] by force
from this[unfolded nat_neq_iff]
have "?d < q"
using gr_implies_not0 ‹p < q› nat_dvd_not_less by blast
hence "1 ≤ q - ?d"
by linarith
have "?d' < q - p"
using gcd_le2_pos[OF per_not_zero[OF ‹period (FW_word p (q - p)) (q - p)›], of p] divhyp2[unfolded gcd_nat.absorb_iff2] nat_less_le by blast
hence "p ≤ ❙|(FW_word p (q - p))❙|"
unfolding ‹❙|FW_word p (q - p)❙| = p + (q - p) - ?d' - 1› diff_diff_left discrete by linarith
have "FW_word p (q - p) ≠ ε"
unfolding length_0_conv[symmetric] using ‹p ≤ ❙|FW_word p (q - p)❙|› ‹p ≠ 0›[folded le_zero_eq]
by linarith
have "❙|FW_word p q❙| = p + q - ?d - 1"
proof-
have "p + (q - p) = q" using less_imp_le[OF ‹p < q›] by fastforce
have "❙|FW_word p q❙| = ❙|take p (FW_word p (q - p))❙| + ❙|FW_word p (q - p)❙|"
using fw lenmorph[of "take p (FW_word p (q - p))" "FW_word p (q - p)"]
by presburger
also have "... = p + (p + (q - p) - ?d' - 1)"
unfolding ‹❙|FW_word p (q - p)❙| = p + (q - p) - ?d' - 1›
take_len[OF ‹p ≤ ❙|FW_word p (q - p)❙|›] by blast
also have "... = p + (q - ?d - 1)"
unfolding ‹?d = ?d'› ‹p + (q - p) = q›..
also have "... = p + (q - ?d) - 1"
using Nat.add_diff_assoc[OF ‹1 ≤ q - ?d›].
also have "... = p + q - ?d - 1"
by (simp add: ‹?d < q› less_or_eq_imp_le)
finally show "❙|FW_word p q❙| = p + q - ?d - 1"
by presburger
qed
have "period (FW_word p q) p"
using fw ext_per_left[OF ‹period (FW_word p (q-p)) p› ‹p ≤ ❙|FW_word p (q - p)❙|›]
by presburger
have "period (FW_word p q) q"
using ext_per_sum[OF ‹period (FW_word p (q - p)) p› ‹period (FW_word p (q - p)) (q - p)› ‹p ≤ ❙|FW_word p (q - p)❙|›, folded fw, unfolded ‹p + (q-p) = q›].
have "¬ period (FW_word p q) ?d"
using ‹¬ period (FW_word p (q -p)) (gcd p (q-p))›
unfolding ‹?d = ?d'›[symmetric]
using period_fac[of "take p (FW_word p (q - p))" "FW_word p (q - p)" ε "?d", unfolded append_Nil2,
OF _ ‹FW_word p (q - p) ≠ ε›, folded fw] by blast
thus ?thesis
using ‹period (FW_word p q) p› ‹period (FW_word p q) q› ‹❙|FW_word p q❙| = p + q - ?d - 1› by blast
qed
qed
qed
theorem fw_word: assumes "¬ p dvd q" "¬ q dvd p"
shows "❙|FW_word p q❙| = p + q - gcd p q - 1" and "period (FW_word p q) p" and "period (FW_word p q) q" and "¬ period (FW_word p q) (gcd p q)"
using fw_word'[OF assms] by blast+
text‹Calculation examples›
section "Other variants of the periodicity lemma"
text ‹Periodicity lemma is one of the most frequent tools in Combinatorics on words.
Here are some useful variants.›
text‹Note that the following lemmas are stronger versions of @{thm per_lemma_pref_suf fac_two_conjug_primroot fac_two_conjug_primroot' fac_two_conjug_primroot'' fac_two_prim_conjug} that have a relaxed length assumption @{term "❙|p❙| + ❙|q❙| ≤ ❙|w❙|"} instead of @{term "❙|p❙| + ❙|q❙| - (gcd ❙|p❙| ❙|q❙|) ≤ ❙|w❙|"} (and which follow from the relaxed version of periodicity lemma @{thm two_pers}.›
lemma per_lemma_pref_suf_gcd: assumes "w <p p ⋅ w" and "w <s w ⋅ q" and
fw: "❙|p❙| + ❙|q❙| - (gcd ❙|p❙| ❙|q❙|) ≤ ❙|w❙|"
obtains r s k l m where "p = (r ⋅ s)⇧@k" and "q = (s ⋅ r)⇧@l" and "w = (r ⋅ s)⇧@m ⋅ r" and "primitive (r⋅s)"
proof-
let ?q = "(w ⋅ q)⇧<¯w"
have "w <p ?q ⋅ w"
using ssufD1[OF ‹w <s w ⋅ q›] rq_suf[symmetric, THEN per_rootI[OF prefI rq_ssuf[OF ‹w <s w ⋅ q›]]]
by argo
have "q ∼ ?q"
by (meson assms(2) conjugI1 conjug_sym rq_suf suffix_order.less_imp_le)
have nemps': "p ≠ ε" "?q ≠ ε"
using assms(1) ‹w <p ?q⋅w› by fastforce+
have "❙|p❙| + ❙|?q❙| - gcd (❙|p❙|) (❙|?q❙|) ≤ ❙|w❙|" using fw
unfolding conjug_len[OF ‹q ∼ ?q›].
from per_lemma_comm[OF sprefD1[OF ‹w <p p ⋅ w›] sprefD1[OF ‹w <p ?q⋅w›] this]
have "p ⋅ ?q = ?q ⋅ p".
then have "ρ p = ρ ?q" using comm_primroots[OF nemps'] by force
hence [symmetric]: "ρ q ∼ ρ p"
using conjug_primroot[OF ‹q ∼ (w ⋅ q)⇧<¯w›]
by argo
from conjug_primrootsE[OF this]
obtain r s k l where
"p = (r ⋅ s) ⇧@ k" and
"q = (s ⋅ r) ⇧@ l" and
"primitive (r ⋅ s)".
have "w ≤p (r⋅s)⋅w"
using assms per_root_drop_exp sprefD1 ‹p = (r ⋅ s) ⇧@ k›
by meson
have "w ≤s w⋅(s⋅r)"
using assms(2) per_root_drop_exp[reversed] ssufD1 ‹q = (s ⋅ r) ⇧@ l›
by meson
have "❙|r ⋅ s❙| ≤ ❙|w❙|"
using conjug_nemp_iff[OF ‹q ∼ ?q›] dual_order.trans length_0_conv nemps' per_lemma_len_le[OF fw] primroot_len_le[OF nemps'(1)]
unfolding primroot_unique[OF nemps'(1) ‹primitive (r ⋅ s)› ‹p = (r ⋅ s) ⇧@ k›]
by blast
from root_suf_conjug[OF ‹primitive (r ⋅ s)› ‹w ≤p (r⋅s)⋅w› ‹w ≤s w⋅(s⋅r)› this]
obtain m where "w = (r ⋅ s) ⇧@ m ⋅ r".
from that[OF ‹p = (r ⋅ s) ⇧@ k› ‹q = (s ⋅ r) ⇧@ l› this ‹primitive (r ⋅ s)›]
show ?thesis.
qed
lemma fac_two_conjug_primroot_gcd:
assumes facs: "w ≤f p⇧@k" "w ≤f q⇧@l" and nemps: "p ≠ ε" "q ≠ ε" and len: "❙|p❙| + ❙|q❙| - gcd (❙|p❙|) (❙|q❙|) ≤ ❙|w❙|"
obtains r s m where "ρ p ∼ r ⋅ s" and "ρ q ∼ r ⋅ s" and "w = (r ⋅ s)⇧@m ⋅ r" and "primitive (r⋅s)"
proof -
obtain p' where "w <p p'⋅w" "p ∼ p'" "p' ≠ ε"
using conjug_nemp_iff fac_pow_pref_conjug[OF facs(1)] nemps(1) per_rootI' by metis
obtain q' where "w <s w⋅q'" "q ∼ q'" "q' ≠ ε"
using fac_pow_pref_conjug[reversed, OF ‹w ≤f q⇧@l›] conjug_nemp_iff nemps(2) per_rootI'[reversed] by metis
from per_lemma_pref_suf_gcd[OF ‹w <p p'⋅w› ‹w <s w⋅q'›]
obtain r s k l m where
"p' = (r ⋅ s) ⇧@ k" and
"q' = (s ⋅ r) ⇧@ l" and
"w = (r ⋅ s) ⇧@ m ⋅ r" and
"primitive (r ⋅ s)"
using len[unfolded conjug_len[OF ‹p ∼ p'›] conjug_len[OF ‹q ∼ q'›]]
by blast
moreover have "ρ p' = r⋅s"
using ‹p' = (r ⋅ s) ⇧@ k› ‹primitive (r ⋅ s)› ‹p' ≠ ε› primroot_unique by blast
hence "ρ p ∼ r⋅s"
using conjug_primroot[OF ‹p ∼ p'›]
by simp
moreover have "ρ q' = s⋅r"
using ‹q' = (s ⋅ r) ⇧@ l› ‹primitive (r ⋅ s)›[unfolded conjug_prim_iff'[of r]] ‹q' ≠ ε› primroot_unique by blast
hence "ρ q ∼ s⋅r"
using conjug_primroot[OF ‹q ∼ q'›] by simp
hence "ρ q ∼ r⋅s"
using conjug_trans[OF _ conjugI']
by meson
ultimately show ?thesis
using that by blast
qed
corollary fac_two_conjug_primroot'_gcd:
assumes facs: "u ≤f r⇧@k" "u ≤f s⇧@l" and nemps: "r ≠ ε" "s ≠ ε" and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "ρ r ∼ ρ s"
using fac_two_conjug_primroot_gcd[OF assms] conjug_trans[OF _ conjug_sym[of "ρ s"]].
lemma fac_two_conjug_primroot''_gcd:
assumes facs: "u ≤f r⇧@k" "u ≤f s⇧@l" and "u ≠ ε" and len: "❙|r❙| + ❙|s❙| - gcd (❙|r❙|) (❙|s❙|) ≤ ❙|u❙|"
shows "ρ r ∼ ρ s"
proof -
have nemps: "r ≠ ε" "s ≠ ε" using facs ‹u ≠ ε› by auto
show "conjugate (ρ r) (ρ s)" using fac_two_conjug_primroot'_gcd[OF facs nemps len].
qed
lemma fac_two_prim_conjug_gcd:
assumes "w ≤f u⇧@n" "w ≤f v⇧@m" "primitive u" "primitive v" "❙|u❙| + ❙|v❙| - gcd (❙|u❙|) (❙|v❙|) ≤ ❙|w❙|"
shows "u ∼ v"
using fac_two_conjug_primroot'_gcd[OF assms(1-2) _ _ assms(5)] prim_nemp[OF ‹primitive u›] prim_nemp[OF ‹primitive v›]
unfolding prim_self_root[OF ‹primitive u›] prim_self_root[OF ‹primitive v›].
lemma two_pers_1:
assumes pu: "w ≤p u ⋅ w" and pv: "w ≤p v ⋅ w" and len: "❙|u❙| + ❙|v❙| - 1 ≤ ❙|w❙|"
shows "u ⋅ v = v ⋅ u"
proof
assume "u ≠ ε" "v ≠ ε"
hence "1 ≤ gcd ❙|u❙| ❙|v❙|"
using nemp_len by (simp add: Suc_leI)
thus ?thesis
using per_lemma_comm[OF pu pv] len by linarith
qed
end