Correspondence Theory

[McCP95] [Ben97]

Correspondence diagrams and their faithfulness constraints. A Corr Role α gives each role a string (form) and each ordered role pair a correspondence relation edge between positions. Each faithfulness constraint is a map Corr Role α → Role → Role → ℕ.

Following [McCP95] (Def. 10), edge r₁ r₂ is the directed relation ℛ ⊆ S₁ × S₂ that every constraint reads (MAX off its Domain, DEP off its Range, …). Symmetry — "correspondents of one another" — is a derived property (IsSymmetric, proved of the constructors), not built into the type, since M&P's ℛ is a directed subset. The position-relation encoding follows the model-theoretic treatment of [PVH17] and [PP02] (reduplicative B-R: [DH20]).

Main definitions

• Corr — a correspondence diagram (form plus the directed relation edge).
• Corr.maxViol, depViol, identViol, linearityViol, contigIViol, anchorLViol, integrityViol, uniformityViol — the faithfulness families; named constraints are partial applications (MAX-IO is c.maxViol .input .output).
• Corr.diagram — the universal constructor; parallel, identity, reduplication are diagonal specializations.
• Corr.IsSymmetric — correspondence symmetry, derived for the constructors.
• Corr.RoleQuiv — the labeled-quiver structure on Role.

Main results

• Corr.IsFaithful — the conjunction of the five order-relevant zeros (MAX, DEP, INTEGRITY, UNIFORMITY, LINEARITY).
• Corr.isFaithful_iff_exists_orderIso — a correspondence is faithful iff its edge is the graph of an order isomorphism between the two position orders.
• Corr.exists_orderIso_of_faithful — the forward direction (the converse of the identity_*_zero lemmas).

Binary and ternary roles

inductive OptimalityTheory.Correspondence.Side : Type

Roles for a binary correspondence (Corr.parallel, Corr.identity).

• lhs : Side
• rhs : Side

@[implicit_reducible]

instance OptimalityTheory.Correspondence.instDecidableEqSide : DecidableEq Side

Equations

• OptimalityTheory.Correspondence.instDecidableEqSide x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance OptimalityTheory.Correspondence.instReprSide : Repr Side

Equations

• OptimalityTheory.Correspondence.instReprSide = { reprPrec := OptimalityTheory.Correspondence.instReprSide.repr }

def OptimalityTheory.Correspondence.instReprSide.repr : Side → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive OptimalityTheory.Correspondence.RedupRole : Type

Roles for a reduplicative correspondence: input, base, reduplicant ([McCP95]); used by Corr.reduplication.

• input : RedupRole
• base : RedupRole
• reduplicant : RedupRole

@[implicit_reducible]

instance OptimalityTheory.Correspondence.instDecidableEqRedupRole : DecidableEq RedupRole

Equations

• OptimalityTheory.Correspondence.instDecidableEqRedupRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def OptimalityTheory.Correspondence.instReprRedupRole.repr : RedupRole → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance OptimalityTheory.Correspondence.instReprRedupRole : Repr RedupRole

Equations

• OptimalityTheory.Correspondence.instReprRedupRole = { reprPrec := OptimalityTheory.Correspondence.instReprRedupRole.repr }

The correspondence diagram

structure OptimalityTheory.Correspondence.Corr (Role : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A correspondence diagram: role-indexed forms and a directed correspondence relation edge between positions ([McCP95] Def. 10). The in-range bound is carried by the Fin-indexed type of edge rather than a separate well-formedness field.

• form : Role → List α
• edge (r₁ r₂ : Role) : Finset (Fin (self.form r₁).length × Fin (self.form r₂).length)

def OptimalityTheory.Correspondence.Corr.IsSymmetric {Role : Type u_1} {α : Type u_2} (c : Corr Role α) : Prop

Correspondence is symmetric — "correspondents of one another" ([McCP95] Def. 10): each relation is the converse of the reverse one. A derived property (diagram_isSymmetric), not a field.

Equations

• c.IsSymmetric = ∀ (r₁ r₂ : Role), c.edge r₂ r₁ = Finset.image Prod.swap (c.edge r₁ r₂)

Constraint families

def OptimalityTheory.Correspondence.Corr.maxViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

MAX ([McCP95] A.1): the count of form r₁ positions with no correspondent in form r₂. MAX-OO is basemap faithfulness ([Ben97]).

Equations

• c.maxViol r₁ r₂ = (Finset.univ \ Finset.image Prod.fst (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.Corr.depViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

DEP ([McCP95] A.2): the count of form r₂ positions with no correspondent in form r₁. DEP-IO prohibits epenthesis.

Equations

• c.depViol r₁ r₂ = (Finset.univ \ Finset.image Prod.snd (c.edge r₁ r₂)).card

def OptimalityTheory.Correspondence.Corr.identViol {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : Corr Role α) (r₁ r₂ : Role) : ℕ

IDENT ([McCP95] A.3): corresponding pairs whose segments differ. IDENT-OO is OO-faithfulness ([Ben97], [McC05], [Rol18]). Each coordinate of a correspondence pair is a Fin in range, so (form r₁)[p.1] is the total indexed lookup (no Option). See identViolFeature for the feature-by-feature variant.

Equations

• c.identViol r₁ r₂ = {p ∈ c.edge r₁ r₂ | (c.form r₁)[p.1] ≠ (c.form r₂)[p.2]}.card

def OptimalityTheory.Correspondence.Corr.identViolFeature {Role : Type u_1} {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (c : Corr Role α) (r₁ r₂ : Role) : ℕ

Featural IDENT ([McCP95] A.3): corresponding pairs differing under proj ([Ben97], [RW11]).

Equations

• OptimalityTheory.Correspondence.Corr.identViolFeature proj c r₁ r₂ = {p ∈ c.edge r₁ r₂ | proj (c.form r₁)[p.1] ≠ proj (c.form r₂)[p.2]}.card

Contiguity

@[reducible, inline]

abbrev OptimalityTheory.Correspondence.Corr.IsContiguous (l : List ℕ) : Prop

A ℕ-list is contiguous iff consecutive elements differ by 1.

Equations

• OptimalityTheory.Correspondence.Corr.IsContiguous l = List.IsChain (fun (a b : ℕ) => b = a + 1) l

@[implicit_reducible]

instance OptimalityTheory.Correspondence.Corr.instDecidableIsContiguous (l : List ℕ) : Decidable (IsContiguous l)

Equations

• OptimalityTheory.Correspondence.Corr.instDecidableIsContiguous l = l.instDecidableIsChainOfDecidableRel

def OptimalityTheory.Correspondence.Corr.contigIViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

I-CONTIGUITY "No Skipping" ([McCP95] A.4a): the domain of correspondence is contiguous in form r₁. The Fin-valued domain is projected to its ℕ values and sorted before the chain check.

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Corr.contigOViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

O-CONTIGUITY "No Intrusion" ([McCP95] A.4b): the range of correspondence is contiguous in form r₂.

Equations

• One or more equations did not get rendered due to their size.

Anchors

def OptimalityTheory.Correspondence.Corr.anchorLViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

L-ANCHOR ([McCP95] A.5): leftmost positions correspond. When either form is empty there is no leftmost position, so the constraint is vacuously satisfied; otherwise the Fin endpoints are the two 0s.

Equations

• c.anchorLViol r₁ r₂ = if h : (c.form r₁).length = 0 ∨ (c.form r₂).length = 0 then 0 else have h₁ := ⋯; have h₂ := ⋯; if (⟨0, h₁⟩, ⟨0, h₂⟩) ∈ c.edge r₁ r₂ then 0 else 1

def OptimalityTheory.Correspondence.Corr.anchorRViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

R-ANCHOR ([McCP95] A.5): rightmost positions correspond. The Fin endpoints are the two Fin.lasts when both forms are nonempty.

Equations

• One or more equations did not get rendered due to their size.

Linearity, uniformity, integrity

def OptimalityTheory.Correspondence.Corr.linearityViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

LINEARITY "No Metathesis" ([McCP95] A.6): the count of inversion pairs (i₁,j₁), (i₂,j₂) ∈ edge with i₁ < i₂ but j₂ < j₁ (coordinates compared via Fin.lt).

Equations

• c.linearityViol r₁ r₂ = {pq ∈ c.edge r₁ r₂ ×ˢ c.edge r₁ r₂ | pq.1.1 < pq.2.1 ∧ pq.2.2 < pq.1.2}.card

def OptimalityTheory.Correspondence.Corr.uniformityViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

UNIFORMITY "No Coalescence" ([McCP95] A.7): the count of form r₂ positions with more than one correspondent in form r₁.

Equations

• c.uniformityViol r₁ r₂ = {j : Fin (c.form r₂).length | {p ∈ c.edge r₁ r₂ | p.2 = j}.card > 1}.card

def OptimalityTheory.Correspondence.Corr.integrityViol {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : ℕ

INTEGRITY "No Breaking" ([McCP95] A.8): the count of form r₁ positions with more than one correspondent in form r₂.

Equations

• c.integrityViol r₁ r₂ = {i : Fin (c.form r₁).length | {p ∈ c.edge r₁ r₂ | p.1 = i}.card > 1}.card

Faithfulness predicate bridges

Each cardinal constraint vanishes iff the correspondence has the corresponding order-theoretic property (maxViol = 0 ⟺ left-total, etc.). These are the named characterizations the order-isomorphism theorem is assembled from.

theorem OptimalityTheory.Correspondence.Corr.maxViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.maxViol r₁ r₂ = 0 ↔ Finset.univ ⊆ Finset.image Prod.fst (c.edge r₁ r₂)

theorem OptimalityTheory.Correspondence.Corr.depViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.depViol r₁ r₂ = 0 ↔ Finset.univ ⊆ Finset.image Prod.snd (c.edge r₁ r₂)

theorem OptimalityTheory.Correspondence.Corr.integrityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.integrityViol r₁ r₂ = 0 ↔ ∀ (i : Fin (c.form r₁).length), {p ∈ c.edge r₁ r₂ | p.1 = i}.card ≤ 1

theorem OptimalityTheory.Correspondence.Corr.uniformityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.uniformityViol r₁ r₂ = 0 ↔ ∀ (j : Fin (c.form r₂).length), {p ∈ c.edge r₁ r₂ | p.2 = j}.card ≤ 1

theorem OptimalityTheory.Correspondence.Corr.linearityViol_eq_zero_iff {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.linearityViol r₁ r₂ = 0 ↔ ∀ p ∈ c.edge r₁ r₂, ∀ q ∈ c.edge r₁ r₂, p.1 < q.1 → ¬q.2 < p.2

Universal constructors

def OptimalityTheory.Correspondence.Corr.diagDiag (m n : ℕ) : Finset (Fin m × Fin n)

The parallel-pair diagonal in Fin-coordinates: (0,0), (1,1), … up to min m n, each index cast up into the two position types via Fin.castLE.

Equations

• OptimalityTheory.Correspondence.Corr.diagDiag m n = Finset.image (fun (i : Fin (min m n)) => (Fin.castLE ⋯ i, Fin.castLE ⋯ i)) Finset.univ

theorem OptimalityTheory.Correspondence.Corr.mem_diagDiag {m n : ℕ} (a : Fin m) (b : Fin n) : (a, b) ∈ diagDiag m n ↔ ↑a = ↑b

Membership in the diagonal: (a, b) ∈ diagDiag m n iff the two indices have equal underlying values.

theorem OptimalityTheory.Correspondence.Corr.diagDiag_image_fst {m : ℕ} : Finset.image Prod.fst (diagDiag m m) = Finset.univ

theorem OptimalityTheory.Correspondence.Corr.diagDiag_image_snd {m : ℕ} : Finset.image Prod.snd (diagDiag m m) = Finset.univ

theorem OptimalityTheory.Correspondence.Corr.diagDiag_card (m n : ℕ) : (diagDiag m n).card = min m n

The diagonal has min m n pairs — one per index of the shorter form.

def OptimalityTheory.Correspondence.Corr.diagram {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] : Corr Role α

Universal constructor: where hasEdge holds, the parallel-pair correspondence (0,0), (1,1), … truncated to min of the two lengths; elsewhere none. For non-parallel structure (infixation, re-alignment) build edge directly (e.g. Benua1997.diagramWithEdge).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OptimalityTheory.Correspondence.Corr.diagram_form {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] (r : Role) : (diagram form hasEdge).form r = form r

theorem OptimalityTheory.Correspondence.Corr.diagram_edge {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] (r₁ r₂ : Role) : (diagram form hasEdge).edge r₁ r₂ = if hasEdge r₁ r₂ then diagDiag (form r₁).length (form r₂).length else ∅

theorem OptimalityTheory.Correspondence.Corr.diagram_edge_pos {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] {r₁ r₂ : Role} (h : hasEdge r₁ r₂) : (diagram form hasEdge).edge r₁ r₂ = diagDiag (form r₁).length (form r₂).length

theorem OptimalityTheory.Correspondence.Corr.diagram_edge_neg {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] {r₁ r₂ : Role} (h : ¬hasEdge r₁ r₂) : (diagram form hasEdge).edge r₁ r₂ = ∅

theorem OptimalityTheory.Correspondence.Corr.diagram_isSymmetric {Role : Type u_1} {α : Type u_2} (form : Role → List α) (hasEdge : Role → Role → Prop) [DecidableRel hasEdge] (hsymm : Symmetric hasEdge) : (diagram form hasEdge).IsSymmetric

A diagram over a symmetric predicate is a symmetric correspondence — symmetry derived, not stipulated.

def OptimalityTheory.Correspondence.Corr.parallel {α : Type u_2} (s₁ s₂ : List α) : Corr Side α

Parallel-pair correspondence between two strings, truncated to the shorter (List.zip semantics).

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Corr.identity {α : Type u_2} (s : List α) : Corr Side α

The fully-faithful candidate: identity correspondence on one string ([McCP95]).

Equations

• OptimalityTheory.Correspondence.Corr.identity s = OptimalityTheory.Correspondence.Corr.parallel s s

def OptimalityTheory.Correspondence.Corr.reduplication {α : Type u_2} (input base reduplicant : List α) : Corr RedupRole α

3-role input/base/reduplicant diagram with parallel-pair cross-role edges ([McCP95]).

Equations

• One or more equations did not get rendered due to their size.

theorem OptimalityTheory.Correspondence.Corr.parallel_isSymmetric {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).IsSymmetric

theorem OptimalityTheory.Correspondence.Corr.reduplication_isSymmetric {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).IsSymmetric

@[simp]

theorem OptimalityTheory.Correspondence.Corr.reduplication_form_input {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.input = input

@[simp]

theorem OptimalityTheory.Correspondence.Corr.reduplication_form_base {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.base = base

@[simp]

theorem OptimalityTheory.Correspondence.Corr.reduplication_form_reduplicant {α : Type u_2} (input base reduplicant : List α) : (reduplication input base reduplicant).form RedupRole.reduplicant = reduplicant

Identity-correspondence zero lemmas

@[simp]

theorem OptimalityTheory.Correspondence.Corr.parallel_form_lhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).form Side.lhs = s₁

@[simp]

theorem OptimalityTheory.Correspondence.Corr.parallel_form_rhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).form Side.rhs = s₂

@[simp]

theorem OptimalityTheory.Correspondence.Corr.parallel_edge_diag {α : Type u_2} (s₁ s₂ : List α) (r : Side) : (parallel s₁ s₂).edge r r = ∅

@[simp]

theorem OptimalityTheory.Correspondence.Corr.parallel_edge_lhs_rhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge Side.lhs Side.rhs = diagDiag s₁.length s₂.length

@[simp]

theorem OptimalityTheory.Correspondence.Corr.parallel_edge_rhs_lhs {α : Type u_2} (s₁ s₂ : List α) : (parallel s₁ s₂).edge Side.rhs Side.lhs = diagDiag s₂.length s₁.length

theorem OptimalityTheory.Correspondence.Corr.maxViol_eq_zero_of_diag {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagDiag (c.form r₁).length (c.form r₂).length) : c.maxViol r₁ r₂ = 0

MAX vanishes on a diagonal edge between equal forms: if c.edge r₁ r₂ is the parallel-pair diagonal and c.form r₁ = c.form r₂, every r₁ position has a correspondent. The role-agnostic core of identity_max_zero — it also fires for total reduplication (r₁, r₂ the base/reduplicant roles with equal forms).

theorem OptimalityTheory.Correspondence.Corr.depViol_eq_zero_of_diag {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagDiag (c.form r₁).length (c.form r₂).length) : c.depViol r₁ r₂ = 0

DEP vanishes on a diagonal edge between equal forms — the dual of maxViol_eq_zero_of_diag: every r₂ position has a correspondent.

theorem OptimalityTheory.Correspondence.Corr.identity_max_zero {α : Type u_2} (s : List α) : (identity s).maxViol Side.lhs Side.rhs = 0

theorem OptimalityTheory.Correspondence.Corr.identity_dep_zero {α : Type u_2} (s : List α) : (identity s).depViol Side.lhs Side.rhs = 0

theorem OptimalityTheory.Correspondence.Corr.identViol_eq_zero_of_diag {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : Corr Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagDiag (c.form r₁).length (c.form r₂).length) : c.identViol r₁ r₂ = 0

IDENT vanishes on a diagonal edge between equal forms: corresponding positions hold the same segment. Unlike MAX/DEP, this needs c.form r₁ = c.form r₂, not just equal length — an order-isomorphic edge between distinct strings can still violate IDENT.

theorem OptimalityTheory.Correspondence.Corr.identViolFeature_eq_zero_of_diag {Role : Type u_1} {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (c : Corr Role α) (r₁ r₂ : Role) (hform : c.form r₁ = c.form r₂) (hedge : c.edge r₁ r₂ = diagDiag (c.form r₁).length (c.form r₂).length) : identViolFeature proj c r₁ r₂ = 0

Featural IDENT vanishes on a diagonal edge between equal forms — the proj-relativized form of identViol_eq_zero_of_diag.

theorem OptimalityTheory.Correspondence.Corr.identity_ident_zero {α : Type u_2} [DecidableEq α] (s : List α) : (identity s).identViol Side.lhs Side.rhs = 0

theorem OptimalityTheory.Correspondence.Corr.identity_identFeature_zero {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (s : List α) : identViolFeature proj (identity s) Side.lhs Side.rhs = 0

Faithfulness as order-isomorphism

structure OptimalityTheory.Correspondence.Corr.IsFaithful {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : Prop

The five order-relevant zeros bundled: a correspondence is faithful (on the (r₁, r₂) edge) when it has no MAX, DEP, INTEGRITY, UNIFORMITY, or LINEARITY violation ([McCP95] (A.1), (A.2), (A.6), (A.7), (A.8)). This is exactly the hypothesis set under which the edge is the graph of an order isomorphism.

• max : c.maxViol r₁ r₂ = 0
• dep : c.depViol r₁ r₂ = 0
• integrity : c.integrityViol r₁ r₂ = 0
• uniformity : c.uniformityViol r₁ r₂ = 0
• linearity : c.linearityViol r₁ r₂ = 0

theorem OptimalityTheory.Correspondence.Corr.isFaithful_iff_exists_orderIso {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) : c.IsFaithful r₁ r₂ ↔ ∃ (e : Fin (c.form r₁).length ≃o Fin (c.form r₂).length), ∀ (i : Fin (c.form r₁).length) (j : Fin (c.form r₂).length), (i, j) ∈ c.edge r₁ r₂ ↔ e i = j

Faithful ⟺ order-isomorphism. A correspondence is faithful (no MAX, DEP, INTEGRITY, UNIFORMITY, or LINEARITY violation) iff its edge is the graph of an order isomorphism between the two position orders. The forward direction is the converse of the identity_*_zero lemmas, and the formal content of M&P's fully-faithful candidate being the identity.

theorem OptimalityTheory.Correspondence.Corr.exists_orderIso_of_faithful {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) (hmax : c.maxViol r₁ r₂ = 0) (hdep : c.depViol r₁ r₂ = 0) (hint : c.integrityViol r₁ r₂ = 0) (huni : c.uniformityViol r₁ r₂ = 0) (hlin : c.linearityViol r₁ r₂ = 0) : ∃ (e : Fin (c.form r₁).length ≃o Fin (c.form r₂).length), ∀ (i : Fin (c.form r₁).length) (j : Fin (c.form r₂).length), (i, j) ∈ c.edge r₁ r₂ ↔ e i = j

Faithful ⟹ order-isomorphism (the forward direction of isFaithful_iff_exists_orderIso).

theorem OptimalityTheory.Correspondence.Corr.length_eq_of_faithful {Role : Type u_1} {α : Type u_2} (c : Corr Role α) (r₁ r₂ : Role) (hmax : c.maxViol r₁ r₂ = 0) (hdep : c.depViol r₁ r₂ = 0) (hint : c.integrityViol r₁ r₂ = 0) (huni : c.uniformityViol r₁ r₂ = 0) (hlin : c.linearityViol r₁ r₂ = 0) : (c.form r₁).length = (c.form r₂).length

A faithful correspondence forces equal lengths (no deletion, no epenthesis).

Constraint bridges

Corr-violation functions packaged as bare Constraint (Corr Role α) (= Corr Role α → ℕ). The faithfulness/markedness family is recovered structurally below (VanishesOnIdentity / IsMarkedness), not stamped by a tag.

def OptimalityTheory.Correspondence.Corr.toIdentConstraint {Role : Type u_1} {α : Type u_2} [DecidableEq α] (r₁ r₂ : Role) : Constraints.Constraint (Corr Role α)

IDENT over a Corr: featural-identity violations between roles r₁, r₂.

Equations

• OptimalityTheory.Correspondence.Corr.toIdentConstraint r₁ r₂ c = c.identViol r₁ r₂

def OptimalityTheory.Correspondence.Corr.toIdentFeatureConstraint {Role : Type u_1} {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (r₁ r₂ : Role) : Constraints.Constraint (Corr Role α)

IDENT[F] over a Corr: violations of the feature picked out by proj.

Equations

• OptimalityTheory.Correspondence.Corr.toIdentFeatureConstraint proj r₁ r₂ c = OptimalityTheory.Correspondence.Corr.identViolFeature proj c r₁ r₂

def OptimalityTheory.Correspondence.Corr.toMaxConstraint {Role : Type u_1} {α : Type u_2} (r₁ r₂ : Role) : Constraints.Constraint (Corr Role α)

MAX over a Corr: deletion (input segments lacking a correspondent).

Equations

• OptimalityTheory.Correspondence.Corr.toMaxConstraint r₁ r₂ c = c.maxViol r₁ r₂

def OptimalityTheory.Correspondence.Corr.toDepConstraint {Role : Type u_1} {α : Type u_2} (r₁ r₂ : Role) : Constraints.Constraint (Corr Role α)

DEP over a Corr: epenthesis (output segments lacking a correspondent).

Equations

• OptimalityTheory.Correspondence.Corr.toDepConstraint r₁ r₂ c = c.depViol r₁ r₂

Faithfulness of the bridges: vanishing on the faithful candidate

The MAX/DEP/IDENT bridges assign zero violations to the fully faithful candidate identity s — the defining behaviour of a Correspondence-Theory faithfulness constraint ([McCP95]). This is the structural faithfulness now captured by VanishesOnIdentity (there is no .faithfulness tag). Markedness is non-vacuously different (exists_markedness_not_vanishesOnIdentity). Anti-faithfulness ([Ald01]) is out of scope — it demands disparity and is maximal on identity.

@[simp]

theorem OptimalityTheory.Correspondence.Corr.toMaxConstraint_eval_identity {α : Type u_2} (s : List α) : toMaxConstraint Side.lhs Side.rhs (identity s) = 0

@[simp]

theorem OptimalityTheory.Correspondence.Corr.toDepConstraint_eval_identity {α : Type u_2} (s : List α) : toDepConstraint Side.lhs Side.rhs (identity s) = 0

@[simp]

theorem OptimalityTheory.Correspondence.Corr.toIdentConstraint_eval_identity {α : Type u_2} [DecidableEq α] (s : List α) : toIdentConstraint Side.lhs Side.rhs (identity s) = 0

@[simp]

theorem OptimalityTheory.Correspondence.Corr.toIdentFeatureConstraint_eval_identity {α : Type u_2} {F : Type u_3} [DecidableEq F] (proj : α → F) (s : List α) : toIdentFeatureConstraint proj Side.lhs Side.rhs (identity s) = 0

def OptimalityTheory.Correspondence.Corr.VanishesOnIdentity {α : Type u_2} (c : Constraints.Constraint (Corr Side α)) : Prop

A correspondence constraint vanishes on the faithful candidate — scores no violations on any fully faithful identity s. This is the structural definition of a faithfulness constraint ([McCP95]), replacing the old .faithfulness tag.

Equations

• OptimalityTheory.Correspondence.Corr.VanishesOnIdentity c = ∀ (s : List α), c (OptimalityTheory.Correspondence.Corr.identity s) = 0

def OptimalityTheory.Correspondence.Corr.IsMarkedness {Role : Type u_1} {α : Type u_2} (out : Role) (c : Constraints.Constraint (Corr Role α)) : Prop

A correspondence constraint is markedness when it depends only on the out form — it scores equal violations on candidates agreeing on · .form out. The structural dual of VanishesOnIdentity, replacing the old .markedness tag.

Equations

• OptimalityTheory.Correspondence.Corr.IsMarkedness out c = ∀ (c₁ c₂ : OptimalityTheory.Correspondence.Corr Role α), c₁.form out = c₂.form out → c c₁ = c c₂

theorem OptimalityTheory.Correspondence.Corr.toMaxConstraint_vanishesOnIdentity {α : Type u_2} : VanishesOnIdentity (toMaxConstraint Side.lhs Side.rhs)

theorem OptimalityTheory.Correspondence.Corr.toDepConstraint_vanishesOnIdentity {α : Type u_2} : VanishesOnIdentity (toDepConstraint Side.lhs Side.rhs)

theorem OptimalityTheory.Correspondence.Corr.toIdentConstraint_vanishesOnIdentity {α : Type u_2} [DecidableEq α] : VanishesOnIdentity (toIdentConstraint Side.lhs Side.rhs)

theorem OptimalityTheory.Correspondence.Corr.exists_markedness_not_vanishesOnIdentity {α : Type u_2} [Inhabited α] : ∃ (c : Constraints.Constraint (Corr Side α)), IsMarkedness Side.rhs c ∧ ¬VanishesOnIdentity c

Markedness need not vanish on the faithful candidate. *Struc (one violation per output segment) is markedness yet fires on identity s, so the faith/mark split is non-vacuous — and structural, not tag-based.

Reduplication constraints

The canonical [McCP95] reduplicative-faithfulness constraints as Constraint (Corr RedupRole α); study files import these names rather than re-rolling Corr.toMaxConstraint .input .base.

def OptimalityTheory.Correspondence.Reduplication.maxIO {α : Type u_1} : Constraints.Constraint (Corr RedupRole α)

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Reduplication.maxBR {α : Type u_1} : Constraints.Constraint (Corr RedupRole α)

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Reduplication.depIO {α : Type u_1} : Constraints.Constraint (Corr RedupRole α)

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Reduplication.identBR {α : Type u_1} [DecidableEq α] : Constraints.Constraint (Corr RedupRole α)

Equations

• One or more equations did not get rendered due to their size.

def OptimalityTheory.Correspondence.Reduplication.identIO {α : Type u_1} [DecidableEq α] : Constraints.Constraint (Corr RedupRole α)

Equations

• One or more equations did not get rendered due to their size.

Quiver structure

def OptimalityTheory.Correspondence.Corr.RoleQuiv {Role : Type u_1} {α : Type u_2} : Corr Role α → Type u_1

The labeled-quiver structure on Role: morphisms r₁ ⟶ r₂ are the correspondence pairs (i, j) ∈ c.edge r₁ r₂. Carried by a value-indexed newtype since the instance depends on c; path-based (stratal, OT-CC) evaluation via Quiver.Path is not yet formalised.

Equations

• x✝.RoleQuiv = Role

@[implicit_reducible]

instance OptimalityTheory.Correspondence.Corr.instQuiverRoleQuiv {Role : Type u_1} {α : Type u_2} (c : Corr Role α) : Quiver c.RoleQuiv

Equations

• c.instQuiverRoleQuiv = { Hom := fun (r₁ r₂ : c.RoleQuiv) => ↥(c.edge r₁ r₂) }