Finish refactor (for real this time)

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

ConNF/Counting/Conclusions.lean

@@ -22,11 +22,6 @@ theorem mk_codingFunction (β : Λ) [i : LeLevel β] (hzero : #(CodingFunction 0
   · 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 ?_ ?_
@@ -35,9 +30,11 @@ theorem mk_codingFunction (β : Λ) [i : LeLevel β] (hzero : #(CodingFunction 0
         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γ))
+    refine Params.μ_isStrongLimit.2 _ ?_
+    refine (mk_raisedSingleton_le hγ).trans_lt ?_
+    exact mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le
+      (mul_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le Params.κ_lt_μ this)
+      (ih γ (WithBot.coe_lt_coe.mp hγ))
   · simp only [WithBot.coe_lt_coe, not_exists, not_lt] at h
     cases le_antisymm (h 0) (Params.Λ_zero_le β)
     exact hzero

ConNF/Counting/CountCodingFunction.lean

@@ -14,22 +14,23 @@ namespace ConNF
 variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions]
   {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : (γ : TypeIndex) < β)
 
-def RecodeType (S : Support β) : Type u :=
-  { x : Set (RaisedSingleton hγ S) //
-    ∃ ho : ∀ U ∈ SupportOrbit.mk S, AppearsRaised hγ (Subtype.val '' x) U,
-    ∀ U, ∀ hU : U ∈ SupportOrbit.mk S,
+def RecodeType (o : SupportOrbit β) : Type u :=
+  { x : Set (RaisedSingleton hγ) //
+    ∃ ho : ∀ U ∈ o, AppearsRaised hγ (Subtype.val '' x) U,
+    ∀ U, ∀ hU : U ∈ o,
       Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' x) U (ho U hU)) }
 
-noncomputable def recodeSurjection (S : Support β) (x : RecodeType hγ S) :
+noncomputable def recodeSurjection (o : SupportOrbit β) (x : RecodeType hγ o) :
     CodingFunction β :=
-  raisedCodingFunction hγ (Subtype.val '' x.val) (SupportOrbit.mk S)
+  raisedCodingFunction hγ (Subtype.val '' x.val) o
     x.prop.choose x.prop.choose_spec
 
 theorem recodeSurjection_surjective :
-    Surjective (fun (x : (S : Support β) × RecodeType hγ S) => recodeSurjection hγ x.1 x.2) := by
+    Surjective (fun (x : (o : SupportOrbit β) × RecodeType hγ o) =>
+      recodeSurjection hγ x.1 x.2) := by
   rintro χ
   obtain ⟨S, hS⟩ := χ.dom_nonempty
-  refine ⟨⟨S, Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hS),
+  refine ⟨⟨SupportOrbit.mk S, Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hS),
       ?_, ?_⟩, ?_⟩
   · intro U hU
     rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
@@ -44,89 +45,23 @@ theorem recodeSurjection_surjective :
     conv_rhs => rw [CodingFunction.eq_code hS,
       ← recode_eq hγ S ((χ.decode S).get hS) (χ.supports_decode S hS)]
 
-/-
-def RaisedSingleton.smul {S : Support β} (r : RaisedSingleton hγ S) (ρ : Allowable β) :
-    RaisedSingleton hγ (ρ • S) :=
-  ⟨r.val, by
-    obtain ⟨u, hu⟩ := r.prop
-    refine ⟨Allowable.comp (Hom.toPath hγ) ρ • u, ?_⟩
-    rw [hu]⟩
-
-@[simp]
-theorem RaisedSingleton.smul_val {S : Support β} (r : RaisedSingleton hγ S) (ρ : Allowable β) :
-    (r.smul hγ ρ).val = r.val :=
-  rfl
-
-theorem RaisedSingleton.smul_image_val {S : Support β} {ρ : Allowable β}
-    (x : Set (RaisedSingleton hγ (ρ • S))) :
-    Subtype.val '' {u : RaisedSingleton hγ S | u.smul hγ ρ ∈ x} = Subtype.val '' x := by
-  refine le_antisymm ?_ ?_
-  · rintro _ ⟨r, h, rfl⟩
-    exact ⟨RaisedSingleton.smul hγ r ρ, h, rfl⟩
-  · rintro _ ⟨r, h, rfl⟩
-    refine ⟨⟨r.val, ?_⟩, h, rfl⟩
-    obtain ⟨u, hu⟩ := (RaisedSingleton.smul hγ r ρ⁻¹).prop
-    simp only [smul_val, inv_smul_smul] at hu
-    exact ⟨u, hu⟩
--/
-
-theorem recodeSurjection_range_smul_subset (S : Support β) (ρ : Allowable β) :
-    Set.range (recodeSurjection hγ (ρ • S)) ⊆ Set.range (recodeSurjection hγ S) := by
-  rintro _ ⟨⟨x, h₁, h₂⟩, rfl⟩
-  sorry
-  -- refine ⟨⟨{u | u.smul hγ ρ ∈ x}, ?_, ?_⟩, ?_⟩
-  -- · intro U hU
-  --   rw [RaisedSingleton.smul_image_val]
-  --   refine h₁ U ?_
-  --   simp only [SupportOrbit.mem_mk_iff, orbit_smul] at hU ⊢
-  --   exact hU
-  -- · intro U hU ρ' h
-  --   have := h₂ U ?_ ρ' h
-  --   · simp_rw [RaisedSingleton.smul_image_val hγ x]
-  --     exact this
-  --   · simp only [SupportOrbit.mem_mk_iff, orbit_smul] at hU ⊢
-  --     exact hU
-  -- · rw [recodeSurjection, recodeSurjection]
-  --   simp only
-  --   simp_rw [RaisedSingleton.smul_image_val hγ x]
-  --   congr 1
-  --   rw [← SupportOrbit.mem_def, SupportOrbit.mem_mk_iff]
-  --   refine ⟨ρ⁻¹, ?_⟩
-  --   simp only [inv_smul_smul]
-
-theorem recodeSurjection_range_smul (S : Support β) (ρ : Allowable β) :
-    Set.range (recodeSurjection hγ (ρ • S)) = Set.range (recodeSurjection hγ S) := by
-  refine subset_antisymm ?_ ?_
-  · exact recodeSurjection_range_smul_subset hγ S ρ
-  · have := recodeSurjection_range_smul_subset hγ (ρ • S) ρ⁻¹
-    rw [inv_smul_smul] at this
-    exact this
-
 theorem recodeSurjection_range :
-    Set.univ ⊆ ⋃ (o : SupportOrbit β), Set.range (recodeSurjection hγ o.out) := by
+    Set.univ ⊆ Set.range (fun (x : (o : SupportOrbit β) × RecodeType hγ o) =>
+      recodeSurjection hγ x.1 x.2) := by
   intro χ _
-  simp only [mem_iUnion, mem_range]
-  obtain ⟨⟨S, x⟩, h⟩ := recodeSurjection_surjective hγ χ
-  refine ⟨SupportOrbit.mk S, ?_⟩
-  have := SupportOrbit.out_mem (SupportOrbit.mk S)
-  rw [SupportOrbit.mem_mk_iff] at this
-  obtain ⟨ρ, hρ⟩ := this
-  dsimp only at hρ
-  obtain ⟨y, rfl⟩ := (Set.ext_iff.mp (recodeSurjection_range_smul hγ S ρ) χ).mpr ⟨x, h⟩
-  refine ⟨hρ ▸ y, ?_⟩
-  congr 1
-  · exact hρ.symm
-  · simp only [eqRec_heq_iff_heq, heq_eq_eq]
+  exact recodeSurjection_surjective hγ χ
 
 theorem mk_codingFunction_le :
-    #(CodingFunction β) ≤ sum (fun o : SupportOrbit β => 2 ^ #(RaisedSingleton hγ o.out)) := by
+    #(CodingFunction β) ≤ #(SupportOrbit β) * 2 ^ #(RaisedSingleton hγ) := by
   have := mk_subtype_le_of_subset (recodeSurjection_range hγ)
-  have := mk_univ.symm.trans_le (this.trans (mk_iUnion_le_sum_mk))
-  suffices h : ∀ S, #(Set.range (recodeSurjection hγ S)) ≤ 2 ^ #(RaisedSingleton hγ S)
-  · exact this.trans (sum_le_sum _ _ (fun o => h _))
-  intro S
-  refine mk_range_le.trans ?_
-  refine (mk_subtype_le _).trans ?_
-  simp only [mk_prod, mk_set, lift_id, le_refl]
+  have := mk_univ.symm.trans_le (this.trans mk_range_le)
+  rw [mk_sigma] at this
+  have h : ∀ o, #(RecodeType hγ o) ≤ 2 ^ #(RaisedSingleton hγ)
+  · intro o
+    refine (mk_subtype_le _).trans ?_
+    rw [mk_set]
+  have := this.trans (Cardinal.sum_le_sum _ _ h)
+  simp only [sum_const, lift_id] at this
+  exact this
 
 end ConNF

ConNF/Counting/CountRaisedSingleton.lean

@@ -16,79 +16,55 @@ namespace ConNF
 variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions]
     {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : (γ : TypeIndex) < β)
 
-noncomputable def RaisedSingleton.code (S : Support β) (r : RaisedSingleton hγ S) :
-    SupportOrbit β × CodingFunction γ :=
-  (SupportOrbit.mk (raisedSupport hγ S r.prop.choose),
-    CodingFunction.code _ _ (Shell.support_supports r.prop.choose))
+theorem mem_orbit_of_raiseSingleton_eq (S₁ S₂ : Support β) (u₁ u₂ : Shell γ)
+    (hS : S₁.max = S₂.max)
+    (hu : CodingFunction.code _ _ (Shell.support_supports u₁) =
+      CodingFunction.code _ _ (Shell.support_supports u₂))
+    (hSu : SupportOrbit.mk (raisedSupport hγ S₁ u₁) = SupportOrbit.mk (raisedSupport hγ S₂ u₂)) :
+    raiseSingleton hγ S₁ u₁ = raiseSingleton hγ S₂ u₂ := by
+  rw [CodingFunction.code_eq_code_iff] at hu
+  obtain ⟨ρ₁, hρ₁, rfl⟩ := hu
+  symm at hSu
+  rw [← SupportOrbit.mem_def, SupportOrbit.mem_mk_iff] at hSu
+  obtain ⟨ρ₂, hSu⟩ := hSu
+  simp only [raiseSingleton, raisedSupport, CodingFunction.code_eq_code_iff,
+    Enumeration.smul_add] at hSu ⊢
+  obtain ⟨rfl, hSu'⟩ := Enumeration.add_congr (by exact hS) hSu
+  have : Allowable.comp (Hom.toPath hγ) ρ₂ • u₁ = ρ₁ • u₁
+  · rw [← inv_smul_eq_iff, smul_smul]
+    refine u₁.support_supports _ ?_
+    rintro c ⟨i, hi, rfl⟩
+    rw [mul_smul, inv_smul_eq_iff]
+    have := support_f_congr hSu' i hi
+    simp only [Enumeration.smul_f, Enumeration.image_f, hρ₁, raise,
+      raiseIndex, Allowable.smul_address, Allowable.toStructPerm_comp, Tree.comp_apply] at this ⊢
+    refine Address.ext _ _ rfl ?_
+    have := congr_arg Address.value this
+    exact this
+  refine ⟨ρ₂, hSu.symm, ?_⟩
+  rw [← this, Shell.singleton_smul]
 
-/-- TODO: Move this -/
-instance : IsLeftCancelAdd κ := by
-  constructor
-  intro i j k h
-  have := congr_arg (Ordinal.typein (· < ·)) h
-  rw [Params.κ_add_typein, Params.κ_add_typein, Ordinal.add_left_cancel] at this
-  exact Ordinal.typein_injective _ this
+noncomputable def RaisedSingleton.code (r : RaisedSingleton hγ) :
+    κ × SupportOrbit β × CodingFunction γ :=
+  (r.prop.choose.max,
+    SupportOrbit.mk (raisedSupport hγ r.prop.choose r.prop.choose_spec.choose),
+    CodingFunction.code _ _ (Shell.support_supports r.prop.choose_spec.choose))
 
-theorem smul_singleton_smul (S : Support β) (u : Shell γ) (ρ₁ : Allowable β) (ρ₂ : Allowable γ)
-    (h₁ : ρ₁ • raisedSupport hγ S (ρ₂ • u) = raisedSupport hγ S u) :
-    ρ₁ • Shell.singleton β γ hγ (ρ₂ • u) = Shell.singleton β γ hγ u := by
-  rw [Shell.singleton_smul]
-  refine congr_arg _ ?_
-  rw [smul_smul]
-  have := Shell.support_supports u
-    (Allowable.comp (Hom.toPath hγ) ρ₁ * (ρ₂ • u).twist * u.twist⁻¹) ?_
-  · refine Eq.trans ?_ this
-    simp only [mul_smul, smul_left_cancel_iff]
-    rw [← (smul_eq_iff_eq_inv_smul _).mp u.eq_twist_smul,
-      ← Shell.Orbit.mk_smul u ρ₂, (ρ₂ • u).eq_twist_smul]
-  rintro c ⟨i, hi, hc⟩
-  rw [raisedSupport, raisedSupport] at h₁
-  have hi' : i < (ρ₂ • u).support.max
-  · have := congr_arg Enumeration.max h₁
-    simp only [Enumeration.smul_add, Enumeration.add_max, Enumeration.smul_max,
-      Enumeration.image_max, add_right_inj] at this
-    rw [this]
-    exact hi
-  have := support_f_congr h₁ (S.max + i) ?_
-  swap
-  · rw [Enumeration.smul_max, Enumeration.add_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 (by exact hi')] at this
-  refine Address.ext _ _ rfl ?_
-  simp only [Enumeration.image_f, raise, raiseIndex, Allowable.smul_address, ← hc,
-    Address.mk.injEq] at this
-  simp only [Shell.support, Shell.Orbit.mk_smul, Enumeration.smul_f, Allowable.smul_address,
-    mul_smul, map_inv, Tree.inv_apply, Allowable.toStructPerm_comp, Tree.comp_apply] at this ⊢
-  obtain ⟨h₁, h₂⟩ := this
-  rw [Path.comp_inj_right] at h₁
-  rw [h₁] at h₂
-  refine Eq.trans ?_ h₂
-  rw [smul_left_cancel_iff, smul_left_cancel_iff]
-  simp only [Shell.support] at hc
-  rw [congr_arg Address.value hc, Enumeration.smul_f]
-  simp only [inv_smul_eq_iff, Allowable.smul_address, h₁]
-
-theorem RaisedSingleton.code_injective (S : Support β) :
-    Function.Injective (RaisedSingleton.code hγ S) := by
+theorem RaisedSingleton.code_injective :
+    Function.Injective (RaisedSingleton.code hγ) := 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 [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ρ₁
+  rw [r₁.prop.choose_spec.choose_spec, r₂.prop.choose_spec.choose_spec]
+  exact mem_orbit_of_raiseSingleton_eq hγ _ _ _ _
+    (congr_arg (fun x => x.1) h)
+    (congr_arg (fun x => x.2.2) h)
+    (congr_arg (fun x => x.2.1) 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
+theorem mk_raisedSingleton_le :
+    #(RaisedSingleton hγ) ≤ #κ * #(SupportOrbit β) * #(CodingFunction γ) := by
+  have := mk_le_of_injective (RaisedSingleton.code_injective hγ)
+  simp only [mk_prod, lift_id, ← mul_assoc] at this
   exact this
 
 end ConNF

ConNF/Counting/Hypotheses.lean

@@ -61,4 +61,26 @@ theorem singleton_smul (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeInd
       simp only [Enumeration.smul_f, Enumeration.image_f, Allowable.smul_address, smul_support,
         Allowable.toStructPerm_comp, Tree.comp_apply]
 
+theorem singleton_injective (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) :
+    Function.Injective (singleton β γ h) := by
+  intro t₁ t₂ ht
+  refine tangle_ext γ _ _ ?_ ?_
+  · have h₁ := singleton_toPretangle β γ h t₁
+    have h₂ := singleton_toPretangle β γ h t₂
+    rw [ht, h₂, singleton_eq_singleton_iff] at h₁
+    exact h₁.symm
+  · have h₁ := singleton_support β γ h t₁
+    have h₂ := singleton_support β γ h t₂
+    rw [ht, h₂] at h₁
+    refine Enumeration.ext' ?_ ?_
+    · have := congr_arg Enumeration.max h₁
+      simp only [Enumeration.image_max] at this
+      exact this.symm
+    · intro i hi₁ hi₂
+      have := support_f_congr h₁ i hi₂
+      simp only [Enumeration.image_f, Address.mk.injEq] at this
+      refine Address.ext _ _ ?_ ?_
+      · exact Path.comp_inj_right.mp this.1.symm
+      · exact this.2.symm
+
 end ConNF

ConNF/Counting/Recode.lean

@@ -148,8 +148,8 @@ noncomputable def raiseSingleton (S : Support β) (u : Shell γ) : CodingFunctio
     (Shell.singleton β γ hγ u)
     (raisedSupport_supports hγ S u)
 
-def RaisedSingleton (S : Support β) : Type u :=
-  {χ : CodingFunction β // ∃ u : Shell γ, χ = raiseSingleton hγ S u}
+def RaisedSingleton : Type u :=
+  {χ : CodingFunction β // ∃ S : Support β, ∃ u : Shell γ, χ = raiseSingleton hγ S u}
 
 theorem smul_raise_eq (ρ : Allowable β) (c : Address γ) :
     ρ • raise hγ c = raise hγ (Allowable.comp (Hom.toPath hγ) ρ • c) := by
@@ -170,9 +170,9 @@ def raiseSingletons (S : Support β) (t : Shell β) : Set (CodingFunction β) :=
 
 theorem raiseSingletons_subset_range {S : Support β} {t : Shell β} :
     raiseSingletons hγ S t ⊆
-    range (Subtype.val : RaisedSingleton hγ S → CodingFunction β) := by
+    range (Subtype.val : RaisedSingleton hγ → CodingFunction β) := by
   rintro _ ⟨u, _, rfl⟩
-  exact ⟨⟨raiseSingleton hγ S u, ⟨u, rfl⟩⟩, rfl⟩
+  exact ⟨⟨raiseSingleton hγ S u, ⟨S, u, rfl⟩⟩, rfl⟩
 
 theorem smul_reducedSupport_eq (S : Support β) (v : Shell γ) (ρ : Allowable β)
     (hUV : S ≤ ρ • raisedSupport hγ S v)

ConNF/Counting/Shell.lean

@@ -136,6 +136,15 @@ theorem eq_twist_smul (s : Shell β) :
     s.twist • ofTangle (Orbit.mk s).repr = s :=
   s.has_twist.choose_spec
 
+theorem twist_smul (s : Shell β) (ρ : Allowable β) :
+    ρ • s = (ρ • s).twist • s.twist⁻¹ • s := by
+  have := eq_twist_smul s
+  rw [smul_eq_iff_eq_inv_smul] at this
+  rw [← this]
+  have := eq_twist_smul (ρ • s)
+  rw [Orbit.mk_smul] at this
+  exact this.symm
+
 /-- A canonical tangle chosen for this shell. -/
 noncomputable def out (s : Shell β) : Tangle β :=
   s.twist • (Orbit.mk s).repr
@@ -172,6 +181,11 @@ theorem smul_support_max (s : Shell β) (ρ : Allowable β) :
     (ρ • s).support.max = s.support.max := by
   rw [support, support, Orbit.mk_smul, Enumeration.smul_max, Enumeration.smul_max]
 
+@[simp]
+theorem smul_support (s : Shell β) (ρ : Allowable β) :
+    (ρ • s).support = (ρ • s).twist • s.twist⁻¹ • s.support := by
+  rw [support, support, inv_smul_smul, Orbit.mk_smul]
+
 protected noncomputable def singleton
     (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ] (h : (γ : TypeIndex) < β)
     (t : Shell γ) : Shell β :=
@@ -193,6 +207,15 @@ protected theorem singleton_smul
   simp only [Shell.singleton, smul_ofTangle, singleton_smul, ofTangle_p, singleton_toPretangle,
     toPretangle_smul, out_toPretangle, mem_singleton_iff, smul_p]
 
+protected theorem singleton_injective
+    (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ] (h : (γ : TypeIndex) < β) :
+    Function.Injective (Shell.singleton β γ h) := by
+  intro s₁ s₂ hs
+  have h₁ := Shell.singleton_toPretangle β γ h s₁
+  have h₂ := Shell.singleton_toPretangle β γ h s₂
+  rw [hs, h₂, singleton_eq_singleton_iff] at h₁
+  exact Shell.ext _ _ h₁.symm
+
 end Shell
 
 end ConNF