DLM and the Head-Direction Generalization

@cite{dryer-1992} @cite{gibson-2025}

Connects the DLM (dependency length minimization) prediction that harmonic word order is cheaper to the WALS typological observation that harmonic word order is more common across languages (Phenomena.WordOrder.Typology).

For each of the 3 construction pairs in WALS:

• DLM predicts: disharmonic order is costly (higher TDL in recursive structures)
• WALS observes: disharmonic order is rare (fewer languages)

Also verifies well-formedness, projectivity, and Behaghel's law for the example trees from HarmonicOrder.lean.

def Phenomena.WordOrder.Studies.Dryer1992.walsConfirmsHarmonic (t : Typology.CrossTab) : Bool

WALS confirms harmonic order is more common, for a given table.

Equations

• Phenomena.WordOrder.Studies.Dryer1992.walsConfirmsHarmonic t = t.harmonicDominant

def Phenomena.WordOrder.Studies.Dryer1992.dlmWalsConsistent (t : Typology.CrossTab) : Bool

Combined consistency check: DLM prediction and WALS observation agree.

Equations

• Phenomena.WordOrder.Studies.Dryer1992.dlmWalsConsistent t = (DepGrammar.HarmonicOrder.dlmPredictsHarmonicCheaper && Phenomena.WordOrder.Studies.Dryer1992.walsConfirmsHarmonic t)

theorem Phenomena.WordOrder.Studies.Dryer1992.dlm_explains_head_direction_generalization : Typology.allTables.all dlmWalsConsistent = true

For all 3 construction pairs, DLM predicts harmonic is cheaper AND WALS confirms harmonic is more common.

This is @cite{gibson-2025}'s central claim: DLM explains the head-direction generalization.

theorem Phenomena.WordOrder.Studies.Dryer1992.vo_adposition_consistent : dlmWalsConsistent Typology.voAdposition = true

Per-table consistency theorems.

theorem Phenomena.WordOrder.Studies.Dryer1992.vo_subordinator_consistent : dlmWalsConsistent Typology.voSubordinator = true

theorem Phenomena.WordOrder.Studies.Dryer1992.vo_relative_clause_consistent : dlmWalsConsistent Typology.voRelativeClause = true