From 5a2d0cad2e074fb8e2a455208f7634f4956bd9e9 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Wed, 3 Jun 2026 17:37:33 -0700 Subject: [PATCH] refactor(EpistemicScale): rehome pure math, drop aggregator --- Linglib.lean | 6 +-- .../Caratheodory.lean | 0 .../EpistemicScale => Order}/SignVectors.lean | 8 +-- Linglib/Core/Scales/Defs.lean | 32 +++++++++++ .../EpistemicScale/CancellationFin4.lean | 4 +- .../Completeness.lean} | 53 ++++--------------- 6 files changed, 52 insertions(+), 51 deletions(-) rename Linglib/Core/{Scales/EpistemicScale => Order}/Caratheodory.lean (100%) rename Linglib/Core/{Scales/EpistemicScale => Order}/SignVectors.lean (99%) rename Linglib/Core/Scales/{EpistemicScale.lean => EpistemicScale/Completeness.lean} (86%) diff --git a/Linglib.lean b/Linglib.lean index 6841d6cec..e01bc6e50 100644 --- a/Linglib.lean +++ b/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 diff --git a/Linglib/Core/Scales/EpistemicScale/Caratheodory.lean b/Linglib/Core/Order/Caratheodory.lean similarity index 100% rename from Linglib/Core/Scales/EpistemicScale/Caratheodory.lean rename to Linglib/Core/Order/Caratheodory.lean diff --git a/Linglib/Core/Scales/EpistemicScale/SignVectors.lean b/Linglib/Core/Order/SignVectors.lean similarity index 99% rename from Linglib/Core/Scales/EpistemicScale/SignVectors.lean rename to Linglib/Core/Order/SignVectors.lean index 147d287e4..22d4adc4c 100644 --- a/Linglib/Core/Scales/EpistemicScale/SignVectors.lean +++ b/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 diff --git a/Linglib/Core/Scales/Defs.lean b/Linglib/Core/Scales/Defs.lean index 605e355ce..889d014c6 100644 --- a/Linglib/Core/Scales/Defs.lean +++ b/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 -- ════════════════════════════════════════════════════ diff --git a/Linglib/Core/Scales/EpistemicScale/CancellationFin4.lean b/Linglib/Core/Scales/EpistemicScale/CancellationFin4.lean index 05b6a71d6..66b312c12 100644 --- a/Linglib/Core/Scales/EpistemicScale/CancellationFin4.lean +++ b/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 diff --git a/Linglib/Core/Scales/EpistemicScale.lean b/Linglib/Core/Scales/EpistemicScale/Completeness.lean similarity index 86% rename from Linglib/Core/Scales/EpistemicScale.lean rename to Linglib/Core/Scales/EpistemicScale/Completeness.lean index d24e60d06..50f737b85 100644 --- a/Linglib/Core/Scales/EpistemicScale.lean +++ b/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