Progress on exists_swap

Signed-off-by: Sky Wilshaw <[email protected]>

ConNF.lean

@@ -6,6 +6,7 @@ import ConNF.Aux.Rel
 import ConNF.Aux.Set
 import ConNF.Aux.Transfer
 import ConNF.Aux.WellOrder
+import ConNF.Counting.BaseCoding
 import ConNF.Counting.CodingFunction
 import ConNF.Counting.Recode
 import ConNF.Counting.SmulSpec

ConNF/Aux/Rel.lean

@@ -80,6 +80,7 @@ theorem codomEqDom_iff' (r : Rel α α) :
 theorem OneOne.inv {r : Rel α β} (h : r.OneOne) : r.inv.OneOne :=
   ⟨⟨h.coinjective⟩, ⟨h.injective⟩⟩
 
+@[simp]
 theorem inv_apply {r : Rel α β} {x : α} {y : β} :
     r.inv y x ↔ r x y :=
   Iff.rfl

ConNF/Counting/BaseCoding.lean

@@ -0,0 +1,105 @@
+import ConNF.Counting.SpecSame
+
+/-!
+# Coding the base type
+
+In this file, we prove a consequence of freedom of action for `⊥`: a base support can support at
+most `2 ^ #κ`-many different sets of atoms under the action of base permutations.
+
+## Main declarations
+
+* `ConNF.foo`: Something new.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal
+
+namespace ConNF
+
+variable [Params.{u}]
+
+def addAtom' (S : BaseSupport) (a : Atom) : BaseSupport where
+  atoms := Sᴬ + .singleton a
+  nearLitters := Sᴺ
+
+theorem addAtom'_atoms (S : BaseSupport) (a : Atom) :
+    (addAtom' S a)ᴬ = Sᴬ + .singleton a :=
+  rfl
+
+theorem addAtom'_nearLitters (S : BaseSupport) (a : Atom) :
+    (addAtom' S a)ᴺ = Sᴺ :=
+  rfl
+
+theorem addAtom'_closed (S : BaseSupport) (a : Atom) (hS : S.Closed) :
+    (addAtom' S a).Closed := by
+  constructor
+  intro N₁ N₂ hN₁ hN₂ b hb
+  rw [addAtom'_atoms, Enumeration.mem_add_iff]
+  exact Or.inl (hS.interference_subset hN₁ hN₂ b hb)
+
+def Support.ofBase (S : BaseSupport) : Support ⊥ where
+  atoms :=
+    Sᴬ.invImage Prod.snd (λ _ _ ↦ Prod.ext ((Path.eq_nil _).trans (Path.eq_nil _).symm))
+  nearLitters :=
+    Sᴺ.invImage Prod.snd (λ _ _ ↦ Prod.ext ((Path.eq_nil _).trans (Path.eq_nil _).symm))
+
+@[simp]
+theorem Support.ofBase_derivBot (S : BaseSupport) (A : ⊥ ↝ ⊥) :
+    Support.ofBase S ⇘. A = S :=
+  rfl
+
+variable [Level] [CoherentData]
+
+theorem bot_preStrong (S : Support ⊥) : S.PreStrong := by
+  constructor
+  intro A N _ P
+  have := le_antisymm P.A.le bot_le
+  have := P.hδ.trans_eq this
+  cases not_lt_bot this
+
+def addAtom (S : BaseSupport) (a : Atom) : Support ⊥ :=
+  .ofBase (addAtom' S a)
+
+omit [Level] [CoherentData] in
+theorem addAtom_derivBot (S : BaseSupport) (a : Atom) (A : ⊥ ↝ ⊥) :
+    addAtom S a ⇘. A = addAtom' S a :=
+  rfl
+
+theorem addAtom_strong (S : BaseSupport) (a : Atom) (hS : S.Closed) : (addAtom S a).Strong := by
+  constructor
+  · exact bot_preStrong _
+  · constructor
+    intro A
+    rw [addAtom_derivBot]
+    exact addAtom'_closed S a hS
+
+theorem addAtom_spec_eq_spec {S : BaseSupport} (hS : S.Closed) {a₁ a₂ : Atom}
+    (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) :
+    (addAtom S a₁).spec = (addAtom S a₂).spec := by
+  rw [Support.spec_eq_spec_iff]
+  constructor
+  · intro; rfl
+  · intro; rfl
+  all_goals sorry
+
+theorem exists_swap {S : BaseSupport} (h : S.Closed) {a₁ a₂ : Atom}
+    (ha₁ : a₁ ∉ Sᴬ) (ha₂ : a₂ ∉ Sᴬ) (ha : ∀ N ∈ Sᴺ, a₁ ∈ Nᴬ ↔ a₂ ∈ Nᴬ) :
+    ∃ π : BasePerm, π • S = S ∧ π • a₁ = a₂ := by
+  obtain ⟨ρ, hρ⟩ := Support.exists_conv (addAtom_spec_eq_spec h ha₁ ha₂ ha)
+    (addAtom_strong S a₁ h) (addAtom_strong S a₂ h)
+  have hρa := congr_arg (λ S ↦ (S ⇘. .nil)ᴬ) hρ
+  have hρN := congr_arg (λ S ↦ (S ⇘. .nil)ᴺ) hρ
+  simp only [Support.smul_derivBot, BaseSupport.smul_atoms, BaseSupport.smul_nearLitters,
+    addAtom_derivBot, addAtom'_atoms, addAtom'_nearLitters, Enumeration.smul_add] at hρa hρN
+  rw [Enumeration.add_inj_iff_of_bound_eq_bound (by rfl)] at hρa
+  simp only [Enumeration.smul_singleton, Enumeration.singleton_injective.eq_iff] at hρa
+  obtain ⟨hρa, rfl⟩ := hρa
+  refine ⟨ρᵁ .nil, ?_, rfl⟩
+  rw [BaseSupport.smul_eq_iff]
+  constructor
+  · exact Enumeration.eq_of_smul_eq hρa
+  · exact Enumeration.eq_of_smul_eq hρN
+
+end ConNF

ConNF/Counting/SpecSame.lean

@@ -105,7 +105,7 @@ theorem interference_subset_convAtoms_dom (hST : S.spec = T.spec) (hS : S.Strong
   intro a ha
   obtain ⟨N₃, i, hiS, hiT⟩ := hN₁
   obtain ⟨N₄, j, hjS, hjT⟩ := hN₂
-  obtain ⟨k, hkS⟩ := hS.interference_subset ⟨i, hiS⟩ ⟨j, hjS⟩ a ha
+  obtain ⟨k, hkS⟩ := (hS.closed _).interference_subset ⟨i, hiS⟩ ⟨j, hjS⟩ a ha
   rw [spec_eq_spec_iff] at hST
   obtain ⟨a', hkT⟩ := hST.atoms_dom_of_dom hkS
   exact ⟨a', k, hkS, hkT⟩
@@ -117,7 +117,7 @@ theorem interference_subset_convAtoms_codom (hST : S.spec = T.spec) (hT : T.Stro
   intro a ha
   obtain ⟨N₃, i, hiS, hiT⟩ := hN₁
   obtain ⟨N₄, j, hjS, hjT⟩ := hN₂
-  obtain ⟨k, hkT⟩ := hT.interference_subset ⟨i, hiT⟩ ⟨j, hjT⟩ a ha
+  obtain ⟨k, hkT⟩ := (hT.closed _).interference_subset ⟨i, hiT⟩ ⟨j, hjT⟩ a ha
   rw [spec_eq_spec_iff] at hST
   obtain ⟨a', hkS⟩ := (sameSpec_comm hST).atoms_dom_of_dom hkT
   exact ⟨a', k, hkS, hkT⟩

ConNF/Counting/Strong.lean

@@ -21,6 +21,10 @@ namespace ConNF
 
 variable [Params.{u}] {β : TypeIndex}
 
+structure BaseSupport.Closed (S : BaseSupport) : Prop where
+  interference_subset {N₁ N₂ : NearLitter} :
+    N₁ ∈ Sᴺ → N₂ ∈ Sᴺ → ∀ a ∈ interference N₁ N₂, a ∈ Sᴬ
+
 namespace Support
 
 variable [Level] [CoherentData] [LeLevel β]
@@ -31,9 +35,10 @@ structure PreStrong (S : Support β) : Prop where
     (hA : A = P.A ↘ P.hε ↘.) (ht : Nᴸ = fuzz P.hδε t) :
     t.support ≤ S ⇘ (P.A ↘ P.hδ)
 
-structure Strong (S : Support β) extends S.PreStrong : Prop where
-  interference_subset {A : β ↝ ⊥} {N₁ N₂ : NearLitter} :
-    N₁ ∈ (S ⇘. A)ᴺ → N₂ ∈ (S ⇘. A)ᴺ → ∀ a ∈ interference N₁ N₂, a ∈ (S ⇘. A)ᴬ
+structure Closed (S : Support β) : Prop where
+  closed : ∀ A, (S ⇘. A).Closed
+
+structure Strong (S : Support β) extends S.PreStrong, S.Closed : Prop
 
 theorem PreStrong.smul {S : Support β} (hS : S.PreStrong) (ρ : AllPerm β) : (ρᵁ • S).PreStrong := by
   constructor
@@ -51,15 +56,19 @@ theorem PreStrong.smul {S : Support β} (hS : S.PreStrong) (ρ : AllPerm β) : (
       BasePerm.smul_nearLitter_litter, ← Tree.inv_apply, hA, ht]
     rfl
 
-theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong := by
+theorem Closed.smul {S : Support β} (hS : S.Closed) (ρ : AllPerm β) : (ρᵁ • S).Closed := by
+  constructor
+  intro A
   constructor
-  · exact hS.toPreStrong.smul ρ
-  · intro A N₁ N₂ h₁ h₂
-    simp only [smul_derivBot, BaseSupport.smul_nearLitters, BaseSupport.smul_atoms,
-      Enumeration.mem_smul] at h₁ h₂ ⊢
-    intro a ha
-    apply hS.interference_subset h₁ h₂
-    rwa [← BasePerm.smul_interference, Set.smul_mem_smul_set_iff]
+  intro N₁ N₂ h₁ h₂
+  simp only [smul_derivBot, BaseSupport.smul_nearLitters, BaseSupport.smul_atoms,
+    Enumeration.mem_smul] at h₁ h₂ ⊢
+  intro a ha
+  apply (hS.closed A).interference_subset h₁ h₂
+  rwa [← BasePerm.smul_interference, Set.smul_mem_smul_set_iff]
+
+theorem Strong.smul {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong :=
+  ⟨hS.toPreStrong.smul ρ, hS.toClosed.smul ρ⟩
 
 def Constrains : Rel (β ↝ ⊥ × NearLitter) (β ↝ ⊥ × NearLitter) :=
   λ x y ↦ ∃ (P : InflexiblePath β) (t : Tangle P.δ) (B : P.δ ↝ ⊥),
@@ -238,39 +247,53 @@ theorem interferenceSupport_nearLitters (S : Support β) (A : β ↝ ⊥) :
     (S.interferenceSupport ⇘. A)ᴺ = .empty :=
   rfl
 
+def close (S : Support β) : Support β :=
+  S + S.interferenceSupport
+
+theorem le_close (S : Support β) :
+    S ≤ S.close :=
+  le_add_right
+
+theorem close_atoms (S : Support β) (A : β ↝ ⊥) :
+    (S.close ⇘. A)ᴬ = (S ⇘. A)ᴬ + (S.interferenceSupport ⇘. A)ᴬ :=
+  rfl
+
+theorem close_nearLitters (S : Support β) (A : β ↝ ⊥) :
+    (S.close ⇘. A)ᴺ = (S ⇘. A)ᴺ := by
+  rw [close, add_derivBot, BaseSupport.add_nearLitters, interferenceSupport_nearLitters,
+    Enumeration.add_empty]
+
+theorem close_closed (S : Support β) :
+    S.close.Closed := by
+  constructor
+  intro A
+  constructor
+  intro N₁ N₂ hN₁ hN₂ a ha
+  rw [close_nearLitters] at hN₁ hN₂
+  rw [close_atoms, Enumeration.mem_add_iff, mem_interferenceSupport_atoms]
+  exact Or.inr ⟨N₁, hN₁, N₂, hN₂, ha⟩
+
 def strong (S : Support β) : Support β :=
-  S.preStrong + S.preStrong.interferenceSupport
+  S.preStrong.close
 
 theorem preStrong_le_strong (S : Support β) :
     S.preStrong ≤ S.strong :=
-  le_add_right
+  S.preStrong.le_close
 
 theorem le_strong (S : Support β) :
     S ≤ S.strong :=
   S.le_preStrong.trans S.preStrong_le_strong
 
-theorem strong_atoms (S : Support β) (A : β ↝ ⊥) :
-    (S.strong ⇘. A)ᴬ = (S.preStrong ⇘. A)ᴬ + (S.preStrong.interferenceSupport ⇘. A)ᴬ :=
-  rfl
-
-theorem strong_nearLitters (S : Support β) (A : β ↝ ⊥) :
-    (S.strong ⇘. A)ᴺ = (S.preStrong ⇘. A)ᴺ := by
-  rw [strong, add_derivBot, BaseSupport.add_nearLitters, interferenceSupport_nearLitters,
-    Enumeration.add_empty]
-
 theorem strong_strong (S : Support β) :
     S.strong.Strong := by
   constructor
   · constructor
     intro A N hN P t hA ht
-    rw [strong_nearLitters] at hN
+    rw [strong, close_nearLitters] at hN
     apply (S.preStrong_preStrong.support_le hN P t hA ht).trans
     intro B
     exact S.preStrong_le_strong (P.A ↘ P.hδ ⇘ B)
-  · intro A N₁ N₂ hN₁ hN₂ a ha
-    rw [strong_nearLitters] at hN₁ hN₂
-    rw [strong_atoms, Enumeration.mem_add_iff, mem_interferenceSupport_atoms]
-    exact Or.inr ⟨N₁, hN₁, N₂, hN₂, ha⟩
+  · exact close_closed _
 
 end Support
 end ConNF

ConNF/Setup/Enumeration.lean

@@ -294,14 +294,29 @@ theorem mem_smul_iff {G X : Type _} [Group G] [MulAction G X] (x : X) (g : G) (E
     x ∈ g • E ↔ g⁻¹ • x ∈ E :=
   Iff.rfl
 
-theorem eq_of_smul_eq {G X : Type _} [Group G] [MulAction G X] {g₁ g₂ : G} {E : Enumeration X}
+theorem eq_of_smul_eq_smul {G X : Type _} [Group G] [MulAction G X] {g₁ g₂ : G} {E : Enumeration X}
     (h : g₁ • E = g₂ • E) (x : X) (hx : x ∈ E) : g₁ • x = g₂ • x := by
   obtain ⟨i, hi⟩ := hx
   have : (g₁ • E).rel i (g₁ • x) := by rwa [smul_rel, inv_smul_smul]
   rw [h] at this
   have := E.rel_coinjective.coinjective hi this
   exact (eq_inv_smul_iff.mp this).symm
 
+theorem eq_of_smul_eq {G X : Type _} [Group G] [MulAction G X] {g : G} {E : Enumeration X}
+    (h : g • E = E) (x : X) (hx : x ∈ E) : g • x = x := by
+  have := eq_of_smul_eq_smul (g₁ := g) (g₂ := 1) ?_ x hx
+  · rwa [one_smul] at this
+  · rwa [one_smul]
+
+@[simp]
+theorem smul_singleton {G X : Type _} [Group G] [MulAction G X] {g : G} {x : X} :
+    g • singleton x = singleton (g • x) := by
+  apply Enumeration.ext
+  · rfl
+  · ext i y
+    rw [smul_rel]
+    simp only [singleton, and_congr_right_iff, inv_smul_eq_iff]
+
 /-!
 ## Concatenation of enumerations
 -/
@@ -367,6 +382,61 @@ theorem add_empty (E : Enumeration X) :
   · rw [add_bound, empty, add_zero]
   · simp only [empty, rel_add_iff, and_false, exists_const, or_false]
 
+theorem add_inj_of_bound_eq_bound {E F G H : Enumeration X} (h : E.bound = F.bound)
+    (h' : E + G = F + H) : E = F ∧ G = H := by
+  have := congr_arg (·.rel) h'
+  conv at this => dsimp only; rw [funext_iff]; intro; rw [funext_iff]; intro; rw [eq_iff_iff]
+  constructor
+  · apply Enumeration.ext h
+    ext i x
+    constructor
+    · intro hx
+      obtain (hx' | ⟨j, rfl, _⟩) := (this i x).mp (Or.inl hx)
+      · exact hx'
+      · have := E.lt_bound _ ⟨x, hx⟩
+        rw [h, add_lt_iff_neg_left] at this
+        cases (κ_zero_le j).not_lt this
+    · intro hx
+      obtain (hx' | ⟨j, rfl, _⟩) := (this i x).mpr (Or.inl hx)
+      · exact hx'
+      · have := F.lt_bound _ ⟨x, hx⟩
+        rw [h, add_lt_iff_neg_left] at this
+        cases (κ_zero_le j).not_lt this
+  · apply Enumeration.ext
+    · have := congr_arg (·.bound) h'
+      simp only [add_bound, h, add_right_inj] at this
+      exact this
+    ext i x
+    constructor
+    · intro hx
+      obtain (hx' | ⟨j, hj₁, hj₂⟩) := (this (E.bound + i) x).mp (Or.inr ⟨i, rfl, hx⟩)
+      · have := F.lt_bound _ ⟨x, hx'⟩
+        rw [h, add_lt_iff_neg_left] at this
+        cases (κ_zero_le i).not_lt this
+      · simp only [h, Rel.inv_apply, Function.graph_def, add_right_inj] at hj₁
+        rw [← hj₁]
+        exact hj₂
+    · intro hx
+      obtain (hx' | ⟨j, hj₁, hj₂⟩) := (this (F.bound + i) x).mpr (Or.inr ⟨i, rfl, hx⟩)
+      · have := E.lt_bound _ ⟨x, hx'⟩
+        rw [h, add_lt_iff_neg_left] at this
+        cases (κ_zero_le i).not_lt this
+      · simp only [h, Rel.inv_apply, Function.graph_def, add_right_inj] at hj₁
+        rw [← hj₁]
+        exact hj₂
+
+theorem add_inj_iff_of_bound_eq_bound {E F G H : Enumeration X} (h : E.bound = F.bound) :
+    E + G = F + H ↔ E = F ∧ G = H := by
+  constructor
+  · exact add_inj_of_bound_eq_bound h
+  · rintro ⟨rfl, rfl⟩
+    rfl
+
+@[simp]
+theorem smul_add {G X : Type _} [Group G] [MulAction G X] (g : G) (E F : Enumeration X) :
+    g • (E + F) = g • E + g • F :=
+  rfl
+
 -- TODO: Some stuff about the partial order on enumerations and concatenation of enumerations.
 
 end Enumeration

ConNF/Setup/ModelData.lean

@@ -175,13 +175,13 @@ theorem Tangle.smul_atom_eq_of_mem_support {α : TypeIndex} [ModelData α]
     {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t)
     {a : Atom} {A : α ↝ ⊥} (ha : a ∈ (t.support ⇘. A)ᴬ) :
     ρ₁ᵁ A • a = ρ₂ᵁ A • a :=
-  Enumeration.eq_of_smul_eq (congr_arg (λ t ↦ (t.support ⇘. A)ᴬ) h) a ha
+  Enumeration.eq_of_smul_eq_smul (congr_arg (λ t ↦ (t.support ⇘. A)ᴬ) h) a ha
 
 theorem Tangle.smul_nearLitter_eq_of_mem_support {α : TypeIndex} [ModelData α]
     {ρ₁ ρ₂ : AllPerm α} {t : Tangle α} (h : ρ₁ • t = ρ₂ • t)
     {N : NearLitter} {A : α ↝ ⊥} (hN : N ∈ (t.support ⇘. A)ᴺ) :
     ρ₁ᵁ A • N = ρ₂ᵁ A • N :=
-  Enumeration.eq_of_smul_eq (congr_arg (λ t ↦ (t.support ⇘. A)ᴺ) h) N hN
+  Enumeration.eq_of_smul_eq_smul (congr_arg (λ t ↦ (t.support ⇘. A)ᴺ) h) N hN
 
 /-!
 ## Criteria for supports

ConNF/Setup/Support.lean

@@ -130,6 +130,12 @@ theorem smul_eq_smul_iff (π₁ π₂ : BasePerm) (S : BaseSupport) :
         rw [smul_inv_smul, smul_eq_iff_eq_inv_smul] at this
         rwa [← this]
 
+theorem smul_eq_iff (π : BasePerm) (S : BaseSupport) :
+    π • S = S ↔ (∀ a ∈ Sᴬ, π • a = a) ∧ (∀ N ∈ Sᴺ, π • N = N) := by
+  have := smul_eq_smul_iff π 1 S
+  simp only [one_smul] at this
+  exact this
+
 noncomputable instance : Add BaseSupport where
   add S T := ⟨Sᴬ + Tᴬ, Sᴺ + Tᴺ⟩