From 565d72b81dfdacf99bdef28d76b74bb99bd23c82 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 2 Dec 2024 10:47:31 +0000
Subject: [PATCH] feat: Add informal level_fintype

---
 HepLean/FeynmanDiagrams/Wick/Contract.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/HepLean/FeynmanDiagrams/Wick/Contract.lean b/HepLean/FeynmanDiagrams/Wick/Contract.lean
index 5225175..f384106 100644
--- a/HepLean/FeynmanDiagrams/Wick/Contract.lean
+++ b/HepLean/FeynmanDiagrams/Wick/Contract.lean
@@ -635,6 +635,10 @@ def unbound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
     · exact List.Sorted.get_strictMono w.unboundList_sorted
     · exact fun ⦃a b⦄ a => a
 
+informal_lemma level_fintype where
+  math :≈ "Level is a finite type, as there are only finitely many ways to contract a Wick string."
+  deps :≈ [``Level]
+
 informal_definition HasEqualTimeContractions where
   math :≈ "The condition for a Wick contraction to have two fields contracted
     which are of equal time, i.e. come from the same vertex."