refactor(Discourse/CommonGround): rename CG to root-level CommonGround

Linglib/Dialogue/Brandom.lean

@@ -37,7 +37,7 @@ inferential role.
 namespace Dialogue.Brandom
 
 open Discourse.Commitment (CommitmentSlate)
-open Discourse.CommonGround (ContextSet CG)
+open CommonGround (ContextSet)
 
 -- ════════════════════════════════════════════════════
 -- § 1. Normative Status
@@ -220,7 +220,7 @@ theorem scorekeepers_can_disagree :
 -- § 7. HasContextSet instance
 -- ════════════════════════════════════════════════════
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- Brandom states project to a context set via `effectiveContextSet`
     (the lossy Brandom → Stalnaker projection: intersection of all
     self-attributed commitments). The lossy projection is the price of

Linglib/Dialogue/CommitmentSpace.lean

@@ -10,7 +10,7 @@ import Linglib.Discourse.SpeechAct.Update
 @cite{krifka-2015} @cite{cohen-krifka-2014}
 
 Krifka's commitment-space framework: the discourse state is a tree — the
-root (√C) is the current CG holding speaker-indexed commitments `S⊢φ`,
+root (√C) is the current CommonGround holding speaker-indexed commitments `S⊢φ`,
 and continuations are proposed future states from questions.
 
 - Assertion narrows every state with `commit speaker φ`.
@@ -27,11 +27,11 @@ the commitment/belief separation (lying, hedging).
 ## Speaker indexing
 
 The paper's central primitive is the Frege turnstile `S⊢φ` (p. 332):
-assertion is responsibility-undertaking, so what enters the CG is
+assertion is responsibility-undertaking, so what enters the CommonGround is
 "speaker S is committed to the truth of φ", not bare φ. The substrate uses
 `Discourse.Commitment.IndexedCommitment` to model this — the root
 holds indexed commitments, projected to a flat context set via
-`IndexedCommitment.toCommitment` for the CG-as-set view.
+`IndexedCommitment.toCommitment` for the CommonGround-as-set view.
 
 ## Sibling files
 
@@ -54,7 +54,7 @@ Out of scope (would need substrate extensions):
 - **Time-indexed commitments** (Lauer 2013 PB/PEP carry a `t` index): the
   substrate has no time index; `rejectFirst` is the closest proxy for
   rescission. True time-indexed commitment dynamics need a separate layer.
-- **Anderson 2021 distributional CG**: requires `weight_nonneg` on the
+- **Anderson 2021 distributional CommonGround**: requires `weight_nonneg` on the
   per-world weight. Hosting Anderson via `CommitmentSpace W ℝ` would need
   an `[OrderedAddCommMonoid G]` constraint or an Anderson wrapper —
   current substrate does not enforce non-negativity.
@@ -75,7 +75,7 @@ open Discourse.Commitment
   (CommitmentSlate IndexedCommitment IndexedWeightedCommitment CommitmentForce
    HasSupport CommitmentGrade)
 open Discourse (DiscourseRole)
-open Discourse.CommonGround (ContextSet)
+open CommonGround (ContextSet)
 open Semantics.Mood (IllocutionaryMood)
 
 -- ════════════════════════════════════════════════════
@@ -125,10 +125,10 @@ abbrev KAgent := DiscourseRole
     - Reject: prune a continuation (= return to `{√C}` disjunct).
 
     The tree structure captures the assertion/question asymmetry:
-    assertions modify the root (the CG changes), while questions only
-    add continuations (the CG is preserved until acceptance). -/
+    assertions modify the root (the CommonGround changes), while questions only
+    add continuations (the CommonGround is preserved until acceptance). -/
 structure CommitmentSpace (W : Type*) (G : Type*) where
-  /-- Root commitment state √C: indexed commitments currently in the CG.
+  /-- Root commitment state √C: indexed commitments currently in the CommonGround.
       The grade type `G` lets the same shape host binary (G = Prop),
       distributional (G = ℝ), or credence-bounded (G = ℚ) commitments. -/
   root : List (IndexedWeightedCommitment W G)
@@ -165,7 +165,7 @@ def assert (cs : CommitmentSpace W G) (committer : DiscourseRole)
 
     `C + ?φ = {√C} ∪ (C + S₂⊢φ)`
 
-    The root stays unchanged (CG preserved). A new continuation is added
+    The root stays unchanged (CommonGround preserved). A new continuation is added
     where the addressee has committed to `weight`. Existing continuations
     are also extended by the addressee-commitment. The committer is
     hardcoded to `.addressee` per Krifka's discussion of (30), p. 337:
@@ -213,13 +213,13 @@ instance : DecidablePred (@hasNoOpenContinuations W G) := fun cs => by
     cases conts <;> (unfold hasNoOpenContinuations; infer_instance)
 
 /-- Accept the first continuation: it becomes the new root.
-    The CG is updated to the accepted proposal's content. -/
+    The CommonGround is updated to the accepted proposal's content. -/
 def acceptFirst : CommitmentSpace W G → CommitmentSpace W G
   | ⟨_, c :: rest⟩ => ⟨c, rest⟩
   | cs => cs
 
 /-- Reject the first continuation: prune it.
-    The CG is unchanged; the proposal is discarded. -/
+    The CommonGround is unchanged; the proposal is discarded. -/
 def rejectFirst : CommitmentSpace W G → CommitmentSpace W G
   | ⟨r, _ :: rest⟩ => ⟨r, rest⟩
   | cs => cs
@@ -249,7 +249,7 @@ def denegate (actMarker : IndexedWeightedCommitment W G → Prop)
     continuations := cs.continuations.filter
       (fun cont => decide (¬ ∃ ic ∈ cont, actMarker ic)) }
 
-/-- Denegation preserves the root (CG unchanged) — Krifka 2015 p. 330:
+/-- Denegation preserves the root (CommonGround unchanged) — Krifka 2015 p. 330:
     "denegation does not change the root of the commitment space, but
     prunes its legal developments." -/
 @[simp]
@@ -449,13 +449,13 @@ theorem assert_in_root (cs : CommitmentSpace W Prop) (s : DiscourseRole)
     IndexedCommitment.commit s φ ∈ (cs.assert s φ).root := by
   simp only [assert, IndexedCommitment.commit, List.mem_cons, true_or]
 
-/-- Monopolar question preserves the root (CG unchanged). -/
+/-- Monopolar question preserves the root (CommonGround unchanged). -/
 @[simp]
 theorem monopolarQuestion_preserves_root (cs : CommitmentSpace W G)
     (weight : W → G) :
     (cs.monopolarQuestion weight).root = cs.root := rfl
 
-/-- Bipolar question preserves the root (CG unchanged). -/
+/-- Bipolar question preserves the root (CommonGround unchanged). -/
 @[simp]
 theorem bipolarQuestion_preserves_root [CommitmentGrade G]
     (cs : CommitmentSpace W G) (φ : W → G) :
@@ -467,15 +467,15 @@ end CommitmentSpace
     commitment space (tree).
 
     The commitment space tracks the shared discourse structure: what's in
-    the CG (root) and what's been proposed (continuations). Per-agent
+    the CommonGround (root) and what's been proposed (continuations). Per-agent
     slates track individual public commitments, enabling the
     commitment/belief separation central to Krifka's theory. -/
 structure KrifkaState (W : Type*) where
   /-- Speaker's individual commitment slate (binary, propositional). -/
   speakerCS : CommitmentSlate W
   /-- Addressee's individual commitment slate. -/
   addresseeCS : CommitmentSlate W
-  /-- Shared commitment space (tree): CG + proposed updates.
+  /-- Shared commitment space (tree): CommonGround + proposed updates.
       Binary specialisation `CommitmentSpace W Prop` of the polymorphic
       `CommitmentSpace W G`. Future graded-state extensions
       (Lauer-credence, Anderson-distributional) belong in a separate
@@ -528,15 +528,15 @@ def negatedQuestionLow (s : KrifkaState W) (φ : W → Prop) : KrifkaState W :=
 def negatedQuestionHigh (s : KrifkaState W) (φ : W → Prop) : KrifkaState W :=
   { s with space := s.space.negatedQuestionHigh φ }
 
-/-- Accept the first continuation: it becomes the new CG root. -/
+/-- Accept the first continuation: it becomes the new CommonGround root. -/
 def acceptContinuation (s : KrifkaState W) : KrifkaState W :=
   { s with space := s.space.acceptFirst }
 
 /-- Reject the first continuation: prune it. -/
 def rejectContinuation (s : KrifkaState W) : KrifkaState W :=
   { s with space := s.space.rejectFirst }
 
-/-- Context set: from the commitment space root (= CG), via
+/-- Context set: from the commitment space root (= CommonGround), via
     `IndexedCommitment.toCommitment` projection. -/
 def contextSet (s : KrifkaState W) : ContextSet W :=
   s.space.toContextSet
@@ -566,12 +566,12 @@ theorem commitment_closure {W : Type*} (s : KrifkaState W) (p : W → Prop)
       IndexedCommitment.commit committer p :: s.space.root := by
   cases committer <;> rfl
 
-/-- Questions don't change the CG: the root is preserved. -/
+/-- Questions don't change the CommonGround: the root is preserved. -/
 theorem monopolarQuestion_preserves_cg {W : Type*} (s : KrifkaState W) (p : W → Prop) :
     (s.monopolarQuestion p).space.root = s.space.root := rfl
 
 /-- Question then accept ≈ assert (on the root): accepting a monopolar
-    question's sole continuation yields the same CG as the addressee
+    question's sole continuation yields the same CommonGround as the addressee
     directly asserting φ.
 
     This connects the two modes of updating: direct assertion (committer
@@ -756,22 +756,22 @@ end KrifkaState
 -- § 5. HasContextSet Instances
 -- ════════════════════════════════════════════════════
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- A polymorphic commitment space projects to a context set via its root,
     using the `[HasSupport G]` typeclass's `support` projection. Recovers
     the binary case at `G = Prop` definitionally (via `support := id` in
-    the `Prop` instance). Anderson 2021's distributional CG (`G = ℝ`)
+    the `Prop` instance). Anderson 2021's distributional CommonGround (`G = ℝ`)
     becomes a consumer via `HasSupport ℝ` provided in `Anderson2021.lean`. -/
 instance {W G : Type*} [HasSupport G] :
     HasContextSet (CommitmentSpace W G) W where
   toContextSet := CommitmentSpace.toContextSet
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- A Krifka state projects to a context set via the commitment space root. -/
 instance {W : Type*} : HasContextSet (KrifkaState W) W where
   toContextSet := KrifkaState.contextSet
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- KrifkaState context set agrees with CommitmentSpace context set. -/
 theorem krifkaState_contextSet_eq_space {W : Type*} (s : KrifkaState W) :
     HasContextSet.toContextSet s = HasContextSet.toContextSet s.space := rfl

Linglib/Dialogue/CredenceThreshold.lean

@@ -41,15 +41,15 @@ substrate-supported elsewhere:
   maps to the rationality parameter
 
 Closest to Stalnaker in structure (no explicit commitment/belief
-separation), but adds a probabilistic dimension that the bare CG
+separation), but adds a probabilistic dimension that the bare CommonGround
 model lacks.
 
 -/
 
 namespace Dialogue.CredenceThreshold
 
 open Discourse.Commitment (CommitmentSlate)
-open Discourse.CommonGround (ContextSet)
+open CommonGround (ContextSet)
 
 -- ════════════════════════════════════════════════════
 -- § 1. Credence Functions
@@ -166,7 +166,7 @@ theorem always_stable {W : Type*} (s : State W) :
 -- HasContextSet instance
 -- ════════════════════════════════════════════════════
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- Credence-threshold states project to a context set via the
     asserted-list intersection (`contextSet`). The credence + threshold
     machinery gates *which* assertions can occur; once asserted, the

Linglib/Dialogue/DisjunctiveUpdate.lean

@@ -58,7 +58,7 @@ sequential update = single conjunctive update — apply directly.
 
 namespace Dialogue.DisjunctiveUpdate
 
-open Discourse.CommonGround (ContextSet)
+open CommonGround (ContextSet)
 open Semantics.Dynamic.ParameterizedUpdate
 
 

Linglib/Dialogue/DistributionalCG.lean

@@ -11,7 +11,7 @@ import Linglib.Dialogue.CommitmentSpace
 
 A non-negative real-valued weight function over worlds, refining
 @cite{stalnaker-2002}'s sharp set-membership context set with graded
-plausibility. The probabilistic counterpart of `Discourse.CommonGround.CG W`.
+plausibility. The probabilistic counterpart of `CommonGround W`.
 
 ## Substrate role
 
@@ -43,7 +43,7 @@ frameworks.
 
 namespace Dialogue
 
-open Discourse.CommonGround (ContextSet HasContextSet)
+open CommonGround (ContextSet HasContextSet)
 open Discourse (DiscourseRole)
 open Discourse.Commitment (HasSupport IndexedWeightedCommitment CommitmentForce)
 
@@ -54,7 +54,7 @@ open Discourse.Commitment (HasSupport IndexedWeightedCommitment CommitmentForce)
 /-- A distributional common ground: a non-negative weight function
     over worlds (@cite{anderson-2021}). The probabilistic
     counterpart of @cite{stalnaker-2002}'s context set — instead of
-    a sharp membership predicate (`W → Prop`), the CG assigns graded
+    a sharp membership predicate (`W → Prop`), the CommonGround assigns graded
     plausibility (`W → ℝ`). -/
 structure DistributionalCG (W : Type*) where
   weight : W → ℝ
@@ -64,7 +64,7 @@ namespace DistributionalCG
 
 variable {W : Type*}
 
-/-- Uniform distributional CG: all worlds equally plausible (empty CG). -/
+/-- Uniform distributional CommonGround: all worlds equally plausible (empty CommonGround). -/
 noncomputable def uniform : DistributionalCG W where
   weight _ := 1
   weight_nonneg _ := le_of_lt one_pos
@@ -75,7 +75,7 @@ noncomputable def uniform : DistributionalCG W where
 def toContextSet (cg : DistributionalCG W) : ContextSet W :=
   λ w => 0 < cg.weight w
 
-/-- Uniform distributional CG maps to the trivial context set. -/
+/-- Uniform distributional CommonGround maps to the trivial context set. -/
 theorem uniform_toContextSet :
     (uniform : DistributionalCG W).toContextSet = ContextSet.trivial := by
   funext w
@@ -91,7 +91,7 @@ theorem zero_weight_excluded (cg : DistributionalCG W) (w : W)
 
 end DistributionalCG
 
-/-- A distributional CG projects to a context set: worlds with
+/-- A distributional CommonGround projects to a context set: worlds with
     positive weight. -/
 instance {W : Type*} : HasContextSet (DistributionalCG W) W where
   toContextSet := DistributionalCG.toContextSet
@@ -102,7 +102,7 @@ instance {W : Type*} : HasContextSet (DistributionalCG W) W where
 
 /-- `[HasSupport ℝ]` instance for distributional CGs.
     `support g := 0 < g` matches Anderson's "world has positive weight
-    iff in CG" projection (cf. `DistributionalCG.toContextSet`).
+    iff in CommonGround" projection (cf. `DistributionalCG.toContextSet`).
 
     Provides ONLY `HasSupport ℝ`, NOT `CommitmentGrade ℝ`: the latter
     would require the involution law on `complement`, which fails on
@@ -114,7 +114,7 @@ instance : HasSupport ℝ where
 -- § 3. Bridge to polymorphic CommitmentSpace W ℝ
 -- ════════════════════════════════════════════════════
 
-/-- Bridge: a distributional CG embeds into a commitment space at
+/-- Bridge: a distributional CommonGround embeds into a commitment space at
     `G = ℝ`. The speaker's distributional weights become a single
     `commit speaker .doxastic weight` entry in the root.
 
@@ -129,10 +129,10 @@ noncomputable def DistributionalCG.toCommitmentSpace {W : Type*}
   root := [IndexedWeightedCommitment.commit .speaker .doxastic cg.weight]
   continuations := []
 
-/-- Bridge theorem: the support of a distributional CG equals the
+/-- Bridge theorem: the support of a distributional CommonGround equals the
     `toContextSet` projection of the bridged commitment space.
     Demonstrates that the polymorphic substrate at `G = ℝ`
-    faithfully captures Anderson's distributional CG when projected
+    faithfully captures Anderson's distributional CommonGround when projected
     to its support. -/
 theorem DistributionalCG.toCommitmentSpace_support {W : Type*}
     (cg : DistributionalCG W) (w : W) :

Linglib/Dialogue/FarkasBruce.lean

@@ -43,7 +43,7 @@ properties — `assert_adds_to_dcS`, `assert_preserves_cg`,
 
 namespace Dialogue.FarkasBruce
 
-open Discourse.CommonGround
+open CommonGround
 
 
 /--
@@ -124,7 +124,7 @@ def empty : DiscourseState W := ⟨[], [], [], []⟩
 /--
 Convert common ground to a ContextSet (worlds where all cg props hold).
 
-Bridges to the existing `Discourse.CommonGround` infrastructure as the
+Bridges to the existing `CommonGround` infrastructure as the
 fold-intersection of the cg list.
 -/
 def toContextSet (ds : DiscourseState W) : ContextSet W :=
@@ -251,17 +251,17 @@ def acceptTop (ds : DiscourseState W) : DiscourseState W :=
 
 
 /--
-Convert the common ground component to a `CG` structure.
+Convert the common ground component to a `CommonGround` structure.
 -/
-def toCG (ds : DiscourseState W) : CG W :=
+def toCG (ds : DiscourseState W) : CommonGround W :=
   { propositions := ds.cg }
 
 /--
-Create a discourse state from a `CG` structure.
+Create a discourse state from a `CommonGround` structure.
 
-Sets cg, dcS, and dcL all to the CG propositions (everyone agrees).
+Sets cg, dcS, and dcL all to the CommonGround propositions (everyone agrees).
 -/
-def fromCG (cg : CG W) : DiscourseState W :=
+def fromCG (cg : CommonGround W) : DiscourseState W :=
   { dcS := cg.propositions
     dcL := cg.propositions
     cg := cg.propositions
@@ -341,7 +341,7 @@ end DiscourseState
 -- HasContextSet instance
 -- ════════════════════════════════════════════════════
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- F&B states project to a context set via `cg`-only intersection
     (`toContextSet`). Note: this projection deliberately ignores
     `dcS`/`dcL` and `table` — F&B's whole point is that assertion

Linglib/Dialogue/Gunlogson.lean

@@ -37,7 +37,7 @@ Source determines who can challenge:
 namespace Dialogue.Gunlogson
 
 open Discourse.Commitment
-open Discourse.CommonGround (ContextSet CG)
+open CommonGround (ContextSet)
 open Discourse (DiscourseRole)
 open Semantics.Modality.BiasedPQ (ContextualEvidence)
 
@@ -48,7 +48,7 @@ open Semantics.Modality.BiasedPQ (ContextualEvidence)
 /-- Gunlogson's discourse state: source-tagged commitment slates
     for speaker and addressee.
 
-    Unlike Stalnaker (single CG) or Farkas & Bruce (dcS + dcL + cg),
+    Unlike Stalnaker (single CommonGround) or Farkas & Bruce (dcS + dcL + cg),
     Gunlogson tracks the SOURCE of each commitment, not just which
     participant holds it. -/
 structure GunlogsonState (W : Type*) where
@@ -338,7 +338,7 @@ theorem confirm_still_unstable {W : Type*} (p : Set W) :
 -- HasContextSet instance
 -- ════════════════════════════════════════════════════
 
-open Discourse.CommonGround in
+open CommonGround in
 /-- Gunlogson states project to a context set via `contextSet` —
     the intersection of both participants' commitment contexts
     (regardless of source). -/