Begin CountSpec

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

ConNF/Counting.lean

@@ -2,3 +2,6 @@ import ConNF.Counting.CodingFunction
 import ConNF.Counting.Spec
 import ConNF.Counting.SpecSMul
 import ConNF.Counting.SpecSame
+import ConNF.Counting.SupportOrbit
+import ConNF.Counting.ExistsSpec
+import ConNF.Counting.CountSpec

ConNF/Counting/CountSpec.lean

@@ -0,0 +1,55 @@
+import ConNF.Counting.ExistsSpec
+import ConNF.Counting.SpecSMul
+import ConNF.Counting.SpecSame
+import ConNF.Counting.SupportOrbit
+
+open Quiver Set Sum WithBot
+
+open scoped symmDiff
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+
+theorem SupportOrbit.hasSpec (o : SupportOrbit β) (ho : o.Strong) :
+    ∃ σ : Spec β, ∀ S (hS : S ∈ o), σ.Specifies S (ho S hS) := by
+  revert ho
+  refine inductionOn
+    (motive := fun o => ∀ (ho : o.Strong),
+      ∃ σ : Spec β, ∀ S (hS : S ∈ o), σ.Specifies S (ho S hS)) o ?_
+  intro S ho
+  refine ⟨S.spec (ho S (mem_mk S)), ?_⟩
+  intro T hT
+  rw [mem_mk_iff] at hT
+  obtain ⟨ρ, rfl⟩ := hT
+  exact (S.spec_specifies (ho S (mem_mk S))).smul ρ
+
+noncomputable def SupportOrbit.spec (o : SupportOrbit β) (ho : o.Strong) : Spec β :=
+  (o.hasSpec ho).choose
+
+theorem SupportOrbit.spec_specifies (o : SupportOrbit β) (ho : o.Strong)
+    (S : Support β) (hS : S ∈ o) : (o.spec ho).Specifies S (ho S hS) :=
+  (o.hasSpec ho).choose_spec S hS
+
+theorem SupportOrbit.spec_injective (o₁ o₂ : SupportOrbit β)
+    (ho₁ : o₁.Strong) (ho₂ : o₂.Strong) (h : o₁.spec ho₁ = o₂.spec ho₂) :
+    o₁ = o₂ := by
+  revert ho₁ ho₂ h
+  refine inductionOn (motive := fun o =>
+    ∀ (ho₁ : o.Strong) (ho₂ : o₂.Strong), o.spec ho₁ = o₂.spec ho₂ → o = o₂) o₁ ?_
+  intro S₁
+  refine inductionOn (motive := fun o =>
+    ∀ (ho₁ : (mk S₁).Strong) (ho₂ : o.Strong),
+      (mk S₁).spec ho₁ = o.spec ho₂ → (mk S₁) = o) o₂ ?_
+  intro S₂
+  intro hS₁ hS₂ h
+  have h₁ := spec_specifies (mk S₁) hS₁ S₁ (mem_mk S₁)
+  have h₂ := spec_specifies (mk S₂) hS₂ S₂ (mem_mk S₂)
+  rw [h] at h₁
+  have := convertAllowable_smul h₂ h₁
+  rw [← mem_def, mem_mk_iff]
+  exact ⟨_, this⟩
+
+end ConNF

ConNF/Counting/ExistsSpec.lean

@@ -0,0 +1,113 @@
+import ConNF.Counting.Spec
+
+open Quiver Set Sum WithBot
+
+open scoped Classical Cardinal symmDiff
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ}
+
+noncomputable def Support.spec (S : Support β) (hS : S.Strong) : Spec β where
+  max := S.max
+  f i hi :=
+    if h : ∃ A a, S.f i hi = ⟨A, inl a⟩ then
+      let A := h.choose
+      let a := h.choose_spec.choose
+      SpecCondition.atom A
+          {j | ∃ hj, S.f j hj = ⟨A, inl a⟩} {j | ∃ hj N, S.f j hj = ⟨A, inr N⟩ ∧ a ∈ N}
+    else if h : ∃ A N, S.f i hi = ⟨A, inr N⟩ then
+      let A := h.choose
+      let N := h.choose_spec.choose
+      if h₁ : Nonempty (InflexibleCoe A N.1) then
+        SpecCondition.inflexibleCoe A h₁.some.path
+          (CodingFunction.code ((S.before i hi).comp (h₁.some.path.B.cons h₁.some.path.hδ))
+            h₁.some.t (Spec.before_comp_supports S hS hi h₁.some h.choose_spec.choose_spec))
+          (CodingFunction.code_strong _ _ _
+            (Support.comp_strong _ _ (Support.before_strong _ _ _ hS)))
+          (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
+            N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+            S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
+      else if h₂ : Nonempty (InflexibleBot A N.1) then
+        SpecCondition.inflexibleBot A h₂.some.path
+          {j | ∃ hj, S.f j hj = ⟨h₂.some.path.B.cons (bot_lt_coe _), inl h₂.some.a⟩}
+          (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
+              N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+              S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
+      else
+        SpecCondition.flexible A
+          {j | ∃ hj, ∃ (N' : NearLitter), S.f j hj = ⟨A, inr N'⟩ ∧ N'.1 = N.1}
+          (fun j => {k | ∃ hj hk, ∃ (a : Atom) (N' : NearLitter),
+            N'.1 = N.1 ∧ a ∈ (N : Set Atom) ∆ N' ∧
+            S.f j hj = ⟨A, inr N'⟩ ∧ S.f k hk = ⟨A, inl a⟩})
+    else
+      SpecCondition.atom (S.f i hi).1 ∅ ∅
+
+theorem Support.spec_specifies (S : Support β) (hS : S.Strong) : (S.spec hS).Specifies S hS := by
+  constructor
+  case max_eq_max => rfl
+  case atom_spec =>
+    intro i hi A a h
+    unfold spec
+    dsimp only
+    have : ∃ A a, S.f i hi = ⟨A, inl a⟩ := ⟨A, a, h⟩
+    rw [dif_pos this]
+    have := h.symm.trans this.choose_spec.choose_spec
+    simp only [Address.mk.injEq, inl.injEq] at this
+    simp only [this, and_self]
+  case flexible_spec =>
+    intro i hi A N hN h
+    unfold spec
+    dsimp only
+    have h₁ : ¬∃ A a, S.f i hi = ⟨A, inl a⟩
+    · rintro ⟨B, b, h'⟩
+      cases h.symm.trans h'
+    have h₂ : ∃ A N, S.f i hi = ⟨A, inr N⟩ := ⟨A, N, h⟩
+    rw [dif_neg h₁, dif_pos h₂]
+    have := h.symm.trans h₂.choose_spec.choose_spec
+    simp only [Address.mk.injEq, inr.injEq] at this
+    simp only [this] at hN ⊢
+    rw [dif_neg, dif_neg]
+    · rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
+      rw [not_nonempty_iff]
+      exact hN.1
+    · rw [flexible_iff_not_inflexibleBot_inflexibleCoe] at hN
+      rw [not_nonempty_iff]
+      exact hN.2
+  case inflexibleCoe_spec =>
+    rintro i hi A N hN h
+    unfold spec
+    dsimp only
+    have h₁ : ¬∃ A a, S.f i hi = ⟨A, inl a⟩
+    · rintro ⟨B, b, h'⟩
+      cases h.symm.trans h'
+    have h₂ : ∃ A N, S.f i hi = ⟨A, inr N⟩ := ⟨A, N, h⟩
+    rw [dif_neg h₁, dif_pos h₂]
+    cases h.symm.trans h₂.choose_spec.choose_spec
+    have h₁ : Nonempty (InflexibleCoe h₂.choose h₂.choose_spec.choose.1) := ⟨hN⟩
+    rw [dif_pos h₁]
+    have : hN = h₁.some := Subsingleton.elim _ _
+    cases this
+    rfl
+  case inflexibleBot_spec =>
+    rintro i hi A N hN h
+    unfold spec
+    dsimp only
+    have h₁ : ¬∃ A a, S.f i hi = ⟨A, inl a⟩
+    · rintro ⟨B, b, h'⟩
+      cases h.symm.trans h'
+    have h₂ : ∃ A N, S.f i hi = ⟨A, inr N⟩ := ⟨A, N, h⟩
+    rw [dif_neg h₁, dif_pos h₂]
+    cases h.symm.trans h₂.choose_spec.choose_spec
+    have h₁ : ¬Nonempty (InflexibleCoe h₂.choose h₂.choose_spec.choose.1)
+    · rintro ⟨h⟩
+      exact inflexibleBot_inflexibleCoe hN h
+    have h₂ : Nonempty (InflexibleBot h₂.choose h₂.choose_spec.choose.1) := ⟨hN⟩
+    rw [dif_neg h₁, dif_pos h₂]
+    have : hN = h₂.some := Subsingleton.elim _ _
+    cases this
+    rfl
+
+end ConNF

ConNF/Counting/SpecSMul.lean

@@ -15,7 +15,7 @@ namespace ConNF
 variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
   {S T : Support β} {hS : S.Strong} {σ : Spec β} (hσS : σ.Specifies S hS) (ρ : Allowable β)
 
-theorem Support.Specifies.smul : σ.Specifies (ρ • S) (hS.smul ρ) := by
+theorem Spec.Specifies.smul : σ.Specifies (ρ • S) (hS.smul ρ) := by
   constructor
   case max_eq_max => exact hσS.max_eq_max
   case atom_spec =>
@@ -117,7 +117,7 @@ theorem Support.Specifies.smul : σ.Specifies (ρ • S) (hS.smul ρ) := by
     · simp only [NearLitterPerm.smul_nearLitter_fst, inflexibleCoe_smul_path, inflexibleCoe_smul_t,
         Tree.inv_apply, ne_eq, eq_mp_eq_cast, CodingFunction.code_eq_code_iff]
       refine ⟨Allowable.comp (P.B.cons P.hδ) ρ, ?_, (smul_inv_smul _ _).symm⟩
-      simp only [before_smul, comp_smul, NearLitterPerm.smul_nearLitter_fst,
+      simp only [Support.before_smul, Support.comp_smul, NearLitterPerm.smul_nearLitter_fst,
         inflexibleCoe_smul_path, inflexibleCoe_smul_t, Tree.inv_apply, ne_eq, eq_mp_eq_cast]
     · ext j k
       constructor

ConNF/Counting/SupportOrbit.lean

@@ -0,0 +1,79 @@
+import Mathlib.GroupTheory.GroupAction.Basic
+import ConNF.Counting.StrongSupport
+
+open Quiver Set Sum WithBot
+
+open scoped symmDiff
+
+universe u
+
+namespace ConNF
+
+variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+
+def SupportOrbit (β : Λ) [LeLevel β] : Type u :=
+  MulAction.orbitRel.Quotient (Allowable β) (Support β)
+
+namespace SupportOrbit
+
+/-- The orbit of a given ordered support. -/
+def mk (S : Support β) : SupportOrbit β :=
+  ⟦S⟧
+
+protected theorem eq {S T : Support β} : mk S = mk T ↔ S ∈ MulAction.orbit (Allowable β) T :=
+  Quotient.eq (r := _)
+
+instance : SetLike (SupportOrbit β) (Support β) where
+  coe o := {S | mk S = o}
+  coe_injective' := by
+    intro o₁ o₂
+    refine Quotient.inductionOn₂ o₁ o₂ ?_
+    intro S₁ S₂ h
+    simp only [ext_iff, mem_setOf_eq] at h
+    exact (h S₁).mp rfl
+
+theorem mem_mk (S : Support β) : S ∈ mk S :=
+  rfl
+
+theorem mem_def (S : Support β) (o : SupportOrbit β) : S ∈ o ↔ mk S = o := Iff.rfl
+
+@[simp]
+theorem mem_mk_iff (S T : Support β) : S ∈ mk T ↔ S ∈ MulAction.orbit (Allowable β) T := by
+  rw [mem_def, mk, mk, ← MulAction.orbitRel_apply, Quotient.eq (r := _)]
+  rfl
+
+theorem smul_mem_of_mem {S : Support β} {o : SupportOrbit β} (ρ : Allowable β) (h : S ∈ o) :
+    ρ • S ∈ o := by
+  refine Quotient.inductionOn o ?_ h
+  intro T hST
+  change _ ∈ mk _ at hST ⊢
+  rw [mem_mk_iff] at hST ⊢
+  obtain ⟨ρ', rfl⟩ := hST
+  rw [smul_smul]
+  exact ⟨ρ * ρ', rfl⟩
+
+theorem smul_mem_iff_mem {S : Support β} {o : SupportOrbit β} (ρ : Allowable β) :
+    ρ • S ∈ o ↔ S ∈ o := by
+  refine ⟨?_, smul_mem_of_mem ρ⟩
+  intro h
+  have := smul_mem_of_mem ρ⁻¹ h
+  rw [inv_smul_smul] at this
+  exact this
+
+theorem eq_of_mem_orbit {o₁ o₂ : SupportOrbit β} {S₁ S₂ : Support β}
+    (h₁ : S₁ ∈ o₁) (h₂ : S₂ ∈ o₂) (h : S₁ ∈ MulAction.orbit (Allowable β) S₂) : o₁ = o₂ := by
+  rw [mem_def] at h₁ h₂
+  rw [← h₁, ← h₂, SupportOrbit.eq]
+  exact h
+
+theorem inductionOn {motive : SupportOrbit β → Prop} (o : SupportOrbit β) (h : ∀ S, motive (mk S)) :
+    motive o :=
+  Quotient.inductionOn o h
+
+/-- An orbit of ordered supports is *strong* if it contains a strong support. -/
+def Strong (o : SupportOrbit β) : Prop :=
+  ∀ S ∈ o, S.Strong
+
+end SupportOrbit
+
+end ConNF