Count coding functions better

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

ConNF/Counting.lean

@@ -9,3 +9,4 @@ import ConNF.Counting.CountStrongOrbit
 import ConNF.Counting.Hypotheses
 import ConNF.Counting.Recode
 import ConNF.Counting.CountCodingFunction
+import ConNF.Counting.CountRaisedSingleton

ConNF/Counting/CountCodingFunction.lean

@@ -4,7 +4,7 @@ import ConNF.Counting.Recode
 # Counting coding functions
 -/
 
-open Cardinal Function MulAction Set
+open Cardinal Function MulAction Set Quiver
 open scoped Cardinal
 
 universe u
@@ -14,18 +14,22 @@ namespace ConNF
 variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
   (hγ : (γ : TypeIndex) < β)
 
-noncomputable def recodeSurjection
-    (x : { x : Set (RaisedSingleton hγ) × SupportOrbit β //
-      ∃ ho : ∀ U ∈ x.2, AppearsRaised hγ (Subtype.val '' x.1) U,
-      ∀ U, ∀ hU : U ∈ x.2,
-        Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' x.1) U (ho U hU)) }) :
+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,
+      Supports (Allowable β) {c | c ∈ U} (decodeRaised hγ (Subtype.val '' x) U (ho U hU)) }
+
+noncomputable def recodeSurjection (S : Support β) (x : RecodeType hγ S) :
     CodingFunction β :=
-  raisedCodingFunction hγ (Subtype.val '' x.val.1) x.val.2 x.prop.choose x.prop.choose_spec
+  raisedCodingFunction hγ (Subtype.val '' x.val) (SupportOrbit.mk S)
+    x.prop.choose x.prop.choose_spec
 
-theorem recodeSurjection_surjective : Surjective (recodeSurjection hγ) := by
+theorem recodeSurjection_surjective :
+    Surjective (fun (x : (S : Support β) × RecodeType hγ S) => recodeSurjection hγ x.1 x.2) := by
   rintro χ
   obtain ⟨S, hS⟩ := χ.dom_nonempty
-  refine ⟨⟨⟨Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hS), SupportOrbit.mk S⟩,
+  refine ⟨⟨S, Subtype.val ⁻¹' raiseSingletons hγ S ((χ.decode S).get hS),
       ?_, ?_⟩, ?_⟩
   · intro U hU
     rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
@@ -34,15 +38,91 @@ theorem recodeSurjection_surjective : Surjective (recodeSurjection hγ) := by
     conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
     exact supports_decodeRaised_of_mem_orbit hγ S
       ((χ.decode S).get hS) (χ.supports_decode S hS) U hU
-  · rw [recodeSurjection]
+  · dsimp only
+    rw [recodeSurjection]
     conv in (Subtype.val '' _) => rw [image_preimage_eq_of_subset (raiseSingletons_subset_range hγ)]
     conv_rhs => rw [CodingFunction.eq_code hS,
       ← recode_eq hγ S ((χ.decode S).get hS) (χ.supports_decode S hS)]
 
-/-- The main lemma about counting coding functions. -/
-theorem mk_strong_codingFunction_le :
-    #(CodingFunction β) ≤ 2 ^ #(RaisedSingleton hγ) * #(SupportOrbit β) := by
-  refine (mk_le_of_surjective (recodeSurjection_surjective hγ)).trans ?_
+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, raiseSingleton_smul]⟩
+
+@[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⟩
+  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
+  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]
+
+theorem mk_codingFunction_le :
+    #(CodingFunction β) ≤ sum (fun o : SupportOrbit β => 2 ^ #(RaisedSingleton hγ o.out)) := 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]
 

ConNF/Counting/CountRaisedSingleton.lean

@@ -0,0 +1,34 @@
+import ConNF.Counting.Recode
+import ConNF.Counting.Spec
+
+/-!
+# Counting raised singletons
+-/
+
+open Cardinal Function MulAction Set Quiver
+
+open scoped Cardinal
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
+    (hγ : (γ : TypeIndex) < β)
+
+noncomputable def RaisedSingleton.code (S : Support β) (r : RaisedSingleton hγ S) :
+    CodingFunction γ :=
+  CodingFunction.code _ _ (support_supports r.prop.choose)
+
+theorem RaisedSingleton.code_injective (S : Support β) :
+    Function.Injective (RaisedSingleton.code hγ S) := by
+  rintro r₁ r₂ h
+  refine Subtype.coe_injective ?_
+  dsimp only
+  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
+
+end ConNF

ConNF/Counting/Hypotheses.lean

@@ -28,11 +28,13 @@ class CountingAssumptions extends FOAAssumptions where
     t₁ = t₂
   /-- Any `γ`-tangle can be treated as a singleton at level `β` if `γ < β`. -/
   singleton (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) : Tangle β
+  singleton_injective (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) :
+    Function.Injective (singleton β γ h)
   singleton_toPretangle (β : Λ) [LeLevel β] (γ : TypeIndex) [LeLevel γ] (h : γ < β) (t : Tangle γ) :
     Pretangle.ofCoe (toPretangle β (singleton β γ h t)) γ h = {toPretangle γ t}
 
 export CountingAssumptions (toPretangle toPretangle_smul eq_toPretangle_of_mem toPretangle_ext
-  singleton singleton_toPretangle)
+  singleton singleton_injective singleton_toPretangle)
 
 variable [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : γ < β)
 

ConNF/Counting/Recode.lean

@@ -124,7 +124,7 @@ def tangleExtension (t : Tangle β) : Set (Tangle γ) :=
 
 /-- A support for a `γ`-tangle, expressed as a set of `β`-support conditions. -/
 noncomputable def raisedSupport (S : Support β) (u : Tangle γ) : Support β :=
-  S + Enumeration.ofSet (raise hγ '' u.support) u.support.small.image
+  S + u.support.image (raise hγ)
 
 theorem le_raisedSupport (S : Support β) (u : Tangle γ) :
     S ≤ raisedSupport hγ S u :=
@@ -139,17 +139,60 @@ theorem raisedSupport_supports (S : Support β) (u : Tangle γ) :
   intro c hc
   rw [← smul_raise_eq_iff]
   refine h ?_
-  erw [raisedSupport, Enumeration.mem_add_iff, Enumeration.mem_ofSet_iff, mem_image]
-  exact Or.inr ⟨c, hc, rfl⟩
+  erw [raisedSupport, Enumeration.mem_add_iff]
+  exact Or.inr (Enumeration.apply_mem_image hc _)
 
 noncomputable def raiseSingleton (S : Support β) (u : Tangle γ) : CodingFunction β :=
   CodingFunction.code
     (raisedSupport hγ S u)
     (singleton β γ hγ u)
     (raisedSupport_supports hγ S u)
 
-def RaisedSingleton : Type u :=
-  {χ : CodingFunction β // ∃ S : Support β, ∃ u : Tangle γ, χ = raiseSingleton hγ S u}
+def RaisedSingleton (S : Support β) : Type u :=
+  {χ : CodingFunction β // ∃ u : Tangle γ, χ = raiseSingleton hγ S u}
+
+theorem smul_raise_eq (ρ : Allowable β) (c : Address γ) :
+    ρ • raise hγ c = raise hγ (Allowable.comp (Hom.toPath hγ) ρ • c) := by
+  simp only [raise, raiseIndex, Allowable.smul_address, Allowable.toStructPerm_comp,
+    Tree.comp_apply]
+
+theorem smul_image_raise_eq (ρ : Allowable β) (T : Support γ) :
+    ρ • T.image (raise hγ) = (Allowable.comp (Hom.toPath hγ) ρ • T).image (raise hγ) := by
+  refine Enumeration.ext' rfl ?_
+  intro i hE hF
+  dsimp only [Enumeration.smul_f, Enumeration.image_f]
+  rw [smul_raise_eq]
+
+theorem smul_raisedSupport (S : Support β) (u : Tangle γ) (ρ : Allowable β) :
+    ρ • raisedSupport hγ S u =
+      raisedSupport hγ (ρ • S) (Allowable.comp (Hom.toPath hγ) ρ • u) := by
+  simp only [raisedSupport, Enumeration.smul_add, smul_support, smul_image_raise_eq]
+
+theorem raiseSingleton_smul (S : Support β) (u : Tangle γ) (ρ : Allowable β) :
+    raiseSingleton hγ S u = raiseSingleton hγ (ρ • S) (Allowable.comp (Hom.toPath hγ) ρ • u) := by
+  rw [raiseSingleton, raiseSingleton, CodingFunction.code_eq_code_iff]
+  refine ⟨ρ, (smul_raisedSupport hγ S u ρ).symm, ?_⟩
+  rw [singleton_smul]
+
+theorem raiseSingleton_eq (S₁ S₂ : Support β) (h : S₁.max = S₂.max) (u₁ u₂ : Tangle γ)
+    (h : raiseSingleton hγ S₁ u₁ = raiseSingleton hγ S₂ u₂) :
+    ∃ ρ : Allowable β, S₂ = ρ • S₁ ∧ u₂ = Allowable.comp (Hom.toPath hγ) ρ • u₁ := by
+  rw [raiseSingleton, raiseSingleton, CodingFunction.code_eq_code_iff] at h
+  obtain ⟨ρ, hρ₁, hρ₂⟩ := h
+  refine ⟨ρ, ?_, ?_⟩
+  · rw [smul_raisedSupport, raisedSupport, raisedSupport] at hρ₁
+    refine Enumeration.ext' h.symm ?_
+    intro i h₂ h₁
+    have := support_f_congr hρ₁ i ?_
+    swap
+    · rw [Enumeration.add_max]
+      refine h₂.trans_le ?_
+      simp only [Enumeration.image_max, le_add_iff_nonneg_right]
+      exact κ_pos _
+    rw [Enumeration.add_f_left, Enumeration.add_f_left] at this
+    exact this
+  · rw [singleton_smul, (singleton_injective _ _ _).eq_iff] at hρ₂
+    exact hρ₂
 
 /-- Take the `γ`-extension of `t`, treated as a set of `α`-level singletons, and turn them into
 coding functions. -/
@@ -158,9 +201,9 @@ def raiseSingletons (S : Support β) (t : Tangle β) : Set (CodingFunction β) :
 
 theorem raiseSingletons_subset_range {S : Support β} {t : Tangle β} :
     raiseSingletons hγ S t ⊆
-    range (Subtype.val : RaisedSingleton hγ → CodingFunction β) := by
+    range (Subtype.val : RaisedSingleton hγ S → CodingFunction β) := by
   rintro _ ⟨u, _, rfl⟩
-  exact ⟨⟨raiseSingleton hγ S u, ⟨S, u, rfl⟩⟩, rfl⟩
+  exact ⟨⟨raiseSingleton hγ S u, ⟨u, rfl⟩⟩, rfl⟩
 
 theorem smul_reducedSupport_eq (S : Support β) (v : Tangle γ) (ρ : Allowable β)
     (hUV : S ≤ ρ • raisedSupport hγ S v)

ConNF/Counting/SupportOrbit.lean

@@ -75,6 +75,12 @@ theorem nonempty (o : SupportOrbit β) : Set.Nonempty {S | S ∈ o} := by
   intro S
   exact ⟨S, mem_mk _⟩
 
+noncomputable def out (o : SupportOrbit β) : Support β :=
+  Quotient.out (s := _) o
+
+theorem out_mem (o : SupportOrbit β) : o.out ∈ o :=
+  Quotient.out_eq (s := _) o
+
 theorem eq_mk_of_mem {S : Support β} {o : SupportOrbit β} (h : S ∈ o) : o = mk S :=
   h.symm