Conclude counting argument

Signed-off-by: zeramorphic <[email protected]>

ConNF.lean

@@ -9,6 +9,7 @@ import ConNF.Aux.WellOrder
 import ConNF.Counting.BaseCoding
 import ConNF.Counting.BaseCounting
 import ConNF.Counting.CodingFunction
+import ConNF.Counting.Conclusions
 import ConNF.Counting.CountSupportOrbit
 import ConNF.Counting.Recode
 import ConNF.Counting.SMulSpec

ConNF/Counting/Conclusions.lean

@@ -0,0 +1,81 @@
+import ConNF.Counting.BaseCounting
+import ConNF.Counting.CountSupportOrbit
+import ConNF.Counting.Recode
+
+/-!
+# Concluding the counting argument
+
+In this file, we finish the counting argument.
+
+## Main declarations
+
+* `ConNF.card_tSet_le`: There are at most `μ`-many t-sets at each level.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [CoherentData]
+
+theorem card_codingFunction (β : TypeIndex) [LeLevel β] :
+    #(CodingFunction β) < #μ := by
+  revert β
+  intro β
+  induction β using WellFoundedLT.induction
+  case a β ih =>
+  intro
+  cases β using WithBot.recBotCoe
+  case bot => exact card_bot_codingFunction_lt
+  case coe β _ =>
+  by_cases hβ : IsMin β
+  · exact card_codingFunction_lt_of_isMin hβ
+  rw [not_isMin_iff] at hβ
+  obtain ⟨γ, hγ⟩ := hβ
+  have hγ := WithBot.coe_lt_coe.mpr hγ
+  have : LeLevel γ := ⟨hγ.le.trans LeLevel.elim⟩
+  have := exists_combination_raisedSingleton hγ
+  choose s o h₁ h₂ using this
+  refine (mk_le_of_injective (f := λ χ ↦ (s χ, o χ)) ?_).trans_lt ?_
+  · intro χ₁ χ₂ h
+    rw [Prod.mk.injEq] at h
+    have hχ₁ := h₂ χ₁
+    have hχ₂ := h₂ χ₂
+    simp only [h.1, h.2, ← hχ₂] at hχ₁
+    exact hχ₁
+  · rw [mk_prod, mk_set, Cardinal.lift_id, Cardinal.lift_id]
+    refine mul_lt_of_lt μ_isStrongLimit.aleph0_le ?_ (card_supportOrbit_lt ih)
+    apply μ_isStrongLimit.2
+    exact card_raisedSingleton_lt _ (card_supportOrbit_lt ih) ih
+
+theorem card_supportOrbit (β : TypeIndex) [LeLevel β] :
+    #(SupportOrbit β) < #μ := by
+  apply card_supportOrbit_lt
+  intro δ _ _
+  exact card_codingFunction δ
+
+/-- Note that we cannot prove the reverse implication because all of our hypotheses at this stage
+are about permutations, not objects. -/
+theorem card_tSet_le (β : TypeIndex) [LeLevel β] :
+    #(TSet β) ≤ #μ := by
+  refine (mk_le_of_injective
+    (f := λ x : TSet β ↦ (Tangle.code ⟨x, designatedSupport x, designatedSupport_supports x⟩,
+      designatedSupport x)) ?_).trans ?_
+  · intro x y h
+    rw [Prod.mk.injEq, Tangle.code_eq_code_iff] at h
+    obtain ⟨⟨ρ, hρ⟩, h⟩ := h
+    have := (designatedSupport_supports x).supports ρ ?_
+    · have hρx := congr_arg (·.set) hρ
+      simp only [Tangle.smul_set] at hρx
+      rw [← hρx, this]
+    · have hρx := congr_arg (·.support) hρ
+      simp only [Tangle.smul_support] at hρx
+      rw [hρx, h]
+  · rw [mk_prod, Cardinal.lift_id, Cardinal.lift_id]
+    apply mul_le_of_le μ_isStrongLimit.aleph0_le (card_codingFunction β).le
+    rw [card_support]
+
+end ConNF

ConNF/Counting/Recode.lean

@@ -191,4 +191,73 @@ theorem exists_combination_raisedSingleton (χ : CodingFunction β) :
     · rintro ⟨y, hy, rfl⟩
       exact ⟨_, ⟨y, hy, rfl⟩, rfl⟩
 
+structure RaisedSingletonData (β γ : Λ) [LeLevel β] [LeLevel γ] : Type u where
+  ba : κ
+  bN : κ
+  o : SupportOrbit β
+  χ : CodingFunction γ
+
+def RaisedSingletonData.mk' (S : Support β) (y : TSet γ) :
+    RaisedSingletonData β γ where
+  ba := Sᴬ.bound
+  bN := Sᴺ.bound
+  o := (S + designatedSupport y ↗ hγ).orbit
+  χ := Tangle.code ⟨y, designatedSupport y, designatedSupport_supports y⟩
+
+theorem RaisedSingletonData.mk'_eq_mk'
+    {S₁ S₂ : Support β} {y₁ y₂ : TSet γ}
+    (h : RaisedSingletonData.mk' hγ S₁ y₁ = RaisedSingletonData.mk' hγ S₂ y₂) :
+    raisedSingleton hγ S₁ y₁ = raisedSingleton hγ S₂ y₂ := by
+  rw [mk', mk', mk.injEq, Support.orbit_eq_iff, Tangle.code_eq_code_iff] at h
+  obtain ⟨ha, hN, ⟨ρ₁, hρ₁⟩, ⟨ρ₂, hρ₂⟩⟩ := h
+  rw [Support.smul_add] at hρ₁
+  have := Support.add_inj_of_bound_eq_bound ?_ ?_ hρ₁
+  swap; exact ha
+  swap; exact hN
+  obtain ⟨rfl, hρ₁y⟩ := this
+  have hρ₂y := congr_arg (·.set) hρ₂
+  dsimp only [Tangle.smul_set] at hρ₂y
+  cases hρ₂y
+  rw [raisedSingleton, raisedSingleton, Tangle.code_eq_code_iff]
+  use ρ₁
+  ext : 1
+  swap
+  · simp only [Tangle.smul_support, Support.smul_add, hρ₁y]
+  simp only [Tangle.smul_set]
+  apply tSet_ext hγ
+  intro z
+  rw [TSet.mem_smul_iff, typedMem_singleton_iff, typedMem_singleton_iff]
+  have hρ₂y' := congr_arg (·.support) hρ₂
+  simp only [Tangle.smul_support] at hρ₂y'
+  rw [← hρ₂y', Support.smul_scoderiv, Support.scoderiv_inj, ← allPermSderiv_forget] at hρ₁y
+  rw [← (designatedSupport_supports y₁).smul_eq_smul hρ₁y, allPerm_inv_sderiv, inv_smul_eq_iff]
+
+theorem card_raisedSingleton_lt' :
+    #(RaisedSingleton hγ) ≤ #(RaisedSingletonData β γ) := by
+  apply mk_le_of_injective
+    (f := λ s ↦ RaisedSingletonData.mk' hγ s.prop.choose s.prop.choose_spec.choose)
+  intro s t h
+  have := RaisedSingletonData.mk'_eq_mk' hγ h
+  rw [← s.prop.choose_spec.choose_spec, ← t.prop.choose_spec.choose_spec] at this
+  exact Subtype.coe_injective this
+
+def raisedSingletonDataEquiv (β γ : Λ) [LeLevel β] [LeLevel γ] :
+    RaisedSingletonData β γ ≃ κ × κ × SupportOrbit β × CodingFunction γ where
+  toFun d := ⟨d.ba, d.bN, d.o, d.χ⟩
+  invFun d := ⟨d.1, d.2.1, d.2.2.1, d.2.2.2⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+theorem card_raisedSingleton_lt (h₁ : #(SupportOrbit β) < #μ)
+    (h₂ : ∀ δ < (β : TypeIndex), [LeLevel δ] → #(CodingFunction δ) < #μ) :
+    #(RaisedSingleton hγ) < #μ := by
+  apply (card_raisedSingleton_lt' hγ).trans_lt
+  rw [Cardinal.eq.mpr ⟨raisedSingletonDataEquiv β γ⟩]
+  simp only [mk_prod, Cardinal.lift_id]
+  apply mul_lt_of_lt μ_isStrongLimit.aleph0_le κ_lt_μ
+  apply mul_lt_of_lt μ_isStrongLimit.aleph0_le κ_lt_μ
+  apply mul_lt_of_lt μ_isStrongLimit.aleph0_le
+  · exact h₁
+  · exact h₂ _ hγ
+
 end ConNF

ConNF/Setup/Support.lean

@@ -271,6 +271,23 @@ theorem coderiv_deriv_eq {α β : TypeIndex} (S : Support β) (A : α ↝ β) :
     S ⇗ A ⇘ A = S :=
   ext' (Sᴬ.coderiv_deriv_eq A) (Sᴺ.coderiv_deriv_eq A)
 
+@[simp]
+theorem coderiv_inj {α β : TypeIndex} (S T : Support β) (A : α ↝ β) :
+    S ⇗ A = T ⇗ A ↔ S = T := by
+  constructor
+  swap
+  · rintro rfl
+    rfl
+  intro h
+  ext B : 1
+  have : S ⇗ A ⇘ A ⇘. B = T ⇗ A ⇘ A ⇘. B := by rw [h]
+  rwa [coderiv_deriv_eq, coderiv_deriv_eq] at this
+
+@[simp]
+theorem scoderiv_inj {α β : TypeIndex} (S T : Support β) (h : β < α) :
+    S ↗ h = T ↗ h ↔ S = T :=
+  coderiv_inj S T (.single h)
+
 instance {α : TypeIndex} : SMul (StrPerm α) (Support α) where
   smul π S := ⟨π • Sᴬ, π • Sᴺ⟩
 
@@ -309,6 +326,34 @@ theorem smul_derivBot {α : TypeIndex} (π : StrPerm α) (S : Support α) (A : 
     (π • S) ⇘. A = π A • (S ⇘. A) :=
   rfl
 
+theorem smul_coderiv {α : TypeIndex} (π : StrPerm α) (S : Support β) (A : α ↝ β) :
+    π • S ⇗ A = (π ⇘ A • S) ⇗ A := by
+  ext B i x
+  · rfl
+  · constructor
+    · rintro ⟨⟨C, x⟩, hS, hx⟩
+      simp only [Prod.mk.injEq] at hx
+      obtain ⟨rfl, rfl⟩ := hx
+      exact ⟨⟨C, x⟩, hS, rfl⟩
+    · rintro ⟨⟨C, x⟩, hS, hx⟩
+      simp only [Prod.mk.injEq] at hx
+      obtain ⟨rfl, rfl⟩ := hx
+      exact ⟨⟨C, _⟩, hS, rfl⟩
+  · rfl
+  · constructor
+    · rintro ⟨⟨C, x⟩, hS, hx⟩
+      simp only [Prod.mk.injEq] at hx
+      obtain ⟨rfl, rfl⟩ := hx
+      exact ⟨⟨C, x⟩, hS, rfl⟩
+    · rintro ⟨⟨C, a⟩, hS, hx⟩
+      simp only [Prod.mk.injEq] at hx
+      obtain ⟨rfl, rfl⟩ := hx
+      exact ⟨⟨C, _⟩, hS, rfl⟩
+
+theorem smul_scoderiv {α : TypeIndex} (π : StrPerm α) (S : Support β) (h : β < α) :
+    π • S ↗ h = (π ↘ h • S) ↗ h :=
+  smul_coderiv π S (Path.single h)
+
 theorem smul_eq_smul_iff (π₁ π₂ : StrPerm β) (S : Support β) :
     π₁ • S = π₂ • S ↔
       ∀ A, (∀ a ∈ (S ⇘. A)ᴬ, π₁ A • a = π₂ A • a) ∧ (∀ N ∈ (S ⇘. A)ᴺ, π₁ A • N = π₂ A • N) := by
@@ -337,6 +382,20 @@ theorem add_derivBot (S T : Support α) (A : α ↝ ⊥) :
     (S + T) ⇘. A = (S ⇘. A) + (T ⇘. A) :=
   rfl
 
+@[simp]
+theorem smul_add (S T : Support α) (π : StrPerm α) :
+    π • (S + T) = π • S + π • T :=
+  rfl
+
+theorem add_inj_of_bound_eq_bound {S T U V : Support α}
+    (ha : Sᴬ.bound = Tᴬ.bound) (hN : Sᴺ.bound = Tᴺ.bound)
+    (h' : S + U = T + V) : S = T ∧ U = V := by
+  have ha' := Enumeration.add_inj_of_bound_eq_bound ha (congr_arg (·ᴬ) h')
+  have hN' := Enumeration.add_inj_of_bound_eq_bound hN (congr_arg (·ᴺ) h')
+  constructor
+  · exact Support.ext' ha'.1 hN'.1
+  · exact Support.ext' ha'.2 hN'.2
+
 end Support
 
 def supportEquiv {α : TypeIndex} : Support α ≃