Begin conclusions

Signed-off-by: zeramorphic <zeramorphic@proton.me>

ConNF/Counting.lean

@@ -10,3 +10,4 @@ import ConNF.Counting.Hypotheses
 import ConNF.Counting.Recode
 import ConNF.Counting.CountCodingFunction
 import ConNF.Counting.CountRaisedSingleton
+import ConNF.Counting.Conclusions

ConNF/Counting/Conclusions.lean

@@ -0,0 +1,42 @@
+import ConNF.Counting.CountSpec
+import ConNF.Counting.CountStrongOrbit
+import ConNF.Counting.CountCodingFunction
+import ConNF.Counting.CountRaisedSingleton
+
+open Cardinal Function MulAction Set Quiver
+
+open scoped Cardinal
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [CountingAssumptions]
+
+theorem mk_codingFunction (β : Λ) [i : LeLevel β] : #(CodingFunction β) < #μ := by
+  revert i
+  refine Params.Λ_isWellOrder.induction (C := fun β => [LeLevel β] → #(CodingFunction β) < #μ) β ?_
+  intro β ih _
+  by_cases h : ∃ γ : Λ, (γ : TypeIndex) < β
+  · obtain ⟨γ, hγ⟩ := h
+    have : LeLevel γ := ⟨le_trans hγ.le LeLevel.elim⟩
+    refine (mk_codingFunction_le hγ).trans_lt ?_
+    refine (sum_le_sum _ (fun _ => 2 ^ (#(SupportOrbit β) * #(CodingFunction γ))) ?_).trans_lt ?_
+    · intro o
+      have := mk_raisedSingleton_le hγ o.out
+      exact Cardinal.pow_mono_left 2 two_ne_zero this
+    rw [sum_const, lift_id, lift_id]
+    have : #(SupportOrbit β) < #μ
+    · refine (mk_supportOrbit_le β).trans_lt ?_
+      refine mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le ?_ ?_
+      · exact Params.μ_isStrongLimit.2 _ Params.κ_lt_μ
+      · refine mk_spec ?_
+        intro δ _ hδ
+        exact ih δ hδ
+    refine mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le this ?_
+    · refine Params.μ_isStrongLimit.2 _ ?_
+      exact mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le this
+        (ih γ (WithBot.coe_lt_coe.mp hγ))
+  · sorry
+
+end ConNF

ConNF/Counting/CountRaisedSingleton.lean

@@ -17,18 +17,55 @@ variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [L
     (hγ : (γ : TypeIndex) < β)
 
 noncomputable def RaisedSingleton.code (S : Support β) (r : RaisedSingleton hγ S) :
-    CodingFunction γ :=
-  CodingFunction.code _ _ (support_supports r.prop.choose)
+    SupportOrbit β × CodingFunction γ :=
+  (SupportOrbit.mk (raisedSupport hγ S r.prop.choose),
+    CodingFunction.code _ _ (support_supports r.prop.choose))
+
+theorem smul_singleton_smul (S : Support β) (u : Tangle γ) (ρ₁ : Allowable β) (ρ₂ : Allowable γ)
+    (h₁ : ρ₁ • raisedSupport hγ S (ρ₂ • u) = raisedSupport hγ S u) :
+    ρ₁ • singleton β γ hγ (ρ₂ • u) = singleton β γ hγ u := by
+  rw [singleton_smul]
+  refine congr_arg _ ?_
+  rw [smul_smul]
+  refine support_supports u (Allowable.comp (Hom.toPath hγ) ρ₁ * ρ₂) ?_
+  rintro c ⟨i, hi, hc⟩
+  rw [raisedSupport, raisedSupport] at h₁
+  have := support_f_congr h₁ (S.max + i) ?_
+  swap
+  · simp only [smul_support, Enumeration.add_max, Enumeration.smul_max, Enumeration.image_max,
+      add_lt_add_iff_left]
+    exact hi
+  rw [Enumeration.add_f_right_add (by exact hi), Enumeration.smul_f,
+    Enumeration.add_f_right_add] at this
+  swap
+  · simp only [smul_support, Enumeration.image_max, Enumeration.smul_max]
+    exact hi
+  simp only [smul_support, Enumeration.image_f, raise, raiseIndex, Enumeration.smul_f, ← hc,
+    Allowable.smul_address, Address.mk.injEq, true_and] at this
+  refine Address.ext _ _ rfl ?_
+  simp only [mul_smul, Allowable.smul_address, Allowable.toStructPerm_comp, Tree.comp_apply]
+  exact this
 
 theorem RaisedSingleton.code_injective (S : Support β) :
     Function.Injective (RaisedSingleton.code hγ S) := by
   rintro r₁ r₂ h
   refine Subtype.coe_injective ?_
   dsimp only
+  rw [code, code, Prod.mk.injEq, CodingFunction.code_eq_code_iff] at h
+  rw [← SupportOrbit.mem_def, SupportOrbit.mem_mk_iff] at h
+  obtain ⟨⟨ρ₁, hρ₁⟩, ⟨ρ₂, hρ₂, hρ₂'⟩⟩ := h
   rw [r₁.prop.choose_spec, r₂.prop.choose_spec, raiseSingleton, raiseSingleton]
-  rw [code, code] at h
-  rw [CodingFunction.code_eq_code_iff] at h ⊢
-  obtain ⟨ρ, hρ₁, hρ₂⟩ := h
-  sorry
+  rw [CodingFunction.code_eq_code_iff]
+  refine ⟨ρ₁⁻¹ , ?_, ?_⟩
+  · rw [← hρ₁, inv_smul_smul]
+  rw [hρ₂'] at hρ₁ ⊢
+  rw [← smul_eq_iff_eq_inv_smul]
+  exact smul_singleton_smul hγ S _ ρ₁ ρ₂ hρ₁
+
+theorem mk_raisedSingleton_le (S : Support β) :
+    #(RaisedSingleton hγ S) ≤ #(SupportOrbit β) * #(CodingFunction γ) := by
+  have := mk_le_of_injective (RaisedSingleton.code_injective hγ S)
+  simp only [mk_prod, lift_id] at this
+  exact this
 
 end ConNF

ConNF/Counting/CountStrongOrbit.lean

@@ -120,4 +120,32 @@ theorem mk_supportOrbit_le_mk_weakSpec (β : Λ) [LeLevel β] :
     #(SupportOrbit β) ≤ #(WeakSpec β) :=
   ⟨⟨SupportOrbit.weakSpec, SupportOrbit.spec_injective⟩⟩
 
+def WeakSpec.decompose (W : WeakSpec β) :
+    κ × (κ → κ) × Spec β :=
+  (W.max, W.f, W.σ)
+
+theorem WeakSpec.decompose_injective : Function.Injective (WeakSpec.decompose (β := β)) := by
+  rintro ⟨m₁, f₁, σ₁⟩ ⟨m₂, f₂, σ₂⟩ h
+  cases h
+  rfl
+
+theorem mk_supportOrbit_le (β : Λ) [LeLevel β] :
+    #(SupportOrbit β) ≤ 2 ^ #κ * #(Spec β) := by
+  refine (mk_supportOrbit_le_mk_weakSpec β).trans ?_
+  refine (Cardinal.mk_le_of_injective WeakSpec.decompose_injective).trans ?_
+  simp only [Cardinal.mk_prod, Cardinal.lift_id, Cardinal.mk_pi, Cardinal.prod_const]
+  rw [← mul_assoc]
+  have hκ := Cardinal.lt_pow (a := 2) (b := #κ) Nat.one_lt_ofNat
+  refine Cardinal.mul_le_of_le (Cardinal.mul_le_of_le ?_ ?_ ?_) ?_ ?_
+  · exact hκ.le.trans (Cardinal.le_mul_right mk_enumeration_ne_zero)
+  · rw [Cardinal.power_self_eq Params.κ_isRegular.aleph0_le]
+    exact Cardinal.le_mul_right mk_enumeration_ne_zero
+  · exact Params.κ_isRegular.aleph0_le.trans
+      (hκ.le.trans (Cardinal.le_mul_right mk_enumeration_ne_zero))
+  · refine Cardinal.le_mul_left ?_
+    have := Cardinal.aleph0_pos.trans_le (Params.κ_isRegular.aleph0_le.trans hκ.le)
+    exact ne_of_gt this
+  · exact Params.κ_isRegular.aleph0_le.trans
+      (hκ.le.trans (Cardinal.le_mul_right mk_enumeration_ne_zero))
+
 end ConNF

ConNF/Structural/Enumeration.lean

@@ -251,6 +251,10 @@ theorem _root_.Cardinal.lt_pow {a b : Cardinal} (h : 1 < a) : b < a ^ b := by
   simp only [sum_const, Cardinal.lift_id, mul_one, prod_const] at this
   exact this
 
+theorem mk_enumeration_ne_zero {α : Type u} : #(Enumeration α) ≠ 0 := by
+  rw [Cardinal.mk_ne_zero_iff]
+  exact ⟨⟨0, fun _ hi => (κ_not_lt_zero _ hi).elim⟩⟩
+
 /-- A bound on the amount of enumerations. -/
 theorem mk_enumeration_le {α : Type u} [Nontrivial α] : #(Enumeration α) ≤ #α ^ #κ := by
   rw [mk_congr enumerationEquiv]