Lexical Conservatism — Steriade 2000

@cite{steriade-2000}

The paper-specific Lexical Conservatism (LC) anchoring of the generic liftPairwise combinator from ParadigmUniformity/Defs.lean. LC differs from OP (@cite{mccarthy-2005}) by anchoring on attestation: a candidate surfacing form preferentially aligns with the attested wordform of the lexeme — and the strength of the alignment scales with how well-attested the anchor is.

LC predicts that paradigms with no attested anchor (e.g., bound stems with no free wordform) impose no LC pressure; the candidate is free to satisfy markedness alone. Paradigms with a strongly-attested anchor impose strong LC pressure that preserves the anchor's segments. The Breiss-Katsuda-Kawahara compounds (@cite{breiss-katsuda-kawahara-2026}) instantiate this: in bound-N2 compounds the velar nasalises categorically; in free-N2 compounds, nasalisation is suppressed in proportion to the N2's free- form attestation strength.

Architecture

LC reuses the same liftPairwise combinator as OP — the difference is which forms enter the paradigm. LC's lcParadigm constructor takes a candidate plus an optional attested anchor, returning a singleton when the anchor is absent (no LC pressure) and a pair when present (LC pressure scales with the anchor's mismatch from the candidate). The strength of the LC pressure is then a downstream frequency-conditioned weight on the constraint, supplied by Theories/Phonology/ItemSpecificity/ScaledWeights.lean or sibling files.

Connection to OP

The OP combinator (mkOPMaxV in ParadigmUniformity/OptimalParadigms.lean) sums over every pair in the paradigm, with no distinguished anchor. LC's lcParadigm makes the anchor structurally optional — its absence yields a singleton paradigm and zero LC violations. OP cannot model the bound/free split without auxiliary stipulation; LC handles it by paradigm membership.

Out of scope

• The specific shape of attestation strength (sigmoid, linear, step) — supplied externally via ItemSpecificity/. LC only commits to the qualitative claim that strength is monotone in attestation.
• Specific segment-level mismatch metrics — passed in as mismatch : Form → Form → Nat, with the only requirement that mismatch f f = 0 (well-formedness on the diagonal).

def Phonology.ParadigmUniformity.lcParadigm {Form : Type} (candidate : Form) (anchor : Option Form) : List Form

Build an LC paradigm from a candidate form and an optional attested anchor. When the anchor is present, the paradigm is [candidate, anchor]; when absent, it is [candidate]. Anchor presence is the LC channel: bound/unattested → singleton, free/ attested → pair.

Equations

• Phonology.ParadigmUniformity.lcParadigm candidate none = [candidate]
• Phonology.ParadigmUniformity.lcParadigm candidate (some a) = [candidate, a]

@[simp]

theorem Phonology.ParadigmUniformity.lcParadigm_none {Form : Type} (candidate : Form) : lcParadigm candidate none = [candidate]

@[simp]

theorem Phonology.ParadigmUniformity.lcParadigm_some {Form : Type} (candidate anchor : Form) : lcParadigm candidate (some anchor) = [candidate, anchor]

def Phonology.ParadigmUniformity.mkLCFaith {Form : Type} (name : String) (mismatch : Form → Form → ℕ) : Core.Constraint.OT.NamedConstraint (List Form)

Build an LC-FAITH constraint: per-pair faithfulness mismatch summed over the LC paradigm. The same liftPairwise is reused; what distinguishes LC from OP is the paradigm-construction discipline (lcParadigm), not the lift itself.

Equations

• Phonology.ParadigmUniformity.mkLCFaith name mismatch = Phonology.ParadigmUniformity.liftPairwise name Core.Constraint.OT.ConstraintFamily.faithfulness mismatch

def Phonology.ParadigmUniformity.mismatchFromTier {Form τ : Type} [DecidableEq τ] (proj : Form → List τ) (a b : Form) : ℕ

Featural mismatch derived from Corr.identViol via a tier projection. The structural realization of "LC-FAITH on tier τ": the count comes from the unifying Corr substrate, not a stipulated callback.

mismatch f f = 0 follows automatically from Corr.identity_ident_zero, discharging the h_diagonal precondition of lc_unanchored_zero by construction.

Equations

• Phonology.ParadigmUniformity.mismatchFromTier proj a b = (Phonology.Correspondence.Corr.parallel (proj a) (proj b)).identViol Phonology.Correspondence.Side.lhs Phonology.Correspondence.Side.rhs

theorem Phonology.ParadigmUniformity.mismatchFromTier_self_zero {Form τ : Type} [DecidableEq τ] (proj : Form → List τ) (f : Form) : mismatchFromTier proj f f = 0

The diagonal-zero property of mismatchFromTier is now a theorem, derived from Corr.identity_ident_zero rather than stipulated as a precondition.

def Phonology.ParadigmUniformity.mkLCFaithFromTier {Form τ : Type} [DecidableEq τ] (name : String) (proj : Form → List τ) : Core.Constraint.OT.NamedConstraint (List Form)

Build an LC-FAITH constraint with the mismatch derived from a tier projection. New code should use this in preference to the abstract mkLCFaith callback form.

Equations

• Phonology.ParadigmUniformity.mkLCFaithFromTier name proj = Phonology.ParadigmUniformity.mkLCFaith name (Phonology.ParadigmUniformity.mismatchFromTier proj)

theorem Phonology.ParadigmUniformity.lc_unanchored_zero {Form : Type} (name : String) (mismatch : Form → Form → ℕ) (h_diagonal : ∀ (f : Form), mismatch f f = 0) (candidate : Form) : (mkLCFaith name mismatch).eval (lcParadigm candidate none) = 0

A paradigm with no attested anchor (singleton) has zero LC-FAITH violations: the only ordered pair is the diagonal, and a well-formed mismatch returns 0 on the diagonal. This is the structural source of the prediction that bound stems exhibit no LC effect — a derived consequence of paradigm construction, not a stipulation.