proposition: Lemma Birkhoff_valid m (r : seq G) : Birkhoff_check n m -> scycle rlink r -> size r = n.+1 -> nontrivial_ring m r = false.
proof: Proof. case=> nm cps ctu0 gtu0 basis chkb bk1ok bk2ok; move: r. have chkbP (r : seq G) (Ur : scycle rlink r) (bGd := snipd_ring planarG Ur) : size r = n.+1 -> nontrivial_ring m r -> forall ctu, chkb ctu -> exists2 et, ring_trace bGd (ctrace et) & ~~ ctree_mem ctu (etrace et). - move=> sz_r nt_r ctu; move: bk1ok {bk2ok}; rewrite {}/chkb {}/basis. elim: cps => [|cp cps IHcp] //= /andP[/and3P[cpQ ltn_cp szr_cp] bk1ok]. case/orP=> [{cps bk1ok IHcp}ctu'cp|]; last exact: IHcp. pose Gr := cpmap cp; pose bGr : seq Gr := rotr 1 (rev (cpring Gr)). have ntGr : proper_cpring Gr := cpmap_proper cpQ. have cycNbGr: ufcycle node bGr. by rewrite rot_ucycle /ucycle cycle_rev_cpring rev_uniq cpring_uniq. set Gd := snip_disk planarG Ur in bGd *. have cycEbGd: sfcycle edge bGd by apply: scycle_snipd_ring. have sz_bGdr: size bGd = size bGr. rewrite size_rot size_rev size_ring_cpmap (eqP szr_cp) -sz_r. by rewrite -(map_snipd_ring planarG Ur) size_map. pose G2 := sew_map cycEbGd cycNbGr sz_bGdr. have ppG2 := sew_map_patch cycEbGd cycNbGr sz_bGdr. have ppGd := snip_patch planarG Ur; rewrite -/bGd in ppGd. move: plainG; rewrite (plain_patch ppGd) => /andP[plainGd plainGrr]. move: cubicG; rewrite (cubic_patch ppGd) => /andP[cubicGd cubicGrr]. have planarG2: planar G2. by rewrite /planar (genus_patch ppG2) addn_eq0 cpmap_planar // planar_snipd. have plainG2: plain G2. by rewrite (plain_patch ppG2); apply/andP; split; last apply: cpmap_plain. have cubicG2: cubic G2. rewrite (cubic_patch ppG2); apply/andP; split => //. by apply/subsetP=> x; rewrite !inE mem_rot => /(subsetP (cpmap_cubic cpQ)). have bridge'G2: bridgeless G2. have [bridge'Gd _] := patch_bridgeless ppGd bridge'G. apply: bridgeless_patch ppG2 bridge'Gd (cpmap_bridgeless cpQ) _. apply/idPn=> chord_bGd. have [r1 Ur1 [nt_r1 lt_r1r]] := ring_disk_chord geoG nt_r chord_bGd. by rewrite (leq_n_trivial Ur1) // -ltnS -sz_r in nt_r1. have colG2: four_colorable G2. apply: minG; try by do ![split | apply: cubic_precubic]. rewrite ltnNge -(leq_add2l (size bGd)). move: (card_patch ppG2) (card_patch ppGd); rewrite !size_map -/G2 => <- <-. rewrite leq_add2l -ltnNge -ltnS card_cpmap (leq_trans ltn_cp) //. pose bGrr := snipr_ring planarG Ur. have sz_bGrr: size bGrr = n.+1. by rewrite -sz_r -(size_rev r) -(map_snipr_ring planarG Ur) size_map. case DbGrr: bGrr (sz_bGrr) => // [z0 bGrr1] _. have geoGrr: ucycle_plain_quasicubic_connected bGrr. split; first by split; [ split | apply: ucycle_snipr_ring]. exact: (patch_connected_r ppGd ccG). move: (planar_snipr planarG Ur); rewrite (quasicubic_Euler geoGrr) /nilp. rewrite sz_bGrr add1n (patch_fcard_face_r ppGd) /outer -/Gr. move: #|_| => nGrr; pose arF := [predU diskFC r & fband r]. have nbFarF: fcard face arF = n.+1 + fcard face (diskFC r). rewrite -sz_r -(scycle_fcard_fband Ur) -cardUI addnC eq_card0 => [|x]. apply: eq_card => x; rewrite !inE. by case: (x \in fband r); rewrite andbF ?orbT ?orbF. by rewrite !inE; case: (x \in fband r); rewrite !andbF. rewrite mulnSr addnA (addnA _ 6 6) eqn_add2r. rewrite -(@eq_n_comp_r _ _ arF) => [|x]. rewrite nbFarF addSn mulnSr eqn_add2r mulnDr (mulnDl 4 2) addnC. rewrite mul2n addnA doubleS -2!addSnnS eqn_add2r -ltnS => /eqP <-. by rewrite ltn_add2r ltn_pmul2l //; case/andP: nt_r. have imGr := codom_snipr planarG Ur. apply/idP/exists_inP=> [|[y]]. rewrite !inE orbC unfold_in; case: hasP => [[y ry xFy] | _ dN'x]. by exists y; rewrite // !inE imGr !inE ry. by exists x; rewrite !inE // imGr !inE (negPf dN'x) andbF. rewrite !(inE, imGr) orbC => xFy; apply: contraR. case/norP=> rF'x; rewrite rF'x negbK => dNx. have /andP[/= rF'y ->]: y \in diskF r. by rewrite -(closed_connect (diskF_face r) xFy) !inE rF'x. by rewrite (contra (subsetP (ring_fband r) _)). have [/(_ colG2)[et Det_d Det_r] _] := colorable_patch ppG2. case/lastP: et => [|et e] in Det_d Det_r. have [k _ /esym/nilP/negP[]] := Det_r. by rewrite /nilp size_trace size_map size_rot size_rev head_cpring. have De: sumt et = e. apply/eqP; have [k _ /(congr1 (sumt \o rotr 1))/eqP] := Det_d. by rewrite /= rotr1_rcons -[rotr 1 _]trace_rot sumt_trace /= addcC addc_eq0. exists et => [|{Det_d}]; first by rewrite /ctrace De. rewrite (ctree_mem_disjoint ctu'cp) //; apply/ctree_mem_cpcolor. split; first exact: even_etrace; rewrite /etrace sumt_permt De. have [k col_k Det] := Det_r; exists (etrace_perm et \o k). by apply: coloring_inj col_k; apply: permc_inj. rewrite -/Gr map_comp trace_permt -(revK (cpring Gr)) map_rev trace_rev. rewrite -rev_rotr -[rotr 1 _]trace_rot size_trace -[rot _ _]map_rotr -Det. by rewrite !(rev_rcons, rot1_cons) revK. case Dn: {1}n => [|n'] => [[|x[]] // /andP[/andP[]] | r Ur sz_r]. by rewrite /rlink cfaceC bridgeless_cface. apply: contraTF bk2ok => nt_r; have Ur2 := scycle_rev_ring geoG Ur. pose P Ur1 et := ~ ring_trace (snipd_ring planarG Ur1) et. pose kv r1 Ur1 := Kempe_valid n' (P r1 Ur1) ctu0 CtreeEmpty GtreeEmpty gtu0. have: kv _ Ur2 by rewrite /kv /ctu0 /gtu0 Dn; apply: Kempe_valid_init. have: kv r Ur by rewrite /kv /ctu0 /gtu0 Dn; apply: Kempe_valid_init. move: sz_r nt_r Ur Ur2; rewrite {}/kv -Dn. elim: nm r ctu0 gtu0 {2 4}ctu0 {2 4}gtu0 => // nm IHnm r1 ctu1 gtu1 ctu2 gtu2. set r2 := rev_ring r1 => sz_r1 nt_r1 Ur1 Ur2 r1valid r2valid /=. have sz_r2: size r2 = n.+1 by rewrite size_rev size_map. have nt_r2: nontrivial_ring m r2 by apply: (nontrivial_rev_ring geoG). have r1closed := @ring_disk_closed _ geoG planarG _ Ur1 _ nt_r1 cubicG. have r2closed := @ring_disk_closed _ geoG planarG _ Ur2 _ nt_r2 cubicG. case Det: (ctree_pick_rev ctu1 ctu2) => //= [e et]. have Dct0 (ct0 := untrace Color0 (e :: et)): trace ct0 = e :: et. by rewrite trace_untrace // -Det sumt_ctree_pick_rev. have sz_et: size et = n. have [[ctu2ok _] _] := r2valid; have:= size_ctree_pick_rev ctu1 ctu2ok. by rewrite Det !inE /= -Dn => /eqP[]. apply/andP=> [[r1check r2check]]; case: noncolG. apply: (@colorable_from_ring _ geoG planarG _ Ur1 _ nt_r1 (e :: et)). have [// | tr1'et] := decide_ring_trace (snipd_ring planarG Ur1) (e :: et). move: r1check {r2check}; rewrite /do_Birkhoff_check2 {1}Dn. set ctr := ctree_of_ttail _; case: ifPn => // et'0. have []:= @Kempe_tree_closure_correct n' (P _ Ur1) n ctu1 ctr gtu1. apply: Kempe_valid_restrict r1valid => et1 /ctree_of_ttail_mem Det1. rewrite Det1 ?memc0_permt // ctrace_permt. split; last by rewrite size_map size_belast sz_et. move: (etrace_perm _) => g /r1closed[tr1_et _]; case: tr1'et. suffices ->: e :: et = ctrace (belast e et). by rewrite -[ctrace _](mapK (inv_permc g)); apply: tr1_et. by rewrite -Dct0 /= (scanlK addKc). case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et}r1valid _. case/orP=> [/(chkbP r1)[]// et1 tr_et1 ct3'et1 | {r1closed}/idPn[]]. suffices sz_et1: size et1 = n'.+1. by have[] := Kempe_validP r1valid sz_et1 ct3'et1 r1closed tr_et1. have [k _ /(congr1 size)] := tr_et1; rewrite size_rcons size_trace size_map. by rewrite -(size_map snipd) (map_snipd_ring planarG Ur1) sz_r1 Dn => [][]. by rewrite -(rev_rev_ring geoG r1) in Ur1 r1valid; apply: (IHnm r2). have [| tr2'et] := decide_ring_trace (snipd_ring planarG Ur2) (rev (e :: et)). by congr (ring_trace (snipd_ring _ _) _); apply: bool_irrelevance. move: r2check {r1check}; rewrite /do_Birkhoff_check2 {1}Dn. set ctr := ctree_of_ttail _; case: ifPn => // et'0. have []:= @Kempe_tree_closure_correct n' (P r2 Ur2) n ctu2 ctr gtu2. apply: Kempe_valid_restrict r2valid => et2 /ctree_of_ttail_mem-Det2. rewrite {}Det2 ?memc0_permt {et'0}// ctrace_permt. split; last by rewrite size_map size_rev -Dn. move: (etrace_perm _) => g /r2closed[tr2_et _]; case: tr2'et. suffices ->: rev (e :: et) = ctrace (rev et). by rewrite -[ctrace _](mapK (inv_permc g)); apply: tr2_et. suffices /eqP: sumt (rev (rcons et e)) = Color0. by rewrite rev_cons rev_rcons /= addc_eq0 => /eqP->. rewrite -rot1_cons -Dct0 -[rev _](rotrK 1) -rev_rot -!trace_rot -trace_rev. exact: sumt_trace. case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr2'et}r2valid _. case/orP=> [/(chkbP r2)[]// et3 tr_et3 ct'et3 | /idPn[]]; last exact: (IHnm r1). suffices sz_et3: size et3 = n'.+1. by have [] := Kempe_validP r2valid sz_et3 ct'et3 r2closed tr_et3. have [k _ /(congr1 size)] := tr_et3; rewrite size_rcons size_trace size_map. by rewrite -(size_map snipd) map_snipd_ring sz_r2 Dn => [][]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)