Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.Koszul.KoszulSignInsert public import Physlib.Mathematics.List.InsertionSort import all Physlib.Mathematics.List

Koszul sign

@[expose] public section

Gives a factor of - 1 for every fermion-fermion (q is 1) crossing that occurs when sorting a list of based on r.

def koszulSign (q : 𝓕 FieldStatistic) (le : 𝓕 𝓕 Prop) [DecidableRel le] : List 𝓕 | [] => 1 | a :: l => koszulSignInsert q le a l * koszulSign q le l
@[simp] lemma koszulSign_singleton (q : 𝓕 FieldStatistic) (le : 𝓕 𝓕 Prop) [DecidableRel le] (φ : 𝓕) : koszulSign q le [φ] = 1 := 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕koszulSign q le [φ] = 1 All goals completed! 🐙All goals completed! 🐙@[simp] lemma koszulSign_freeMonoid_of (φ : 𝓕) : koszulSign q le (FreeMonoid.of φ) = 1 := 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕koszulSign q le (FreeMonoid.of φ) = 1 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕koszulSign q le [φ] = 1 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕koszulSignInsert q le φ [] = 1 All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:h:n + 1 (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) n, hnsLnro:Fin (rs.length + 1) := (orderedInsertPos le rs φ1), hns:rs.get ni = φhc1:ni.castSucc < nro ¬le φ1 φhc2:¬ni.castSucc < nro le φ1 φhn:¬ni.castSucc < nro(if le φ1 φ then 1 else if q φ1 = fermionic q φ = fermionic then -1 else 1) = 1 All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:h:n + 1 (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) n, hnsLnro:Fin (rs.length + 1) := (orderedInsertPos le rs φ1), hns:rs.get ni = φhc1:ni.castSucc < nro ¬le φ1 φhc2:¬ni.castSucc < nro le φ1 φhn:¬ni.castSucc < nronro ni All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs:List 𝓕n:h:n + 1 (φ1 :: φs).lengthrs:List 𝓕 := List.insertionSort le (φs.insertIdx n φ)hnsL:n < (φs.insertIdx n φ).lengthni:Fin rs.length := (insertionSortEquiv le (φs.insertIdx n φ)) n, hnsLnro:Fin (rs.length + 1) := (orderedInsertPos le rs φ1), hns:rs.get ni = φhc1:ni.castSucc < nro ¬le φ1 φhc2:¬ni.castSucc < nro le φ1 φhn:¬ni.castSucc < nronro rs.length All goals completed! 🐙lemma insertIdx_eraseIdx {I : Type} : (n : ) (r : List I) (hn : n < r.length) List.insertIdx (r.eraseIdx n) n (r.get n, hn) = r I:Typen:hn:n < [].length([].eraseIdx n).insertIdx n ([].get n, hn) = [] I:Typen:hn:n < [].length([].eraseIdx n).insertIdx n ([].get n, hn) = [] All goals completed! 🐙 I:Typer0:Ir:List Ihn:0 < (r0 :: r).length((r0 :: r).eraseIdx 0).insertIdx 0 ((r0 :: r).get 0, hn) = r0 :: r I:Typer0:Ir:List Ihn:0 < (r0 :: r).length((r0 :: r).eraseIdx 0).insertIdx 0 ((r0 :: r).get 0, hn) = r0 :: r All goals completed! 🐙 I:Typen:r0:Ir:List Ihn:n + 1 < (r0 :: r).length((r0 :: r).eraseIdx (n + 1)).insertIdx (n + 1) ((r0 :: r).get n + 1, hn) = r0 :: r I:Typen:r0:Ir:List Ihn:n + 1 < (r0 :: r).length((r0 :: r).eraseIdx (n + 1)).insertIdx (n + 1) ((r0 :: r).get n + 1, hn) = r0 :: r I:Typen:r0:Ir:List Ihn:n + 1 < (r0 :: r).length(r.eraseIdx n).insertIdx n r[n] = r All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φskoszulSign q le (φs.eraseIdx n) * ((exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs))) * ((exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs)))) = (exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * koszulSign q le (φs.eraseIdx n) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((Fin.castOrderIso ).toEquiv ((insertionSortEquiv le φs) ((Fin.castOrderIso ).toEquiv n, )))) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs)) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φskoszulSign q le (φs.eraseIdx n) * ((exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs))) * ((exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs)))) = (exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * koszulSign q le (φs.eraseIdx n) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs)) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) All goals completed! 🐙 conv_rhs => 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑((insertionSortEquiv le φs) n)) (List.insertionSort le φs))) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| 1 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φskoszulSign q le (φs.eraseIdx n) = koszulSign q le (φs.eraseIdx n) * ((exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs))) conv_rhs => 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| (exchangeSign (q φs[n])) (ofList q (List.take (↑n) (φs.eraseIdx n))) * (exchangeSign (q φs[n])) (ofList q (List.take (↑n) φs)) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕n:Fin φs.lengthφs':List 𝓕 := φs.eraseIdx nhφs:φs'.insertIdx (↑n) (φs.get n) = φs| 1 All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) conv_lhs => 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs)))) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| ofList q (List.take (↑((insertionSortEquiv le (φ :: φs)) (insertionSortMinPos le φ φs))) (List.insertionSort le (φ :: φs))) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| q 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕| q erw [𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑0, ) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs)))𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕koszulSign q le (φ :: φs) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) * (exchangeSign (q ((φ :: φs).get (insertionSortMinPos le φ φs)))) (ofList q (List.take (↑0, ) (List.insertionSort le (φ :: φs)))) = koszulSign q le (φ :: φs) * (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕(exchangeSign (q (φ :: φs)[(insertionSortMinPos le φ φs)])) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) = (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) koszulSign q le (φ :: φs) = 0 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕(exchangeSign (q (φ :: φs)[(insertionSortMinPos le φ φs)])) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) = (exchangeSign (q (insertionSortMin le φ φs))) (ofList q (List.take (↑(insertionSortMinPos le φ φs)) (φ :: φs))) All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφs':List 𝓕koszulSignInsert q le ψ φs' * koszulSignInsert q le φ (ψ :: φs') = koszulSignInsert q le ψ (φ :: φs') * koszulSignInsert q le φ φs' All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕koszulSignInsert q le φ'' (φs ++ φ :: ψ :: φs') * koszulSign q le (φs ++ ψ :: φ :: φs') = koszulSignInsert q le φ'' (φs ++ ψ :: φ :: φs') * koszulSign q le (φs ++ ψ :: φ :: φs') 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕koszulSignInsert q le φ'' (φs ++ φ :: ψ :: φs') = koszulSignInsert q le φ'' (φs ++ ψ :: φ :: φs') 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leψ:𝓕φ:𝓕h1:le φ ψh2:le ψ φφ'':𝓕φs:List 𝓕φs':List 𝓕(φs ++ φ :: ψ :: φs').Perm (φs ++ ψ :: φ :: φs') All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leψ:𝓕φ:𝓕inst✝:IsTrans 𝓕 leh1:le φ ψh2:le ψ φhq:q ψ = q φφs:List 𝓕koszulSignInsert q le ψ φs * koszulSignInsert q le ψ φs = 1 All goals completed! 🐙All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕φs:List 𝓕h:(∀ a' φs, le φ a') List.Pairwise le φskoszulSignInsert q le φ φs * 1 = 1 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝:DecidableRel leφ:𝓕φs:List 𝓕h:(∀ a' φs, le φ a') List.Pairwise le φskoszulSignInsert q le φ φs = 1 All goals completed! 🐙@[simp] lemma koszulSign_of_insertionSort [Std.Total le] [IsTrans 𝓕 le] (φs : List 𝓕) : koszulSign q le (List.insertionSort le φs) = 1 := 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕koszulSign q le (List.insertionSort le φs) = 1 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕List.Pairwise le (List.insertionSort le φs) All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕φ:𝓕φs':List 𝓕h1:φs ++ φ :: φs' = (φs ++ φs').insertIdx φs.length φh2:List.insertionSort le φs ++ φ :: φs' = (List.insertionSort le φs ++ φs').insertIdx (List.insertionSort le φs).length φList.insertionSort le (φs ++ φ :: φs') = List.insertionSort le (List.insertionSort le φs ++ φ :: φs') 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφs:List 𝓕φ:𝓕φs':List 𝓕h1:φs ++ φ :: φs' = (φs ++ φs').insertIdx φs.length φh2:List.insertionSort le φs ++ φ :: φs' = (List.insertionSort le φs ++ φs').insertIdx (List.insertionSort le φs).length φList.insertionSort le (List.insertionSort le φs ++ φ :: φs') = List.insertionSort le (φs ++ φ :: φs') All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕koszulSignInsert q le φ'' (φs'' ++ φs ++ φs') * koszulSign q le (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le φs = koszulSignInsert q le φ'' (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le (φs'' ++ List.insertionSort le φs ++ φs') * koszulSign q le φs 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕koszulSignInsert q le φ'' (φs'' ++ φs ++ φs') = koszulSignInsert q le φ'' (φs'' ++ List.insertionSort le φs ++ φs') 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕(φs'' ++ φs ++ φs').Perm (φs'' ++ List.insertionSort le φs ++ φs') 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕(φs'' ++ φs).Perm (φs'' ++ List.insertionSort le φs) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leφ'':𝓕φs'':List 𝓕φs:List 𝓕φs':List 𝓕φs.Perm (List.insertionSort le φs) All goals completed! 🐙

koszulSign with permutations

lemma koszulSign_perm_eq_append [IsTrans 𝓕 le] (φ : 𝓕) (φs φs' φs2 : List 𝓕) (hp : φs.Perm φs') : (h : φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) := 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'(∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)(∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)motive φs φs' hp 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)motive [] [] 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) (x : 𝓕) {l₁ l₂ : List 𝓕} (a : l₁.Perm l₂), motive l₁ l₂ a motive (x :: l₁) (x :: l₂) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) (x y : 𝓕) (l : List 𝓕), motive (y :: x :: l) (x :: y :: l) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) {l₁ l₂ l₃ : List 𝓕} (a : l₁.Perm l₂) (a_1 : l₂.Perm l₃), motive l₁ l₂ a motive l₂ l₃ a_1 motive l₁ l₃ 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)motive [] [] All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) (x : 𝓕) {l₁ l₂ : List 𝓕} (a : l₁.Perm l₂), motive l₁ l₂ a motive (x :: l₁) (x :: l₂) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:motive l1 l2 hhxφ: φ' x :: l1, le φ φ' le φ' φkoszulSign q le (x :: l1 ++ φs2) = koszulSign q le (x :: l2 ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x le x φ) a l1, le φ a le a φkoszulSign q le (x :: (l1 ++ φs2)) = koszulSign q le (x :: (l2 ++ φs2)) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x le x φ) a l1, le φ a le a φkoszulSignInsert q le x (l1 ++ φs2) = koszulSignInsert q le x (l2 ++ φs2) koszulSign q le (l2 ++ φs2) = 0 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x le x φ) a l1, le φ a le a φkoszulSignInsert q le x (l1 ++ φs2) = koszulSignInsert q le x (l2 ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕l1:List 𝓕l2:List 𝓕h:l1.Perm l2ih:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)hxφ:(le φ x le x φ) a l1, le φ a le a φ(l1 ++ φs2).Perm (l2 ++ φs2) All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) (x y : 𝓕) (l : List 𝓕), motive (y :: x :: l) (x :: y :: l) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h: φ' y :: x :: l, le φ φ' le φ' φkoszulSign q le (y :: x :: l ++ φs2) = koszulSign q le (x :: y :: l ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y le y φ) (le φ x le x φ) a l, le φ a le a φkoszulSign q le (y :: x :: (l ++ φs2)) = koszulSign q le (x :: y :: (l ++ φs2)) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y le y φ) (le φ x le x φ) a l, le φ a le a φle y x𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y le y φ) (le φ x le x φ) a l, le φ a le a φle x y 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y le y φ) (le φ x le x φ) a l, le φ a le a φle y x All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)x:𝓕y:𝓕l:List 𝓕h:(le φ y le y φ) (le φ x le x φ) a l, le φ a le a φle x y All goals completed! 🐙 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2) {l₁ l₂ l₃ : List 𝓕} (a : l₁.Perm l₂) (a_1 : l₂.Perm l₃), motive l₁ l₂ a motive l₂ l₃ a_1 motive l₁ l₃ 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:motive l1 l2 h1ih2:motive l2 l3 h2h: φ' l1, le φ φ' le φ' φkoszulSign q le (l1 ++ φs2) = koszulSign q le (l3 ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' l2, le φ φ' le φ' φ) koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h: φ' l1, le φ φ' le φ' φkoszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' l2, le φ φ' le φ' φ) koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h: φ' l1, le φ φ' le φ' φ φ' l2, le φ φ' le φ' φ 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' l2, le φ φ' le φ' φ) koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h: φ' l1, le φ φ' le φ' φφ':𝓕:φ' l2le φ φ' le φ' φ 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕hp:φs.Perm φs'motive:(φs φs' : List 𝓕) φs.Perm φs' Prop := fun φs φs' hp => (∀ φ' φs, le φ φ' le φ' φ) koszulSign q le (φs ++ φs2) = koszulSign q le (φs' ++ φs2)l1:List 𝓕l2:List 𝓕l3:List 𝓕h1:l1.Perm l2h2:l2.Perm l3ih1:koszulSign q le (l1 ++ φs2) = koszulSign q le (l2 ++ φs2)ih2:(∀ φ' l2, le φ φ' le φ' φ) koszulSign q le (l2 ++ φs2) = koszulSign q le (l3 ++ φs2)h: φ' l1, le φ φ' le φ' φφ':𝓕:φ' l2φ' l1 All goals completed! 🐙𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h: φ' φs, le φ φ' le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)koszulSignInsert q le φ1 (φs1 ++ φs ++ φs2) * koszulSign q le (φs1 ++ φs' ++ φs2) = koszulSignInsert q le φ1 (φs1 ++ φs' ++ φs2) * koszulSign q le (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h: φ' φs, le φ φ' le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)koszulSignInsert q le φ1 (φs1 ++ φs ++ φs2) = koszulSignInsert q le φ1 (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h: φ' φs, le φ φ' le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)(φs1 ++ φs ++ φs2).Perm (φs1 ++ φs' ++ φs2) 𝓕:Typeq:𝓕 FieldStatisticle:𝓕 𝓕 Propinst✝¹:DecidableRel leinst✝:IsTrans 𝓕 leφ:𝓕φ1:𝓕φs1:List 𝓕φs:List 𝓕φs':List 𝓕φs2:List 𝓕h: φ' φs, le φ φ' le φ' φhp:φs.Perm φs'ih:koszulSign q le (φs1 ++ φs ++ φs2) = koszulSign q le (φs1 ++ φs' ++ φs2)(φs1 ++ φs).Perm (φs1 ++ φs') All goals completed! 🐙