refactor(Phonology): reorganize constraint layer by framework

Linglib.lean

@@ -199,38 +199,39 @@ import Linglib.Semantics.Verb.RootContent
 import Linglib.Semantics.NaturalLogic
 import Linglib.Core.Optimization.Profile
 import Linglib.Phonology.Constraint.Weighted
-import Linglib.Phonology.Constraint.Superoptimal
-import Linglib.Phonology.Constraint.OT.Basic
-import Linglib.Phonology.Constraint.OT.ElementaryRankingCondition
-import Linglib.Phonology.Constraint.OT.Antimatroid
-import Linglib.Phonology.Constraint.OT.EvalMode
-import Linglib.Phonology.Constraint.OT.Iteration
-import Linglib.Phonology.Constraint.OT.HarmonicSerialism
+import Linglib.Pragmatics.Superoptimal
+import Linglib.Phonology.Constraint.Defs
+import Linglib.Phonology.OptimalityTheory.Optimality
+import Linglib.Phonology.OptimalityTheory.ElementaryRankingCondition
+import Linglib.Phonology.OptimalityTheory.Antimatroid
+import Linglib.Phonology.OptimalityTheory.EvalMode
+import Linglib.Phonology.Constraint.Iteration
+import Linglib.Phonology.OptimalityTheory.HarmonicSerialism
 import Linglib.Semantics.Questions.DecisionTheory
 import Linglib.Semantics.Questions.PartitionDT
 import Linglib.Core.DecisionTheory.BayesianUpdate
 import Linglib.Core.DecisionTheory.ExperimentDesign
 import Linglib.Core.DecisionTheory.RationalAction
-import Linglib.Phonology.Constraint.MaxEnt
+import Linglib.Phonology.HarmonicGrammar.MaxEnt
 import Linglib.Core.Optimization.Decoder
 import Linglib.Core.Optimization.NoiseKernel
 import Linglib.Core.Optimization.System
 import Linglib.Core.Optimization.Evaluation
-import Linglib.Phonology.Constraint.OT.Aliases
+import Linglib.Phonology.Constraint.Aliases
 import Linglib.Phonology.Constraint.System
 import Linglib.Core.Optimization.Pareto
 import Linglib.Core.Optimization.Semiring
-import Linglib.Phonology.Constraint.NoisyHG
-import Linglib.Phonology.Constraint.Dequantization.OTLimit
-import Linglib.Phonology.Constraint.Cumulativity
-import Linglib.Phonology.Constraint.PartiallyOrderedConstraints
+import Linglib.Phonology.HarmonicGrammar.NoisyHG
+import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit
+import Linglib.Phonology.HarmonicGrammar.Cumulativity
+import Linglib.Phonology.HarmonicGrammar.PartiallyOrderedConstraints
 import Linglib.Core.Optimization.PermSubsetCombinatorics
-import Linglib.Phonology.Constraint.Separability
-import Linglib.Phonology.Constraint.Dequantization.ViolationSemiring
+import Linglib.Phonology.HarmonicGrammar.Separability
+import Linglib.Phonology.HarmonicGrammar.Dequantization.ViolationSemiring
 import Linglib.Core.Optimization.Dequantization.LogSumExp.Basic
 import Linglib.Core.Optimization.Dequantization.LogSumExp.Limit
 import Linglib.Core.Optimization.Dequantization.LogSumExp.Softmax
-import Linglib.Phonology.Constraint.Dequantization.Deformation
+import Linglib.Phonology.HarmonicGrammar.Dequantization.Deformation
 import Linglib.Pragmatics.SoftmaxOptimality
 import Linglib.Core.DecisionTheory.UtilityTheory
 import Linglib.Core.DecisionTheory.ChoiceApproximations

Linglib/Core/Probability/CoupledEvaluation.lean

@@ -249,7 +249,7 @@ def CoupledSoftmax.genuinelyCoupled
     - `couplingScore f = systemicScore(f)`
 
     This shows that the MaxEnt systemic constraint framework from
-    `Phonology.Constraint.MaxEnt` is an instance of
+    `Phonology.HarmonicGrammar.MaxEnt` is an instance of
     the general coupled evaluation pattern. The `marginal_eq_classical_when_no_systemic`
     theorem in `MaxEnt.lean` is a corollary of `marginal_eq_independent_when_uncoupled`. -/
 noncomputable def coupledSoftmaxOfMaxEnt

Linglib/Fragments/Amharic/ConsonantalRoots.lean

@@ -84,6 +84,6 @@ theorem wd_biradical : wd.biradical = true := rfl
     not violated at the root level. The biradical analysis (shared
     with [broselow-1984]) is therefore maintained. -/
 theorem wd_no_adjacent_identical :
-    Phonology.Constraints.adjacentIdentical wd.segments = 0 := rfl
+    OptimalityTheory.adjacentIdentical wd.segments = 0 := rfl
 
 end Amharic

Linglib/Phonology/Autosegmental/BasemapCorrespondence.lean

@@ -1,6 +1,7 @@
 import Linglib.Phonology.Autosegmental.GrammaticalTone
 import Linglib.Phonology.OptimalityTheory.Correspondence
-import Linglib.Phonology.Constraint.OT.Basic
+import Linglib.Phonology.Constraint.Defs
+import Linglib.Phonology.OptimalityTheory.Optimality
 
 /-!
 # Matrix-Basemap Correspondence (MxBM-C)
@@ -66,8 +67,8 @@ namespace Phonology.Autosegmental.BasemapCorrespondence
 
 open Phonology.Autosegmental.GrammaticalTone
 open Phonology.Autosegmental.RegisterTier (TRN)
-open Phonology.Correspondence (Corr)
-open Phonology.Constraint.OT (NamedConstraint ConstraintFamily)
+open OptimalityTheory.Correspondence (Corr)
+open Constraint OptimalityTheory
 
 /-! ### Basemap — deficient projection -/
 

Linglib/Phonology/Constraint/OT/Aliases.lean → Linglib/Phonology/Constraint/Aliases.lean

@@ -15,7 +15,7 @@ Any Phonology file using OT-tradition names should import this module
 (rather than `Core.Optimization.Evaluation` directly).
 -/
 
-namespace Phonology.Constraint.OT
+namespace Constraint
 
 open Core.Optimization.Evaluation
 
@@ -68,4 +68,4 @@ theorem ViolationProfile.le_apply_zero {n : Nat}
     {a b : ViolationProfile (n + 1)} (h : a ≤ b) : a 0 ≤ b 0 :=
   Core.Optimization.Evaluation.lexFinNat_le_apply_zero h
 
-end Phonology.Constraint.OT
+end Constraint

Linglib/Phonology/Constraint/Defs.lean

@@ -0,0 +1,131 @@
+import Linglib.Core.Optimization.Evaluation
+import Linglib.Phonology.Constraint.Aliases
+import Mathlib.Computability.Language
+
+/-!
+# Optimality Theory — Core Vocabulary
+
+OT-specific vocabulary layered on `Core.Optimization.Evaluation`. Provides
+named constraints with a faithfulness/markedness distinction, convenience
+constructors for building tableaux from ranked constraint lists, and factorial
+typology computation.
+
+## Connection to Evaluation
+
+`Core.Optimization.Evaluation` provides the generic engine (`LexLE`, `Tableau`,
+`Tableau.optimal`). This module adds OT-specific structure: constraint
+families, named constraints, `mkTableau` for building tableaux from ranked
+constraint lists, and factorial typology computation.
+-/
+
+namespace Constraint
+
+
+open Core.Optimization.Evaluation
+
+-- ============================================================================
+
+/-- Constraint families in OT. -/
+inductive ConstraintFamily where
+  /-- Faithfulness: penalizes deviation from the input. -/
+  | faithfulness
+  /-- Markedness: penalizes marked structures in the output. -/
+  | markedness
+  deriving DecidableEq, Repr
+
+/-- A named OT constraint with family classification.
+    `eval c` returns the number of violations candidate `c` incurs.
+
+    The `name` field is purely documentary — no evaluation function reads it.
+    It defaults to `""` so constraints can be defined without a name when
+    the string label adds no information. -/
+structure NamedConstraint (C : Type*) where
+  name : String := ""
+  family : ConstraintFamily
+  eval : C → Nat
+
+-- ============================================================================
+-- § 1b: Constraint Constructors
+-- ============================================================================
+
+/-- Build a binary markedness constraint (violated → 1, otherwise 0).
+
+    Takes a `Prop`-valued predicate with `[DecidablePred]` so that callers
+    can use propositional equality (`=`) and other Prop predicates rather
+    than `Bool`-valued operators (`==`). Decidability is required to evaluate
+    the constraint on a candidate. -/
+def mkMark {C : Type*} (name : String) (P : C → Prop) [DecidablePred P] :
+    NamedConstraint C :=
+  { name, family := .markedness, eval := fun c => if P c then 1 else 0 }
+
+/-- Build a binary faithfulness constraint (violated → 1, otherwise 0).
+
+    Takes a `Prop`-valued predicate with `[DecidablePred]` so that callers
+    can use propositional equality (`=`) and other Prop predicates rather
+    than `Bool`-valued operators (`==`). -/
+def mkFaith {C : Type*} (name : String) (P : C → Prop) [DecidablePred P] :
+    NamedConstraint C :=
+  { name, family := .faithfulness, eval := fun c => if P c then 1 else 0 }
+
+/-- Build a gradient markedness constraint with a Nat-valued violation count. -/
+def mkMarkGrad {C : Type*} (name : String) (violations : C → Nat) : NamedConstraint C :=
+  { name, family := .markedness, eval := violations }
+
+/-- Build a gradient faithfulness constraint with a Nat-valued violation count. -/
+def mkFaithGrad {C : Type*} (name : String) (violations : C → Nat) : NamedConstraint C :=
+  { name, family := .faithfulness, eval := violations }
+
+/-- Pull a `NamedConstraint D` back along a candidate map `f : C → D`. The
+    name and family are inherited; the new `eval` composes the original
+    with the projection. Lets paper-specific carrier types reuse a
+    constraint defined on a more general carrier. -/
+def NamedConstraint.comap {C D : Type*} (f : C → D) (c : NamedConstraint D) :
+    NamedConstraint C :=
+  { name := c.name, family := c.family, eval := c.eval ∘ f }
+
+@[simp] theorem NamedConstraint.comap_eval {C D : Type*} (f : C → D)
+    (c : NamedConstraint D) (x : C) :
+    (c.comap f).eval x = c.eval (f x) := rfl
+
+@[simp] theorem NamedConstraint.comap_name {C D : Type*} (f : C → D)
+    (c : NamedConstraint D) : (c.comap f).name = c.name := rfl
+
+@[simp] theorem NamedConstraint.comap_family {C D : Type*} (f : C → D)
+    (c : NamedConstraint D) : (c.comap f).family = c.family := rfl
+
+/-- The zero-violation set of a `NamedConstraint` over list candidates,
+viewed as a `Language α`. Lets the OT-side `eval = 0` predicate compose
+with mathlib's `Language.IsRegular` and the project's
+`IsTierStrictlyLocal`/`IsBTC` classifiers. The dot-notation form
+`c.zeroSet` is the canonical access pattern. -/
+def NamedConstraint.zeroSet {α : Type*} (c : NamedConstraint (List α)) :
+    Language α :=
+  { w | c.eval w = 0 }
+
+lemma NamedConstraint.mem_zeroSet {α : Type*}
+    (c : NamedConstraint (List α)) (w : List α) :
+    w ∈ c.zeroSet ↔ c.eval w = 0 := Iff.rfl
+
+-- ============================================================================
+-- § 2: Tableau Construction
+-- ============================================================================
+
+/-- Build a `ViolationProfile ranking.length` from a ranked list of named
+    constraints. This is the fixed-length analog of the profile computation
+    inside `mkTableau` — use it to inspect or compare violation counts
+    outside a tableau context. -/
+def mkProfile {C : Type*} (ranking : List (NamedConstraint C)) (c : C)
+    : ViolationProfile ranking.length :=
+  buildViolationProfile (fun i c => (ranking.get i).eval c) c
+
+/-- Create a `ViolationProfile n` from a `List Nat` literal.
+
+    The length proof defaults to `by decide`, so study files can write
+    readable profile comparisons without an explicit proof:
+    ```
+    theorem t24a_profile : mkProfile ranking c = vpOfList [2, 2, 0] := by decide
+    ``` -/
+def vpOfList {n : Nat} (vs : List Nat) (h : vs.length = n := by decide)
+    : ViolationProfile n :=
+  toLex fun (i : Fin n) => vs.get ⟨i.val, by omega⟩
+end Constraint

Linglib/Phonology/Constraint/OT/Iteration.lean → Linglib/Phonology/Constraint/Iteration.lean

@@ -42,7 +42,7 @@ the iteration loop — see
 `Phonology/OptimalityTheory/Stratal.lean`.)
 -/
 
-namespace Phonology.Constraint.OT
+namespace Constraint
 
 
 variable {C : Type*}
@@ -252,4 +252,4 @@ theorem iterateGen_eventually_constant [DecidableEq C]
                 iterateGen_succ_of_step _ hcv hp,
                 IH' n hn']
 
-end Phonology.Constraint.OT
+end Constraint

Linglib/Phonology/Constraint/System.lean

@@ -1,7 +1,8 @@
 import Linglib.Core.Optimization.System
 import Linglib.Phonology.Constraint.Weighted
 import Linglib.Core.Optimization.Profile
-import Linglib.Phonology.Constraint.OT.Basic
+import Linglib.Phonology.Constraint.Defs
+import Linglib.Phonology.OptimalityTheory.Optimality
 
 /-!
 # Constraint Systems — OT/HG/MaxEnt instantiations of `Core.Optimization.ConstraintSystem`
@@ -22,7 +23,7 @@ A `tableauSystem` bridge view shows that the established `Tableau` API
 is `argminDecoder` over a `LexProfile Nat n` score in disguise.
 -/
 
-namespace Phonology.Constraint
+namespace Constraint
 
 open Core.Optimization
 
@@ -73,7 +74,7 @@ noncomputable def maxEntSystem {Cand : Type*}
 -- § 2: Tableau Bridge
 -- ============================================================================
 
-/-! `Phonology.Constraint.OT.Tableau` is the established study-file API for
+/-! `Constraint.Tableau` is the established study-file API for
 OT (used by `mkTableau ... .optimal = {winner}` patterns). The bridge below
 shows that `Tableau` is a special case of `ConstraintSystem`: the OT score
 `profile : C → ViolationProfile n` is exactly a `LexProfile Nat n`-valued
@@ -83,7 +84,7 @@ score (definitionally), and `Tableau.optimal` is exactly the support of the
 `ConstraintSystem.predict` view via `tableauSystem`. -/
 
 open Core.Optimization.Evaluation
-open Phonology.Constraint.OT
+open Constraint OptimalityTheory
 
 /-- An OT tableau viewed as a generic `ConstraintSystem`. The score type
     `LexProfile Nat n` is definitionally `ViolationProfile n`, so the
@@ -140,4 +141,4 @@ theorem tableauSystem_predict_loser {C : Type*} [DecidableEq C] {n : Nat}
     (tableauSystem t).predict loser = 0 := by
   rw [tableauSystem_predict_eq, h]; simp [hne]
 
-end Phonology.Constraint
+end Constraint

Linglib/Phonology/Constraint/Weighted.lean

@@ -1,4 +1,5 @@
-import Linglib.Phonology.Constraint.OT.Basic
+import Linglib.Phonology.Constraint.Defs
+import Linglib.Phonology.OptimalityTheory.Optimality
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Rat.Cast.Order
 
@@ -12,7 +13,7 @@ The shared foundation for any constraint framework that assigns numerical
 - Noisy HG [boersma-pater-2016]
 - Normal MaxEnt [flemming-2021]
 
-A `WeightedConstraint C` extends `NamedConstraint C` (from `Phonology.Constraint.OT`)
+A `WeightedConstraint C` extends `NamedConstraint C` (from `Constraint`)
 with a rational `weight`. The `harmonyScore` of a candidate is the negated
 weighted sum of its violations: `H(c) = -Σⱼ wⱼ · Cⱼ(c)`.
 
@@ -22,10 +23,10 @@ modules in `Core.Optimization.*` consume them; framework-specific wrappers
 (MaxEnt, NHG, ...) live in their respective theory directories.
 -/
 
-namespace Phonology.Constraint
+namespace Constraint
 
 
-open Phonology.Constraint.OT
+open Constraint OptimalityTheory
 
 -- ============================================================================
 -- § 1: Weighted Constraints
@@ -116,4 +117,4 @@ theorem harmonyScoreR_lt_of_dominates {C : Type*}
     harmonyScoreR constraints b < harmonyScoreR constraints a :=
   (harmonyScoreR_lt_iff_harmonyScore_lt _ _ _).mpr h
 
-end Phonology.Constraint
+end Constraint

Linglib/Phonology/Constraint/Cumulativity.lean → Linglib/Phonology/HarmonicGrammar/Cumulativity.lean

@@ -1,4 +1,4 @@
-import Linglib.Phonology.Constraint.Dequantization.OTLimit
+import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit
 
 /-!
 # The Cumulativity Gap: HG ⊋ OT
@@ -52,10 +52,10 @@ likewise consume `hg_strictly_contains_ot` rather than re-deriving the
 gap per-paper.
 -/
 
-namespace Phonology.Constraint
+namespace HarmonicGrammar
 
 
-open Phonology.Constraint.OT Finset
+open Constraint OptimalityTheory Finset
 
 -- ============================================================================
 -- § 1: Decidable Lex Comparison
@@ -259,4 +259,4 @@ theorem hg_strictly_contains_ot :
     Cumulativity.lyman_isHGRealizable,
     Cumulativity.lyman_not_isOTRealizable⟩
 
-end Phonology.Constraint
+end HarmonicGrammar

Linglib/Phonology/Constraint/Dequantization/Deformation.lean → Linglib/Phonology/HarmonicGrammar/Dequantization/Deformation.lean

@@ -1,7 +1,7 @@
 import Linglib.Core.Optimization.Semiring
 import Linglib.Core.Optimization.Dequantization.LogSumExp.Softmax
-import Linglib.Phonology.Constraint.Dequantization.ViolationSemiring
-import Linglib.Phonology.Constraint.Dequantization.OTLimit
+import Linglib.Phonology.HarmonicGrammar.Dequantization.ViolationSemiring
+import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit
 
 /-!
 # The Constraint-Framework Deformation Lattice
@@ -71,13 +71,14 @@ harmony "tracks the soft aggregator all the way to the limit." Every
 other candidate's softmax probability decays exponentially in the gap.
 -/
 
-namespace Phonology.Constraint
+namespace HarmonicGrammar
+open Constraint
 
 open Core.Optimization
 
 
 open Real Filter Topology Finset
-open Phonology.Constraint.OT Phonology.Constraint.ViolationSemiring
+open Constraint OptimalityTheory HarmonicGrammar.ViolationSemiring
 
 -- ============================================================================
 -- § 1: The Soft Aggregator on Harmony Scores
@@ -141,4 +142,4 @@ theorem softmax_decoder_gap_form {Cand : Type*} (α : ℝ) (hα : α ≠ 0)
       = exp (α * (score c - lseFinset α cands score)) :=
   softmaxDecoder_eq_exp_score_sub_lse α hα score hc
 
-end Phonology.Constraint
+end HarmonicGrammar