diff --git a/Linglib.lean b/Linglib.lean index 67d01c4c2..3362c617b 100644 --- a/Linglib.lean +++ b/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 diff --git a/Linglib/Core/Probability/CoupledEvaluation.lean b/Linglib/Core/Probability/CoupledEvaluation.lean index 223626e57..84fda2934 100644 --- a/Linglib/Core/Probability/CoupledEvaluation.lean +++ b/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 diff --git a/Linglib/Fragments/Amharic/ConsonantalRoots.lean b/Linglib/Fragments/Amharic/ConsonantalRoots.lean index 515eb2d33..c01a38fff 100644 --- a/Linglib/Fragments/Amharic/ConsonantalRoots.lean +++ b/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 diff --git a/Linglib/Phonology/Autosegmental/BasemapCorrespondence.lean b/Linglib/Phonology/Autosegmental/BasemapCorrespondence.lean index 889f1cd9e..27c875207 100644 --- a/Linglib/Phonology/Autosegmental/BasemapCorrespondence.lean +++ b/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 -/ diff --git a/Linglib/Phonology/Constraint/OT/Aliases.lean b/Linglib/Phonology/Constraint/Aliases.lean similarity index 97% rename from Linglib/Phonology/Constraint/OT/Aliases.lean rename to Linglib/Phonology/Constraint/Aliases.lean index 5dac366c9..04e6d8155 100644 --- a/Linglib/Phonology/Constraint/OT/Aliases.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/Defs.lean b/Linglib/Phonology/Constraint/Defs.lean new file mode 100644 index 000000000..1599e746a --- /dev/null +++ b/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 diff --git a/Linglib/Phonology/Constraint/OT/Iteration.lean b/Linglib/Phonology/Constraint/Iteration.lean similarity index 99% rename from Linglib/Phonology/Constraint/OT/Iteration.lean rename to Linglib/Phonology/Constraint/Iteration.lean index 97ee17065..5fbd5eb3b 100644 --- a/Linglib/Phonology/Constraint/OT/Iteration.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/System.lean b/Linglib/Phonology/Constraint/System.lean index adefaefe8..9f898e5ce 100644 --- a/Linglib/Phonology/Constraint/System.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/Weighted.lean b/Linglib/Phonology/Constraint/Weighted.lean index 51b4c5b68..6cd9dd430 100644 --- a/Linglib/Phonology/Constraint/Weighted.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/Cumulativity.lean b/Linglib/Phonology/HarmonicGrammar/Cumulativity.lean similarity index 98% rename from Linglib/Phonology/Constraint/Cumulativity.lean rename to Linglib/Phonology/HarmonicGrammar/Cumulativity.lean index aeeaf3319..9f786a2b4 100644 --- a/Linglib/Phonology/Constraint/Cumulativity.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/Dequantization/Deformation.lean b/Linglib/Phonology/HarmonicGrammar/Dequantization/Deformation.lean similarity index 96% rename from Linglib/Phonology/Constraint/Dequantization/Deformation.lean rename to Linglib/Phonology/HarmonicGrammar/Dequantization/Deformation.lean index 31c445151..ec58fbb16 100644 --- a/Linglib/Phonology/Constraint/Dequantization/Deformation.lean +++ b/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 diff --git a/Linglib/Phonology/Constraint/Dequantization/OTLimit.lean b/Linglib/Phonology/HarmonicGrammar/Dequantization/OTLimit.lean similarity index 99% rename from Linglib/Phonology/Constraint/Dequantization/OTLimit.lean rename to Linglib/Phonology/HarmonicGrammar/Dequantization/OTLimit.lean index 924a998c9..c62f01d1c 100644 --- a/Linglib/Phonology/Constraint/Dequantization/OTLimit.lean +++ b/Linglib/Phonology/HarmonicGrammar/Dequantization/OTLimit.lean @@ -33,10 +33,11 @@ Together: MaxEnt(α → ∞) → HG winner = OT winner. - `maxent_ot_limit`: main limit theorem -/ -namespace Phonology.Constraint +namespace HarmonicGrammar +open Constraint -open Core Phonology.Constraint.OT Core.Optimization.Evaluation Real Finset +open Core Constraint OptimalityTheory Core.Optimization.Evaluation Real Finset -- ============================================================================ -- § 1: OT → HG Weight Construction @@ -387,4 +388,4 @@ theorem maxent_ot_limit {C : Type} [Fintype C] [Nonempty C] [DecidableEq C] (fun con hcon => ⟨hbound c_opt con hcon, hbound c con hcon⟩) (hlex c hc) -end Phonology.Constraint +end HarmonicGrammar diff --git a/Linglib/Phonology/Constraint/Dequantization/ViolationSemiring.lean b/Linglib/Phonology/HarmonicGrammar/Dequantization/ViolationSemiring.lean similarity index 96% rename from Linglib/Phonology/Constraint/Dequantization/ViolationSemiring.lean rename to Linglib/Phonology/HarmonicGrammar/Dequantization/ViolationSemiring.lean index ebc6e696f..3b5a7c566 100644 --- a/Linglib/Phonology/Constraint/Dequantization/ViolationSemiring.lean +++ b/Linglib/Phonology/HarmonicGrammar/Dequantization/ViolationSemiring.lean @@ -1,6 +1,6 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.OT.Aliases -import Linglib.Phonology.Constraint.Dequantization.OTLimit +import Linglib.Phonology.Constraint.Aliases +import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit import Mathlib.Algebra.Tropical.Basic /-! @@ -32,7 +32,7 @@ This map always preserves ⊗ (merge/tropical multiplication — linearity of the dot product). It preserves ⊕ (min/tropical addition) when weights are exponentially separated — which is exactly the content of the HG–OT agreement theorem ([smolensky-legendre-2006], formalized in -`Phonology.Constraint.OTLimit`). +`HarmonicGrammar.Dequantization.OTLimit`). ## Monotonicity (Dijkstra's Principle) @@ -42,11 +42,11 @@ algorithms applicable to OT optimization. Riggle: "every subpath of an optimal input–output mapping is itself an optimal mapping." -/ -namespace Phonology.Constraint.ViolationSemiring +namespace HarmonicGrammar.ViolationSemiring -open Core.Optimization.Evaluation Phonology.Constraint -open Phonology.Constraint.OT +open Core.Optimization.Evaluation Constraint +open Constraint OptimalityTheory -- ============================================================================ -- § 1: The Violation Semiring V @@ -143,7 +143,7 @@ abbrev weightedSum {n : Nat} (w : Fin n → ℚ) (v : ViolationProfile n) : ℚ -- ============================================================================ /-- `weightMap` is definitionally equal to `weightedViolations` - from `Phonology.Constraint.OTLimit`. + from `HarmonicGrammar.Dequantization.OTLimit`. This bridges the semiring-theoretic framework (violation profiles as algebraic objects) to the existing HG–OT agreement machinery @@ -217,4 +217,4 @@ theorem weightMap_preserves_minimum {n : Nat} (w : Fin n → ℚ) (M : Nat) fun b hb => weightMap_mono w M hw a b (fun i => ⟨hM a ha i, hM b hb i⟩) (hmin b hb) -end Phonology.Constraint.ViolationSemiring +end HarmonicGrammar.ViolationSemiring diff --git a/Linglib/Phonology/Constraint/MaxEnt.lean b/Linglib/Phonology/HarmonicGrammar/MaxEnt.lean similarity index 98% rename from Linglib/Phonology/Constraint/MaxEnt.lean rename to Linglib/Phonology/HarmonicGrammar/MaxEnt.lean index 7c9ef43c2..301329d4a 100644 --- a/Linglib/Phonology/Constraint/MaxEnt.lean +++ b/Linglib/Phonology/HarmonicGrammar/MaxEnt.lean @@ -25,7 +25,7 @@ candidates by weighted constraint violations. ## Architecture - `MaxEntGrammar` packages inputs, candidate generation, and weighted constraints - (`WeightedConstraint` and `harmonyScore` come from `Phonology.Constraint.Weighted`) + (`WeightedConstraint` and `harmonyScore` come from `Constraint.Weighted`) - `SystemicConstraint` evaluates *tuples* of outputs (different type signature) - `jointHarmonyScore` combines classical + systemic scores over the product space - `marginalProb` marginalizes the joint to recover individual mapping probabilities @@ -38,12 +38,12 @@ score decomposes additively ⇒ the joint distribution factorizes ⇒ each margi equals its factor. -/ -namespace Phonology.Constraint +namespace HarmonicGrammar open Core.Optimization -open Phonology.Constraint.OT Core +open Constraint OptimalityTheory Core Constraint -- ============================================================================ -- § 1: MaxEnt Grammar (Classical — Individual Mappings) @@ -236,4 +236,4 @@ theorem MaxEntGrammar.prob_eq_toSystem_predict {I O : Type*} [Fintype O] [Nonemp show softmax _ o = (softmaxDecoder 1).decode Finset.univ _ o simp [softmaxDecoder, softmax, Finset.mem_univ, MaxEntGrammar.toSystem, one_mul] -end Phonology.Constraint +end HarmonicGrammar diff --git a/Linglib/Phonology/Constraint/NoisyHG.lean b/Linglib/Phonology/HarmonicGrammar/NoisyHG.lean similarity index 99% rename from Linglib/Phonology/Constraint/NoisyHG.lean rename to Linglib/Phonology/HarmonicGrammar/NoisyHG.lean index 4efa5a677..b045c1985 100644 --- a/Linglib/Phonology/Constraint/NoisyHG.lean +++ b/Linglib/Phonology/HarmonicGrammar/NoisyHG.lean @@ -34,10 +34,10 @@ of the violation profile elsewhere. NHG lacks this property because its noise variance σ_d depends on the violation profile. -/ -namespace Phonology.Constraint +namespace HarmonicGrammar -open Core Real +open Core Real Constraint -- ============================================================================ -- § 1: NHG Noise Variance @@ -288,4 +288,4 @@ theorem nhgCovariance_self {C : Type*} congr 1 with acc con ring -end Phonology.Constraint +end HarmonicGrammar diff --git a/Linglib/Phonology/Constraint/PartiallyOrderedConstraints.lean b/Linglib/Phonology/HarmonicGrammar/PartiallyOrderedConstraints.lean similarity index 99% rename from Linglib/Phonology/Constraint/PartiallyOrderedConstraints.lean rename to Linglib/Phonology/HarmonicGrammar/PartiallyOrderedConstraints.lean index 70969e1c1..db7608d77 100644 --- a/Linglib/Phonology/Constraint/PartiallyOrderedConstraints.lean +++ b/Linglib/Phonology/HarmonicGrammar/PartiallyOrderedConstraints.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.Cumulativity +import Linglib.Phonology.HarmonicGrammar.Cumulativity import Linglib.Core.Optimization.PermSubsetCombinatorics import Mathlib.Order.Extension.Linear @@ -54,7 +54,7 @@ substrate directly — `pocPredict`, `PicksAt`, and `pocPredict_discrete_binary_ over the discrete partial order — rather than enumerating rankings by hand. -/ -namespace Phonology.Constraint +namespace HarmonicGrammar open Core.Optimization @@ -431,7 +431,7 @@ theorem picksAt_binary_iff_permDList_head_lt {Output : Type*} [DecidableEq Outpu -- Step 1: PicksAt with binary cands reduces to LexStrictlyBetter on chosen vs other have h_picksAt_iff_lex : PicksAt cands vp σ i chosen ↔ - Phonology.Constraint.LexStrictlyBetter + HarmonicGrammar.LexStrictlyBetter (fun k => vp i chosen (σ k)) (fun k => vp i other (σ k)) := by unfold PicksAt constructor @@ -595,4 +595,4 @@ theorem pocPredict_discrete_binary_rate end PartialOrderConstraints -end Phonology.Constraint +end HarmonicGrammar diff --git a/Linglib/Phonology/Constraint/Separability.lean b/Linglib/Phonology/HarmonicGrammar/Separability.lean similarity index 99% rename from Linglib/Phonology/Constraint/Separability.lean rename to Linglib/Phonology/HarmonicGrammar/Separability.lean index efa444022..20a673b1c 100644 --- a/Linglib/Phonology/Constraint/Separability.lean +++ b/Linglib/Phonology/HarmonicGrammar/Separability.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.NoisyHG +import Linglib.Phonology.HarmonicGrammar.NoisyHG /-! # Separable Harmonies and HZ's Generalization [magri-2025] @@ -56,10 +56,10 @@ These enable applying separability results (independence → HZ, rescaling) to any `WeightedConstraint` list without re-proving in Fin-indexed form. -/ -namespace Phonology.Constraint +namespace HarmonicGrammar -open Core Real Finset +open Core Real Finset Constraint -- ============================================================================ -- § 1: The 2×2 Square of Underlying Forms (§2.4) @@ -517,4 +517,4 @@ theorem constantLogitDiff_mono_consistent {X : Type*} (d : X → ℝ) (f : ℝ · exact mul_pos_of_neg_of_neg (sub_neg.mpr (hf hlt)) (sub_neg.mpr (hf (by linarith))) · exact mul_pos (sub_pos.mpr (hf hgt)) (sub_pos.mpr (hf (by linarith))) -end Phonology.Constraint +end HarmonicGrammar diff --git a/Linglib/Phonology/ItemSpecificity/IndexedConstraints.lean b/Linglib/Phonology/ItemSpecificity/IndexedConstraints.lean index b67370f5a..b083f18f0 100644 --- a/Linglib/Phonology/ItemSpecificity/IndexedConstraints.lean +++ b/Linglib/Phonology/ItemSpecificity/IndexedConstraints.lean @@ -1,5 +1,6 @@ import Linglib.Phonology.ItemSpecificity.Defs -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Indexed Constraints @@ -31,7 +32,7 @@ theory under-fits relative to `ScaledWeights` / namespace Phonology.ItemSpecificity.Indexed open Phonology.ItemSpecificity -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Stratification diff --git a/Linglib/Phonology/ItemSpecificity/ScaledWeights.lean b/Linglib/Phonology/ItemSpecificity/ScaledWeights.lean index e88f51079..f62e2aa50 100644 --- a/Linglib/Phonology/ItemSpecificity/ScaledWeights.lean +++ b/Linglib/Phonology/ItemSpecificity/ScaledWeights.lean @@ -1,5 +1,6 @@ import Linglib.Phonology.ItemSpecificity.Defs -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Frequency-Scaled Weights @@ -40,7 +41,7 @@ remains a viable account. namespace Phonology.ItemSpecificity.Scaled open Phonology.ItemSpecificity -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Scaled weight diff --git a/Linglib/Phonology/ItemSpecificity/Separation.lean b/Linglib/Phonology/ItemSpecificity/Separation.lean index 6975f3696..89ef6b0f7 100644 --- a/Linglib/Phonology/ItemSpecificity/Separation.lean +++ b/Linglib/Phonology/ItemSpecificity/Separation.lean @@ -67,7 +67,7 @@ open Phonology.ItemSpecificity.Indexed open Phonology.ItemSpecificity.Scaled open Phonology.ItemSpecificity.UseListed open Phonology.ItemSpecificity.RepStrength -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Toy lexicon for separation witnesses diff --git a/Linglib/Phonology/Constraint/OT/Antimatroid.lean b/Linglib/Phonology/OptimalityTheory/Antimatroid.lean similarity index 99% rename from Linglib/Phonology/Constraint/OT/Antimatroid.lean rename to Linglib/Phonology/OptimalityTheory/Antimatroid.lean index 7170588be..3d85d15c2 100644 --- a/Linglib/Phonology/Constraint/OT/Antimatroid.lean +++ b/Linglib/Phonology/OptimalityTheory/Antimatroid.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.OT.ElementaryRankingCondition +import Linglib.Phonology.OptimalityTheory.ElementaryRankingCondition import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Finite.Basic import Mathlib.Data.Fintype.Card @@ -58,7 +58,8 @@ The design follows mathlib's `Matroid` pattern: bundled structure with ERC sets and antimatroids -/ -namespace Phonology.Constraint.OT +namespace OptimalityTheory +open Constraint -- ============================================================================ @@ -686,4 +687,4 @@ theorem RCErc_entailment {n : Nat} -- TODO: requires full RCErc definition : True := trivial -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/OptimalityTheory/Constraints.lean b/Linglib/Phonology/OptimalityTheory/Constraints.lean index 6ea1fc0b7..5dc14e989 100644 --- a/Linglib/Phonology/OptimalityTheory/Constraints.lean +++ b/Linglib/Phonology/OptimalityTheory/Constraints.lean @@ -1,4 +1,5 @@ -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Phonology.Constraint.Weighted import Linglib.Core.Computability.StringHom import Linglib.Core.Computability.Subregular.ForbiddenPairs @@ -43,10 +44,10 @@ Binary constraints use a `Bool` predicate; gradient constraints use a `Nat`-valued evaluation function directly. -/ -namespace Phonology.Constraints +namespace OptimalityTheory -open Phonology.Constraint -open Phonology.Constraint.OT +open Constraint +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Faithfulness Constraint Constructors @@ -139,12 +140,12 @@ theorem mkIntegrity_is_faithfulness {C : Type} (name : String) (mkIntegrity name P).family = .faithfulness := rfl -- ============================================================================ --- § 2: Markedness Constraint Constructors (re-exported from Phonology.Constraint.OT) +-- § 2: Markedness Constraint Constructors (re-exported from Constraint) -- ============================================================================ --- `mkMark`, `mkFaith`, `mkMarkGrad`, `mkFaithGrad` are defined in `Phonology.Constraint.OT`. --- Re-export them so `open Phonology.Constraints` includes them. -export Phonology.Constraint.OT (mkMark mkFaith mkMarkGrad mkFaithGrad) +-- `mkMark`, `mkFaith`, `mkMarkGrad`, `mkFaithGrad` are defined in `Constraint`. +-- Re-export them so `open OptimalityTheory` includes them. +export Constraint (mkMark mkFaith mkMarkGrad mkFaithGrad) -- ============================================================================ -- § 2b: Forbidden-Pair Markedness (OCP, sibilant-harmony, …) @@ -153,7 +154,7 @@ export Phonology.Constraint.OT (mkMark mkFaith mkMarkGrad mkFaithGrad) -- `countAdjacent` lives at the substrate layer in -- `Core.Computability.Subregular.ForbiddenPairs` since it is alphabet-generic -- list combinatorics with nothing OT-specific. Re-exported here so consumers --- of `Phonology.Constraints` see it under the conventional name. +-- of `OptimalityTheory` see it under the conventional name. export Core.Computability.Subregular (countAdjacent) /-- Build a markedness constraint penalizing tier-adjacent forbidden pairs. @@ -355,7 +356,7 @@ theorem mkMaxCtx_bounded {C : Type} (name : String) -- § 5: Weighted Constraint Constructors -- ============================================================================ -open Phonology.Constraint +open Constraint /-- Build a weighted MAX constraint with a given weight. -/ def mkMaxW {C : Type} (name : String) (P : C → Prop) [DecidablePred P] (w : ℚ) : @@ -389,4 +390,4 @@ def mkMarkGradW {C : Type} (name : String) (violations : C → Nat) (w : ℚ) : WeightedConstraint C := { toNamedConstraint := mkMarkGrad name violations, weight := w } -end Phonology.Constraints +end OptimalityTheory diff --git a/Linglib/Phonology/OptimalityTheory/CophonologyByPhrase.lean b/Linglib/Phonology/OptimalityTheory/CophonologyByPhrase.lean index 57eafa498..7da0c5545 100644 --- a/Linglib/Phonology/OptimalityTheory/CophonologyByPhrase.lean +++ b/Linglib/Phonology/OptimalityTheory/CophonologyByPhrase.lean @@ -53,7 +53,7 @@ constraint subranking. The activation predicate is just a `SyntacticObject → Bool` so it can match phases by category, by specifier content, by feature, or by anything else the analyst can decide. `phrasalCophonologicalEval` delegates to -`Phonology.CophonologyTheory.cophonologicalEval` once the matched +`OptimalityTheory.CophonologyTheory.cophonologicalEval` once the matched cophonology has been selected — there is no parallel ranking-merge machinery, just a different trigger. @@ -68,11 +68,11 @@ The substrate's neutral position is to make the SBJ 2020 / SCD 2026 view expressible without forcing it on consumers. -/ -namespace Phonology.CophonologyByPhrase +namespace OptimalityTheory.CophonologyByPhrase -open Phonology.CophonologyTheory (cophonologicalEval mergeRanking +open OptimalityTheory.CophonologyTheory (cophonologicalEval mergeRanking mergeRanking_empty_sub cophonologicalEval_empty_sub) -open Phonology.Constraint.OT (NamedConstraint) +open Constraint OptimalityTheory open Minimalist (Phase SyntacticObject) -- ============================================================================ @@ -127,7 +127,7 @@ theorem phrasalCophonologicalEval_empty_sub {C : Type} [DecidableEq C] (candidates : List C) (h : candidates ≠ []) (hsub : pc.subranking = []) : phrasalCophonologicalEval defaultRanking pc candidates h - = (Phonology.Constraint.OT.mkTableau candidates defaultRanking h).optimal := by + = (OptimalityTheory.mkTableau candidates defaultRanking h).optimal := by unfold phrasalCophonologicalEval rw [hsub] exact cophonologicalEval_empty_sub defaultRanking candidates h @@ -167,4 +167,4 @@ theorem selectCophonology_applies {C : Type} theorem selectCophonology_empty {C : Type} (ph : Phase) : selectCophonology ([] : List (PhrasalCophonology C)) ph = none := rfl -end Phonology.CophonologyByPhrase +end OptimalityTheory.CophonologyByPhrase diff --git a/Linglib/Phonology/OptimalityTheory/CophonologyTheory.lean b/Linglib/Phonology/OptimalityTheory/CophonologyTheory.lean index 8b28891f9..13ebc14ab 100644 --- a/Linglib/Phonology/OptimalityTheory/CophonologyTheory.lean +++ b/Linglib/Phonology/OptimalityTheory/CophonologyTheory.lean @@ -1,5 +1,6 @@ import Linglib.Morphology.DM.VocabularyInsertion -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Cophonology Theory @@ -31,7 +32,7 @@ This gives DM's Vocabulary Item a four-part structure: `cophonologicalEval` function merges the winning VI's subranking with the default ranking and runs `Tableau.optimal`, connecting DM vocabulary insertion (`Morphology.DM.VI`) to OT constraint evaluation -(`Phonology.Constraint.OT` / `Core.Optimization.Evaluation`). +(`Constraint` / `Core.Optimization.Evaluation`). ## Phasal extension: see `CophonologyByPhrase.lean` @@ -46,11 +47,11 @@ word) — e.g. `Studies/SandeClemDabkowski2026.lean` remains the right substrate for morpheme-internal effects. -/ -namespace Phonology.CophonologyTheory +namespace OptimalityTheory.CophonologyTheory open Morphology.DM.VI (VocabItem) -open Phonology.Constraint.OT (NamedConstraint mkTableau mkTableau_optimal_zero_first mkTableau_optimal_mem) -open Phonology.Constraint.OT (Tableau) +open Constraint OptimalityTheory +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Cophonological Vocabulary Item @@ -185,4 +186,4 @@ theorem coph_dominant_complement {Ctx Root C : Type} cvi.isDominantCoph = !cvi.isNonDominantCoph := by simp [CophVocabItem.isDominantCoph, CophVocabItem.isNonDominantCoph] -end Phonology.CophonologyTheory +end OptimalityTheory.CophonologyTheory diff --git a/Linglib/Phonology/OptimalityTheory/Correspondence.lean b/Linglib/Phonology/OptimalityTheory/Correspondence.lean index 9fe4d83df..20bf93290 100644 --- a/Linglib/Phonology/OptimalityTheory/Correspondence.lean +++ b/Linglib/Phonology/OptimalityTheory/Correspondence.lean @@ -6,7 +6,8 @@ import Mathlib.Combinatorics.Quiver.Basic import Mathlib.Order.Hom.Basic import Mathlib.Order.Hom.Set import Mathlib.Data.Fintype.Card -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Phonology.OptimalityTheory.Constraints /-! @@ -49,9 +50,9 @@ model-theoretic treatment of [payne-vu-heinz-2017] and of the `identity_*_zero` lemmas). -/ -namespace Phonology.Correspondence +namespace OptimalityTheory.Correspondence -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Finset /-! ### Binary and ternary roles -/ @@ -524,7 +525,7 @@ theorem length_eq_of_faithful (c : Corr Role α) (r₁ r₂ : Role) /-! ### NamedConstraint bridges -/ /-- Bridge a `Corr`-violation function into a `NamedConstraint` — the single - plumbing point into `Phonology.Constraint.OT`'s evaluation machinery. -/ + plumbing point into `Constraint`'s evaluation machinery. -/ def toConstraint (family : ConstraintFamily) (label : String) (eval : Corr Role α → ℕ) : NamedConstraint (Corr Role α) where name := label @@ -591,4 +592,4 @@ instance {Role α : Type*} (c : Corr Role α) : Quiver (RoleQuiv c) where end Corr -end Phonology.Correspondence +end OptimalityTheory.Correspondence diff --git a/Linglib/Phonology/Constraint/OT/DirectionalTableau.lean b/Linglib/Phonology/OptimalityTheory/DirectionalTableau.lean similarity index 98% rename from Linglib/Phonology/Constraint/OT/DirectionalTableau.lean rename to Linglib/Phonology/OptimalityTheory/DirectionalTableau.lean index 7363ed4af..c0f2a04bd 100644 --- a/Linglib/Phonology/Constraint/OT/DirectionalTableau.lean +++ b/Linglib/Phonology/OptimalityTheory/DirectionalTableau.lean @@ -1,5 +1,5 @@ -import Linglib.Phonology.Constraint.OT.Basic -import Linglib.Phonology.Constraint.OT.EvalMode +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.EvalMode /-! # Directional Tableau — Position-Vector EVAL @@ -38,7 +38,8 @@ It deliberately does NOT yet ship: `HSDerivation` dispatches on `evalMode`; deferred to follow-up) -/ -namespace Phonology.Constraint.OT +namespace OptimalityTheory +open Constraint open Core.Optimization.Evaluation @@ -204,4 +205,4 @@ example : LexLEByMode .parallel [[2]] [[2]] := by decide end SmokeTest -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/OptimalityTheory/Doubling.lean b/Linglib/Phonology/OptimalityTheory/Doubling.lean index 6868c5c5d..75f8cba57 100644 --- a/Linglib/Phonology/OptimalityTheory/Doubling.lean +++ b/Linglib/Phonology/OptimalityTheory/Doubling.lean @@ -1,4 +1,5 @@ -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Phonology.OptimalityTheory.Constraints import Linglib.Morphology.MorphProfile @@ -41,10 +42,10 @@ reduplication for other functions while excluding *f*). [berent-2026] -/ -namespace Phonology.Doubling +namespace OptimalityTheory.Doubling -open Phonology.Constraint.OT -open Phonology.Constraints +open Constraint OptimalityTheory +open OptimalityTheory -- ============================================================================ -- § 1: Doubling Functions @@ -374,4 +375,4 @@ theorem doubling_reversal : = {.reduplication} := by exact ⟨phon_prefers_XY, morph_prefers_reduplication⟩ -end Phonology.Doubling +end OptimalityTheory.Doubling diff --git a/Linglib/Phonology/Constraint/OT/ElementaryRankingCondition.lean b/Linglib/Phonology/OptimalityTheory/ElementaryRankingCondition.lean similarity index 99% rename from Linglib/Phonology/Constraint/OT/ElementaryRankingCondition.lean rename to Linglib/Phonology/OptimalityTheory/ElementaryRankingCondition.lean index 3331b710c..4cc5f8fbd 100644 --- a/Linglib/Phonology/Constraint/OT/ElementaryRankingCondition.lean +++ b/Linglib/Phonology/OptimalityTheory/ElementaryRankingCondition.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.OT.Aliases +import Linglib.Phonology.Constraint.Aliases import Mathlib.GroupTheory.Perm.Basic import Mathlib.Data.Sign.Basic import Mathlib.Data.Fintype.Perm @@ -43,7 +43,8 @@ some `W`-constraint ([prince-2002] §0 (3)/(4)). open Core.Optimization.Evaluation -namespace Phonology.Constraint.OT +namespace OptimalityTheory +open Constraint variable {n : ℕ} @@ -386,4 +387,4 @@ theorem simpleERC_consistent {i j : Fin n} (hij : i ≠ j) : rw [Equiv.symm_swap, Equiv.swap_apply_left, Equiv.swap_apply_right] exact hgt -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/Constraint/OT/EvalMode.lean b/Linglib/Phonology/OptimalityTheory/EvalMode.lean similarity index 98% rename from Linglib/Phonology/Constraint/OT/EvalMode.lean rename to Linglib/Phonology/OptimalityTheory/EvalMode.lean index 320c2fb4e..c513fb3bd 100644 --- a/Linglib/Phonology/Constraint/OT/EvalMode.lean +++ b/Linglib/Phonology/OptimalityTheory/EvalMode.lean @@ -1,5 +1,5 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.OT.Aliases +import Linglib.Phonology.Constraint.Aliases /-! # OT — Evaluation Mode (Parallel vs Directional) @@ -72,7 +72,8 @@ by `HarmonicSerialism.lean`'s combinator, which currently routes the `DirectionalTableau` consumer lands when a study file requires it. -/ -namespace Phonology.Constraint.OT +namespace OptimalityTheory +open Constraint /-- Direction of lex comparison on violation position vectors. @@ -159,4 +160,4 @@ theorem le_singleton (m : EvalMode) (k k' : Nat) : end EvalMode -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/Constraint/OT/HarmonicSerialism.lean b/Linglib/Phonology/OptimalityTheory/HarmonicSerialism.lean similarity index 97% rename from Linglib/Phonology/Constraint/OT/HarmonicSerialism.lean rename to Linglib/Phonology/OptimalityTheory/HarmonicSerialism.lean index 9247e9a91..f737adb9b 100644 --- a/Linglib/Phonology/Constraint/OT/HarmonicSerialism.lean +++ b/Linglib/Phonology/OptimalityTheory/HarmonicSerialism.lean @@ -1,7 +1,7 @@ -import Linglib.Phonology.Constraint.OT.Basic -import Linglib.Phonology.Constraint.OT.EvalMode -import Linglib.Phonology.Constraint.OT.Iteration -import Linglib.Phonology.Constraint.OT.DirectionalTableau +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.EvalMode +import Linglib.Phonology.Constraint.Iteration +import Linglib.Phonology.OptimalityTheory.DirectionalTableau /-! # Harmonic Serialism — The Combinator @@ -57,11 +57,11 @@ reuses `Tableau.optimal` directly. Future directional dispatch silently routing directional callers to the parallel optimum. -/ -namespace Phonology.Constraint.OT +namespace OptimalityTheory +open Constraint open Core.Optimization.Evaluation -open Phonology.Constraint.OT -- ============================================================================ -- § 1: HSDerivation Specification @@ -303,4 +303,4 @@ def derive (D : DirectionalHSDerivation C) (pick : Finset C → Option C) end DirectionalHSDerivation -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/Constraint/OT/Basic.lean b/Linglib/Phonology/OptimalityTheory/Optimality.lean similarity index 66% rename from Linglib/Phonology/Constraint/OT/Basic.lean rename to Linglib/Phonology/OptimalityTheory/Optimality.lean index 9a472a9d3..7de63e15a 100644 --- a/Linglib/Phonology/Constraint/OT/Basic.lean +++ b/Linglib/Phonology/OptimalityTheory/Optimality.lean @@ -1,6 +1,6 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.OT.Aliases -import Mathlib.Computability.Language +import Linglib.Phonology.Constraint.Aliases +import Linglib.Phonology.Constraint.Defs /-! # Optimality Theory — Core Vocabulary @@ -18,116 +18,11 @@ families, named constraints, `mkTableau` for building tableaux from ranked constraint lists, and factorial typology computation. -/ -namespace Phonology.Constraint.OT +namespace OptimalityTheory 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⟩ +open Constraint -- ============================================================================ -- § 3: Permutations (for factorial typology) @@ -346,4 +241,4 @@ def mkFactorialTypologySize {C : Type*} [DecidableEq C] (h : candidates ≠ [] := by decide) : Nat := (mkFactorialOptima candidates constraints h).length -end Phonology.Constraint.OT +end OptimalityTheory diff --git a/Linglib/Phonology/OptimalityTheory/Stratal.lean b/Linglib/Phonology/OptimalityTheory/Stratal.lean index ee0e7a38b..4fa797576 100644 --- a/Linglib/Phonology/OptimalityTheory/Stratal.lean +++ b/Linglib/Phonology/OptimalityTheory/Stratal.lean @@ -1,7 +1,8 @@ import Mathlib.Order.Nat import Mathlib.Data.List.Dedup import Mathlib.Logic.Relation -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Core.Relation.ReflTransGen /-! @@ -49,7 +50,7 @@ otherwise constraint-based framework. Linglib's siblings: ## Connection to Linglib -Each individual stratum is evaluated using `Phonology.Constraint.OT.mkTableau` and +Each individual stratum is evaluated using `OptimalityTheory.mkTableau` and `Tableau.optimal`. This module adds the stratal architecture: strata ordering, cross-stratal chaining, and reranking specification. @@ -59,9 +60,9 @@ Phrase strata derives the *-am*/*-āni* alternation from a single underlying form. -/ -namespace Phonology.Stratal +namespace OptimalityTheory.Stratal -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily mkTableau) +open Constraint OptimalityTheory open Core.Optimization.Evaluation -- ============================================================================ @@ -332,4 +333,4 @@ theorem stem_feeds_word : isOutputFeeding .stem .word := rfl theorem word_feeds_phrase : isOutputFeeding .word .phrase := rfl theorem stem_not_feeds_phrase : ¬ isOutputFeeding .stem .phrase := by decide -end Phonology.Stratal +end OptimalityTheory.Stratal diff --git a/Linglib/Phonology/OptimalityTheory/StratalCorr.lean b/Linglib/Phonology/OptimalityTheory/StratalCorr.lean index 67a92bad9..a02bb26c2 100644 --- a/Linglib/Phonology/OptimalityTheory/StratalCorr.lean +++ b/Linglib/Phonology/OptimalityTheory/StratalCorr.lean @@ -58,9 +58,9 @@ the grammar bridge in shared types — currently `StratalDerivation` and `Corr TCT.Role α` live in non-communicating namespaces. -/ -namespace Phonology.Stratal +namespace OptimalityTheory.Stratal -open Phonology.Correspondence (Corr Side) +open OptimalityTheory.Correspondence (Corr Side) -- ============================================================================ -- § 1: StratalRole — the four salient time-points @@ -159,17 +159,17 @@ def stratalDerivToCorr {α : Type} (input stemOut wordOut phraseOut : List α) : (stratalDerivToCorr input stemOut wordOut phraseOut).form .pOut = phraseOut := rfl -end Phonology.Stratal +end OptimalityTheory.Stratal -- ============================================================================ -- § 4: StratalRole → TCT.Role projection -- ============================================================================ -namespace Phonology.StratalToTCT +namespace OptimalityTheory.StratalToTCT -open Phonology.Correspondence (Corr) -open Phonology.Stratal (StratalRole stratalDerivToCorr parallelEdge) -open Phonology.TCT (Role) +open OptimalityTheory.Correspondence (Corr) +open OptimalityTheory.Stratal (StratalRole stratalDerivToCorr parallelEdge) +open OptimalityTheory.TCT (Role) /-- The canonical projection from stratal roles to TCT roles, encoding Benua's identification: @@ -253,4 +253,4 @@ theorem project_oo_edge_eq_parallel {α : Type} rw [Corr.diagram_edge_pos _ _ (by decide)] rfl -end Phonology.StratalToTCT +end OptimalityTheory.StratalToTCT diff --git a/Linglib/Phonology/OptimalityTheory/TCT.lean b/Linglib/Phonology/OptimalityTheory/TCT.lean index fe9c72f76..abc7133d3 100644 --- a/Linglib/Phonology/OptimalityTheory/TCT.lean +++ b/Linglib/Phonology/OptimalityTheory/TCT.lean @@ -1,5 +1,6 @@ import Linglib.Phonology.OptimalityTheory.Correspondence -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Transderivational Correspondence Theory (TCT) @@ -57,10 +58,10 @@ within-paradigm OO-Faith) lives in `ParadigmUniformity/Transderivational.lean`. -/ -namespace Phonology.TCT +namespace OptimalityTheory.TCT -open Phonology.Correspondence (Corr) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open OptimalityTheory.Correspondence (Corr) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: TCT Roles @@ -207,4 +208,4 @@ theorem TetruSchema.oo_decides_when_m1_ties {C : Type} (s : TetruSchema C) (hOO : s.ooIdent.eval cand₁ < s.ooIdent.eval cand₂) : s.ooIdent.eval cand₁ < s.ooIdent.eval cand₂ := hOO -end Phonology.TCT +end OptimalityTheory.TCT diff --git a/Linglib/Phonology/ParadigmUniformity/Antifaithfulness.lean b/Linglib/Phonology/ParadigmUniformity/Antifaithfulness.lean index 4a5345ded..d009902e9 100644 --- a/Linglib/Phonology/ParadigmUniformity/Antifaithfulness.lean +++ b/Linglib/Phonology/ParadigmUniformity/Antifaithfulness.lean @@ -1,5 +1,6 @@ import Linglib.Phonology.OptimalityTheory.Correspondence -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Antifaithfulness — Alderete 2001 @@ -46,8 +47,8 @@ counts pairs where they *differ*. Together they partition the edge: namespace Phonology.ParadigmUniformity.Antifaithfulness -open Phonology.Correspondence (Corr) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open OptimalityTheory.Correspondence (Corr) +open Constraint OptimalityTheory variable {Role : Type*} {α : Type*} @@ -89,11 +90,11 @@ theorem antifaith_plus_ident_eq_edge_card [DecidableEq α] achieves *maximum* antifaith violations: every paired position counts. -/ theorem identity_antifaith_max [DecidableEq α] (s : List α) : antifaithViol (Corr.identity s) - Phonology.Correspondence.Side.lhs - Phonology.Correspondence.Side.rhs = s.length := by + OptimalityTheory.Correspondence.Side.lhs + OptimalityTheory.Correspondence.Side.rhs = s.length := by have hAdd := antifaith_plus_ident_eq_edge_card (Corr.identity s) - Phonology.Correspondence.Side.lhs - Phonology.Correspondence.Side.rhs + OptimalityTheory.Correspondence.Side.lhs + OptimalityTheory.Correspondence.Side.rhs rw [Corr.identity_ident_zero, Nat.add_zero] at hAdd rw [hAdd] simp only [Corr.identity, Corr.parallel_edge_lhs_rhs] diff --git a/Linglib/Phonology/ParadigmUniformity/Defs.lean b/Linglib/Phonology/ParadigmUniformity/Defs.lean index 8a058511a..6eb6bb24f 100644 --- a/Linglib/Phonology/ParadigmUniformity/Defs.lean +++ b/Linglib/Phonology/ParadigmUniformity/Defs.lean @@ -1,4 +1,5 @@ -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Paradigm Uniformity — generic lift combinators @@ -46,7 +47,7 @@ which pairing best fits Japanese velar nasalisation. namespace Phonology.ParadigmUniformity -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Generic lift combinators diff --git a/Linglib/Phonology/ParadigmUniformity/LexicalConservatism.lean b/Linglib/Phonology/ParadigmUniformity/LexicalConservatism.lean index 80bc1f84e..2de5bd58e 100644 --- a/Linglib/Phonology/ParadigmUniformity/LexicalConservatism.lean +++ b/Linglib/Phonology/ParadigmUniformity/LexicalConservatism.lean @@ -55,8 +55,8 @@ without auxiliary stipulation; LC handles it by paradigm membership. namespace Phonology.ParadigmUniformity -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) -open Phonology.Correspondence (Corr) +open Constraint OptimalityTheory +open OptimalityTheory.Correspondence (Corr) -- ============================================================================ -- § 1: Anchored paradigm diff --git a/Linglib/Phonology/ParadigmUniformity/OptimalParadigms.lean b/Linglib/Phonology/ParadigmUniformity/OptimalParadigms.lean index a6c389146..47e43e860 100644 --- a/Linglib/Phonology/ParadigmUniformity/OptimalParadigms.lean +++ b/Linglib/Phonology/ParadigmUniformity/OptimalParadigms.lean @@ -42,8 +42,8 @@ that phonological behavior tracks paradigm structure. See namespace Phonology.ParadigmUniformity -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) -open Phonology.Correspondence (Corr) +open Constraint OptimalityTheory +open OptimalityTheory.Correspondence (Corr) -- ============================================================================ -- § 1: OP-MAX-V derived from `Corr.maxViol` via tier projection diff --git a/Linglib/Phonology/ParadigmUniformity/Transderivational.lean b/Linglib/Phonology/ParadigmUniformity/Transderivational.lean index 95173ef80..6ae57d599 100644 --- a/Linglib/Phonology/ParadigmUniformity/Transderivational.lean +++ b/Linglib/Phonology/ParadigmUniformity/Transderivational.lean @@ -1,6 +1,7 @@ import Linglib.Phonology.OptimalityTheory.Correspondence import Linglib.Phonology.OptimalityTheory.TCT -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Transderivational Paradigm Uniformity — Benua 1997 @@ -33,9 +34,9 @@ base-priority), which is captured in `TCT.TCTGrammar`'s type signatures. namespace Phonology.ParadigmUniformity.Transderivational -open Phonology.Correspondence (Corr) -open Phonology.TCT (Role) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open OptimalityTheory.Correspondence (Corr) +open OptimalityTheory.TCT (Role) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: TCT Diagram constructors diff --git a/Linglib/Phonology/Prosodic/Templates.lean b/Linglib/Phonology/Prosodic/Templates.lean index c32a2d8c5..238ee6e28 100644 --- a/Linglib/Phonology/Prosodic/Templates.lean +++ b/Linglib/Phonology/Prosodic/Templates.lean @@ -32,8 +32,8 @@ the first place — the central analytical move of [faust-2026] §4. namespace Phonology.Templates open Morphology -open Phonology.Constraint.OT (NamedConstraint) -open Phonology.Constraints (mkAlign) +open Constraint OptimalityTheory +open OptimalityTheory (mkAlign) -- ============================================================================ -- § 1: CV Slots @@ -333,7 +333,7 @@ theorem intrusionLicensed_with_intruder (m : RootTemplateMatch α) /-- The \*Misalignment constraint of [faust-2026] (2): a markedness constraint that fires on `RootTemplateMatch` candidates whose `isMisaligned` predicate holds. Built via the generic `mkAlign` - constructor from `Phonology.Constraints`. -/ + constructor from `OptimalityTheory`. -/ def starMisalign {α : Type} : NamedConstraint (RootTemplateMatch α) := mkAlign "*Misalign" fun m => RootTemplateMatch.isMisaligned m = true @@ -348,7 +348,7 @@ theorem starMisalign_is_markedness {α : Type} : violates \*Misalign, and the grammar prefers the FILL-violating candidate. -/ def fill {α : Type} : NamedConstraint (RootTemplateMatch α) := - Phonology.Constraints.mkMark "FILL" + OptimalityTheory.mkMark "FILL" (fun m => RootTemplateMatch.allCSlotsFilled m = false) /-- FILL is classified as markedness. -/ @@ -358,7 +358,7 @@ theorem fill_is_markedness {α : Type} : /-- NoCross ([goldsmith-1976]): a markedness constraint penalizing candidates whose intruder associations cross root associations. -/ def noCross {α : Type} : NamedConstraint (RootTemplateMatch α) := - Phonology.Constraints.mkMark "NoCross" + OptimalityTheory.mkMark "NoCross" (fun m => RootTemplateMatch.violatesNCC m = true) /-- NoCross is classified as markedness. -/ diff --git a/Linglib/Phonology/Subregular/Agree.lean b/Linglib/Phonology/Subregular/Agree.lean index eb263b272..16ddcc043 100644 --- a/Linglib/Phonology/Subregular/Agree.lean +++ b/Linglib/Phonology/Subregular/Agree.lean @@ -37,10 +37,10 @@ downstream consumers reference. namespace Phonology.Subregular -open Phonology.Constraints +open OptimalityTheory open Core Core.Computability.Subregular --- `α : Type` (rather than `Type*`) is forced by `Phonology.Constraints` +-- `α : Type` (rather than `Type*`) is forced by `OptimalityTheory` -- and `Core.Optimization.eval`, which are monomorphic in universe 0. See -- the parallel comment in `OCP.lean`. variable {α : Type} diff --git a/Linglib/Phonology/Subregular/ForbidPairs.lean b/Linglib/Phonology/Subregular/ForbidPairs.lean index 9abe21bf1..a723b33ba 100644 --- a/Linglib/Phonology/Subregular/ForbidPairs.lean +++ b/Linglib/Phonology/Subregular/ForbidPairs.lean @@ -24,7 +24,7 @@ corollary. namespace Phonology.Subregular -open Phonology.Constraints +open OptimalityTheory open Core Core.Computability.Subregular variable {α : Type} diff --git a/Linglib/Phonology/Subregular/OCP.lean b/Linglib/Phonology/Subregular/OCP.lean index 7ba9e69b7..e27b431da 100644 --- a/Linglib/Phonology/Subregular/OCP.lean +++ b/Linglib/Phonology/Subregular/OCP.lean @@ -46,10 +46,10 @@ formalisations but the constraint and a retraction onto it, both characterising namespace Phonology.Subregular -open Phonology.Constraints +open OptimalityTheory open Core Core.Computability.Subregular --- `α : Type` (rather than `Type*`) is forced by `Phonology.Constraints` +-- `α : Type` (rather than `Type*`) is forced by `OptimalityTheory` -- and `Core.Optimization.eval`, which are monomorphic in universe 0. variable {α : Type} @@ -107,7 +107,7 @@ theorem mkOCPOnTier_zero_iff_isClean [DecidableEq α] {C : Type} /-- **Shared satisfaction predicate** (off-tier): the optimality-theoretic OCP markedness constraint `mkOCP` scores zero iff its projection is -`Phonology.OCP.IsClean` — routing `Phonology.Constraints.adjacentIdentical` (the +`Phonology.OCP.IsClean` — routing `OptimalityTheory.adjacentIdentical` (the `countAdjacent` form behind `mkOCP`, consumed by Berent2026/Belth2026) through the unified predicate. The flat-string companion of `mkOCPOnTier_zero_iff_isClean`. -/ theorem mkOCP_zero_iff_isClean {C : Type} [DecidableEq α] diff --git a/Linglib/Phonology/Subregular/OTBound.lean b/Linglib/Phonology/Subregular/OTBound.lean index ab8d5b84f..cf943ab00 100644 --- a/Linglib/Phonology/Subregular/OTBound.lean +++ b/Linglib/Phonology/Subregular/OTBound.lean @@ -53,9 +53,9 @@ subregular hierarchy. namespace Phonology.Subregular.OTBound -open Phonology.Constraints +open OptimalityTheory open Core Core.Computability.Subregular -open Phonology.Constraint.OT (NamedConstraint mkMarkGrad) +open Constraint OptimalityTheory -- ============================================================================ -- § 2. Existing bridges, restated in zero-set form diff --git a/Linglib/Phonology/Tone/Constraints.lean b/Linglib/Phonology/Tone/Constraints.lean index 9b806d5b7..bc0c9cd80 100644 --- a/Linglib/Phonology/Tone/Constraints.lean +++ b/Linglib/Phonology/Tone/Constraints.lean @@ -1,5 +1,5 @@ import Linglib.Phonology.Autosegmental.Floating -import Linglib.Phonology.Constraint.OT.DirectionalTableau +import Linglib.Phonology.OptimalityTheory.DirectionalTableau /-! # Tonal Constraints — Generic Constructors over `FloatingForm` @@ -39,7 +39,7 @@ namespace Phonology.Tone open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) -open Phonology.Constraint.OT (DirectionalConstraint ConstraintFamily) +open Constraint OptimalityTheory variable {S : Type} [DecidableEq S] diff --git a/Linglib/Pragmatics/Bidirectional.lean b/Linglib/Pragmatics/Bidirectional.lean index 7a190d9ca..211a4acab 100644 --- a/Linglib/Pragmatics/Bidirectional.lean +++ b/Linglib/Pragmatics/Bidirectional.lean @@ -1,5 +1,5 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.Superoptimal +import Linglib.Pragmatics.Superoptimal /-! # Bidirectional Optimality Theory @@ -78,7 +78,7 @@ set_option autoImplicit false namespace Pragmatics.Bidirectional open Core.Optimization.Evaluation -open Phonology.Constraint +open Constraint -- ============================================================================ -- § 1: Q-Principle and I-Principle as Bool Predicates (List-based, decidable) diff --git a/Linglib/Phonology/Constraint/Superoptimal.lean b/Linglib/Pragmatics/Superoptimal.lean similarity index 99% rename from Linglib/Phonology/Constraint/Superoptimal.lean rename to Linglib/Pragmatics/Superoptimal.lean index 4c3725b99..f2481805a 100644 --- a/Linglib/Phonology/Constraint/Superoptimal.lean +++ b/Linglib/Pragmatics/Superoptimal.lean @@ -1,5 +1,5 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.OT.Aliases +import Linglib.Phonology.Constraint.Aliases import Mathlib.Order.FixedPoints import Mathlib.Order.Preorder.Finite /-! @@ -32,7 +32,7 @@ pair via blocking. The maximality direction goes through the `LexNatList` preorder from `Core/Optimization/Evaluation.lean`. -/ -namespace Phonology.Constraint +namespace Pragmatics.Bidirectional open Core.Optimization.Evaluation @@ -478,4 +478,4 @@ theorem strongOptimal_subset_superoptimal rw [← superoptimal_coe_eq_set _ _ h_converged] at hp_gfp rwa [Finset.mem_coe] at hp_gfp -end Phonology.Constraint +end Pragmatics.Bidirectional diff --git a/Linglib/Semantics/Presupposition/MaximizePresupposition.lean b/Linglib/Semantics/Presupposition/MaximizePresupposition.lean index 780d93a6f..a66a84c81 100644 --- a/Linglib/Semantics/Presupposition/MaximizePresupposition.lean +++ b/Linglib/Semantics/Presupposition/MaximizePresupposition.lean @@ -1,5 +1,6 @@ import Linglib.Features.ContainmentPair -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Semantics.Presupposition.PhiFeatures /-! @@ -68,8 +69,7 @@ set_option autoImplicit false namespace Semantics.Presupposition.MaximizePresupposition open Features (ContainmentPair) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily mkTableau - mkTableau_optimal_zero_first mkTableau_optimal_mem) +open Constraint OptimalityTheory open Core.Optimization.Evaluation open Semantics.Presupposition.PhiFeatures diff --git a/Linglib/Studies/AfkirZellou2025.lean b/Linglib/Studies/AfkirZellou2025.lean index 34e7b26f2..7fe08c4e0 100644 --- a/Linglib/Studies/AfkirZellou2025.lean +++ b/Linglib/Studies/AfkirZellou2025.lean @@ -57,10 +57,10 @@ paper notes these as partly idiosyncratic (Table 7). namespace AfkirZellou2025 -open Core.Optimization Phonology.Constraint Phonology.Constraints +open Core.Optimization Constraint OptimalityTheory open Phonology.Syllable open Tarifit.Inventory -open Core.Optimization Phonology.Constraint.OT +open Core.Optimization Constraint OptimalityTheory -- ============================================================================ -- § 1: Surface Forms and Candidates @@ -342,7 +342,7 @@ theorem faithful_disjoint (c : TarifitCandidate) (h : c.surface = .faithful) : -- ============================================================================ /-! [afkir-zellou-2025]'s MaxEnt grammar realised through the -generic `ConstraintSystem` API in `Phonology.Constraint.System`. The same +generic `ConstraintSystem` API in `Constraint.System`. The same softmax decoder used for English onset phonotactics (`HayesWilson2008.onsetSystem`), French hiatus resolution (`Storme2026.stormeSystem`), and AAVE t/d-deletion @@ -350,7 +350,7 @@ softmax decoder used for English onset phonotactics section PredictAPI -open Phonology.Constraint Core.Optimization Phonology.Constraint.OT +open Constraint Core.Optimization Constraint OptimalityTheory instance : Fintype SurfaceForm where elems := {.faithful, .intrusive, .vowelless} diff --git a/Linglib/Studies/Aissen2003.lean b/Linglib/Studies/Aissen2003.lean index af35253e6..e9ce8595c 100644 --- a/Linglib/Studies/Aissen2003.lean +++ b/Linglib/Studies/Aissen2003.lean @@ -41,7 +41,7 @@ to a possible OT grammar. namespace Aissen2003 open Features.Prominence -open Phonology.Constraint.OT Phonology.Constraints +open Constraint OptimalityTheory OptimalityTheory open Core.Optimization.Evaluation (Finset.checkAll Finset.checkAny) diff --git a/Linglib/Studies/Aitha2026.lean b/Linglib/Studies/Aitha2026.lean index aaebca340..5a859e137 100644 --- a/Linglib/Studies/Aitha2026.lean +++ b/Linglib/Studies/Aitha2026.lean @@ -53,7 +53,7 @@ Telugu nouns exhibit two stem alternation patterns: namespace Aitha2026 -open Core Phonology.Constraint.OT Core.Optimization Core.Optimization.Evaluation +open Core Constraint OptimalityTheory Core.Optimization Core.Optimization.Evaluation open Morphology.DM.VI open Phonology.Syllable @@ -497,7 +497,7 @@ theorem stem_optimal : section WordLevel -open Phonology.Stratal +open OptimalityTheory.Stratal open Phonology.ProsodicWord -- ──────────────────────────────────────────────────────────────────── @@ -700,7 +700,7 @@ repaired by compensatory lengthening. -/ section PhraseLevel -open Phonology.Stratal +open OptimalityTheory.Stratal /-- Phrase-level candidates for the postpositional input `('sa.mu).('dram).('nun).('ci)` ('ocean-from'), the Word-level @@ -765,7 +765,7 @@ representations at each level. -/ section StratalRecords -open Phonology.Stratal +open OptimalityTheory.Stratal /-- The Stratal-OT derivation of NOM `samudram` 'ocean-NOM'. @@ -821,7 +821,7 @@ so the same-`C` `isPromoted`/`isDemoted` would not typecheck. -/ section CrossStratumReranking -open Phonology.Stratal +open OptimalityTheory.Stratal /-- `*DIST-0` is at the *highest* rank in the Word DAT ranking (`wordDatRanking`, position 0) and at a *lower* rank in the Phrase @@ -831,13 +831,13 @@ open Phonology.Stratal m-retention at phrase boundaries vs m-deletion + CL inside the prosodic word. -/ theorem dist0_demoted_phrase_relative_to_word : - Phonology.Stratal.isDemotedAcross "*DIST-0" phrasePostpRanking wordDatRanking := by + OptimalityTheory.Stratal.isDemotedAcross "*DIST-0" phrasePostpRanking wordDatRanking := by decide /-- Conversely, `MAX` is **promoted** going Word → Phrase. Dual aspect of the same reranking. -/ theorem max_promoted_phrase_relative_to_word : - Phonology.Stratal.isPromotedAcross "MAX" phrasePostpRanking wordDatRanking := by + OptimalityTheory.Stratal.isPromotedAcross "MAX" phrasePostpRanking wordDatRanking := by decide end CrossStratumReranking @@ -1020,7 +1020,7 @@ end MoraicCLConnection becomes a probability-1 claim per stratum. -/ section PredictAPI -open Core.Optimization Phonology.Constraint +open Core.Optimization Constraint /-- Stem-level metrical parse tableau as a generic `ConstraintSystem`. -/ noncomputable def stemSystem : ConstraintSystem StemCandidate (LexProfile Nat 3) := diff --git a/Linglib/Studies/AkinboFwangwar2026.lean b/Linglib/Studies/AkinboFwangwar2026.lean index 4f7de05be..4bf632096 100644 --- a/Linglib/Studies/AkinboFwangwar2026.lean +++ b/Linglib/Studies/AkinboFwangwar2026.lean @@ -6,7 +6,7 @@ import Linglib.Phonology.Autosegmental.Floating import Linglib.Phonology.Autosegmental.BasemapCorrespondence import Linglib.Phonology.OptimalityTheory.CophonologyTheory import Linglib.Phonology.Tone.Constraints -import Linglib.Phonology.Constraint.OT.HarmonicSerialism +import Linglib.Phonology.OptimalityTheory.HarmonicSerialism import Linglib.Studies.Hyman2006 /-! @@ -71,7 +71,7 @@ anchor combinators defined in §2 below. namespace AkinboFwangwar2026 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (integrityTone) @@ -745,7 +745,7 @@ section DominantCophAgreement open Phonology.Autosegmental.GrammaticalTone (TBU Spec tonalOverwrite) open Phonology.Autosegmental.BasemapCorrespondence -open Phonology.CophonologyTheory (mergeRanking cophonologicalEval) +open OptimalityTheory.CophonologyTheory (mergeRanking cophonologicalEval) /-- **The general agreement theorem**: when MxBM-C (basemap faithfulness) is in the cophonological subranking, every OT-optimal candidate is diff --git a/Linglib/Studies/Anttila1997.lean b/Linglib/Studies/Anttila1997.lean index 268ffbbff..29e93a174 100644 --- a/Linglib/Studies/Anttila1997.lean +++ b/Linglib/Studies/Anttila1997.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.PartiallyOrderedConstraints +import Linglib.Phonology.HarmonicGrammar.PartiallyOrderedConstraints import Linglib.Core.Optimization.PermSubsetCombinatorics import Mathlib.Tactic.NormNum @@ -103,7 +103,7 @@ consumers. namespace Anttila1997 -open Core.Optimization Phonology.Constraint.PartialOrderConstraints +open Core.Optimization HarmonicGrammar.PartialOrderConstraints /-! ## § 0: Variant type — strong vs weak genitive plural -/ diff --git a/Linglib/Studies/ArnoldEtAl2000.lean b/Linglib/Studies/ArnoldEtAl2000.lean index 11f9bf5f1..7f97084c4 100644 --- a/Linglib/Studies/ArnoldEtAl2000.lean +++ b/Linglib/Studies/ArnoldEtAl2000.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.MaxEnt +import Linglib.Phonology.HarmonicGrammar.MaxEnt import Linglib.Phonology.Constraint.Weighted import Linglib.Features.Givenness import Linglib.Syntax.DependencyGrammar.Formal.DependencyLength @@ -68,7 +68,7 @@ contradicting the paper's findings. ## Bridges -- `Phonology.Constraint.MaxEntGrammar` — the grammar packages as a generic +- `HarmonicGrammar.MaxEntGrammar` — the grammar packages as a generic MaxEnt grammar (`maxEntGrammar`), making the softmax probability machinery available without redefinition. - `Features.BinaryGivenness` — discourse-status partition. The paper @@ -101,7 +101,7 @@ contradicting the paper's findings. namespace ArnoldEtAl2000 -open Phonology.Constraint.OT Core.Optimization Phonology.Constraint Features +open Constraint OptimalityTheory Core.Optimization Constraint HarmonicGrammar Features open DepGrammar DepGrammar.DependencyLength -- ============================================================================ diff --git a/Linglib/Studies/Beaver2004.lean b/Linglib/Studies/Beaver2004.lean index 6cb1283ce..7c895eb76 100644 --- a/Linglib/Studies/Beaver2004.lean +++ b/Linglib/Studies/Beaver2004.lean @@ -1,7 +1,8 @@ import Linglib.Discourse.Centering.Basic import Linglib.Discourse.Centering.Rule1 import Linglib.Discourse.Centering.Instances.GrammaticalRole -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # [beaver-2004]: The Optimization of Discourse Anaphora @@ -83,7 +84,7 @@ set_option autoImplicit false namespace Beaver2004 -open Discourse.Centering Phonology.Constraint.OT Core.Optimization.Evaluation +open Discourse.Centering Constraint OptimalityTheory Core.Optimization.Evaluation -- ════════════════════════════════════════════════════ -- § 1. Candidate type @@ -569,7 +570,7 @@ def d12_profile_l_eq_j : ViolationProfile 6 := OT optimization mechanism (lex-min on Nat-vector profiles) picks `cand_l_eq_i` as the unique optimal candidate. This is the kernel-checked OT-mechanism witness, exercising the - `Phonology.Constraint.OT` substrate's `mkProfile` / + `Constraint` substrate's `mkProfile` / `ViolationProfile.LinearOrder` infrastructure. -/ theorem d12_lex_picks_l_eq_i : d12_profile_l_eq_i < d12_profile_l_eq_j := by decide diff --git a/Linglib/Studies/Belth2026.lean b/Linglib/Studies/Belth2026.lean index 79e03ed9c..8370b167e 100644 --- a/Linglib/Studies/Belth2026.lean +++ b/Linglib/Studies/Belth2026.lean @@ -2,7 +2,7 @@ import Linglib.Phonology.Subregular.TierRule import Linglib.Phonology.OptimalityTheory.Constraints import Linglib.Phonology.Subregular.OCP import Linglib.Studies.Yang2016 -import Linglib.Phonology.Constraint.OT.ElementaryRankingCondition +import Linglib.Phonology.OptimalityTheory.ElementaryRankingCondition import Linglib.Core.Computability.Subregular.Tier import Linglib.Core.Computability.Subregular.Multitier @@ -56,7 +56,7 @@ This study formalizes: consonant tier in the [lambert-2022]/[heinz-rawal-tanner-2011] TSL formalism; - an OCP-on-tier OT constraint (`latinOCP`, via - `Phonology.Constraints.mkOCPOnTier`) and an OT tableau bridge: each + `OptimalityTheory.mkOCPOnTier`) and an OT tableau bridge: each empirical contrast becomes a winner-loser pair, `tableauERC` extracts the Elementary Ranking Condition ([merchant-riggle-2016]), and the OT analysis is shown to track the rule-based analysis exactly, @@ -322,16 +322,16 @@ def latinTSLGrammar : Core.Computability.Subregular.TSLGrammar 2 LatSeg := /-- Belth's tier-based dissimilation has a natural OCP twin: surface forms produced by the rule should not contain adjacent `[+lat]` segments on the consonant tier. We expose this connection via - `Phonology.Constraints.mkOCPOnTier`, which already accepts a generic + `OptimalityTheory.mkOCPOnTier`, which already accepts a generic `Core.Tier`. A tier-adjacent pair of identical liquids contributes one violation. -/ -def latinOCP : Phonology.Constraint.OT.NamedConstraint (List LatSeg) := - Phonology.Constraints.mkOCPOnTier "OCP/[+cons]" LatSeg.consTier id +def latinOCP : Constraint.NamedConstraint (List LatSeg) := + OptimalityTheory.mkOCPOnTier "OCP/[+cons]" LatSeg.consTier id /-- The OCP constraint is a markedness constraint by construction. -/ theorem latinOCP_is_markedness : - latinOCP.family = Phonology.Constraint.OT.ConstraintFamily.markedness := - Phonology.Constraints.mkOCPOnTier_is_markedness _ _ _ + latinOCP.family = Constraint.ConstraintFamily.markedness := + OptimalityTheory.mkOCPOnTier_is_markedness _ _ _ /-- The OCP-on-tier evaluation of `latinOCP` on a candidate is zero iff that candidate is in `latinTSLGrammar.lang`. Specialization of @@ -354,7 +354,7 @@ theorem latinOCP_zero_iff_in_TSL (c : List LatSeg) : is unrankable — its ERC is contradictory (no W, one L), recapitulating the rule's empirical limit. -/ -open Phonology.Constraint.OT +open Constraint OptimalityTheory /-- Substitute `val` for every `L` in a candidate string. The two surface candidates for an underlying form are `substL .l ur` and diff --git a/Linglib/Studies/Benua1997.lean b/Linglib/Studies/Benua1997.lean index 931fe2674..d95bcd48e 100644 --- a/Linglib/Studies/Benua1997.lean +++ b/Linglib/Studies/Benua1997.lean @@ -3,7 +3,8 @@ import Linglib.Phonology.OptimalityTheory.TCT import Linglib.Phonology.OptimalityTheory.Stratal import Linglib.Phonology.OptimalityTheory.StratalCorr import Linglib.Phonology.ParadigmUniformity.Transderivational -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Benua 1997 — Misapplication Unification @@ -63,11 +64,11 @@ machinery — the cross-linguistic point of [benua-1997] is that namespace Benua1997 -open Phonology.Correspondence (Corr) -open Phonology.TCT (Role TetruSchema) +open OptimalityTheory.Correspondence (Corr) +open OptimalityTheory.TCT (Role TetruSchema) open Phonology.ParadigmUniformity.Transderivational (diagramWithEdge identOOViol) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Shared Segmental Inventory @@ -423,8 +424,8 @@ the architecturally-distinct derivations producing identical phraseOutput. namespace StratalComparison -open Phonology.Stratal (StratalDerivation StratalRole stratalDerivToCorr) -open Phonology.StratalToTCT (project project_preserves_phrase_as_derivative +open OptimalityTheory.Stratal (StratalDerivation StratalRole stratalDerivToCorr) +open OptimalityTheory.StratalToTCT (project project_preserves_phrase_as_derivative project_preserves_stem_as_base project_preserves_underlying_as_input project_oo_edge_eq_parallel) @@ -502,7 +503,7 @@ theorem stratal_stem_is_tct_base : `(.base, .derivative)` correspondence. -/ theorem stratal_chain_collapses_to_oo_edge : sundaneseStratalAsTCT.edge .base .derivative = - Phonology.Stratal.parallelEdge Sundanese.baseOutput + OptimalityTheory.Stratal.parallelEdge Sundanese.baseOutput Sundanese.derivOutputOverapplied := project_oo_edge_eq_parallel _ _ _ _ diff --git a/Linglib/Studies/Berent2026.lean b/Linglib/Studies/Berent2026.lean index 708b46524..7a2829952 100644 --- a/Linglib/Studies/Berent2026.lean +++ b/Linglib/Studies/Berent2026.lean @@ -52,12 +52,12 @@ data supporting the doubling reversal is in -/ open Phonology.Syllable (SonorityRank) -open Phonology.Constraints -open Phonology.Doubling +open OptimalityTheory +open OptimalityTheory.Doubling namespace Berent2026 -open Core.Optimization Phonology.Constraint.OT +open Core.Optimization Constraint OptimalityTheory -- ============================================================================ -- § 1: Onset Markedness — the sonority gradient @@ -162,7 +162,7 @@ theorem ocp_passes_ab {α : Type} [DecidableEq α] (a b : α) (rest : List α) This is the core of [berent-2026]'s third argument: the reversal is amodal (it transfers from speech to sign) and L1-dependent (it depends on the speaker's morphological system). - See `Phonology.Doubling.doubling_reversal` for the proof + See `OptimalityTheory.Doubling.doubling_reversal` for the proof and [berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016] for the experimental evidence. -/ theorem amodal_doubling_reversal : @@ -183,7 +183,7 @@ probability-1 reversal: the same OCP-XX assigns probability 1 to morphological contexts. -/ section PredictAPI -open Core.Optimization Phonology.Constraint +open Core.Optimization Constraint /-- Phonological-context tableau as a generic `ConstraintSystem`. -/ noncomputable def phonSystem : ConstraintSystem DoublingParse (LexProfile Nat 2) := diff --git a/Linglib/Studies/BerentEtAl2016.lean b/Linglib/Studies/BerentEtAl2016.lean index a5568f388..281c80452 100644 --- a/Linglib/Studies/BerentEtAl2016.lean +++ b/Linglib/Studies/BerentEtAl2016.lean @@ -48,11 +48,11 @@ Hebrew and proves the four cells of the dissociation table as OT theorems. [berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016] -/ -open Phonology.Doubling +open OptimalityTheory.Doubling namespace BerentEtAl2016 -open Phonology.Constraint.OT +open Constraint OptimalityTheory -- ============================================================================ -- § 1: L1 Morphological Grammars diff --git a/Linglib/Studies/Blutner2000.lean b/Linglib/Studies/Blutner2000.lean index c8f4180d2..5a00fac48 100644 --- a/Linglib/Studies/Blutner2000.lean +++ b/Linglib/Studies/Blutner2000.lean @@ -1,5 +1,5 @@ import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.Superoptimal +import Linglib.Pragmatics.Superoptimal import Linglib.Pragmatics.Bidirectional import Linglib.Semantics.Presupposition.Accommodation @@ -69,7 +69,7 @@ set_option autoImplicit false namespace Blutner2000 open Core.Optimization.Evaluation -open Phonology.Constraint +open Constraint Pragmatics.Bidirectional -- ============================================================================ -- § 1: Projection Sites diff --git a/Linglib/Studies/BreissKatsudaKawahara2026.lean b/Linglib/Studies/BreissKatsudaKawahara2026.lean index f7a6b74a4..c6d2393cc 100644 --- a/Linglib/Studies/BreissKatsudaKawahara2026.lean +++ b/Linglib/Studies/BreissKatsudaKawahara2026.lean @@ -125,7 +125,7 @@ open Phonology.ParadigmUniformity (liftPairwise lcParadigm mkLCFaith lc_unanchor open Morphology.WugTest (Attestation HasFactor HasAttestation HasFrequency Rate NovelShowsFreqGradient NovelInvariantInFrequency novelGradient_inconsistent_with_invariance) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Real lexical entries from the paper diff --git a/Linglib/Studies/CoetzeePater2011.lean b/Linglib/Studies/CoetzeePater2011.lean index 790f58f4e..64d6427e3 100644 --- a/Linglib/Studies/CoetzeePater2011.lean +++ b/Linglib/Studies/CoetzeePater2011.lean @@ -1,6 +1,6 @@ import Linglib.Phonology.Constraint.Weighted import Linglib.Phonology.Constraint.System -import Linglib.Phonology.Constraint.PartiallyOrderedConstraints +import Linglib.Phonology.HarmonicGrammar.PartiallyOrderedConstraints import Linglib.Core.Optimization.PermSubsetCombinatorics import Linglib.Phonology.OptimalityTheory.Constraints @@ -49,9 +49,9 @@ modeling phonological variation, illustrated with English t/d-deletion. namespace CoetzeePater2011 -open Phonology.Constraint.OT Core.Optimization Core.Optimization.Evaluation -open Core.Optimization Phonology.Constraint -open Phonology.Constraints +open Constraint OptimalityTheory Core.Optimization Core.Optimization.Evaluation +open Core.Optimization Constraint HarmonicGrammar +open OptimalityTheory /-! ### Empirical data (tables 7 and 10) -/ diff --git a/Linglib/Studies/DeHoopMalchukov2008.lean b/Linglib/Studies/DeHoopMalchukov2008.lean index d745d1eec..63876fb34 100644 --- a/Linglib/Studies/DeHoopMalchukov2008.lean +++ b/Linglib/Studies/DeHoopMalchukov2008.lean @@ -1,6 +1,7 @@ -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Core.Optimization.Evaluation -import Linglib.Phonology.Constraint.Superoptimal +import Linglib.Pragmatics.Superoptimal import Linglib.Features.Prominence import Linglib.Studies.Aissen2003 @@ -76,9 +77,9 @@ This derives: DOM ↔ nom-acc, DSM ↔ ergative (p. 580). namespace DeHoopMalchukov2008 -open Phonology.Constraint (superoptimal superoptimalSet +open Pragmatics.Bidirectional (superoptimal superoptimalSet superoptimal_coe_eq_set Blocks) -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Features.Prominence open Aissen2003 open Aissen2003 diff --git a/Linglib/Studies/Erlewine2016.lean b/Linglib/Studies/Erlewine2016.lean index 0a21f7ed2..197f510b8 100644 --- a/Linglib/Studies/Erlewine2016.lean +++ b/Linglib/Studies/Erlewine2016.lean @@ -1,6 +1,7 @@ import Linglib.Fragments.Mayan.Kaqchikel.AgentFocus import Linglib.Syntax.Minimalist.Position -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality /-! # Erlewine 2016: Anti-Locality and Optimality in Kaqchikel Agent Focus @@ -55,7 +56,7 @@ many subsequent papers; [erlewine-2016]'s contribution is the specific application to Kichean AF as an OT-competing-candidate analysis. -### Connection to Phonology.Constraint.OT +### Connection to Constraint The OT tableau uses the lexicographic comparison from `Phonology/Constraint/OT/Basic.lean`. The key result `af_is_optimal` shows @@ -88,7 +89,7 @@ derivation via AF (alternation strategy). Both use namespace Erlewine2016 open Kaqchikel Minimalist -open Phonology.Constraint.OT (mkTableau NamedConstraint ConstraintFamily) +open Constraint OptimalityTheory -- ============================================================================ -- § 1: Competing Derivations diff --git a/Linglib/Studies/Faust2026.lean b/Linglib/Studies/Faust2026.lean index 644e9a28d..49c9318a9 100644 --- a/Linglib/Studies/Faust2026.lean +++ b/Linglib/Studies/Faust2026.lean @@ -60,7 +60,7 @@ This file consumes and exercises the shared infrastructure: `satisfies`. - `Phonology.Templates.starMisalign` — the \*Misalignment alignment constraint, built via the generic `mkAlign` constructor. -- `Phonology.Constraints.adjacentIdentical` — drives the root-level +- `OptimalityTheory.adjacentIdentical` — drives the root-level OCP, used to verify [faust-2026]'s OCP-related reanalysis. Per-derivation `decide` theorems test all four combinations of @@ -671,7 +671,7 @@ Two demonstrations: doing real work — without \*Misalignment dominating, the spreading candidate would win on template-satisfaction grounds. -/ -open Phonology.Constraint.OT (mkTableau mkFactorialOptima) +open Constraint OptimalityTheory /-- The √klj candidate set: the spreading attempt and the empty-slot actual surface form. Built as the `RootTemplateMatch` values from diff --git a/Linglib/Studies/Flemming2021.lean b/Linglib/Studies/Flemming2021.lean index 6c9f03763..c68874008 100644 --- a/Linglib/Studies/Flemming2021.lean +++ b/Linglib/Studies/Flemming2021.lean @@ -1,5 +1,5 @@ -import Linglib.Phonology.Constraint.NoisyHG -import Linglib.Phonology.Constraint.Separability +import Linglib.Phonology.HarmonicGrammar.NoisyHG +import Linglib.Phonology.HarmonicGrammar.Separability import Linglib.Phonology.Constraint.System import Linglib.Core.DecisionTheory.GumbelLuce @@ -53,7 +53,7 @@ under MaxEnt. We encode this data and verify: namespace Flemming2021 -open Core.Optimization Phonology.Constraint Core Real +open Core.Optimization Constraint HarmonicGrammar Core Real -- ============================================================================ -- § 1: MaxEnt as Gumbel RUM (McFadden) diff --git a/Linglib/Studies/GoldwaterJohnson2003.lean b/Linglib/Studies/GoldwaterJohnson2003.lean index 1eb5d2b95..7fcb8b375 100644 --- a/Linglib/Studies/GoldwaterJohnson2003.lean +++ b/Linglib/Studies/GoldwaterJohnson2003.lean @@ -1,5 +1,5 @@ -import Linglib.Phonology.Constraint.Dequantization.OTLimit -import Linglib.Phonology.Constraint.MaxEnt +import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit +import Linglib.Phonology.HarmonicGrammar.MaxEnt import Linglib.Core.Probability.SoftmaxTheory /-! @@ -43,7 +43,7 @@ models over weighted features, differing only in what the features measure. namespace GoldwaterJohnson2003 -open Core.Optimization Phonology.Constraint Core Finset Real +open Core.Optimization Constraint HarmonicGrammar Core Finset Real -- ============================================================================ -- § 1: MaxEnt = softmax (eq (1)) diff --git a/Linglib/Studies/Hansson2010.lean b/Linglib/Studies/Hansson2010.lean index ebc41ba03..88290f4b9 100644 --- a/Linglib/Studies/Hansson2010.lean +++ b/Linglib/Studies/Hansson2010.lean @@ -253,14 +253,14 @@ tier-adjacent disagreeing sibilant pair on the sibilant tier. The OT-side counterpart of `navajoSibilantHarmony` — same tier predicate, packaged as a `NamedConstraint` via the `mkAgreeOnTier` specialization. The TSL grammar characterizes the *language*; this constraint *evaluates* it. -/ -def navajoAgree : Phonology.Constraint.OT.NamedConstraint (List NSeg) := - Phonology.Constraints.mkAgreeOnTier +def navajoAgree : Constraint.NamedConstraint (List NSeg) := + OptimalityTheory.mkAgreeOnTier "AGREE-[ant]/CC" (Tier.byClass NSeg.onTier) id /-- `navajoAgree` is a markedness constraint by construction. -/ theorem navajoAgree_is_markedness : - navajoAgree.family = Phonology.Constraint.OT.ConstraintFamily.markedness := - Phonology.Constraints.mkAgreeOnTier_is_markedness _ _ _ + navajoAgree.family = Constraint.ConstraintFamily.markedness := + OptimalityTheory.mkAgreeOnTier_is_markedness _ _ _ /-- **Bridge**: `navajoAgree` evaluates to zero on a candidate iff the candidate is in the TSL_2 language. The "OT-side" and "subregular-side" diff --git a/Linglib/Studies/Haspelmath2021.lean b/Linglib/Studies/Haspelmath2021.lean index fc8436439..9db527b06 100644 --- a/Linglib/Studies/Haspelmath2021.lean +++ b/Linglib/Studies/Haspelmath2021.lean @@ -82,7 +82,7 @@ namespace Haspelmath2021 open Features.Prominence open Core.Optimization.Evaluation -open Phonology.Constraint +open Constraint Pragmatics.Bidirectional open Aissen2003 open DeHoopMalchukov2008 open Typology.Alignment diff --git a/Linglib/Studies/HayesWilson2008.lean b/Linglib/Studies/HayesWilson2008.lean index 55dd00e79..df1c57dfb 100644 --- a/Linglib/Studies/HayesWilson2008.lean +++ b/Linglib/Studies/HayesWilson2008.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.Dequantization.OTLimit +import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit import Linglib.Phonology.Constraint.System import Linglib.Phonology.Constraint.Weighted import Linglib.Phonology.OptimalityTheory.Constraints @@ -38,8 +38,8 @@ the model assigns higher harmony (= higher MaxEnt probability via namespace HayesWilson2008 -open Phonology Core.Optimization Phonology.Constraint Phonology.Constraints -open Core Core.Optimization Phonology.Constraint.OT Finset Real +open Phonology Core.Optimization Constraint HarmonicGrammar OptimalityTheory +open Core Core.Optimization Constraint OptimalityTheory Finset Real -- ============================================================================ -- § 1: English Onset Constraints (Table (4) subset) @@ -101,7 +101,7 @@ def onsetGrammar : List (WeightedConstraint Onset) := [c1_star_son_dors, c4_star_blank_cont, c5_star_blank_voice, c6_star_son_blank] -- ============================================================================ --- § 2: Harmony Predictions (using harmonyScore from Phonology.Constraint.Weighted) +-- § 2: Harmony Predictions (using harmonyScore from Constraint.Weighted) -- ============================================================================ open English.Phonology in @@ -136,7 +136,7 @@ open English.Phonology /-- **MaxEnt probability ordering**: higher harmony ⟹ higher `exp(harmonyScore)` ⟹ higher MaxEnt probability. - Applies `exp_lt_exp` (Mathlib) to `harmonyScoreR` (Phonology.Constraint.Weighted). -/ + Applies `exp_lt_exp` (Mathlib) to `harmonyScoreR` (Constraint.Weighted). -/ theorem maxent_prob_k_gt_ŋ : exp (harmonyScoreR onsetGrammar [ŋ]) < exp (harmonyScoreR onsetGrammar [k]) := by @@ -160,7 +160,7 @@ end MaxEntProb -- ============================================================================ /-! Phonological MaxEnt is one instance of the framework-agnostic -`ConstraintSystem` abstraction in `Phonology.Constraint.System`. The same +`ConstraintSystem` abstraction in `Constraint.System`. The same `maxEntSystem` constructor that scores phonological onsets here also scores syntactic candidates in HG/MaxEnt syntax models, RSA utterances in soft-max pragmatic listeners, etc. The decoder (`softmaxDecoder 1`) diff --git a/Linglib/Studies/Jaeger2007.lean b/Linglib/Studies/Jaeger2007.lean index 6885176b4..01e35ce0d 100644 --- a/Linglib/Studies/Jaeger2007.lean +++ b/Linglib/Studies/Jaeger2007.lean @@ -1,7 +1,7 @@ import Linglib.Core.DecisionTheory.Learning import Linglib.Core.Probability.SoftmaxTheory -import Linglib.Phonology.Constraint.Dequantization.OTLimit -import Linglib.Phonology.Constraint.MaxEnt +import Linglib.Phonology.HarmonicGrammar.Dequantization.OTLimit +import Linglib.Phonology.HarmonicGrammar.MaxEnt /-! # [jaeger-2007]: Maximum Entropy Models and Stochastic Optimality Theory @@ -43,7 +43,7 @@ Gradient Ascent (SGA) for Maximum Entropy models. This unifies two traditions: namespace Jaeger2007 -open Core Core.Optimization Phonology.Constraint Real +open Core Core.Optimization Constraint HarmonicGrammar Real -- ============================================================================ -- § 1: GLA = SGA (Main Theorem) diff --git a/Linglib/Studies/Jenks2018.lean b/Linglib/Studies/Jenks2018.lean index 656e55f30..9bd9c5241 100644 --- a/Linglib/Studies/Jenks2018.lean +++ b/Linglib/Studies/Jenks2018.lean @@ -314,7 +314,7 @@ def indexStrength (c : IndexCandidate) : Nat := to the binary indexed/non-indexed competition. Per paper p. 524, "Index! is a specific instance of Maximize Presupposition! (Heim 1990)". -/ -def indexConstraint : Phonology.Constraint.OT.NamedConstraint IndexCandidate := +def indexConstraint : Constraint.NamedConstraint IndexCandidate := Semantics.Presupposition.MaximizePresupposition.mpConstraintOf 1 indexStrength @@ -381,7 +381,7 @@ def topicAwareIndexStrength (c : TopicCandidate) : Nat := /-- The topic-aware Index! constraint. -/ def topicAwareIndexConstraint : - Phonology.Constraint.OT.NamedConstraint TopicCandidate := + Constraint.NamedConstraint TopicCandidate := Semantics.Presupposition.MaximizePresupposition.mpConstraintOf 1 topicAwareIndexStrength diff --git a/Linglib/Studies/Krifka2007.lean b/Linglib/Studies/Krifka2007.lean index b413e4ae1..017b19ee0 100644 --- a/Linglib/Studies/Krifka2007.lean +++ b/Linglib/Studies/Krifka2007.lean @@ -2,8 +2,9 @@ import Linglib.Semantics.Gradability.Antonymy import Linglib.Semantics.Gradability.AntonymPrediction import Linglib.Pragmatics.Implicature.Markedness import Linglib.Data.Examples.TesslerFranke2019 -import Linglib.Phonology.Constraint.OT.Basic -import Linglib.Phonology.Constraint.Superoptimal +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality +import Linglib.Pragmatics.Superoptimal /-! # [krifka-2007b] — Negated Antonyms: Creating and Filling the Gap @@ -72,9 +73,9 @@ open Semantics.Gradability.Antonymy open Semantics.Degree (positiveMeaning) open Data.Examples open Features (NegationType) -open Phonology.Constraint (superoptimal superoptimalSet +open Pragmatics.Bidirectional (superoptimal superoptimalSet superoptimal_coe_eq_set Blocks) -open Phonology.Constraint.OT (NamedConstraint) +open Constraint OptimalityTheory -- ════════════════════════════════════════════════════ -- § 1. Quadruplet: The Central Data Structure diff --git a/Linglib/Studies/Magri2025.lean b/Linglib/Studies/Magri2025.lean index b46ea824b..a3ab1191d 100644 --- a/Linglib/Studies/Magri2025.lean +++ b/Linglib/Studies/Magri2025.lean @@ -36,7 +36,7 @@ the sub-square setup from Z&H 2017). namespace Magri2025 -open Core.Optimization Phonology.Constraint Phonology.Constraint.OT +open Core.Optimization Constraint Constraint OptimalityTheory HarmonicGrammar open ZurawHayes2017 /-! ## § 1: Constraint Independence diff --git a/Linglib/Studies/MarcoRasin2026.lean b/Linglib/Studies/MarcoRasin2026.lean index 82a9446a0..91c021c05 100644 --- a/Linglib/Studies/MarcoRasin2026.lean +++ b/Linglib/Studies/MarcoRasin2026.lean @@ -43,8 +43,8 @@ argument that OP fails "regardless of what constitutes a paradigm." namespace MarcoRasin2026 -open Core.Optimization Phonology.Constraint.OT -open Phonology.Constraints +open Core.Optimization Constraint OptimalityTheory +open OptimalityTheory open Phonology.ParadigmUniformity open Phonology.Syllable (SonorityRank) @@ -348,7 +348,7 @@ predictions for verbs and nouns, and the *wrong* prediction for adjectives — the empirical content of [marco-rasin-2026]'s argument. -/ section PredictAPI -open Core.Optimization Phonology.Constraint +open Core.Optimization Constraint /-- Verbal paradigm under McCarthy's OP ranking. -/ noncomputable def verbSystem : ConstraintSystem (List JTAForm) (LexProfile Nat 4) := diff --git a/Linglib/Studies/McCarthyPrince1995.lean b/Linglib/Studies/McCarthyPrince1995.lean index 85e44c07c..a3cf7aef8 100644 --- a/Linglib/Studies/McCarthyPrince1995.lean +++ b/Linglib/Studies/McCarthyPrince1995.lean @@ -38,8 +38,8 @@ three core constraints can produce it. We prove this as namespace McCarthyPrince1995 -open Core.Optimization Phonology.Constraint.OT -open Phonology.Constraints +open Core.Optimization Constraint OptimalityTheory +open OptimalityTheory -- ============================================================================ -- § 1: Javanese Intervocalic h-Deletion (Overapplication) @@ -111,7 +111,7 @@ theorem javanese_overapplication : The constraints `javMaxIO`, `javIdentBR`, `javStarVhV` above stipulate violation counts via λ-tables. This section adds the *structural* substrate: each candidate is associated with a -`Corr Phonology.Correspondence.RedupRole Seg` recording the input → base / +`Corr OptimalityTheory.Correspondence.RedupRole Seg` recording the input → base / base ↔ reduplicant correspondences. MAX-IO and "IDENT-BR" violation counts are then **derived from `Corr.maxViol`** rather than stipulated. @@ -127,7 +127,7 @@ relation.) -/ namespace JavaneseCorr -open Phonology.Correspondence (Corr RedupRole) +open OptimalityTheory.Correspondence (Corr RedupRole) /-- Phonological segments for the Javanese stem. Minimal abstract inventory (just the contrasts that matter for h-deletion). -/ @@ -187,13 +187,13 @@ theorem javIdentBR_eq_corr (c : JavaneseCand) : /-- The Javanese tableau as `NamedConstraint (Corr RedupRole Seg)`s. These are direct uses of the paper-agnostic - `Phonology.Correspondence.Reduplication.maxIO` / `maxBR` — no + `OptimalityTheory.Correspondence.Reduplication.maxIO` / `maxBR` — no Javanese-specific constraint construction needed. -/ abbrev javMaxIOFromCorr : NamedConstraint (Corr RedupRole Seg) := - Phonology.Correspondence.Reduplication.maxIO + OptimalityTheory.Correspondence.Reduplication.maxIO abbrev javMaxBRFromCorr : NamedConstraint (Corr RedupRole Seg) := - Phonology.Correspondence.Reduplication.maxBR + OptimalityTheory.Correspondence.Reduplication.maxBR end JavaneseCorr @@ -286,7 +286,7 @@ markedness over a single output and stays as the original stipulation. -/ namespace BalangaoCorr -open Phonology.Correspondence (Corr RedupRole) +open OptimalityTheory.Correspondence (Corr RedupRole) /-- Phonological segments for the Balangao stem. Minimal abstract inventory (just the contrasts that matter for `tagtag`-reduplication). -/ @@ -675,7 +675,7 @@ constraints. -/ namespace AkanCorr -open Phonology.Correspondence (Corr RedupRole) +open OptimalityTheory.Correspondence (Corr RedupRole) /-- Phonological segments for the Akan /RED-ka/ paradigm. The minimal abstract inventory tracking the [coronal] feature contrast. -/ @@ -756,7 +756,7 @@ For these deterministic OT analyses, the unique-winner pattern collapses the `argminDecoder` distribution to probability 1 on the winner. -/ section PredictAPI -open Core.Optimization Phonology.Constraint +open Core.Optimization Constraint /-- Javanese overapplication tableau as a generic `ConstraintSystem`. -/ noncomputable def javaneseSystem : ConstraintSystem JavaneseCand (LexProfile Nat 3) := diff --git a/Linglib/Studies/McPhersonLamont2026.lean b/Linglib/Studies/McPhersonLamont2026.lean index 4f521187b..37e5e1a63 100644 --- a/Linglib/Studies/McPhersonLamont2026.lean +++ b/Linglib/Studies/McPhersonLamont2026.lean @@ -1,6 +1,7 @@ -import Linglib.Phonology.Constraint.OT.Basic -import Linglib.Phonology.Constraint.OT.ElementaryRankingCondition -import Linglib.Phonology.Constraint.OT.HarmonicSerialism +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality +import Linglib.Phonology.OptimalityTheory.ElementaryRankingCondition +import Linglib.Phonology.OptimalityTheory.HarmonicSerialism import Linglib.Phonology.Tone.Constraints import Linglib.Fragments.Poko.Tone import Linglib.Phonology.Autosegmental.Floating @@ -59,7 +60,7 @@ step witnesses are `decide`-checked (no `sorry`). namespace McPhersonLamont2026 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Core.Optimization.Evaluation -- ============================================================================ @@ -281,7 +282,7 @@ theorem weighted_HG_inadequate : namespace Fig3 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone @@ -581,7 +582,7 @@ end Fig3 namespace Eq24 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone @@ -663,7 +664,7 @@ end Eq24 namespace Eq21 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone @@ -731,7 +732,7 @@ end Eq21 namespace Eq27 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone @@ -801,7 +802,7 @@ end Eq27 namespace Eq30 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone @@ -884,7 +885,7 @@ end Eq30 namespace Eq22 -open Phonology.Constraint.OT +open Constraint OptimalityTheory open Phonology.Autosegmental open Phonology.Autosegmental.RegisterTier (TRN) open Phonology.Tone (starFloat starTautDock starCrowd maxTone depLinkTone diff --git a/Linglib/Studies/PoesioEtAl2004.lean b/Linglib/Studies/PoesioEtAl2004.lean index 98b37b57f..856967db1 100644 --- a/Linglib/Studies/PoesioEtAl2004.lean +++ b/Linglib/Studies/PoesioEtAl2004.lean @@ -104,7 +104,7 @@ type-changing axes, not the bookkeeping ones" recommendation. `HasDerivAt`/`HasFDerivAt`/`lineDeriv` as separate definitions with cross-implications, not a `DerivativeConfig` bundling them.) -- **The OT-bridge to `Phonology.Constraint.OT.Tableau.optimal`** per +- **The OT-bridge to `Constraint.Tableau.optimal`** per Beaver 2004. PSDH §3.1 fn 12 endorse Beaver's OT reformulation of Centering, but the bridge theorem belongs in `Studies/Beaver2004.lean` (queued as a diff --git a/Linglib/Studies/RosaArnold2017.lean b/Linglib/Studies/RosaArnold2017.lean index a25d79ac9..c74dafe26 100644 --- a/Linglib/Studies/RosaArnold2017.lean +++ b/Linglib/Studies/RosaArnold2017.lean @@ -331,7 +331,7 @@ theorem pronoun_at_most_as_heavy : -- § 10. Cross-Study Bridge: [arnold-wasow-losongco-ginstrom-2000] -- ════════════════════════════════════════════════════ -open ArnoldEtAl2000 Phonology.Constraint +open ArnoldEtAl2000 Constraint /-- The goal argument receives a MORE REDUCED referential form than the source argument. This derived contrast — not the individual predictions — diff --git a/Linglib/Studies/RoseWalker2004.lean b/Linglib/Studies/RoseWalker2004.lean index 277152621..5a0000dde 100644 --- a/Linglib/Studies/RoseWalker2004.lean +++ b/Linglib/Studies/RoseWalker2004.lean @@ -210,14 +210,14 @@ characterizes the *language*; this constraint *evaluates* it. This case does *not* use `mkAgreeOnTier` (the symmetric `R := (· ≠ ·)` specialization) because Kikongo's forbidden pair is asymmetric — see the "What this file formalizes" docstring above. -/ -def kikongoAgree : Phonology.Constraint.OT.NamedConstraint (List KSeg) := - Phonology.Constraints.mkForbidPairsOnTier +def kikongoAgree : Constraint.NamedConstraint (List KSeg) := + OptimalityTheory.mkForbidPairsOnTier "AGREE-[nas]/CC" KSeg.forbidNasalStop (Tier.byClass KSeg.onTier) id /-- `kikongoAgree` is a markedness constraint by construction. -/ theorem kikongoAgree_is_markedness : - kikongoAgree.family = Phonology.Constraint.OT.ConstraintFamily.markedness := - Phonology.Constraints.mkForbidPairsOnTier_is_markedness _ _ _ _ + kikongoAgree.family = Constraint.ConstraintFamily.markedness := + OptimalityTheory.mkForbidPairsOnTier_is_markedness _ _ _ _ /-- **Bridge**: `kikongoAgree` evaluates to zero on a candidate iff the candidate is in the TSL_2 language. The "OT-side" and "subregular-side" diff --git a/Linglib/Studies/SandeClemDabkowski2026.lean b/Linglib/Studies/SandeClemDabkowski2026.lean index d5229ea2b..81ec2585a 100644 --- a/Linglib/Studies/SandeClemDabkowski2026.lean +++ b/Linglib/Studies/SandeClemDabkowski2026.lean @@ -123,7 +123,7 @@ open Minimalist (PICStrength) open Minimalist.Linearization (SpelloutAndCheck FrozenFeature FrozenFeatureTable extendFrozenFeatures frozenValue) -open Phonology.CophonologyByPhrase (PhrasalCophonology) +open OptimalityTheory.CophonologyByPhrase (PhrasalCophonology) -- ============================================================================ -- § 1: Guébie vowel inventory and ATR feature diff --git a/Linglib/Studies/Sauerland2003.lean b/Linglib/Studies/Sauerland2003.lean index f185f9b9e..14c883e3c 100644 --- a/Linglib/Studies/Sauerland2003.lean +++ b/Linglib/Studies/Sauerland2003.lean @@ -54,7 +54,7 @@ open Semantics.Plurality.Algebra (star D) open Semantics.Plurality.Cover (IsFinCover algClosure_of_finCover) open Features (ContainmentPair ContainmentPairLike) open Semantics.Presupposition (PartialProp) -open Phonology.Constraint.OT (NamedConstraint mkTableau) +open Constraint OptimalityTheory open Semantics.Presupposition.PhiFeatures open Semantics.Presupposition.MaximizePresupposition (phiMP phi_mp_selects_maximal) diff --git a/Linglib/Studies/SiptarTorkenczy2000.lean b/Linglib/Studies/SiptarTorkenczy2000.lean index 81bfacc50..bff80e68a 100644 --- a/Linglib/Studies/SiptarTorkenczy2000.lean +++ b/Linglib/Studies/SiptarTorkenczy2000.lean @@ -1,6 +1,7 @@ import Linglib.Phonology.Subregular.Harmony import Linglib.Phonology.OptimalityTheory.Correspondence -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Phonology.Constraint.System import Linglib.Fragments.Hungarian.VowelHarmony @@ -14,7 +15,7 @@ End-to-end OT analysis of Hungarian vowel harmony, connecting: 2. **Harmony system** (`Subregular.Harmony`) — trigger/target/transparent predicates 3. **OT constraints** (below) — SPREAD and IDENT derived from `System` (folded in from the former `Harmony/OT.lean`, this file's sole consumer) -4. **Tableaux** (`Phonology.Constraint.OT`) — `mkTableau` + `optimal` select winner +4. **Tableaux** (`Constraint`) — `mkTableau` + `optimal` select winner 5. **Hungarian fragments** (`Hungarian.VowelHarmony`) — concrete vowel segments and `hungarianPalatalHarmony` @@ -43,8 +44,8 @@ namespace SiptarTorkenczy2000 open Phonology (Segment Feature) open Phonology.Harmony -open Phonology.Correspondence (Corr) -open Phonology.Constraint.OT Core.Optimization Core.Optimization.Evaluation +open OptimalityTheory.Correspondence (Corr) +open Constraint OptimalityTheory Core.Optimization Core.Optimization.Evaluation open Hungarian.VowelHarmony -- ============================================================================ @@ -326,7 +327,7 @@ here both expose `predict : Cand → ℝ`; for the deterministic OT case, `predict winner = 1` and `predict loser = 0`. -/ section PredictAPI -open Core.Optimization Phonology.Constraint +open Core.Optimization Constraint /-- *ház* SPREAD ≫ IDENT tableau as a generic `ConstraintSystem`. -/ noncomputable def házSystem : ConstraintSystem VHCandidate (LexProfile Nat 2) := diff --git a/Linglib/Studies/Stojkovic2026.lean b/Linglib/Studies/Stojkovic2026.lean index c108cd367..d40eb78f8 100644 --- a/Linglib/Studies/Stojkovic2026.lean +++ b/Linglib/Studies/Stojkovic2026.lean @@ -76,7 +76,7 @@ hypothetical Ukrainian [uv]~[iv] pairs). namespace Stojkovic2026 -open Phonology.Constraint.OT Core.Optimization.Evaluation Phonology.Constraints +open Constraint OptimalityTheory Core.Optimization.Evaluation OptimalityTheory /-! ### Candidates -/ diff --git a/Linglib/Studies/Storme2026.lean b/Linglib/Studies/Storme2026.lean index 13a61b7f0..4d9dd4ebf 100644 --- a/Linglib/Studies/Storme2026.lean +++ b/Linglib/Studies/Storme2026.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.MaxEnt +import Linglib.Phonology.HarmonicGrammar.MaxEnt import Linglib.Phonology.Constraint.System import Linglib.Phonology.Constraint.Weighted import Linglib.Phonology.OptimalityTheory.Constraints @@ -46,9 +46,9 @@ Following standard OT/MaxEnt constraint families: namespace Storme2026 -open Core.Optimization Phonology.Constraint Phonology.Constraints +open Core.Optimization Constraint HarmonicGrammar OptimalityTheory open Farsi.Phonology -open Core.Optimization Phonology.Constraint.OT +open Core.Optimization Constraint OptimalityTheory -- Fintype instances for HiatusInput/Output (Fintype requires Mathlib, -- which is available here via MaxEnt → RationalAction) diff --git a/Linglib/Studies/Wang2023.lean b/Linglib/Studies/Wang2023.lean index 1ab7101f4..9b250cdb5 100644 --- a/Linglib/Studies/Wang2023.lean +++ b/Linglib/Studies/Wang2023.lean @@ -1,5 +1,6 @@ import Linglib.Features.ContainmentPair -import Linglib.Phonology.Constraint.OT.Basic +import Linglib.Phonology.Constraint.Defs +import Linglib.Phonology.OptimalityTheory.Optimality import Linglib.Semantics.Presupposition.PhiFeatures import Linglib.Semantics.Presupposition.MaximizePresupposition import Linglib.Syntax.Minimalist.Features @@ -38,7 +39,7 @@ This file connects three layers: - `Features.ContainmentPair`: the algebraic structure (specLevel ordering) - `Semantics.Presupposition.PhiFeatures`: presuppositional denotations, semantic markedness, and presuppositional strength ordering -- `Phonology.Constraint.OT`: constraint evaluation and factorial typology +- `Constraint`: constraint evaluation and factorial typology ## Sections @@ -57,8 +58,7 @@ set_option autoImplicit false namespace Wang2023 open Features (ContainmentPair ContainmentPairLike) -open Phonology.Constraint.OT (NamedConstraint ConstraintFamily mkTableau - mkFactorialOptima mkFactorialTypologySize) +open Constraint OptimalityTheory open Semantics.Presupposition.PhiFeatures (isSemanticUnmarked presupStrength presupWeakerThan wellFormed_specLevel_le_two sgSem plSem) @@ -465,8 +465,8 @@ it holds for arbitrary candidate sets. The proof is purely algebraic: section GeneralTheorem -open Phonology.Constraint.OT (mkTableau_optimal_zero_first mkTableau_optimal_mem) -open Phonology.Constraint.OT (Tableau buildViolationProfile) +open Constraint OptimalityTheory +open Constraint OptimalityTheory /-- Every optimal candidate under ToD >> MP! is `.minimal`. The proof: `optimal_zero_first` gives `todConstraint.eval c = 0`, i.e. diff --git a/Linglib/Studies/Zuraw2010.lean b/Linglib/Studies/Zuraw2010.lean index 1cf421e90..37d31c8ea 100644 --- a/Linglib/Studies/Zuraw2010.lean +++ b/Linglib/Studies/Zuraw2010.lean @@ -1,5 +1,5 @@ import Linglib.Phonology.OptimalityTheory.Constraints -import Linglib.Phonology.Constraint.PartiallyOrderedConstraints +import Linglib.Phonology.HarmonicGrammar.PartiallyOrderedConstraints import Linglib.Core.Optimization.PermSubsetCombinatorics /-! @@ -25,7 +25,7 @@ Constraints) substrate. For each stem-initial consonant `c`: computed from `vp` (`{i : vp c .yes i ≠ vp c .no i}` and `{i : vp c .yes i < vp c .no i}` respectively), with concrete `decide`-discharged values. -- `subProb c : ℚ` is `Phonology.Constraint.PartialOrderConstraints.pocPredict` +- `subProb c : ℚ` is `HarmonicGrammar.PartialOrderConstraints.pocPredict` applied to the discrete partial order on `Fin 6` — i.e. uniform sampling over all 720 total orders. - The closed-form rate `|Y_c ∩ D_c| / |D_c|` follows by a single @@ -94,8 +94,8 @@ those definitions must remain stable. namespace Zuraw2010 -open Phonology.Constraint Core.Optimization Phonology.Constraint.OT Phonology.Constraints -open Core.Optimization Phonology.Constraint.PartialOrderConstraints +open Constraint Core.Optimization Constraint OptimalityTheory OptimalityTheory +open Core.Optimization HarmonicGrammar.PartialOrderConstraints open Core.Optimization Core.Optimization.PermSubsetCombinatorics /-! ## § 0: Stems, Substitution Decisions, Dictionary Counts -/ diff --git a/Linglib/Studies/ZurawHayes2017.lean b/Linglib/Studies/ZurawHayes2017.lean index 91a2f526b..60db5b74f 100644 --- a/Linglib/Studies/ZurawHayes2017.lean +++ b/Linglib/Studies/ZurawHayes2017.lean @@ -1,4 +1,4 @@ -import Linglib.Phonology.Constraint.Separability +import Linglib.Phonology.HarmonicGrammar.Separability import Linglib.Studies.Zuraw2010 /-! @@ -58,7 +58,7 @@ sub-grid. namespace ZurawHayes2017 -open Phonology.Constraint Core.Optimization Phonology.Constraint.OT Phonology.Constraints +open Constraint HarmonicGrammar Core.Optimization Constraint OptimalityTheory OptimalityTheory /-! ## § 1: 2×2 Square — Underlying Forms -/