refactor(EpistemicScale): rehome pure math, drop aggregator

Linglib.lean

@@ -90,7 +90,9 @@ import Linglib.Core.Order.PreferenceStructure.EffectivePreference
 import Linglib.Core.Order.PreferenceStructure.MaxInducedOrdering
 import Linglib.Core.Order.ComparativeProbability.Defs
 import Linglib.Core.Order.ComparativeProbability.Patterns
+import Linglib.Core.Order.Caratheodory
 import Linglib.Core.Order.FourierMotzkin
+import Linglib.Core.Order.SignVectors
 import Linglib.Core.Logic.RankingFunction
 import Linglib.Core.Logic.SystemZ
 import Linglib.Features.Register
@@ -313,11 +315,9 @@ import Linglib.Core.Scales.Scale
 import Linglib.Core.Scales.EpistemicScale.Defs
 import Linglib.Core.Scales.EpistemicScale.Entailments
 import Linglib.Core.Scales.EpistemicScale.Conditional
-import Linglib.Core.Scales.EpistemicScale
 import Linglib.Core.Scales.EpistemicScale.Cancellation
 import Linglib.Core.Scales.EpistemicScale.CancellationFin4
-import Linglib.Core.Scales.EpistemicScale.Caratheodory
-import Linglib.Core.Scales.EpistemicScale.SignVectors
+import Linglib.Core.Scales.EpistemicScale.Completeness
 import Linglib.Core.Scales.EpistemicScale.Representability
 import Linglib.Core.Mereology
 import Linglib.Core.Mereotopology

Linglib/Core/Scales/EpistemicScale/SignVectors.lean → Linglib/Core/Order/SignVectors.lean

@@ -13,11 +13,11 @@ The finite combinatorial core of the `Fin 4` cancellation theorem.
 
 ## Main declarations
 
-* `Core.Scale.SignVec.posSupport`, `Core.Scale.SignVec.negSupport` — positive and
+* `SignVec.posSupport`, `SignVec.negSupport` — positive and
   negative supports of a `{-1,0,1}`-valued vector on four coordinates (the sign
   values and the arity are deliberately hardcoded: the pigeonhole and `decide`
   steps below are irreducibly `Fin 4`-specific).
-* `Core.Scale.SignVec.exists_antidom_pair` — any family of sign vectors, each with
+* `SignVec.exists_antidom_pair` — any family of sign vectors, each with
   a positive coordinate, balanced by strictly positive weights, of size at most
   `5`, and pairwise *non-generalized-mergeable* (every pair shares a same-sign
   coordinate), contains an **anti-dominating pair**: two members whose positive
@@ -39,7 +39,7 @@ structure: every consumer below `exists_antidom_pair` is private, and the
 theorem has a single external caller.
 -/
 
-namespace Core.Scale.SignVec
+namespace SignVec
 
 open Finset
 
@@ -802,4 +802,4 @@ theorem exists_antidom_pair (S : Finset (Fin 4 → ℚ)) (d : (Fin 4 → ℚ) 
   · exact core_card_ge4 S hsign hposne hnogm d hd hsum (Or.inr hc)
 
 
-end Core.Scale.SignVec
+end SignVec

Linglib/Core/Scales/Defs.lean

@@ -135,6 +135,38 @@ theorem universal {α β : Type*} [LicensingPipeline α] [LicensingPipeline β]
 
 end LicensingPipeline
 
+/-- Binary epistemic classification, parallel to `MereoTag`: finitely additive
+    scales are closed (endpoint standards licensed), qualitative scales open. -/
+inductive EpistemicTag where
+  | finitelyAdditive
+  | qualitative
+  deriving DecidableEq, Repr
+
+instance : LicensingPipeline EpistemicTag where
+  toBoundedness
+    | .finitelyAdditive => .closed
+    | .qualitative => .open_
+
+theorem epistemicFA_licensed :
+    LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive = true := rfl
+
+theorem epistemicQualitative_blocked :
+    LicensingPipeline.isLicensed EpistemicTag.qualitative = false := rfl
+
+theorem five_frameworks_agree
+    (m : MereoTag) (e : EpistemicTag)
+    (h : LicensingPipeline.toBoundedness m = LicensingPipeline.toBoundedness e) :
+    LicensingPipeline.isLicensed m = LicensingPipeline.isLicensed e :=
+  LicensingPipeline.universal m e h
+
+theorem epistemicFA_eq_qua :
+    LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive =
+    LicensingPipeline.isLicensed MereoTag.qua := rfl
+
+theorem epistemicQualitative_eq_cum :
+    LicensingPipeline.isLicensed EpistemicTag.qualitative =
+    LicensingPipeline.isLicensed MereoTag.cum := rfl
+
 -- ════════════════════════════════════════════════════
 -- § 1d. Scale Polarity
 -- ════════════════════════════════════════════════════

Linglib/Core/Scales/EpistemicScale/CancellationFin4.lean

@@ -1,6 +1,6 @@
 import Linglib.Core.Scales.EpistemicScale.Cancellation
-import Linglib.Core.Scales.EpistemicScale.Caratheodory
-import Linglib.Core.Scales.EpistemicScale.SignVectors
+import Linglib.Core.Order.Caratheodory
+import Linglib.Core.Order.SignVectors
 import Mathlib.Data.List.Perm.Basic
 import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.FinCases

Linglib/Core/Scales/EpistemicScale.lean → Linglib/Core/Scales/EpistemicScale/Completeness.lean

@@ -1,21 +1,23 @@
-import Linglib.Core.Scales.EpistemicScale.Defs
-import Linglib.Core.Scales.EpistemicScale.Entailments
 import Linglib.Core.Scales.EpistemicScale.Representability
 import Linglib.Core.Scales.EpistemicScale.CancellationFin4
 
-/-!
-# Epistemic Comparative Likelihood — Main Theorems
+/-! # KPS representation and completeness theorems
 
-[holliday-icard-2013] [halpern-2003] [kraft-pratt-seidenberg-1959] [van-der-hoek-1996]
+The top-level results of [holliday-icard-2013] / [kraft-pratt-seidenberg-1959]:
 
-Re-exports `EpistemicScale.Defs` (axioms, structures, semantics),
-`EpistemicScale.Representability` (KPS counterexample, Fin 0–3 proofs),
-and `EpistemicScale.CancellationFin4` (Fin 4 via Scott cancellation),
-then states the top-level KPS theorems (8a, 8b) and completeness results.
+* `Core.Scale.theorem8a` — for `|W| < 5`, every FA model is representable by a
+  finitely additive probability measure (FA = FP∞ below five worlds).
+* `Core.Scale.theorem8b` — at `|W| = 5`, FA is strictly weaker than FP∞
+  (the KPS counterexample).
+* `Core.Scale.theorem6_completeness`, `theorem2_completeness` — qualitative
+  completeness results ([van-der-hoek-1996]; [halpern-2003] Thm. 7.5.1a).
+* `Core.Scale.axiomA_iff_fa` — Axiom A is equivalent to disjoint-union
+  invariance (finite additivity).
 -/
 
 namespace Core.Scale
 
+
 -- ── Theorem 8 (Kraft, [kraft-pratt-seidenberg-1959]) ───
 
 set_option maxHeartbeats 1600000 in
@@ -259,37 +261,4 @@ theorem axiomA_iff_fa {W : Type*} (ge : Set W → Set W → Prop) :
     rw [hA_eq, hB_eq] at h
     exact h.symm
 
--- ── EpistemicTag + Five Frameworks ──────────────
-
-/-- Binary epistemic classification, parallel to `MereoTag`. -/
-inductive EpistemicTag where
-  | finitelyAdditive
-  | qualitative
-  deriving DecidableEq, Repr
-
-instance : LicensingPipeline EpistemicTag where
-  toBoundedness
-    | .finitelyAdditive => .closed
-    | .qualitative => .open_
-
-theorem epistemicFA_licensed :
-    LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive = true := rfl
-
-theorem epistemicQualitative_blocked :
-    LicensingPipeline.isLicensed EpistemicTag.qualitative = false := rfl
-
-theorem five_frameworks_agree
-    (m : MereoTag) (e : EpistemicTag)
-    (h : LicensingPipeline.toBoundedness m = LicensingPipeline.toBoundedness e) :
-    LicensingPipeline.isLicensed m = LicensingPipeline.isLicensed e :=
-  LicensingPipeline.universal m e h
-
-theorem epistemicFA_eq_qua :
-    LicensingPipeline.isLicensed EpistemicTag.finitelyAdditive =
-    LicensingPipeline.isLicensed MereoTag.qua := rfl
-
-theorem epistemicQualitative_eq_cum :
-    LicensingPipeline.isLicensed EpistemicTag.qualitative =
-    LicensingPipeline.isLicensed MereoTag.cum := rfl
-
 end Core.Scale