Study 2: 54-Language Word-Order Efficiency

@cite{hahn-degen-futrell-2021}

Tests the Efficient Trade-off Hypothesis: the ordering regularities of natural language optimize the memory-surprisal trade-off, serving the communicative interest of the hearer. 54 languages from Universal Dependencies corpora are measured against grammar-preserving random baselines. 50/54 languages have significantly more efficient trade-offs; the 4 exceptions (Latvian, North Sami, Polish, Slovak) all have high word-order freedom (high branching direction entropy).

Key empirical finding (Figure 13): branching direction entropy is negatively correlated with optimization strength (Spearman ρ ≈ −.58, p < .0001). Languages with freer word order show weaker optimization, plausibly because free-order languages use word order to encode information structure rather than minimize processing cost.

Values

• moreEfficient: whether the real language's trade-off AUC is significantly lower than baseline AUCs (two-sided binomial test, Hochberg-corrected p < .01)
• gMean1000: bootstrapped mean G × 1000 (SI Figure 2). G = fraction of baseline grammars less efficient than the real language. 1000 = fully optimized.
• branchDirEntropy1000: branching direction entropy × 1000 (higher = more word-order freedom). From branching_entropy.tsv at https://github.com/m-hahn/memory-surprisal (used in Figure 13 via order_freedom.R). Korean's entropy is unavailable in the published data.

structure Phenomena.WordOrder.Studies.HahnDegenFutrell2021.LanguageEfficiency : Type

Efficiency data for a single language from Study 2.

• name : String
• isoCode : String
• family : String
• moreEfficient : Bool

  Whether the real language's trade-off AUC is significantly lower than baseline AUCs (Hochberg-corrected p < .01). This is the empirical instantiation of Processing.MemorySurprisal.efficientTradeoffHypothesis from the theory module.

• gMean1000 : ℕ

  Bootstrapped mean G × 1000 (from SI Figure 2). 1000 = fully optimized.

• branchDirEntropy1000 : Option ℕ

  Branching direction entropy × 1000 (higher = more word-order freedom). none when the value is unavailable in the published data.

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instReprLanguageEfficiency.repr : LanguageEfficiency → ℕ → Std.Format

Equations

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

instance Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instReprLanguageEfficiency : Repr LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instReprLanguageEfficiency = { reprPrec := Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instReprLanguageEfficiency.repr }

instance Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instDecidableEqLanguageEfficiency : DecidableEq LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instDecidableEqLanguageEfficiency = Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instDecidableEqLanguageEfficiency.decEq

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instDecidableEqLanguageEfficiency.decEq (x✝ x✝¹ : LanguageEfficiency) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instBEqLanguageEfficiency.beq : LanguageEfficiency → LanguageEfficiency → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instBEqLanguageEfficiency.beq x✝¹ x✝ = false

instance Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instBEqLanguageEfficiency : BEq LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instBEqLanguageEfficiency = { beq := Phenomena.WordOrder.Studies.HahnDegenFutrell2021.instBEqLanguageEfficiency.beq }

Efficient languages (50)

G ≥ 0.5 in the LSTM estimator (main paper). Most have G = 1.0.

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.afrikaans : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.amharic : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.arabic : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.armenian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.bambara : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.bambara = { name := "Bambara", isoCode := "bm", family := "Mande", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 110 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.basque : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.basque = { name := "Basque", isoCode := "eu", family := "Isolate", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 397 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.breton : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.bulgarian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.buryat : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.cantonese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.catalan : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.chinese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.croatian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.czech : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.danish : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.dutch : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.english : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.erzya : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.erzya = { name := "Erzya", isoCode := "myv", family := "Uralic", moreEfficient := true, gMean1000 := 990, branchDirEntropy1000 := some 429 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.estonian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.faroese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.finnish : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.finnish = { name := "Finnish", isoCode := "fi", family := "Uralic", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 357 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.french : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.german : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.greek : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.hebrew : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.hindi : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.hungarian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.indonesian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.italian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.japanese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.kazakh : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.kazakh = { name := "Kazakh", isoCode := "kk", family := "Turkic", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 147 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.korean : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.korean = { name := "Korean", isoCode := "ko", family := "Koreanic", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := none }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.kurmanji : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.maltese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.naija : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.naija = { name := "Naija", isoCode := "pcm", family := "Creole", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 239 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.norwegian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.persian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.portuguese : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.romanian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.russian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.serbian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.slovenian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.spanish : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.swedish : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.thai : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.thai = { name := "Thai", isoCode := "th", family := "Kra-Dai", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 149 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.turkish : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.turkish = { name := "Turkish", isoCode := "tr", family := "Turkic", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 246 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.ukrainian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.urdu : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.urdu = { name := "Urdu", isoCode := "ur", family := "Indo-European", moreEfficient := true, gMean1000 := 1000, branchDirEntropy1000 := some 85 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.uyghur : LanguageEfficiency

Equations

• Phenomena.WordOrder.Studies.HahnDegenFutrell2021.uyghur = { name := "Uyghur", isoCode := "ug", family := "Turkic", moreEfficient := true, gMean1000 := 650, branchDirEntropy1000 := some 87 }

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.vietnamese : LanguageEfficiency

Equations

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

Exception languages (4)

G < 0.5 in the LSTM estimator (main paper, Figure 13; SI Figure 2). All have high branching direction entropy (free word order).

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.latvian : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.northSami : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.polish : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.slovak : LanguageEfficiency

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.allLanguages : List LanguageEfficiency

All 54 languages from Study 2 (SI Table 2).

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.efficientLanguages : List LanguageEfficiency

The 50 efficient languages.

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.exceptionLanguages : List LanguageEfficiency

The 4 exception languages.

Equations

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

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.total_count : allLanguages.length = 54

54 languages in total.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.most_languages_efficient : efficientLanguages.length = 50

50 out of 54 languages have more efficient word orders than baselines.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.exceptions_count : exceptionLanguages.length = 4

Exactly 4 exceptions.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.all_exceptions_have_high_word_order_freedom : (exceptionLanguages.all fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e > 300) | none => false) = true

All 4 exceptions have high branching direction entropy (> 300 × 10⁻³).

This supports the paper's explanation: languages with very free word order have weaker optimization pressure because many orderings are nearly equally acceptable, reducing the signal of optimization.

Entropy values from branching_entropy.tsv at https://github.com/m-hahn/memory-surprisal

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.all_exceptions_below_threshold : (exceptionLanguages.all fun (x : LanguageEfficiency) => decide (x.gMean1000 < 500)) = true

All 4 exceptions have G < 500 (below the optimization threshold).

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.efficiency_consistent_with_g_threshold : (allLanguages.all fun (l : LanguageEfficiency) => l.moreEfficient == decide (l.gMean1000 ≥ 500)) = true

The moreEfficient flag is consistent with a G ≥ 500 threshold across all 54 languages. This cross-checks two independently encoded fields: moreEfficient (from the binomial test) and gMean1000 (from SI Figure 2's bootstrapped fraction).

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.exceptions_below_all_efficient : (exceptionLanguages.all fun (exc : LanguageEfficiency) => efficientLanguages.all fun (eff : LanguageEfficiency) => decide (eff.gMean1000 > exc.gMean1000)) = true

The 4 exceptions form a contiguous block at the bottom of the G ranking: no efficient language has G below any exception's G.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.japanese_lowest_known_entropy : ((List.filterMap (fun (x : LanguageEfficiency) => x.branchDirEntropy1000) allLanguages).all fun (x : ℕ) => decide (x ≥ 24)) = true

Japanese has the lowest branching direction entropy among languages with known entropy data (most rigid word order). Korean is excluded because its entropy is not available in the published data.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.estonian_high_entropy_efficient : estonian.branchDirEntropy1000 = some 435 ∧ estonian.moreEfficient = true

Estonian has the highest entropy among efficient languages (435) but is still efficient (G = 0.80), showing that word-order freedom is necessary but not sufficient for being an exception.

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.meanEntropy (ls : List LanguageEfficiency) : ℕ

Mean branching direction entropy is higher for exceptions than efficient languages (computed over languages with known entropy).

Equations

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

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.exceptions_higher_mean_entropy : meanEntropy exceptionLanguages > meanEntropy efficientLanguages

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.slovak_lowest_g : (allLanguages.all fun (x : LanguageEfficiency) => decide (x.gMean1000 ≥ slovak.gMean1000)) = true

Slovak has the lowest G value (least evidence for optimization).

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.most_efficient_fully_optimized : (List.filter (fun (x : LanguageEfficiency) => decide (x.gMean1000 = 1000)) efficientLanguages).length = 42

42 out of 50 efficient languages have G = 1.0 (fully optimized: the real language beats every sampled baseline grammar).

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.futrellIsoCodes : List String

ISO codes appearing in @cite{futrell-gibson-2020}'s 32-language dataset.

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.hahnIsoCodes : List String

ISO codes appearing in this study's 54-language dataset.

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.sharedIsoCodes : List String

Languages in both datasets (by ISO code).

Equations

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

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.many_shared_languages : sharedIsoCodes.length ≥ 20

At least 20 languages appear in both datasets.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.shared_languages_mostly_efficient : (List.filter (fun (iso : String) => (List.filter (fun (x : LanguageEfficiency) => x.isoCode == iso) allLanguages).all fun (x : LanguageEfficiency) => x.moreEfficient) sharedIsoCodes).length ≥ sharedIsoCodes.length - 1

All but one shared language (Polish) are efficient in this study.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.polish_only_shared_exception : List.filter (fun (iso : String) => (List.filter (fun (x : LanguageEfficiency) => x.isoCode == iso) allLanguages).any fun (x : LanguageEfficiency) => !x.moreEfficient) sharedIsoCodes = ["pl"]

Polish is the only shared language that is an exception.

Negative correlation between word-order freedom and optimization

Figure 13 of @cite{hahn-degen-futrell-2021} shows that branching direction entropy (x-axis) is negatively correlated with the surprisal difference between real and baseline orders (y-axis). Spearman ρ ≈ −.58, p < .0001.

We cannot compute a Spearman correlation in Lean without a ranking function, but we can verify the key structural claims that drive the correlation:

• All low-entropy languages are efficient (rigid order → strong optimization)
• All exceptions have high entropy (free order → weak optimization)
• High entropy is necessary but not sufficient for being an exception

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.rigid_order_languages_efficient : ((List.filter (fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e < 300) | none => false) allLanguages).all fun (x : LanguageEfficiency) => x.moreEfficient) = true

Languages with known low branching entropy (< 300) are all efficient. This is the left side of Figure 13: rigid-order languages cluster at high surprisal difference (strong optimization).

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.exceptions_all_high_entropy : (exceptionLanguages.all fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e ≥ 315) | none => false) = true

All 4 exceptions have entropy ≥ 315. This is the lower-right of Figure 13: exceptions cluster at high entropy.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.high_entropy_not_sufficient : ((List.filter (fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e ≥ 315) | none => false) allLanguages).any fun (x : LanguageEfficiency) => x.moreEfficient) = true

Not all high-entropy languages are exceptions: word-order freedom is necessary but not sufficient for being an exception. Estonian (entropy 435) and Finnish (357) are efficient despite high entropy.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.low_entropy_higher_mean_g : have lowEntropy := List.filter (fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e < 250) | none => false) allLanguages; have highEntropy := List.filter (fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e ≥ 250) | none => false) allLanguages; List.foldl (fun (x1 x2 : ℕ) => x1 + x2) 0 (List.map (fun (x : LanguageEfficiency) => x.gMean1000) lowEntropy) / lowEntropy.length > List.foldl (fun (x1 x2 : ℕ) => x1 + x2) 0 (List.map (fun (x : LanguageEfficiency) => x.gMean1000) highEntropy) / highEntropy.length

The mean G value decreases as entropy increases: partition languages into low-entropy (< 250) and high-entropy (≥ 250) groups. The low-entropy group has higher mean G, consistent with the negative correlation.

Information locality generalizes dependency locality

@cite{hahn-degen-futrell-2021} argue (§"Other Kinds of Memory Bottlenecks" and Discussion) that information locality generalizes dependency length minimization: DLM minimizes structural distance between related words, while information locality minimizes the information-theoretic distance at which predictive information concentrates.

The HarmonicOrder module proves that consistent head direction achieves shorter dependency chains (harmonic_always_shorter). The present study shows that languages with shorter dependencies (lower branching entropy, more consistent direction) achieve better memory-surprisal trade-offs (rigid_order_languages_efficient). Together, these two results establish the chain: harmonic order → short dependencies → information locality → efficient trade-off.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.harmonic_dlm_holds : DepGrammar.HarmonicOrder.dlmPredictsHarmonicCheaper = true

The DLM harmonic order prediction holds: consistent head direction produces shorter total dependency length (from HarmonicOrder.lean).

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.dlm_to_efficiency_chain : DepGrammar.HarmonicOrder.dlmPredictsHarmonicCheaper = true ∧ ((List.filter (fun (l : LanguageEfficiency) => match l.branchDirEntropy1000 with | some e => decide (e < 300) | none => false) allLanguages).all fun (x : LanguageEfficiency) => x.moreEfficient) = true

The full chain: all languages with low entropy (consistent direction, short dependencies) are efficient, and the DLM prediction holds. This connects the structural argument (HarmonicOrder) to the information-theoretic result (memory-surprisal efficiency).

WALS Language Validation

The study uses ISO 639-1 codes (2-letter) from Universal Dependencies. WALS uses ISO 639-3 codes (3-letter). This mapping connects them, enabling family classification cross-checks against WALS v2020.4.

Coverage: 51 of 54 languages have WALS entries (missing: Buryat, Croatian, Serbian). Of 51, 42 have identical family names; 9 differ due to terminology (Turkic/Altaic, Japonic/Japanese, Kra-Dai/Tai-Kadai, etc.).

ISO 639-1 codes that coincide with ISO 639-3 pass through directly. For macrolanguages (Arabic, Chinese, Persian, Estonian), the mapping points to the specific ISO 639-3 variety used in WALS.

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.iso1to3 : List (String × String)

ISO 639-1 (study) → ISO 639-3 (WALS) mapping for the 54 languages.

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.walsLookup (l : LanguageEfficiency) : Option Core.WALS.Language

Look up a study language's WALS entry via its ISO code.

Equations

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

def Phenomena.WordOrder.Studies.HahnDegenFutrell2021.walsMatchedLanguages : List LanguageEfficiency

Languages with WALS entries (51 of 54).

Equations

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

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.wals_coverage : walsMatchedLanguages.length = 51

51 of 54 study languages have WALS entries.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.wals_missing : List.map (fun (x : LanguageEfficiency) => x.name) (List.filter (fun (x : LanguageEfficiency) => (walsLookup x).isNone) allLanguages) = ["Buryat", "Croatian", "Serbian"]

The 3 languages without WALS entries are Buryat, Croatian, and Serbian.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.wals_family_agreement_count : (List.filter (fun (l : LanguageEfficiency) => match walsLookup l with | some w => w.family == l.family | none => false) walsMatchedLanguages).length = 42

For all 42 languages where the family names agree, the study family matches the WALS family exactly.

theorem Phenomena.WordOrder.Studies.HahnDegenFutrell2021.wals_family_divergence_count : (List.filter (fun (l : LanguageEfficiency) => match walsLookup l with | some w => w.family != l.family | none => false) walsMatchedLanguages).length = 9

The 9 family-name divergences (all terminological, not errors):

• Basque: study "Isolate" vs WALS "Basque"
• Japanese: "Japonic" vs "Japanese"
• Kazakh/Turkish/Uyghur: "Turkic" vs "Altaic" (Altaic hypothesis disputed)
• Korean: "Koreanic" vs "Korean"
• Naija: "Creole" vs "other"
• Thai: "Kra-Dai" vs "Tai-Kadai"
• Vietnamese: "Austroasiatic" vs "Austro-Asiatic" (hyphenation)