From 178d264707cb84db57a74a8a577b7c1c9aab5ebd Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 30 Sep 2025 02:04:44 +0900
Subject: [PATCH 1/4] wip

---
 Foundation.lean                               |  1 +
 Foundation/Modal/Hilbert/WithRE/Basic.lean    | 17 ++++++
 Foundation/Modal/Neighborhood/Logic/E.lean    | 19 ++++---
 Foundation/Modal/Neighborhood/Logic/ED.lean   | 23 +++++++-
 Foundation/Modal/Neighborhood/Logic/EM.lean   | 21 +++++++
 Foundation/Modal/Neighborhood/Logic/EMC.lean  | 22 ++++++++
 Foundation/Modal/Neighborhood/Logic/EMC4.lean | 21 +++++++
 Foundation/Modal/Neighborhood/Logic/EMCN.lean | 27 ---------
 .../Modal/Neighborhood/Logic/EMCT4.lean       | 56 +++++++++++++++++++
 Foundation/Modal/Neighborhood/Logic/EMN.lean  | 20 -------
 Foundation/Modal/Neighborhood/Logic/EMT4.lean | 38 +++++++++++++
 Foundation/Modal/Neighborhood/Logic/EN.lean   | 20 -------
 Foundation/Modal/Neighborhood/Logic/END.lean  | 23 --------
 Zoo/modal.typ                                 |  1 +
 14 files changed, 210 insertions(+), 99 deletions(-)
 create mode 100644 Foundation/Modal/Neighborhood/Logic/EMCT4.lean

diff --git a/Foundation.lean b/Foundation.lean
index 6dbb6248a..4060d01c8 100644
--- a/Foundation.lean
+++ b/Foundation.lean
@@ -141,6 +141,7 @@ import Foundation.Modal.Neighborhood.Logic.E4
 import Foundation.Modal.Neighborhood.Logic.EMC4
 import Foundation.Modal.Neighborhood.Logic.EMCN
 import Foundation.Modal.Neighborhood.Logic.EMT4
+import Foundation.Modal.Neighborhood.Logic.EMCT4
 import Foundation.Modal.Neighborhood.Logic.END
 import Foundation.Modal.Neighborhood.Logic.ET4
 import Foundation.Modal.Neighborhood.Logic.Incomparability.ED_EP
diff --git a/Foundation/Modal/Hilbert/WithRE/Basic.lean b/Foundation/Modal/Hilbert/WithRE/Basic.lean
index c31bf9450..569cf326d 100644
--- a/Foundation/Modal/Hilbert/WithRE/Basic.lean
+++ b/Foundation/Modal/Hilbert/WithRE/Basic.lean
@@ -205,6 +205,23 @@ instance : EMCN.axioms.HasN where
 protected abbrev EMCN : Logic ℕ := Hilbert.WithRE EMCN.axioms
 instance : Entailment.EMCN Modal.EMCN where
 
+protected abbrev EMCT4.axioms : Axiom ℕ := {
+  Axioms.M (.atom 0) (.atom 1),
+  Axioms.C (.atom 0) (.atom 1),
+  Axioms.T (.atom 0),
+  Axioms.Four (.atom 0)
+}
+namespace EMCT4
+instance : EMCT4.axioms.HasM where p := 0; q := 1
+instance : EMCT4.axioms.HasC where p := 0; q := 1
+instance : EMCT4.axioms.HasT where p := 0;
+instance : EMCT4.axioms.HasFour where p := 0;
+end EMCT4
+protected abbrev EMCT4 : Logic ℕ := Hilbert.WithRE EMCT4.axioms
+instance : Entailment.EMC Modal.EMCT4 where
+instance : Entailment.E4 Modal.EMCT4 where
+instance : Entailment.ET Modal.EMCT4 where
+
 protected abbrev EK.axioms : Axiom ℕ := {Axioms.K (.atom 0) (.atom 1)}
 instance : EK.axioms.HasK where p := 0; q := 1;
 protected abbrev EK : Logic ℕ := Hilbert.WithRE EK.axioms
diff --git a/Foundation/Modal/Neighborhood/Logic/E.lean b/Foundation/Modal/Neighborhood/Logic/E.lean
index 6db72e107..c4edfcadd 100644
--- a/Foundation/Modal/Neighborhood/Logic/E.lean
+++ b/Foundation/Modal/Neighborhood/Logic/E.lean
@@ -12,8 +12,16 @@ namespace Neighborhood
 
 abbrev FrameClass.E : FrameClass := Set.univ
 
+protected abbrev Frame.simple_whitehole : Frame := ⟨Unit, λ _ => ∅⟩
+
+@[simp]
+lemma Frame.simple_whitehole.not_valid_axiomN : ¬Frame.simple_whitehole ⊧ Axioms.N := by
+  simp [Semantics.Realize, ValidOnFrame, ValidOnModel, Satisfies];
+
 end Neighborhood
 
+
+
 instance : Sound Modal.E FrameClass.E := instSound_of_validates_axioms $ by simp;
 
 instance : Entailment.Consistent Modal.E := consistent_of_sound_frameclass FrameClass.E $ by
@@ -65,15 +73,10 @@ instance : Modal.E ⪱ Modal.EN := by
     constructor;
     . simp;
     . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.E);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 1,
-        𝒩 := λ w => ∅,
-        Val := λ w => Set.univ
-      };
-      use M, 0;
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
       constructor;
       . tauto;
-      . simp! [M, Semantics.Realize, Satisfies];
+      . simp;
 
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/ED.lean b/Foundation/Modal/Neighborhood/Logic/ED.lean
index 28938efbc..474dcc6fe 100644
--- a/Foundation/Modal/Neighborhood/Logic/ED.lean
+++ b/Foundation/Modal/Neighborhood/Logic/ED.lean
@@ -21,9 +21,14 @@ instance : Frame.simple_blackhole.IsSerial := by
 @[reducible] protected alias Frame.IsED := Frame.IsSerial
 protected abbrev FrameClass.ED : FrameClass := { F | F.IsED }
 
+instance : Frame.simple_whitehole.IsED where
+  serial := by simp_all [Frame.simple_whitehole, Frame.box];
+
 end Neighborhood
 
 
+namespace ED
+
 instance : Sound Modal.ED FrameClass.ED := instSound_of_validates_axioms $ by
   simp only [Semantics.RealizeSet.singleton_iff];
   intro F hF;
@@ -35,6 +40,9 @@ instance : Entailment.Consistent Modal.ED := consistent_of_sound_frameclass Fram
   simp only [Set.mem_setOf_eq];
   infer_instance;
 
+end ED
+
+
 instance : Modal.E ⪱ Modal.ED := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
@@ -53,6 +61,19 @@ instance : Modal.E ⪱ Modal.ED := by
         have := @hC.serial {1} 1;
         simp [Frame.box, Frame.dia] at this;
 
-
+instance : Modal.ED ⪱ Modal.END := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.N;
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.ED);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr; infer_instance;
+      . simp;
 
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EM.lean b/Foundation/Modal/Neighborhood/Logic/EM.lean
index 2994bcdf0..2fac53f8f 100644
--- a/Foundation/Modal/Neighborhood/Logic/EM.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EM.lean
@@ -12,8 +12,12 @@ namespace Neighborhood
 @[reducible] protected alias Frame.IsEM := Frame.IsMonotonic
 protected abbrev FrameClass.EM : FrameClass := { F | F.IsEM }
 
+instance : Frame.simple_whitehole.IsEM where
+  mono := by simp_all;
+
 end Neighborhood
 
+namespace EM
 
 instance : Sound Modal.EM FrameClass.EM := instSound_of_validates_axioms $ by
   constructor;
@@ -29,6 +33,23 @@ instance : Complete Modal.EM FrameClass.EM := maximalCanonicalFrame.completeness
   apply Set.mem_setOf_eq.mpr;
   infer_instance;
 
+end EM
+
+instance : Modal.EM ⪱ Modal.EMN := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.N;
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EM);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr; infer_instance;
+      . simp;
+
 instance : Modal.E ⪱ Modal.EM := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMC.lean b/Foundation/Modal/Neighborhood/Logic/EMC.lean
index f6b9a1fe8..f79209285 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMC.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMC.lean
@@ -16,6 +16,9 @@ namespace Neighborhood
 protected class Frame.IsEMC (F) extends Frame.IsMonotonic F, Frame.IsRegular F where
 protected abbrev FrameClass.EMC : FrameClass := { F | F.IsEMC }
 
+instance : Frame.simple_whitehole.IsEMC where
+  regular := by simp_all [Frame.simple_whitehole, Frame.box];
+
 abbrev EK_counterframe_for_M_and_C : Frame := {
   World := Fin 4,
   𝒩 := λ _ => {{0, 1}, {0, 2}}
@@ -66,6 +69,8 @@ lemma EK_counterframe_for_M_and_C.validate_axiomM : ¬EK_counterframe_for_M_and_
 end Neighborhood
 
 
+namespace EMC
+
 instance : Sound Modal.EMC FrameClass.EMC := instSound_of_validates_axioms $ by
   constructor;
   rintro _ (rfl | rfl) F (rfl | rfl) <;> simp;
@@ -79,6 +84,23 @@ instance : Complete Modal.EMC FrameClass.EMC := maximalCanonicalFrame.completene
   apply Set.mem_setOf_eq.mpr;
   constructor;
 
+end EMC
+
+instance : Modal.EMC ⪱ Modal.EMCN := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.N;
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMC);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
+      constructor;
+      . tauto;
+      . simp;
+
 instance : Modal.EC ⪱ Modal.EMC := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMC4.lean b/Foundation/Modal/Neighborhood/Logic/EMC4.lean
index 971734745..28833ed89 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMC4.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMC4.lean
@@ -69,4 +69,25 @@ instance : Modal.EMC ⪱ Modal.EMC4 := by
       . constructor;
       . simp;
 
+instance : Modal.EMC4 ⪱ Modal.EMCT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.T (.atom 0);
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMC4);
+      apply not_validOnFrameClass_of_exists_frame;
+      use ⟨Fin 1, λ _ => Set.univ⟩;
+      constructor;
+      . exact {
+          mono := by simp,
+          regular := by simp [Frame.box],
+          trans := by simp [Frame.box]
+        }
+      . apply not_imp_not.mpr isReflexive_of_valid_axiomT;
+        by_contra! hC;
+        simpa [Frame.box] using @hC.refl ∅;
+
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EMCN.lean b/Foundation/Modal/Neighborhood/Logic/EMCN.lean
index edf7fd547..f9c01eed1 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMCN.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMCN.lean
@@ -30,33 +30,6 @@ instance : Complete Modal.EMCN FrameClass.EMCN := maximalCanonicalFrame.complete
   apply Set.mem_setOf_eq.mpr;
   constructor;
 
-instance : Modal.EMC ⪱ Modal.EMCN := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use Axioms.N;
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMC);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 1,
-        𝒩 := λ w => ∅,
-        Val := λ w => Set.univ
-      };
-      use M, 0;
-      constructor;
-      . exact {
-          mono := by
-            rintro X Y w hw;
-            simp_all [M];
-          regular := by
-            rintro X Y w ⟨hwX, hwY⟩;
-            simp_all [M]
-        }
-      . simp! [M, Semantics.Realize, Satisfies];
-
 instance : Modal.ECN ⪱ Modal.EMCN := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMCT4.lean b/Foundation/Modal/Neighborhood/Logic/EMCT4.lean
new file mode 100644
index 000000000..e8d129989
--- /dev/null
+++ b/Foundation/Modal/Neighborhood/Logic/EMCT4.lean
@@ -0,0 +1,56 @@
+import Foundation.Modal.Neighborhood.Hilbert
+import Foundation.Modal.Neighborhood.Logic.EMC4
+import Foundation.Modal.Neighborhood.Logic.EMT4
+
+namespace LO.Modal
+
+open Neighborhood
+open Hilbert.Neighborhood
+open Formula.Neighborhood
+
+namespace Neighborhood
+
+protected class Frame.IsEMCT4 (F : Frame) extends F.IsMonotonic, F.IsRegular, F.IsReflexive, F.IsTransitive where
+protected abbrev FrameClass.EMCT4 : FrameClass := { F | F.IsEMCT4 }
+
+instance : Frame.simple_blackhole.IsEMCT4 where
+
+instance : Frame.simple_whitehole.IsEMCT4 where
+  refl := by simp_all [Frame.simple_whitehole, Frame.box];
+  trans := by simp_all [Frame.simple_whitehole, Frame.box];
+
+end Neighborhood
+
+
+namespace EMCT4
+
+instance : Sound Modal.EMCT4 FrameClass.EMCT4 := instSound_of_validates_axioms $ by
+  constructor;
+  rintro _ (rfl | rfl | rfl | rfl) F ⟨_, _⟩ <;> simp;
+
+instance : Entailment.Consistent Modal.EMCT4 := consistent_of_sound_frameclass FrameClass.EMCT4 $ by
+  use Frame.simple_blackhole;
+  constructor;
+
+instance : Complete Modal.EMCT4 FrameClass.EMCT4 := maximalCanonicalFrame.completeness $ by
+  apply Set.mem_setOf_eq.mpr;
+  constructor;
+
+end EMCT4
+
+instance : Modal.EMCT4 ⪱ Modal.EMCNT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.N;
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMCT4);
+      apply not_validOnFrameClass_of_exists_frame;
+      use Frame.simple_whitehole;
+      constructor;
+      . tauto;
+      . simp;
+
+end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EMN.lean b/Foundation/Modal/Neighborhood/Logic/EMN.lean
index d6ca6582d..cdeed8202 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMN.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMN.lean
@@ -31,26 +31,6 @@ instance : Complete Modal.EMN FrameClass.EMN := maximalCanonicalFrame.completene
   apply Set.mem_setOf_eq.mpr;
   constructor;
 
-instance : Modal.EM ⪱ Modal.EMN := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use Axioms.N;
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EM);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 1,
-        𝒩 := λ w => ∅,
-        Val := λ w => Set.univ
-      };
-      use M, 0;
-      constructor;
-      . exact { mono := by rintro X Y w hw; simp_all [M] }
-      . simp! [M, Semantics.Realize, Satisfies];
-
 instance : Modal.EN ⪱ Modal.EMN := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMT4.lean b/Foundation/Modal/Neighborhood/Logic/EMT4.lean
index 27551e685..fc3ad3665 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMT4.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMT4.lean
@@ -68,4 +68,42 @@ instance : Modal.EMT ⪱ Modal.EMT4 := by
       . constructor;
       . simp;
 
+instance : Modal.EMT4 ⪱ Modal.EMCT4 := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use Axioms.C (.atom 0) (.atom 1);
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMT4);
+      apply not_validOnFrameClass_of_exists_model_world;
+      use {
+        World := Fin 2,
+        𝒩 := λ w =>
+          match w with
+          | 0 => {{0}, {1}, {0, 1}}
+          | 1 => {{1}, {0, 1}},
+        Val := λ w =>
+          match w with
+          | 0 => {0}
+          | 1 => {1}
+          | _ => Set.univ
+      }, 0;
+      constructor;
+      . exact {
+          mono := by sorry;
+          refl := by
+            simp [Frame.box];
+            rintro X w;
+            match w with
+            | 0 => simp; sorry;
+            | 1 => simp; sorry;
+          trans := by
+
+            sorry;
+        }
+      . simp! [Semantics.Realize, Satisfies];
+        tauto_set;
+
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EN.lean b/Foundation/Modal/Neighborhood/Logic/EN.lean
index 8515355e0..2f4a22ce1 100644
--- a/Foundation/Modal/Neighborhood/Logic/EN.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EN.lean
@@ -35,26 +35,6 @@ instance : Complete Modal.EN FrameClass.EN := minimalCanonicalFrame.completeness
   apply Set.mem_setOf_eq.mpr;
   infer_instance;
 
-instance : Modal.E ⪱ Modal.EN := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use Axioms.N;
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.E);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 1,
-        𝒩 := λ w => ∅,
-        Val := λ w => Set.univ
-      };
-      use M, 0;
-      constructor;
-      . tauto;
-      . simp! [M, Semantics.Realize, Satisfies];
-
 
 
 instance : Modal.N ⪱ Modal.EN := by
diff --git a/Foundation/Modal/Neighborhood/Logic/END.lean b/Foundation/Modal/Neighborhood/Logic/END.lean
index 007343216..3f0bfcb13 100644
--- a/Foundation/Modal/Neighborhood/Logic/END.lean
+++ b/Foundation/Modal/Neighborhood/Logic/END.lean
@@ -26,29 +26,6 @@ instance : Entailment.Consistent Modal.END := consistent_of_sound_frameclass Fra
   simp only [Set.mem_setOf_eq];
   constructor;
 
-instance : Modal.ED ⪱ Modal.END := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use Axioms.N;
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.ED);
-      apply not_validOnFrameClass_of_exists_frame;
-      let F : Frame := {
-        World := Fin 1,
-        𝒩 := λ w => ∅,
-      };
-      use F;
-      constructor;
-      . constructor;
-        intro X x;
-        simp [Frame.box, Frame.dia, F];
-      . apply not_imp_not.mpr containsUnit_of_valid_axiomN;
-        by_contra! hC;
-        simpa [F] using F.univ_mem 0;
-
 instance : Modal.EP ⪱ Modal.END := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_provable_axioms;
diff --git a/Zoo/modal.typ b/Zoo/modal.typ
index dd67b1035..d1f687a9e 100644
--- a/Zoo/modal.typ
+++ b/Zoo/modal.typ
@@ -69,6 +69,7 @@
       "LO.Modal.EMC4": $Logic("EMC4")$,
       "LO.Modal.EMCN": $Logic("EMCN")$,
       "LO.Modal.EMCNT": $Logic("EMCNT")$,
+      "LO.Modal.EMCT4": $Logic("EMCT4")$,
       "LO.Modal.EMCNT4": $Logic("EMCNT4")$,
       "LO.Modal.EMN": $Logic("EMN")$,
       "LO.Modal.Empty": $emptyset$,

From 5f9c101993d88b2ab93778d314cd890edf9dd506 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 30 Sep 2025 08:31:04 +0900
Subject: [PATCH 2/4] wip

---
 Foundation/Modal/Neighborhood/Logic/EM.lean   | 59 +++++++++++++
 Foundation/Modal/Neighborhood/Logic/EMC.lean  | 47 -----------
 Foundation/Modal/Neighborhood/Logic/EMCN.lean | 52 ------------
 Foundation/Modal/Neighborhood/Logic/EMN.lean  | 25 ++++++
 Foundation/Modal/Neighborhood/Logic/EMT4.lean | 83 +++++++++++++------
 5 files changed, 140 insertions(+), 126 deletions(-)

diff --git a/Foundation/Modal/Neighborhood/Logic/EM.lean b/Foundation/Modal/Neighborhood/Logic/EM.lean
index 2fac53f8f..49c1c5c1e 100644
--- a/Foundation/Modal/Neighborhood/Logic/EM.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EM.lean
@@ -1,5 +1,6 @@
 import Foundation.Modal.Neighborhood.Logic.E
 import Foundation.Modal.Neighborhood.Supplementation
+import Foundation.Vorspiel.Set.Fin
 
 namespace LO.Modal
 
@@ -15,8 +16,50 @@ protected abbrev FrameClass.EM : FrameClass := { F | F.IsEM }
 instance : Frame.simple_whitehole.IsEM where
   mono := by simp_all;
 
+abbrev counterframe_axiomC₁ : Frame := {
+  World := Fin 2,
+  𝒩 := λ w =>
+    match w with
+    | 0 => {{0}, {1}, {0, 1}}
+    | 1 => {{1}, {0, 1}}
+}
+
+instance : counterframe_axiomC₁.IsEM where
+  mono := by
+    rintro X Y w hw;
+    constructor;
+    . match w with
+      | 0 | 1 =>
+        rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl;
+        case inr.inl =>
+          rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl <;>
+          . simp [counterframe_axiomC₁] at hw;
+            tauto_set;
+        all_goals simp_all [counterframe_axiomC₁];
+    . match w with
+      | 0 | 1 =>
+        rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl;
+        case inr.inl =>
+          rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl <;>
+          . simp [counterframe_axiomC₁] at hw;
+            tauto_set;
+        all_goals simp_all [counterframe_axiomC₁];
+
+@[simp]
+lemma counterframe_axiomC₁.not_validate_axiomC : ¬counterframe_axiomC₁ ⊧ Axioms.C (.atom 0) (.atom 1) := by
+  apply ValidOnFrame.not_of_exists_valuation_world;
+  use (λ a =>
+    match a with
+    | 0 => {0}
+    | 1 => {1}
+    | _ => ∅
+  ), 0;
+  simp [Satisfies];
+  tauto_set;
+
 end Neighborhood
 
+
 namespace EM
 
 instance : Sound Modal.EM FrameClass.EM := instSound_of_validates_axioms $ by
@@ -50,6 +93,22 @@ instance : Modal.EM ⪱ Modal.EMN := by
       . apply Set.mem_setOf_eq.mpr; infer_instance;
       . simp;
 
+instance : Modal.EM ⪱ Modal.EMC := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use (Axioms.C (.atom 0) (.atom 1));
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EM);
+      apply not_validOnFrameClass_of_exists_frame;
+      use counterframe_axiomC₁;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr;
+        infer_instance;
+      . simp;
+
 instance : Modal.E ⪱ Modal.EM := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMC.lean b/Foundation/Modal/Neighborhood/Logic/EMC.lean
index f79209285..b5cb2ff1c 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMC.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMC.lean
@@ -145,53 +145,6 @@ instance : Modal.EC ⪱ Modal.EMC := by
         simp!;
         omega;
 
-instance : Modal.EM ⪱ Modal.EMC := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use (Axioms.C (.atom 0) (.atom 1));
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EM);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 2,
-        𝒩 := λ w =>
-          match w with
-          | 0 => {{0}, {1}, {0, 1}}
-          | 1 => {{1}, {0, 1}},
-        Val := λ w =>
-          match w with
-          | 0 => {0}
-          | 1 => {1}
-          | _ => Set.univ
-      };
-      use M, 0;
-      constructor;
-      . exact {
-          -- TODO: need golf!
-          mono := by
-            rintro X Y w hw;
-            constructor;
-            . match w with
-              | 0 | 1 =>
-                rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl;
-                case inr.inl =>
-                  rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl <;>
-                  . simp [M] at hw; tauto_set;
-                all_goals simp_all [M];
-            . match w with
-              | 0 | 1 =>
-                rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl;
-                case inr.inl =>
-                  rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl <;>
-                  . simp [M] at hw; tauto_set;
-                all_goals simp_all [M];
-        }
-      . simp! [M, Semantics.Realize, Satisfies];
-        tauto_set;
-
 instance : Modal.EK ⪱ Modal.EMC := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_provable_axioms;
diff --git a/Foundation/Modal/Neighborhood/Logic/EMCN.lean b/Foundation/Modal/Neighborhood/Logic/EMCN.lean
index f9c01eed1..2c348634b 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMCN.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMCN.lean
@@ -65,57 +65,5 @@ instance : Modal.ECN ⪱ Modal.EMCN := by
       . simp! [M, Semantics.Realize, Satisfies];
         tauto_set;
 
-instance : Modal.EMN ⪱ Modal.EMCN := by
-  constructor;
-  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
-    simp;
-  . apply Entailment.not_weakerThan_iff.mpr;
-    use (Axioms.C (.atom 0) (.atom 1));
-    constructor;
-    . simp;
-    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMN);
-      apply not_validOnFrameClass_of_exists_model_world;
-      let M : Model := {
-        World := Fin 2,
-        𝒩 := λ w =>
-          match w with
-          | 0 => {{0}, {1}, {0, 1}}
-          | 1 => {{0}, {0, 1}},
-        Val := λ w =>
-          match w with
-          | 0 => {0}
-          | 1 => {1}
-          | _ => Set.univ
-      };
-      use M, 0;
-      constructor;
-      . exact {
-          mono := by
-            rintro X Y e he;
-            constructor;
-            . match e with
-              | 0 => rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl <;> simp_all [M];
-              | 1 =>
-                rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl;
-                case inr.inr.inl =>
-                  rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl <;>
-                  . simp [M] at he; tauto_set;
-                all_goals simp_all [M];
-            . match e with
-              | 0 => rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl <;> simp_all [M];
-              | 1 =>
-                rcases Set.Fin2.all_cases Y with rfl | rfl | rfl | rfl;
-                case inr.inr.inl =>
-                  rcases Set.Fin2.all_cases X with rfl | rfl | rfl | rfl <;>
-                  . simp [M] at he; tauto_set;
-                all_goals simp_all [M];
-          contains_unit := by
-            ext e;
-            match e with | 0 | 1 => simp_all [M, Set.Fin2.eq_univ];
-        }
-      . simp! [M, Semantics.Realize, Satisfies];
-        tauto_set;
-
-
 
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EMN.lean b/Foundation/Modal/Neighborhood/Logic/EMN.lean
index cdeed8202..a7d5616da 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMN.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMN.lean
@@ -15,9 +15,16 @@ namespace Neighborhood
 protected class Frame.IsEMN (F : Frame) extends F.IsMonotonic, F.ContainsUnit where
 protected abbrev FrameClass.EMN : FrameClass := { F | F.IsEMN }
 
+instance : counterframe_axiomC₁.IsEMN where
+  contains_unit := by
+    ext e;
+    match e with | 0 | 1 => simp_all [counterframe_axiomC₁, Set.Fin2.eq_univ];
+
 end Neighborhood
 
 
+namespace EMN
+
 instance : Sound Modal.EMN FrameClass.EMN := instSound_of_validates_axioms $ by
   constructor;
   rintro _ (rfl | rfl) F (rfl | rfl | rfl) <;> simp;
@@ -31,6 +38,8 @@ instance : Complete Modal.EMN FrameClass.EMN := maximalCanonicalFrame.completene
   apply Set.mem_setOf_eq.mpr;
   constructor;
 
+end EMN
+
 instance : Modal.EN ⪱ Modal.EMN := by
   constructor;
   . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
@@ -62,4 +71,20 @@ instance : Modal.EN ⪱ Modal.EMN := by
         }
       . simp! [M, Semantics.Realize, Satisfies];
 
+instance : Modal.EMN ⪱ Modal.EMCN := by
+  constructor;
+  . apply Hilbert.WithRE.weakerThan_of_subset_axioms;
+    simp;
+  . apply Entailment.not_weakerThan_iff.mpr;
+    use (Axioms.C (.atom 0) (.atom 1));
+    constructor;
+    . simp;
+    . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMN);
+      apply not_validOnFrameClass_of_exists_frame;
+      use counterframe_axiomC₁;
+      constructor;
+      . apply Set.mem_setOf_eq.mpr;
+        infer_instance;
+      . simp;
+
 end LO.Modal
diff --git a/Foundation/Modal/Neighborhood/Logic/EMT4.lean b/Foundation/Modal/Neighborhood/Logic/EMT4.lean
index fc3ad3665..8389c40fa 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMT4.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMT4.lean
@@ -7,6 +7,7 @@ open Neighborhood
 open Hilbert.Neighborhood
 open Formula.Neighborhood
 
+
 namespace Neighborhood
 
 protected class Frame.IsEMT4 (F : Frame) extends F.IsMonotonic, F.IsReflexive, F.IsTransitive where
@@ -15,6 +16,56 @@ protected abbrev FrameClass.EMT4 : FrameClass := { F | F.IsEMT4 }
 protected class Frame.IsFiniteEMT4 (F : Frame) extends F.IsEMT4, F.IsFinite
 protected abbrev FrameClass.finite_EMT4 : FrameClass := { F | F.IsFiniteEMT4 }
 
+abbrev counterframe_axiomC₂ : Frame := {
+  World := Fin 2,
+  𝒩 := λ w =>
+    match w with
+    | 0 => {{0}, {1}, {0, 1}}
+    | 1 => {{1}, {0, 1}}
+}
+
+instance : counterframe_axiomC₂.IsEMT4 where
+  mono := by sorry;
+  refl := by sorry;
+  trans := by sorry;
+
+@[simp]
+lemma counterframe_axiomC₂.not_validate_axiomC : ¬counterframe_axiomC₂ ⊧ Axioms.C (.atom 0) (.atom 1) := by
+  apply ValidOnFrame.not_of_exists_valuation_world;
+  use (λ a =>
+    match a with
+    | 0 => {0}
+    | 1 => {1}
+    | _ => ∅
+  ), 0;
+  simp [Satisfies];
+  tauto_set;
+
+/- actual EM4, not EMT4
+instance : counterframe_axiomC₁.IsEMT4 where
+  refl := by sorry;
+  trans := by
+    intro X w;
+    match w with
+    | 0 =>
+      rintro (rfl | rfl | rfl);
+      . left;
+        ext a;
+        match a with | 0 => simp | 1 => simp; tauto_set;
+      . right; right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+      . simp [Frame.box]
+        right; right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+    | 1 =>
+      rintro (rfl | rfl) <;>
+      . right;
+        ext a;
+        match a with | 0 => simp | 1 => simp;
+-/
+
 end Neighborhood
 
 
@@ -77,33 +128,11 @@ instance : Modal.EMT4 ⪱ Modal.EMCT4 := by
     constructor;
     . simp;
     . apply Sound.not_provable_of_countermodel (𝓜 := FrameClass.EMT4);
-      apply not_validOnFrameClass_of_exists_model_world;
-      use {
-        World := Fin 2,
-        𝒩 := λ w =>
-          match w with
-          | 0 => {{0}, {1}, {0, 1}}
-          | 1 => {{1}, {0, 1}},
-        Val := λ w =>
-          match w with
-          | 0 => {0}
-          | 1 => {1}
-          | _ => Set.univ
-      }, 0;
+      apply not_validOnFrameClass_of_exists_frame;
+      use counterframe_axiomC₂;
       constructor;
-      . exact {
-          mono := by sorry;
-          refl := by
-            simp [Frame.box];
-            rintro X w;
-            match w with
-            | 0 => simp; sorry;
-            | 1 => simp; sorry;
-          trans := by
-
-            sorry;
-        }
-      . simp! [Semantics.Realize, Satisfies];
-        tauto_set;
+      . apply Set.mem_setOf_eq.mpr;
+        infer_instance;
+      . simp;
 
 end LO.Modal

From 870f3e3784a212406a356fac201553682cb3f244 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Thu, 2 Oct 2025 16:13:53 +0900
Subject: [PATCH 3/4] refactor

---
 Foundation/Modal/Neighborhood/AxiomC.lean   |  6 ++++++
 Foundation/Modal/Neighborhood/Logic/EM.lean | 12 ++++--------
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/Foundation/Modal/Neighborhood/AxiomC.lean b/Foundation/Modal/Neighborhood/AxiomC.lean
index 8a52a0098..02b80b8ca 100644
--- a/Foundation/Modal/Neighborhood/AxiomC.lean
+++ b/Foundation/Modal/Neighborhood/AxiomC.lean
@@ -47,6 +47,12 @@ lemma valid_axiomC_of_isRegular [F.IsRegular] : F ⊧ Axioms.C (.atom 0) (.atom
   . apply h₁;
   . apply h₂;
 
+lemma isRegular_of_valid_axiomC (h : F ⊧ Axioms.C (.atom 0) (.atom 1)) : F.IsRegular := by
+  constructor;
+  rintro X Y w ⟨hwX, hwY⟩;
+  have := @h (λ a => match a with | 0 => X | 1 => Y | _ => ∅) w;
+  simp [Satisfies] at this;
+  grind;
 
 section
 
diff --git a/Foundation/Modal/Neighborhood/Logic/EM.lean b/Foundation/Modal/Neighborhood/Logic/EM.lean
index 49c1c5c1e..4619e9b42 100644
--- a/Foundation/Modal/Neighborhood/Logic/EM.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EM.lean
@@ -1,5 +1,6 @@
 import Foundation.Modal.Neighborhood.Logic.E
 import Foundation.Modal.Neighborhood.Supplementation
+import Foundation.Modal.Neighborhood.AxiomC
 import Foundation.Vorspiel.Set.Fin
 
 namespace LO.Modal
@@ -47,14 +48,9 @@ instance : counterframe_axiomC₁.IsEM where
 
 @[simp]
 lemma counterframe_axiomC₁.not_validate_axiomC : ¬counterframe_axiomC₁ ⊧ Axioms.C (.atom 0) (.atom 1) := by
-  apply ValidOnFrame.not_of_exists_valuation_world;
-  use (λ a =>
-    match a with
-    | 0 => {0}
-    | 1 => {1}
-    | _ => ∅
-  ), 0;
-  simp [Satisfies];
+  apply not_imp_not.mpr $ @isRegular_of_valid_axiomC (F := counterframe_axiomC₁);
+  by_contra hC;
+  have : ({0} : Set counterframe_axiomC₁) ∩ {1} = {0, 1} := by simpa using @hC.regular {0} {1} 0;
   tauto_set;
 
 end Neighborhood

From 63310c56f907bc75634bbf7ca22bf51ca565b4d7 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 8 Oct 2025 02:39:22 +0900
Subject: [PATCH 4/4] fix

---
 Foundation/Modal/Neighborhood/Logic/EMCT4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Foundation/Modal/Neighborhood/Logic/EMCT4.lean b/Foundation/Modal/Neighborhood/Logic/EMCT4.lean
index e8d129989..27496eb45 100644
--- a/Foundation/Modal/Neighborhood/Logic/EMCT4.lean
+++ b/Foundation/Modal/Neighborhood/Logic/EMCT4.lean
@@ -32,7 +32,7 @@ instance : Entailment.Consistent Modal.EMCT4 := consistent_of_sound_frameclass F
   use Frame.simple_blackhole;
   constructor;
 
-instance : Complete Modal.EMCT4 FrameClass.EMCT4 := maximalCanonicalFrame.completeness $ by
+instance : Complete Modal.EMCT4 FrameClass.EMCT4 := (supplementedMinimalCanonicity _).completeness $ by
   apply Set.mem_setOf_eq.mpr;
   constructor;