refactor(Semantics/Modality): rename WorldHistory to HistoricalAlternatives at root namespace

Linglib/Semantics/Modality/Exclusion.lean

@@ -59,7 +59,7 @@ namespace Semantics.Modality.Exclusion
 
 open Core.Context (KContext ContextTower ContextShift RichContext
   hpShift xMarkingShift DomainExpanding temporalShift)
-open Semantics.Modality.HistoricalAlternatives (WorldHistory historicalBase)
+open HistoricalAlternatives (historicalBase)
 open Semantics.Mood (subjShift)
 open Semantics.Reference.Kaplan (opActually_access opActually_shift_invariant)
 open Semantics.Tense (upperLimitConstraint)
@@ -394,12 +394,12 @@ theorem domain_expansion_avoids_triviality
 backward time shift → the HP-shifted domain contains the original.
 
 Connects three layers:
-1. `BranchingTime.WorldHistory.backwardsClosed` (semantic property)
+1. `BranchingTime.HistoricalAlternatives.backwardsClosed` (semantic property)
 2. `ConditionalShift.history_monotone_set` (set-level monotonicity)
 3. `hpShift` installs the expanded domain -/
 theorem oMarking_hpShift_expanding
     {W : Type*} {T : Type*} [Preorder T]
-    (history : WorldHistory W T) (h_bc : history.backwardsClosed)
+    (history : HistoricalAlternatives W T) (h_bc : history.backwardsClosed)
     (w₀ : W) (t₀ t' : T) (h_earlier : t' ≤ t₀)
     (D : Set W) (h_domain : D ⊆ history ⟨w₀, t₀⟩) :
     D ⊆ history ⟨w₀, t'⟩ :=

Linglib/Semantics/Modality/Selectional.lean

@@ -64,7 +64,7 @@ set_option autoImplicit false
 namespace Semantics.Modality.Selectional
 
 open _root_.Semantics.Conditionals (SelectionFunction)
-open _root_.Semantics.Modality.HistoricalAlternatives
+open HistoricalAlternatives
 open scoped ENNReal
 
 variable {W : Type*}
@@ -286,15 +286,15 @@ Selectional `will` parameterized by the metaphysical modal base of
     the prejacent at the world selected from the metaphysical modal
     base at ⟨w, t⟩. -/
 def willHistorical {Time : Type*} (s : SelectionFunction W)
-    (history : WorldHistory W Time) (A : W → Prop)
+    (history : HistoricalAlternatives W Time) (A : W → Prop)
     (w : W) (t : Time) : Prop :=
   willSem s A (metaphysicalBase history w t) w
 
 /-- When the world-history relation is reflexive (the standard case
     @cite{condoravdi-2002} §4.1 condition (i)), `willHistorical`
     collapses to its prejacent: `will_t A` at `w` reduces to `A w`. -/
 theorem willHistorical_reflexive_collapse {Time : Type*}
-    (s : SelectionFunction W) {history : WorldHistory W Time}
+    (s : SelectionFunction W) {history : HistoricalAlternatives W Time}
     (hRefl : history.reflexive) (A : W → Prop) (w : W) (t : Time) :
     willHistorical s history A w t ↔ A w := by
   unfold willHistorical

Linglib/Semantics/Modality/TemporalConstraint.lean

@@ -17,7 +17,7 @@ bridges from `Attitude` / `ModalFlavor` to `ModalBaseKind`.
 
 The framework-neutral interval predicates (`isActualHistory`,
 `isFutureHistory`, etc.) and the situation-base derivation theorems live
-in `Semantics.Modality.HistoricalAlternatives`. This file's role is the
+in `HistoricalAlternatives`. This file's role is the
 Klecha-specific projection: dispatch on `ModalBaseKind` to select between
 the actual-history (RT ≤ EvalT) and future-history (RT > EvalT)
 constraints.
@@ -33,18 +33,17 @@ in the modal base pronoun:
 
 The ULC is **derived** by `.2` projection from `actualHistoryBase`
 membership (see `actualHistoryBase_derives_ulc` in
-`Semantics.Modality.HistoricalAlternatives`); the dispatch theorem
+`HistoricalAlternatives`); the dispatch theorem
 `attitudeTemporalConstraint_derived_doxastic` below makes the
 Klecha-namespace face of that derivation kernel-checked.
 -/
 
 namespace Semantics.Modality.TemporalConstraint
 
 open Semantics.Modality (ModalBaseKind)
-open Semantics.Modality.HistoricalAlternatives
+open HistoricalAlternatives
   (isActualHistory isFutureHistory actualHistoryBase futureHistoryBase
-   actualHistoryBase_time_actual futureHistoryBase_time_future
-   WorldHistory)
+   actualHistoryBase_time_actual futureHistoryBase_time_future)
 
 
 /-! ## Temporal Constraints on Embedded RT -/
@@ -127,7 +126,7 @@ DOX, `futureHistoryBase` for CIR), not stipulated.
 This is the formal contrast with @cite{abusch-1997}'s ULC, which is
 stipulated as a presupposition on T-nodes; here, ULC follows by `.2`
 projection through the situation-base definition. The substrate
-derivation lives in `Semantics.Modality.HistoricalAlternatives` as
+derivation lives in `HistoricalAlternatives` as
 `actualHistoryBase_time_actual` / `futureHistoryBase_time_future`;
 these theorems re-express it in the Klecha-namespace
 `attitudeTemporalConstraint` form. -/
@@ -137,7 +136,7 @@ these theorems re-express it in the Klecha-namespace
     constraint (Upper Limit Constraint) by `.2` projection. -/
 theorem attitudeTemporalConstraint_derived_doxastic
     {W Time : Type*} [LinearOrder Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (s s' : Core.WorldTimeIndex W Time)
     (h : s' ∈ actualHistoryBase history s) :
     attitudeTemporalConstraint .doxastic s.time s'.time :=
@@ -148,7 +147,7 @@ theorem attitudeTemporalConstraint_derived_doxastic
     temporal constraint (future orientation) by `.2` projection. -/
 theorem attitudeTemporalConstraint_derived_circumstantial
     {W Time : Type*} [LinearOrder Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (s s' : Core.WorldTimeIndex W Time)
     (h : s' ∈ futureHistoryBase history s) :
     attitudeTemporalConstraint .circumstantial s.time s'.time :=

Linglib/Semantics/Mood/Basic.lean

@@ -45,7 +45,7 @@ namespace Semantics.Mood
 open Core (WorldTimeIndex)
 
 open Core.Time
-open Semantics.Modality.HistoricalAlternatives
+open HistoricalAlternatives
 
 
 /--
@@ -86,7 +86,7 @@ The subjunctive:
 Analogous to an indefinite for situations.
 -/
 def SUBJ {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (P : SitPred W Time)
     (s₀ : WorldTimeIndex W Time) : Prop :=
   ∃ s₁ : WorldTimeIndex W Time,
@@ -220,7 +220,7 @@ This explains why SF enables future reference: the subjunctive
 introduces a future situation that the main clause can refer back to.
 -/
 def conditionalSF {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (antecedent : WorldTimeIndex W Time → Prop)  -- "Maria is home"
     (consequent : WorldTimeIndex W Time → WorldTimeIndex W Time → Prop)  -- "she answers"
     (s₀ : WorldTimeIndex W Time) : Prop :=
@@ -245,7 +245,7 @@ def conditionalIND {W Time : Type*}
 SUBJ is existential: it introduces a situation.
 -/
 theorem subj_is_existential {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (P : SitPred W Time)
     (s₀ : WorldTimeIndex W Time) :
     SUBJ history P s₀ → ∃ s₁, P s₁ s₀ := by
@@ -257,7 +257,7 @@ SUBJ constrains to historical base: the introduced situation
 is in the historical alternatives.
 -/
 theorem subj_in_hist {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (P : SitPred W Time)
     (s₀ : WorldTimeIndex W Time) :
     SUBJ history P s₀ → ∃ s₁, s₁ ∈ historicalBase history s₀ ∧ P s₁ s₀ := by
@@ -279,7 +279,7 @@ SUBJ with reflexive history: if the history is reflexive,
 the current situation is always an option.
 -/
 theorem subj_current_option {W Time : Type*} [Preorder Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (h_refl : history.reflexive)
     (P : SitPred W Time)
     (s₀ : WorldTimeIndex W Time)
@@ -313,7 +313,7 @@ This follows from the existential nature of SUBJ: it quantifies over
 situations in the historical base, which includes non-actual futures.
 -/
 theorem subj_nonveridical {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     -- Need: history has an option distinct from the evaluation point
     (h_branching : ∃ s₀ s₁ : WorldTimeIndex W Time,
       s₁ ∈ historicalBase history s₀ ∧ s₀ ≠ s₁) :
@@ -359,7 +359,7 @@ section AttitudeTemporalAnchor
     perspective time shifts to the matrix event time. Both mechanisms
     create a new temporal reference point for embedded evaluation. -/
 theorem subj_temporal_anchor {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (P : SitPred W Time)
     (s₀ : WorldTimeIndex W Time)
     (h : SUBJ history P s₀) :
@@ -428,7 +428,7 @@ theorem subjShift_preserves_agent {E P : Type*}
 
     This is the bridge between the existential `SUBJ` and the tower `push`. -/
 theorem subj_as_tower_push [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (Q : SitPred W Time)
     (s₀ : WorldTimeIndex W Time) :
     SUBJ history Q s₀ ↔

Linglib/Semantics/Mood/Dynamic.lean

@@ -75,7 +75,7 @@ operator and the modal donkey anaphora chain that consumes
 namespace Semantics.Mood
 
 open _root_.Core (Assignment WorldTimeIndex)
-open Semantics.Modality.HistoricalAlternatives
+open HistoricalAlternatives
 open Semantics.Dynamic.Core
 
 
@@ -102,7 +102,7 @@ every `s₁ ∈ historicalBase history s₀`. The current situation is
 updated to the freshly drawn `s₁`, and `v` is bound to it.
 -/
 def dynSUBJ {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar) : SitContext W Time → SitContext W Time :=
   dynIntroduce (historicalBase history) v
 
@@ -117,7 +117,7 @@ theorem dynIND_eq_dynRelationOn_sameWorld {W Time : Type*}
       dynRelationOn (fun gs => gs.2) (fun gs => gs.1 v) sameWorld c := rfl
 
 theorem dynSUBJ_eq_dynIntroduce_historicalBase {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time) (v : SVar) (c : SitContext W Time) :
+    (history : HistoricalAlternatives W Time) (v : SVar) (c : SitContext W Time) :
     dynSUBJ history v c =
       dynIntroduce (historicalBase history) v c := rfl
 
@@ -153,7 +153,7 @@ theorem dynIND_idempotent {W Time : Type*}
 /-- SUBJ is existential over the historical base. Inherited from
 `dynIntroduce_current_in_gen`. -/
 theorem dynSUBJ_existential {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar)
     (c : SitContext W Time)
     (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time)
@@ -164,7 +164,7 @@ theorem dynSUBJ_existential {W Time : Type*} [LE Time]
 /-- After `dynSUBJ`, looking up `v` always returns the current
 situation. Inherited from `dynIntroduce_binds_current`. -/
 theorem dynSUBJ_binds_current {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar)
     (c : SitContext W Time)
     (gs : Assignment (WorldTimeIndex W Time) × WorldTimeIndex W Time)
@@ -212,7 +212,7 @@ set rather than just an existential iff. The output of `dynSUBJ` on
 `s₁ ∈ historicalBase history s₀`.
 -/
 theorem dynSUBJ_singleton_eq {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar)
     (g : Assignment (WorldTimeIndex W Time))
     (s₀ : WorldTimeIndex W Time) :
@@ -236,7 +236,7 @@ For a singleton context `{(g, s₀)}`, the set of situations reachable via
 `SUBJ` existentially quantifies over.
 -/
 theorem dynSUBJ_realizes_SUBJ {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar)
     (g : Assignment (WorldTimeIndex W Time))
     (s₀ : WorldTimeIndex W Time)
@@ -265,7 +265,7 @@ on `v` is trivially satisfied — `gs.2 = s₁ = gs.1 v` by
 shared variables preserves the full SUBJ output.
 -/
 theorem dynIND_after_dynSUBJ_same_var {W Time : Type*} [LE Time]
-    (history : WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (v : SVar)
     (c : SitContext W Time) :
     dynIND v (dynSUBJ history v c) = dynSUBJ history v c := by

Linglib/Semantics/Tense/Basic.lean

@@ -392,7 +392,7 @@ ULC: embedded R' ≤ matrix E (= embedded P).
 **Note on faithfulness:** the value-level reduction `embeddedR ≤ matrixE`
 strips the modal-alternative quantification Abusch's formulation
 carries (the "now of an epistemic alternative" quantifies over
-doxastic alternatives). A modal-layer formulation (over `WorldHistory
+doxastic alternatives). A modal-layer formulation (over `HistoricalAlternatives
 W Time`, à la @cite{klecha-2016}'s `actualHistoryBase`) would be more
 faithful to the original; deferred future work.
 -/

Linglib/Semantics/Tense/ConditionalShift.lean

@@ -37,7 +37,7 @@ open Core (WorldTimeIndex)
 open Core.Time
 open Core.Context (RichContext KContext ContextTower ContextShift
   hpShift DomainExpanding)
-open Semantics.Modality.HistoricalAlternatives
+open HistoricalAlternatives
 open Semantics.Mood
 
 -- ════════════════════════════════════════════════════════════════
@@ -95,7 +95,7 @@ variable {W : Type*} {T : Type*} [Preorder T]
     O-marking (Non-Past / HP) in Japanese Anderson conditionals expands
     the domain without X-marking. -/
 theorem hp_achieves_expansion
-    (history : WorldHistory W T)
+    (history : HistoricalAlternatives W T)
     (h_bc : history.backwardsClosed)
     (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time)
     (w : W) (hw : w ∈ history s₀) :
@@ -111,7 +111,7 @@ theorem hp_achieves_expansion
     evaluation time backward, and backward time yields more historical
     alternatives, i.e., domain expansion. -/
 theorem history_monotone_set
-    (history : WorldHistory W T)
+    (history : HistoricalAlternatives W T)
     (h_bc : history.backwardsClosed)
     (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time) :
     (history s₀ : Set W) ⊆ (history ⟨s₀.world, t'⟩ : Set W) :=
@@ -121,7 +121,7 @@ theorem history_monotone_set
     situations with the same worlds as the later base, plus potentially more.
     This is the situation-level version of domain expansion. -/
 theorem historicalBase_monotone
-    (history : WorldHistory W T)
+    (history : HistoricalAlternatives W T)
     (h_bc : history.backwardsClosed)
     (s₀ : WorldTimeIndex W T) (t' : T) (h_earlier : t' ≤ s₀.time)
     (s₁ : WorldTimeIndex W T) (h_s₁ : s₁ ∈ historicalBase history s₀)
@@ -252,7 +252,7 @@ variable {W : Type*} {T : Type*} [Preorder T]
     When the history is backwards-closed, SUBJ at an earlier time introduces
     a situation whose world is in the expanded historical alternatives. -/
 theorem subj_subsumes_hp_expansion
-    (history : WorldHistory W T)
+    (history : HistoricalAlternatives W T)
     (P : WorldTimeIndex W T → WorldTimeIndex W T → Prop)
     (s : WorldTimeIndex W T)
     (h : SUBJ history P s) :

Linglib/Semantics/Tense/DeRe.lean

@@ -50,7 +50,7 @@ live in `Studies/Abusch1997.lean`.
   shadow this file connects to (the deleted `TemporalDeRe` triple was a
   shadow of *this* shadow; see the `isFelicitousWith_iff_…` theorem
   below for the bridge).
-- `Semantics.Modality.HistoricalAlternatives.actualHistoryBase` —
+- `HistoricalAlternatives.actualHistoryBase` —
   Klecha 2016 DOX substrate, available as the metaphysical instantiation
   via `metaphysicalAlternatives`.
 
@@ -101,7 +101,7 @@ namespace Semantics.Tense.DeRe
 
 open Core (Intension WorldTimeIndex)
 open Core.Context (KContext)
-open Semantics.Modality.HistoricalAlternatives (WorldHistory actualHistoryBase)
+open HistoricalAlternatives (actualHistoryBase)
 open Core.Time.Tense (TensePronoun GramTense TemporalAssignment)
 
 
@@ -282,9 +282,9 @@ theorem isFelicitousWith_of_isAbuschFelicitous [LinearOrder T]
 /-- **Metaphysical** alternative-set instantiation (@cite{klecha-2016}
     DOX): the worlds sharing the holder's actual world's history up to
     her now, paired with times at-or-before her now. Recovers the
-    legacy `WorldHistory`-based behavior as a special case. -/
+    legacy `HistoricalAlternatives`-based behavior as a special case. -/
 def metaphysicalAlternatives [LE T]
-    (history : WorldHistory W T) (dr : TemporalDeReReading W E P T) :
+    (history : HistoricalAlternatives W T) (dr : TemporalDeReReading W E P T) :
     Set (WorldTimeIndex W T) :=
   actualHistoryBase history dr.holderContext.toSituation
 

Linglib/Studies/Abusch1997.lean

@@ -50,7 +50,7 @@ constructors). See `Tense/DeRe.lean` docstring for what's deferred
    formalized at the value level as `embeddedR ≤ matrixE`. **Note:**
    this value-level reduction strips the modal-alternative
    quantification the original formulation carries; making the modal
-   layer explicit (over `WorldHistory W Time` à la @cite{klecha-2016})
+   layer explicit (over `HistoricalAlternatives W Time` à la @cite{klecha-2016})
    is deferred.
 3. **Temporal de re**: tense variable in the res position of an
    attitude. The value-level shadow uses `TensePronoun.fullPresupposition`:
@@ -296,14 +296,14 @@ theorem abusch_derives_temporal_de_re_full
 
 /-- **Metaphysical-instantiation specialization** of
     `abusch_derives_temporal_de_re_full`. Recovers the legacy
-    `WorldHistory`-based formulation as a corollary at the
+    `HistoricalAlternatives`-based formulation as a corollary at the
     `metaphysicalAlternatives` instance, demonstrating backward
     compatibility with Klecha 2016 DOX-shaped reasoning. -/
 theorem abusch_derives_temporal_de_re_full_metaphysical
     {W E P Time : Type*} [LinearOrder Time]
     (dr : Semantics.Tense.DeRe.TemporalDeReReading W E P Time)
     (hRigid : Core.Intension.IsRigid dr.concept)
-    (history : Semantics.Modality.HistoricalAlternatives.WorldHistory W Time)
+    (history : HistoricalAlternatives W Time)
     (hBefore : dr.actualRes < dr.holderContext.time) :
     dr.isAbuschFelicitous (dr.metaphysicalAlternatives history) .past :=
   abusch_derives_temporal_de_re_full dr hRigid _ hBefore