From e981f697636b14ff8fedd0ba32f32809d9343327 Mon Sep 17 00:00:00 2001
From: Robert Hawkins <hawkrobe@gmail.com>
Date: Fri, 19 Jun 2026 19:24:06 -0700
Subject: [PATCH] fix(Semantics/Numerals): restore Intensional open, drop
 Degree orphan

---
 Linglib.lean                           |  1 -
 Linglib/Semantics/Numerals/Basic.lean  |  6 ++----
 Linglib/Semantics/Numerals/Degree.lean | 27 --------------------------
 3 files changed, 2 insertions(+), 32 deletions(-)
 delete mode 100644 Linglib/Semantics/Numerals/Degree.lean

diff --git a/Linglib.lean b/Linglib.lean
index 78b3a6dfc..67d01c4c2 100644
--- a/Linglib.lean
+++ b/Linglib.lean
@@ -2272,7 +2272,6 @@ import Linglib.Studies.AhnZhu2025
 import Linglib.Studies.DeganoAloni2025
 import Linglib.Semantics.Measurement.Basic
 import Linglib.Semantics.Numerals.Basic
-import Linglib.Semantics.Numerals.Degree
 import Linglib.Semantics.Numerals.Precision
 import Linglib.Semantics.Definiteness.Basic
 import Linglib.Semantics.Quantification.DomainRestriction
diff --git a/Linglib/Semantics/Numerals/Basic.lean b/Linglib/Semantics/Numerals/Basic.lean
index 55b839708..8d3a14e4c 100644
--- a/Linglib/Semantics/Numerals/Basic.lean
+++ b/Linglib/Semantics/Numerals/Basic.lean
@@ -42,9 +42,7 @@ interval endpoint; see `Core.Order.Comparison.boundary_mem`.
 7. EXH–type-shift duality (Spector §6.2)
 8. GQT bridge (Bylinina & Nouwen)
 
-The `HasMeasure`-based numeral predicates and `CardinalityDegree` instance
-live in `Numerals/Degree.lean`; precision/halo machinery lives in
-`Numerals/Precision.lean`.
+Precision/halo machinery lives in `Numerals/Precision.lean`.
 -/
 
 namespace Semantics.Numerals
@@ -339,7 +337,7 @@ connects B&N's quantifier view (type ⟨⟨e,t⟩,⟨e,t⟩,t⟩) to the Kennedy
 maximality view (type ⟨d,t⟩). -/
 
 section GQTBridge
-open Classical Core.Logic.Intensional Quantification
+open Classical Intensional Quantification
 
 /-- GQT "at least `n`" agrees with `atLeastMeaning` on intersection cardinality. -/
 theorem gqt_atLeast_agrees {α : Type*} [Fintype α]
diff --git a/Linglib/Semantics/Numerals/Degree.lean b/Linglib/Semantics/Numerals/Degree.lean
deleted file mode 100644
index b5a14f994..000000000
--- a/Linglib/Semantics/Numerals/Degree.lean
+++ /dev/null
@@ -1,27 +0,0 @@
-import Linglib.Semantics.Degree.HasMeasure
-
-/-!
-# Numeral Semantics over `HasMeasure`
-
-[kennedy-2007] [schwarzschild-2005]
-
-Generic numeral predicates parameterized by the `Semantics.Degree.HasMeasure`
-typeclass — applicable to any entity type carrying a measure into a totally
-ordered codomain. The `Nat` → ℚ instance for cardinalities lives here so
-this file is self-contained for callers that just want "compare a stated
-numeral against an entity's measured degree".
-
-The `Nat → Nat → Prop` numeral meanings (Kennedy/Horn `bareMeaning`,
-`atLeastMeaning`, …) live in `Basic.lean`; this file is the degree-typed
-counterpart for measurement domains (cost, height, weight, …).
--/
-
-namespace Semantics.Numerals
-
-open Semantics.Degree
-/-- Cardinality (`Nat`) participates in the `HasMeasure`/`HasMeasure` framework
-    via the canonical embedding into ℚ. -/
-instance CardinalityDegree : HasMeasure Nat ℚ where
-  degree := λ n => (n : ℚ)
-
-end Semantics.Numerals