From a62921089b539db114495eb010b8b29b7430a4a4 Mon Sep 17 00:00:00 2001
From: zeramorphic <zeramorphic@proton.me>
Date: Sat, 16 Mar 2024 16:10:29 +0000
Subject: [PATCH] Prove mk_tangle

Signed-off-by: zeramorphic <zeramorphic@proton.me>
---
 ConNF/Counting/Conclusions.lean | 30 +++++++++++++++++++++++++++++-
 ConNF/Counting/Hypotheses.lean  |  8 +++++++-
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean
index 04ddfebc33..ecc5fddc3d 100644
--- a/ConNF/Counting/Conclusions.lean
+++ b/ConNF/Counting/Conclusions.lean
@@ -37,6 +37,34 @@ theorem mk_codingFunction (β : Λ) [i : LeLevel β] : #(CodingFunction β) < #
     · refine Params.μ_isStrongLimit.2 _ ?_
       exact mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le this
         (ih γ (WithBot.coe_lt_coe.mp hγ))
-  · sorry
+  · simp only [WithBot.coe_lt_coe, not_exists, not_lt] at h
+    cases le_antisymm (h 0) (Params.Λ_zero_le β)
+    exact mk_codingFunction_zero
+
+noncomputable def Tangle.code {β : Λ} [LeLevel β] (t : Tangle β) : CodingFunction β × Support β :=
+  (CodingFunction.code _ _ (support_supports t), t.support)
+
+theorem Tangle.code_injective {β : Λ} [LeLevel β] : Function.Injective (Tangle.code (β := β)) := by
+  intro t₁ t₂ h
+  rw [code, code] at h
+  simp only [Prod.mk.injEq, CodingFunction.code_eq_code_iff] at h
+  obtain ⟨⟨ρ, _, rfl⟩, h⟩ := h
+  refine (support_supports t₁ ρ ?_).symm
+  rintro c ⟨i, hi, hc⟩
+  have := support_f_congr h i hi
+  simp only [← hc, smul_support, Enumeration.smul_f] at this
+  exact this.symm
+
+/-- **Theorem.** There are exactly `μ` tangles at each level. -/
+@[simp]
+theorem mk_tangle (β : Λ) [LeLevel β] : #(Tangle β) = #μ := by
+  refine le_antisymm ?_ ?_
+  · refine (mk_le_of_injective Tangle.code_injective).trans ?_
+    simp only [mk_prod, lift_id, mk_support]
+    exact Cardinal.mul_le_of_le (mk_codingFunction β).le le_rfl
+      Params.μ_isStrongLimit.isLimit.aleph0_le
+  · have := mk_le_of_injective (typedAtom (α := β)).injective
+    simp only [mk_atom] at this
+    exact this
 
 end ConNF
diff --git a/ConNF/Counting/Hypotheses.lean b/ConNF/Counting/Hypotheses.lean
index 1cbb7c8aa6..25bca9624b 100644
--- a/ConNF/Counting/Hypotheses.lean
+++ b/ConNF/Counting/Hypotheses.lean
@@ -1,5 +1,6 @@
 import ConNF.Structural.Pretangle
 import ConNF.FOA.Basic.Reduction
+import ConNF.Counting.CodingFunction
 
 /-!
 # Hypotheses
@@ -7,12 +8,16 @@ import ConNF.FOA.Basic.Reduction
 
 open MulAction Quiver Set Sum WithBot
 
+open scoped Cardinal
+
 universe u
 
 namespace ConNF
 
 variable [Params.{u}] [Level]
 
+instance : LeLevel (0 : Λ) := ⟨WithBot.coe_le_coe.mpr (Params.Λ_zero_le _)⟩
+
 class CountingAssumptions extends FOAAssumptions where
   toPretangle (β : TypeIndex) [LeLevel β] : Tangle β → Pretangle β
   toPretangle_smul (β : TypeIndex) [LeLevel β] (ρ : Allowable β) (t : Tangle β) :
@@ -32,9 +37,10 @@ class CountingAssumptions extends FOAAssumptions where
     Function.Injective (singleton β γ h)
   singleton_toPretangle (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) :
     Pretangle.ofCoe (toPretangle β (singleton β γ h t)) γ h = {toPretangle γ t}
+  mk_codingFunction_zero : #(CodingFunction 0) < #μ
 
 export CountingAssumptions (toPretangle toPretangle_smul eq_toPretangle_of_mem toPretangle_ext
-  singleton singleton_injective singleton_toPretangle)
+  singleton singleton_injective singleton_toPretangle mk_codingFunction_zero)
 
 variable [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : γ < β)