1. Physlib
  2. QFT
  3. PerturbationTheory
  4. Koszul
  5. KoszulSignInsert
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.FieldStatistics.ExchangeSign public import Physlib.Mathematics.List import all Mathlib.Data.List.Sort

Koszul sign insert

@[expose] public section

Gives a factor of -1 when inserting a into a list List I in the ordered position for each fermion-fermion cross.

def koszulSignInsert {𝓕 : Type} (q : 𝓕 β†’ FieldStatistic) (le : 𝓕 β†’ 𝓕 β†’ Prop) [DecidableRel le] (Ο† : 𝓕) : List 𝓕 β†’ β„‚ | [] => 1 | Ο†' :: Ο†s => if le Ο† Ο†' then koszulSignInsert q le Ο† Ο†s else if q Ο† = fermionic ∧ q Ο†' = fermionic then - koszulSignInsert q le Ο† Ο†s else koszulSignInsert q le Ο† Ο†s

When inserting a boson the koszulSignInsert is always 1.

𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕ha:q Ο† = bosonicΟ†':𝓕φs:List π“•βŠ’ (if le Ο† Ο†' then 1 else if bosonic = fermionic ∧ q Ο†' = fermionic then -1 else 1) = 1 All goals completed! πŸ™
All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕hi:βˆ€ (Ο†' : 𝓕), le Ο† Ο†'Ο†':𝓕φs:List 𝓕ih:koszulSignInsert q le Ο† Ο†s = 1⊒ (if le Ο† Ο†' then 1 else if q Ο† = fermionic ∧ q Ο†' = fermionic then -1 else 1) = 1 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕hi:βˆ€ (Ο†' : 𝓕), le Ο† Ο†'Ο†':𝓕φs:List 𝓕ih:koszulSignInsert q le Ο† Ο†s = 1⊒ Β¬le Ο† Ο†' β†’ q Ο† = fermionic β†’ q Ο†' = fermionic β†’ -1 = 1 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕hi:βˆ€ (Ο†' : 𝓕), le Ο† Ο†'Ο†':𝓕φs:List 𝓕ih:koszulSignInsert q le Ο† Ο†s = 1h:Β¬le Ο† Ο†'⊒ q Ο† = fermionic β†’ q Ο†' = fermionic β†’ -1 = 1 All goals completed! πŸ™All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕h:Β¬le Ο† Ο†1⊒ (if q Ο† = fermionic ∧ q Ο†1 = fermionic then -koszulSignInsert q le Ο† (List.filter (fun i => decide Β¬le Ο† i) Ο†s) else koszulSignInsert q le Ο† (List.filter (fun i => decide Β¬le Ο† i) Ο†s)) = if q Ο† = fermionic ∧ q Ο†1 = fermionic then -koszulSignInsert q le Ο† (List.filter (fun i => !decide (le Ο† i)) Ο†s) else koszulSignInsert q le Ο† (List.filter (fun i => !decide (le Ο† i)) Ο†s) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕h:Β¬le Ο† Ο†1⊒ (fun i => decide Β¬le Ο† i) = fun i => !decide (le Ο† i)𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕h:Β¬le Ο† Ο†1⊒ (fun i => decide Β¬le Ο† i) = fun i => !decide (le Ο† i) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕h:Β¬le Ο† Ο†1⊒ (fun i => decide Β¬le Ο† i) = fun i => !decide (le Ο† i) All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕h:Β¬le Ο† Ο†1⊒ (fun i => decide Β¬le Ο† i) = fun i => !decide (le Ο† i) All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝¹:DecidableRel leinst✝:Std.Total leΟ†:𝓕φs:List 𝓕h1:le Ο† Ο†βŠ’ koszulSignInsert q le Ο† Ο†s = if le Ο† Ο† then koszulSignInsert q le Ο† Ο†s else if q Ο† = fermionic then -koszulSignInsert q le Ο† Ο†s else koszulSignInsert q le Ο† Ο†s All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕ih:koszulSignInsert q le Ο† (List.filter (fun i => decide Β¬le Ο† i) Ο†s) = if ofList q [Ο†] = fermionic ∧ ofList q (List.filter (fun i => decide Β¬le Ο† i) Ο†s) = fermionic then -1 else 1hr1:¬¬le Ο† Ο†1⊒ koszulSignInsert q le Ο† (List.filter (fun i => !decide (le Ο† i)) Ο†s) = if ofList q [Ο†] = fermionic ∧ ofList q (List.filter (fun i => !decide (le Ο† i)) Ο†s) = fermionic then -1 else 1 All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†:𝓕φ1:𝓕φs:List 𝓕ih:koszulSignInsert q le Ο† Ο†s = if ofList q [Ο†] = fermionic ∧ ofList q (List.filter (fun i => decide Β¬le Ο† i) Ο†s) = fermionic then -1 else 1hr1:¬¬le Ο† Ο†1⊒ Β¬(decide Β¬le Ο† Ο†1) = true All goals completed! πŸ™All goals completed! πŸ™lemma koszulSignInsert_eq_sort (Ο†s : List 𝓕) (Ο† : 𝓕) : koszulSignInsert q le Ο† Ο†s = koszulSignInsert q le Ο† (List.insertionSort le Ο†s) := 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†s:List 𝓕φ:π“•βŠ’ koszulSignInsert q le Ο† Ο†s = koszulSignInsert q le Ο† (List.insertionSort le Ο†s) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†s:List 𝓕φ:π“•βŠ’ Ο†s.Perm (List.insertionSort le Ο†s) All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leΟ†:𝓕φs:List 𝓕hx:(exchangeSign (q Ο†)) (ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s))) = if ofList q [Ο†] = fermionic ∧ ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s)) = fermionic then -1 else 1h1:List.filter (fun a => decide Β¬le Ο† a) (List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)) = List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)a:𝓕ha:a ∈ List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)⊒ a ∈ [] ++ List.drop (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†) + 1 - (List.takeWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)).length) (Ο† :: List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s))𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leΟ†:𝓕φs:List 𝓕hx:(exchangeSign (q Ο†)) (ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s))) = if ofList q [Ο†] = fermionic ∧ ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s)) = fermionic then -1 else 1h1:List.filter (fun a => decide Β¬le Ο† a) (List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)) = List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)a:𝓕ha:a ∈ List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)⊒ (List.takeWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)).length ≀ ↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†) + 1 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leΟ†:𝓕φs:List 𝓕hx:(exchangeSign (q Ο†)) (ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s))) = if ofList q [Ο†] = fermionic ∧ ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s)) = fermionic then -1 else 1h1:List.filter (fun a => decide Β¬le Ο† a) (List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)) = List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)a:𝓕ha:a ∈ List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)⊒ a ∈ [] ++ List.drop (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†) + 1 - (List.takeWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)).length) (Ο† :: List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)) All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝²:DecidableRel leinst✝¹:Std.Total leinst✝:IsTrans 𝓕 leΟ†:𝓕φs:List 𝓕hx:(exchangeSign (q Ο†)) (ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s))) = if ofList q [Ο†] = fermionic ∧ ofList q (List.take (↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†)) (List.insertionSort le Ο†s)) = fermionic then -1 else 1h1:List.filter (fun a => decide Β¬le Ο† a) (List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)) = List.takeWhile (fun b => decide Β¬le Ο† b) (List.insertionSort le Ο†s)a:𝓕ha:a ∈ List.dropWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)⊒ (List.takeWhile (fun b => !decide (le Ο† b)) (List.insertionSort le Ο†s)).length ≀ ↑(orderedInsertPos le (List.insertionSort le Ο†s) Ο†) + 1 All goals completed! πŸ™lemma koszulSignInsert_insertIdx (i j : 𝓕) (r : List 𝓕) (n : β„•) (hn : n ≀ r.length) : koszulSignInsert q le j (List.insertIdx r n i) = koszulSignInsert q le j (i :: r) := 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel lei:𝓕j:𝓕r:List 𝓕n:β„•hn:n ≀ r.length⊒ koszulSignInsert q le j (r.insertIdx n i) = koszulSignInsert q le j (i :: r) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel lei:𝓕j:𝓕r:List 𝓕n:β„•hn:n ≀ r.length⊒ (r.insertIdx n i).Perm (i :: r) All goals completed! πŸ™

The difference in koszulSignInsert on inserting r0 into r compared to into r1 :: r for any r.

def koszulSignCons (Ο†0 Ο†1 : 𝓕) : β„‚ := if le Ο†0 Ο†1 then 1 else if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1
lemma koszulSignCons_eq_exchangeSign (Ο†0 Ο†1 : 𝓕) : koszulSignCons q le Ο†0 Ο†1 = if le Ο†0 Ο†1 then 1 else 𝓒(q Ο†0, q Ο†1) := 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:π“•βŠ’ koszulSignCons q le Ο†0 Ο†1 = if le Ο†0 Ο†1 then 1 else (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:π“•βŠ’ (if le Ο†0 Ο†1 then 1 else if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = if le Ο†0 Ο†1 then 1 else (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:π“•βŠ’ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1)𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:Β¬q Ο†0 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionich1:q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1)𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionich1:Β¬q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionich1:q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionich1:Β¬q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:q Ο†0 = fermionich1✝:Β¬q Ο†1 = fermionich1:q Ο†1 = bosonic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0:Β¬q Ο†0 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonich1:q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1)𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonich1:Β¬q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonich1:q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonich1:Β¬q Ο†1 = fermionic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕h0✝:Β¬q Ο†0 = fermionich0:q Ο†0 = bosonich1✝:Β¬q Ο†1 = fermionich1:q Ο†1 = bosonic⊒ (if q Ο†0 = fermionic ∧ q Ο†1 = fermionic then -1 else 1) = (exchangeSign (q Ο†0)) (q Ο†1) All goals completed! πŸ™lemma koszulSignInsert_cons (r0 r1 : 𝓕) (r : List 𝓕) : koszulSignInsert q le r0 (r1 :: r) = (koszulSignCons q le r0 r1) * koszulSignInsert q le r0 r := 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel ler0:𝓕r1:𝓕r:List π“•βŠ’ koszulSignInsert q le r0 (r1 :: r) = koszulSignCons q le r0 r1 * koszulSignInsert q le r0 r All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ koszulSignInsert q le Ο†0 Ο†s = 1𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ le Ο†0 Ο†1 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ koszulSignInsert q le Ο†0 Ο†s = 1 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ βˆ€ b ∈ Ο†s, le Ο†0 b 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ βˆ€ b ∈ Ο†s, le Ο†0 b 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 bb:𝓕hb:b ∈ Ο†s⊒ le Ο†0 b All goals completed! πŸ™ 𝓕:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝:DecidableRel leΟ†0:𝓕φ1:𝓕φs:List 𝓕h:βˆ€ b ∈ Ο†1 :: Ο†s, le Ο†0 b⊒ le Ο†0 Ο†1 All goals completed! πŸ™All goals completed! πŸ™π“•:Typeq:𝓕 β†’ FieldStatisticle:𝓕 β†’ 𝓕 β†’ Propinst✝¹:DecidableRel leψ:𝓕φ:𝓕φ':𝓕inst✝:IsTrans 𝓕 leh1:le Ο† ψh2:le ψ Ο†hq:q ψ = q φφs:List 𝓕hΟ†'Ο†:Β¬le Ο†' Ο†hΟ†'ψ:Β¬le Ο†' ψ⊒ (if le Ο†' Ο† then if le Ο†' ψ then koszulSignInsert q le Ο†' Ο†s else if q Ο†' = fermionic ∧ q Ο† = fermionic then -koszulSignInsert q le Ο†' Ο†s else koszulSignInsert q le Ο†' Ο†s else if q Ο†' = fermionic ∧ q Ο† = fermionic then -if le Ο†' ψ then koszulSignInsert q le Ο†' Ο†s else -koszulSignInsert q le Ο†' Ο†s else koszulSignInsert q le Ο†' Ο†s) = koszulSignInsert q le Ο†' Ο†s All goals completed! πŸ™