Intersecting constraint families

Two constraint families intersect ([ZH17]) when a variable process is conditioned by two binary factors and each constraint is sensitive to at most one of them: arranging the four underlying forms that cross the factors into a square, each constraint is insensitive to the rows or to the columns, at every candidate (§2.4 of [Mag25]). [ZH17] and [Hay22] observe that the rates of application to the four forms then fit two shifted sigmoids at shared abscissas. [Mag25] restates the generalization on logit rates: the difference between the logit rates of two forms in one row does not depend on the row (13). Equivalently, the interaction contrast of the logit rates on the square vanishes; this file states the generalization so, as the kernel of a linear functional.

A function of a form's violations that is a sum of per-constraint terms has zero interaction whenever the families intersect, since each term is insensitive to one dimension. The MaxEnt log-odds of two candidates is such a sum, the weighted violation differences, so MaxEnt predicts the generalization for every weighting and every candidate set.

Main definitions

• HarmonicGrammar.Square: four underlying forms crossing two binary factors, (12) of [Mag25].
• Square.interaction: the interaction contrast f tl - f tr - f bl + f br, a linear functional on the functions of the forms.
• Square.InsensitiveToRow, Square.InsensitiveToCol, Square.Independent: the independence of the rows and columns relative to a constraint set.

Main results

• Square.Independent.interaction_sum_eq_zero: under independence, a sum of per-constraint terms has zero interaction.
• Square.Independent.interaction_logOdds_maxEnt: MaxEnt predicts the generalization, (22) of [Mag25].

References

• [ZH17]
• [Hay22]
• [Mag25]

structure HarmonicGrammar.Square (X : Type u_1) : Type u_1

Four underlying forms crossing two binary factors, rows by columns ((12) of [Mag25]).

• tl : X

  The top-left form.

• tr : X

  The top-right form.

• bl : X

  The bottom-left form.

• br : X

  The bottom-right form.

def HarmonicGrammar.Square.transpose {X : Type u_1} (sq : Square X) : Square X

The square with its rows and columns exchanged.

Equations

• sq.transpose = { tl := sq.tl, tr := sq.bl, bl := sq.tr, br := sq.br }

Independence

def HarmonicGrammar.Square.InsensitiveToRow {X : Type u_1} {α : Type u_3} (sq : Square X) (f : X → α) : Prop

f is insensitive to the rows when it agrees on the two forms of each column (Figure 4a of [Mag25]).

Equations

• sq.InsensitiveToRow f = (f sq.tl = f sq.bl ∧ f sq.tr = f sq.br)

def HarmonicGrammar.Square.InsensitiveToCol {X : Type u_1} {α : Type u_3} (sq : Square X) (f : X → α) : Prop

f is insensitive to the columns when it agrees on the two forms of each row (Figure 4b of [Mag25]).

Equations

• sq.InsensitiveToCol f = (f sq.tl = f sq.tr ∧ f sq.bl = f sq.br)

def HarmonicGrammar.Square.Independent {X : Type u_1} {Y : Type u_2} {n : ℕ} (sq : Square X) (con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)) : Prop

The rows and columns are independent dimensions relative to con (§2.4 of [Mag25]): each constraint is insensitive to the rows or to the columns, reading its violations of all the candidates of a form at once.

Equations

• sq.Independent con = ∀ (k : Fin n), sq.InsensitiveToRow (Function.curry (con k)) ∨ sq.InsensitiveToCol (Function.curry (con k))

theorem HarmonicGrammar.Square.InsensitiveToRow.comp {X : Type u_1} {α : Type u_3} {β : Type u_4} {sq : Square X} {f : X → α} (h : sq.InsensitiveToRow f) (g : α → β) : sq.InsensitiveToRow (g ∘ f)

theorem HarmonicGrammar.Square.InsensitiveToCol.comp {X : Type u_1} {α : Type u_3} {β : Type u_4} {sq : Square X} {f : X → α} (h : sq.InsensitiveToCol f) (g : α → β) : sq.InsensitiveToCol (g ∘ f)

The interaction contrast

def HarmonicGrammar.Square.interaction {X : Type u_1} {R : Type u_5} (sq : Square X) [CommRing R] : (X → R) →ₗ[R] R

The interaction contrast is the difference of f along the top row minus its difference along the bottom row.

Equations

• sq.interaction = LinearMap.proj sq.tl - LinearMap.proj sq.tr - LinearMap.proj sq.bl + LinearMap.proj sq.br

@[simp]

theorem HarmonicGrammar.Square.interaction_apply {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] (f : X → R) : sq.interaction f = f sq.tl - f sq.tr - f sq.bl + f sq.br

theorem HarmonicGrammar.Square.interaction_eq_zero_iff {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] {f : X → R} : sq.interaction f = 0 ↔ f sq.tl - f sq.tr = f sq.bl - f sq.br

The interaction vanishes iff the differences along the two rows agree ((13) of [Mag25]).

theorem HarmonicGrammar.Square.interaction_eq_zero_iff' {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] {f : X → R} : sq.interaction f = 0 ↔ f sq.tl - f sq.bl = f sq.tr - f sq.br

The interaction vanishes iff the differences along the two columns agree ((10) of [Mag25]).

@[simp]

theorem HarmonicGrammar.Square.interaction_transpose {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] (f : X → R) : sq.transpose.interaction f = sq.interaction f

theorem HarmonicGrammar.Square.InsensitiveToRow.interaction_eq_zero {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] {f : X → R} (h : sq.InsensitiveToRow f) : sq.interaction f = 0

theorem HarmonicGrammar.Square.InsensitiveToCol.interaction_eq_zero {X : Type u_1} {R : Type u_5} {sq : Square X} [CommRing R] {f : X → R} (h : sq.InsensitiveToCol f) : sq.interaction f = 0

theorem HarmonicGrammar.Square.Independent.interaction_sum_eq_zero {X : Type u_1} {Y : Type u_2} {R : Type u_5} {n : ℕ} {sq : Square X} [CommRing R] {con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)} (h : sq.Independent con) (φ : Fin n → (Y → ℕ) → R) : (sq.interaction fun (x : X) => ∑ k : Fin n, φ k (Function.curry (con k) x)) = 0

Under independence, a sum of per-constraint terms, each reading only its constraint's violations of the candidates of a form, has zero interaction.

theorem HarmonicGrammar.Square.Independent.interaction_harmonyScore_sub {X : Type u_1} {Y : Type u_2} {R : Type u_5} {n : ℕ} {sq : Square X} [CommRing R] {con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)} (h : sq.Independent con) (w : Fin n → R) (a b : Y) : (sq.interaction fun (x : X) => harmonyScore con w (x, a) - harmonyScore con w (x, b)) = 0

Under independence, the harmony difference between two candidates has zero interaction, for every weighting.

theorem HarmonicGrammar.Square.Independent.interaction_logOdds_maxEnt {X : Type u_1} {Y : Type u_2} {n : ℕ} {sq : Square X} [Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] {con : OptimalityTheory.ConstraintSet (X × Y) (Fin n)} (h : sq.Independent con) (w : Fin n → ℝ) (a b : Y) : (sq.interaction fun (x : X) => Real.log ((maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x_1 : Y) => (x, x_1)) con).violations w).real {a} / (maxEnt (OptimalityTheory.ConstraintSet.comap (fun (x_1 : Y) => (x, x_1)) con).violations w).real {b})) = 0

MaxEnt predicts HZ's generalization ((22) of [Mag25]): under independence, the MaxEnt log-odds of two candidates have zero interaction, for every weighting and every candidate set.