Progress on coherent data

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

ConNF/Construction/MainInduction.lean

@@ -1,5 +1,6 @@
-import ConNF.Construction.NewModelData
 import ConNF.Basic.InductiveConstruction
+import ConNF.Construction.NewModelData
+import ConNF.Counting.Conclusions
 
 /-!
 # New file
@@ -26,10 +27,13 @@ structure Motive (α : Λ) where
   typed : TypedNearLitters α
 
 structure Hypothesis (α : Λ) (M : Motive α) (N : (β : Λ) → β < α → Motive β) where
+  allPermSderiv {β : Λ} (h : β < α) : M.data.AllPerm → (N β h).data.AllPerm
+  allPermBotSderiv : M.data.AllPerm → botModelData.AllPerm
+  singleton {β : Λ} (h : β < α) : (N β h).data.TSet → M.data.TSet
 
 theorem card_tangle_bot_le [ModelData ⊥] : #(Tangle ⊥) ≤ #μ := by
   apply card_tangle_le_of_card_tSet
-  apply (mk_le_of_injective (tSetForget_injective' (α := ⊥))).trans
+  apply (mk_le_of_injective (ModelData.tSetForget_injective' (α := ⊥))).trans
   apply (mk_le_of_injective StrSet.botEquiv.injective).trans
   rw [card_atom]
 
@@ -43,8 +47,7 @@ theorem pos_tangle_bot [ModelData ⊥] (t : Tangle ⊥) :
     pos (StrSet.botEquiv t.setᵁ) < pos t :=
   funOfDeny_gt_deny _ _ _ _ _ rfl
 
-def ltData
-    (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+def ltData (α : Λ) (M : (β : Λ) → β < α → Motive β) :
     letI : Level := ⟨α⟩; LtData :=
   letI : Level := ⟨α⟩
   letI data : (β : TypeIndex) → [LtLevel β] → ModelData β :=
@@ -57,15 +60,142 @@ def ltData
     λ β hβ ↦ (M β (WithBot.coe_lt_coe.mp hβ.elim)).typed
   LtData.mk (data := data) (positions := positions) (typedNearLitters := typedNearLitters)
 
+def newModelData' (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; ModelData α :=
+  letI : Level := ⟨α⟩
+  letI : LtData := ltData α M
+  newModelData
+
+def castData (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LeLevel β] : ModelData β :=
+  if h : β = α then
+    cast (by simp_rw [h]) (newModelData' α M)
+  else
+    letI : Level := ⟨α⟩
+    haveI : LtLevel β := ⟨LeLevel.elim.lt_of_ne h⟩
+    (ltData α M).data β
+
+theorem castData_eq_of_eq (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩
+    letI : LeLevel α := ⟨le_rfl⟩
+    castData α M α = newModelData' α M := by
+  letI : Level := ⟨α⟩
+  rw [castData, dif_pos rfl]
+  rfl
+
+theorem castData_eq_of_lt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] :
+    letI : Level := ⟨α⟩
+    castData α M β = (ltData α M).data β := by
+  letI : Level := ⟨α⟩
+  rw [castData, dif_neg]
+  rintro rfl
+  exact LtLevel.elim.ne rfl
+
+def liftCastDataLt (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    {D : (β : TypeIndex) → ModelData β → Type _}
+    (f : letI : Level := ⟨α⟩; (β : TypeIndex) → [LtLevel β] → D β ((ltData α M).data β))
+    (β : TypeIndex) [letI : Level := ⟨α⟩; LtLevel β] : D β (castData α M β) :=
+  cast (by rw [castData_eq_of_lt]) (f β)
+
+def liftCastDataLe (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    {D : (β : TypeIndex) → ModelData β → Type _} (β : TypeIndex)
+    (fβ : letI : Level := ⟨α⟩; [LtLevel β] → D β ((ltData α M).data β))
+    (fα : D α (newModelData' α M))
+    [letI : Level := ⟨α⟩; LeLevel β] : D β (castData α M β) :=
+  if h : β = α then
+    cast (by cases h; rw [castData_eq_of_eq]) fα
+  else
+    letI : Level := ⟨α⟩
+    haveI : LtLevel β := ⟨LeLevel.elim.lt_of_ne h⟩
+    cast (by rw [castData_eq_of_lt]) (fβ)
+
+def leData (α : Λ) (M : (β : Λ) → β < α → Motive β) :
+    letI : Level := ⟨α⟩; LeData :=
+  letI : Level := ⟨α⟩
+  letI data : (β : TypeIndex) → [LeLevel β] → ModelData β := castData α M
+  letI positions : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) :=
+    liftCastDataLt α M
+      (D := λ β (x : ModelData β) ↦ Position (@Tangle _ β x)) (ltData α M).positions
+  LeData.mk (data := data) (positions := positions)
+
+def preCoherentData (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
+    letI : Level := ⟨α⟩; PreCoherentData :=
+  letI : Level := ⟨α⟩
+  letI := leData α M
+  {
+    allPermSderiv := λ {β γ} _ _ hγ ρ ↦
+      -- Case split on `γ = α`.
+      liftCastDataLe α M (D := λ γ Mγ ↦ γ < β → Mγ.AllPerm) γ
+        -- Case split on `β = α`.
+        (λ hγ ↦ liftCastDataLe α M
+          (D := λ _β Mβ ↦ Mβ.AllPerm → ((ltData α M).data γ).AllPerm) β
+          ( -- Case split on `β = ⊥`.
+            β.recBotCoe (C := λ β ↦ [LtLevel β] → γ < β →
+              ((ltData α M).data β).AllPerm → ((ltData α M).data γ).AllPerm)
+            (λ h ↦ (not_lt_bot h).elim)
+            (λ β _ ↦ -- Case split on `γ = ⊥`.
+              γ.recBotCoe (C := λ γ ↦ [LtLevel γ] → γ < β →
+                ((ltData α M).data β).AllPerm → ((ltData α M).data γ).AllPerm)
+              (λ _ ↦ (H β (WithBot.coe_lt_coe.mp LtLevel.elim)).allPermBotSderiv)
+              (λ _γ _ hγ ↦ (H β (WithBot.coe_lt_coe.mp LtLevel.elim)).allPermSderiv
+                  (WithBot.coe_lt_coe.mp hγ)))
+            hγ)
+          (λ ρ ↦ letI : LtData := ltData α M; ρ.sderiv γ)
+          ρ)
+        (λ h' ↦ (LeLevel.elim.not_lt h').elim) hγ
+    singleton := λ {β γ} _ _ hγ x ↦
+      -- Case split on `γ = α`.
+      liftCastDataLe α M (D := λ γ Mγ ↦ γ < β → Mγ.TSet → TSet β) γ
+      (λ _hγ ↦
+        -- Case split on `β = α`.
+        liftCastDataLe α M
+          (D := λ _β Mβ ↦ ((ltData α M).data γ).TSet → Mβ.TSet) β
+          ((H β (WithBot.coe_lt_coe.mp LtLevel.elim)).singleton (WithBot.coe_lt_coe.mp hγ))
+          (λ x ↦ letI : LtData := ltData α M; some (newSingleton x)))
+      (λ h' ↦ (LeLevel.elim.not_lt h').elim) hγ x
+  }
+
+def coherentData
+    (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
+    letI : Level := ⟨α⟩; CoherentData :=
+  letI : Level := ⟨α⟩
+  letI := preCoherentData α M H
+  ⟨sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩
+
+theorem construct_tangle_le_μ' (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
+    letI : Level := ⟨α⟩
+    letI : LeLevel α := ⟨le_rfl⟩
+    letI := coherentData α M H
+    #(Tangle α) ≤ #μ :=
+  letI : Level := ⟨α⟩
+  letI : LeLevel α := ⟨le_rfl⟩
+  letI := coherentData α M H
+  card_tangle_le α
+
+theorem construct_tangle_le_μ (α : Λ) (M : (β : Λ) → β < α → Motive β)
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
+    letI := newModelData' α M
+    #(Tangle α) ≤ #μ :=
+  sorry
+
 def constructMotive (α : Λ) (M : (β : Λ) → β < α → Motive β)
-    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) fun γ h' ↦ M γ (h'.trans h)) :
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
     Motive α :=
   letI : Level := ⟨α⟩
   letI : LtData := ltData α M
-  ⟨newModelData, sorry, sorry⟩
+  letI := newModelData
+  {
+    data := newModelData,
+    pos := newPosition (construct_tangle_le_μ α M H),
+    typed := newTypedNearLitters (construct_tangle_le_μ α M H)
+  }
 
 def constructHypothesis (α : Λ) (M : (β : Λ) → β < α → Motive β)
-    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) fun γ h' ↦ M γ (h'.trans h)) :
+    (H : (β : Λ) → (h : β < α) → Hypothesis β (M β h) λ γ h' ↦ M γ (h'.trans h)) :
     Hypothesis α (constructMotive α M H) M :=
   sorry
 

ConNF/Construction/NewModelData.lean

@@ -264,6 +264,30 @@ def newPreModelData : PreModelData α where
   tSetForget x := x.elim (StrSet.coeEquiv.symm λ _ _ ↦ ∅) (·ᵁ)
   allPermForget := (·ᵁ)
 
+@[simp]
+theorem newPreModelData.tSetForget_none :
+    newPreModelData.tSetForget none = (StrSet.coeEquiv.symm λ _ _ ↦ ∅) :=
+  rfl
+
+@[simp]
+theorem newPreModelData.tSetForget_some (x : NewSet) :
+    newPreModelData.tSetForget (some x) = xᵁ :=
+  rfl
+
+@[simp]
+theorem newPreModelData.tSetForget_none' :
+    (show @TSet _ α newPreModelData from none)ᵁ = (StrSet.coeEquiv.symm λ _ _ ↦ ∅) :=
+  rfl
+
+@[simp]
+theorem newPreModelData.tSetForget_some' (x : NewSet) :
+    (show @TSet _ α newPreModelData from some x)ᵁ = xᵁ :=
+  rfl
+
+theorem StrSet.smul_none (π : StrPerm α) :
+    π • (StrSet.coeEquiv.symm λ _ _ ↦ ∅ : StrSet α) = StrSet.coeEquiv.symm λ _ _ ↦ ∅ := by
+  sorry
+
 theorem NewPerm.forget_injective (ρ₁ ρ₂ : NewPerm) (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂ := by
   ext β hβ : 3
   apply allPermForget_injective
@@ -299,18 +323,38 @@ theorem NewSet.exists_support (x : letI := newPreModelData; TSet α) :
     letI := newPreModelData
     ∃ S : Support α, S.Supports x := by
   letI := newPreModelData
-  obtain ⟨S, hS⟩ := x.hS
-  refine ⟨S, ?_, λ h ↦ (WithBot.bot_ne_coe.symm h).elim⟩
-  intro ρ hρ
-  apply NewSet.ext
-  exact hS ρ hρ
+  obtain (_ | x) := x
+  · use ⟨.empty, .empty⟩
+    constructor
+    · intros
+      rfl
+    · rintro ⟨⟩
+  · obtain ⟨S, hS⟩ := x.hS
+    refine ⟨S, ?_, λ h ↦ (WithBot.bot_ne_coe.symm h).elim⟩
+    intro ρ hρ
+    apply congr_arg some
+    apply NewSet.ext
+    exact hS ρ hρ
+
+theorem NewSet.coe_ne_empty (x : NewSet) : xᵁ ≠ (StrSet.coeEquiv.symm λ _ _ ↦ ∅) := by
+  sorry
 
 def newModelData : ModelData α where
-  tSetForget_injective' := NewSet.forget_injective
+  tSetForget_injective' := by
+    rintro (_ | x) (_ | y) h
+    · rfl
+    · cases NewSet.coe_ne_empty y h.symm
+    · cases NewSet.coe_ne_empty x h
+    · rw [NewSet.forget_injective x y h]
+  tSetForget_surjective_of_bot' := by rintro ⟨⟩
   allPermForget_injective' := NewPerm.forget_injective
   allPermForget_one := NewPerm.forget_one
   allPermForget_mul := NewPerm.forget_mul
-  smul_forget := NewPerm.smul_forget
+  smul_forget := by
+    rintro ρ (_ | x)
+    · rw [newPreModelData.tSetForget_none', StrSet.smul_none]
+      rfl
+    · exact NewPerm.smul_forget ρ x
   exists_support := NewSet.exists_support
   __ := newPreModelData
 
@@ -342,9 +386,14 @@ def NearLitter.code (N : NearLitter) : Code :=
     have : #Nᴬ ≠ 0 := sorry
     rw [Cardinal.mk_ne_zero_iff_nonempty] at this
     obtain ⟨a, ha⟩ := this
-     ⟩
+    obtain ⟨x, hx⟩ := tSetForget_surjective (StrSet.botEquiv.symm a)
+    use x
+    rwa [Set.mem_setOf_eq, hx, Equiv.apply_symm_apply]⟩
 
 def newTyped (N : NearLitter) : NewSet :=
+  N.code.toSet sorry
+
+def newSingleton {γ : Λ} [LtLevel γ] (x : TSet γ) : NewSet :=
   sorry
 
 local instance : ModelData α := newModelData
@@ -360,4 +409,14 @@ theorem card_newPositionDeny (t : Tangle α) :
 def newPosition (h : #(Tangle α) ≤ #μ) : Position (Tangle α) where
   pos := ⟨funOfDeny h newPositionDeny card_newPositionDeny, funOfDeny_injective _ _ _⟩
 
+def newTypedNearLitters (h : #(Tangle α) ≤ #μ) :
+    letI := newPosition h; TypedNearLitters α :=
+  letI := newPosition h
+  {
+    typed := some ∘ newTyped
+    typed_injective := sorry
+    pos_le_pos_of_typed := sorry
+    smul_typed := sorry
+  }
+
 end ConNF

ConNF/Counting/Conclusions.lean

@@ -78,4 +78,8 @@ theorem card_tSet_le (β : TypeIndex) [LeLevel β] :
     apply mul_le_of_le μ_isStrongLimit.aleph0_le (card_codingFunction β).le
     rw [card_support]
 
+theorem card_tangle_le (β : TypeIndex) [LeLevel β] :
+    #(Tangle β) ≤ #μ :=
+  card_tangle_le_of_card_tSet (card_tSet_le β)
+
 end ConNF

ConNF/Setup/CoherentData.lean

@@ -39,7 +39,7 @@ instance [LeData] : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) :
 
 class PreCoherentData extends LeData where
   allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ
-  singleton {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : TSet γ → TSet β
+  singleton {β γ : Λ} [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) : TSet γ → TSet β
 
 export PreCoherentData (singleton)
 
@@ -92,8 +92,9 @@ class CoherentData extends PreCoherentData where
       (ρs hε)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hδ • t)) :
     ∃ ρ : AllPerm γ, ∀ δ : TypeIndex, [LtLevel δ] → ∀ hδ : δ < γ, ρ ↘ hδ = ρs hδ
   tSet_ext {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : (γ : TypeIndex) < β) (x y : TSet β)
-      (h : ∀ z : TSet γ, z ∈[hγ] x ↔ z ∈[hγ] y) : x = y
-  typedMem_singleton_iff {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (hγ : γ < β) (x y : TSet γ) :
+    (h : ∀ z : TSet γ, z ∈[hγ] x ↔ z ∈[hγ] y) : x = y
+  typedMem_singleton_iff {β γ : Λ} [LeLevel β] [LeLevel γ]
+    (hγ : (γ : TypeIndex) < β) (x y : TSet γ) :
     y ∈[hγ] singleton hγ x ↔ y = x
 
 export CoherentData (allPermSderiv_forget pos_atom_lt_pos pos_nearLitter_lt_pos smul_fuzz

ConNF/Setup/ModelData.lean

@@ -61,24 +61,28 @@ theorem Support.Supports.mono {X : Type _} {α : TypeIndex} [PreModelData α]
 
 class ModelData (α : TypeIndex) extends PreModelData α where
   tSetForget_injective' : Function.Injective tSetForget
+  tSetForget_surjective_of_bot' : α = ⊥ → Function.Surjective tSetForget
   allPermForget_injective' : Function.Injective allPermForget
   allPermForget_one : (1 : AllPerm)ᵁ = 1
   allPermForget_mul (ρ₁ ρ₂ : AllPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ
   smul_forget (ρ : AllPerm) (x : TSet) : (ρ • x)ᵁ = ρᵁ • xᵁ
   exists_support (x : TSet) : ∃ S : Support α, S.Supports x
 
-export ModelData (tSetForget_injective' allPermForget_injective' allPermForget_one allPermForget_mul
-  smul_forget exists_support)
+export ModelData (allPermForget_one allPermForget_mul smul_forget exists_support)
 
 attribute [simp] allPermForget_one allPermForget_mul smul_forget
 
 theorem tSetForget_injective {α : TypeIndex} [ModelData α] {x₁ x₂ : TSet α}
     (h : x₁ᵁ = x₂ᵁ) : x₁ = x₂ :=
-  tSetForget_injective' h
+  ModelData.tSetForget_injective' h
+
+theorem tSetForget_surjective [ModelData ⊥] (x : StrSet ⊥) :
+    ∃ y : TSet ⊥, yᵁ = x :=
+  ModelData.tSetForget_surjective_of_bot' rfl x
 
 theorem allPermForget_injective {α : TypeIndex} [ModelData α] {ρ₁ ρ₂ : AllPerm α}
     (h : ρ₁ᵁ = ρ₂ᵁ) : ρ₁ = ρ₂ :=
-  allPermForget_injective' h
+  ModelData.allPermForget_injective' h
 
 @[simp]
 theorem allPermForget_inv {α : TypeIndex} [ModelData α] (ρ : AllPerm α) : ρ⁻¹ᵁ = ρᵁ⁻¹ := by
@@ -243,6 +247,7 @@ def botPreModelData : PreModelData ⊥ where
 
 def botModelData : ModelData ⊥ where
   tSetForget_injective' := Equiv.injective _
+  tSetForget_surjective_of_bot' _ := Equiv.surjective _
   allPermForget_injective' _ _ h := congr_fun h Path.nil
   allPermForget_one := rfl
   allPermForget_mul _ _ := rfl