Rathi, Hahn, and Futrell (2026): Toward an information-theoretic model of morphological fusion based on an efficient tradeoff of memory and surprisal

Rathi, Hahn and Futrell measure the informational fusion of a form as its surprisal under a learner that has seen no form with the same features, and explain which features a language fuses by the tradeoff of memory and surprisal. Their simulations measure a language by the surprisal of its characters given t characters of context, on the stream of its words. We prove the appendix's two arguments for arbitrary languages, show that the second needs joint independence, build the stream and compute its surprisal, and derive the paper's claims about the toy languages of Tables 4 to 6 from it. The corpus studies rest on estimated language models and a neural learner, and are not formalized.

Main statements

• condEntropy_le_condEntropy_fused, VoiceTense.condEntropy_fused_lt: fusing a first feature with a second leaves the third its entropy given the second when the first is independent of the other two jointly, and can fail to when it is independent of each separately.
• pastCondEntropy_char_of_le: once the context spans a word, a stream whose characters reveal their position has the entropy of a word per character.
• VoiceTense.pastCondEntropy_fus_lt_agg_zero_iff, VoiceAspectTense.pastCondEntropy_agg_lt_fuseLow_one_iff: fusing dependent features lowers the surprisal without context, and fusing independent features raises it given one character.
• VoiceTense.pastCondEntropy_nonclustered_zero, VoiceTense.pastCondEntropy_tagged_agg_one_lt: category clustering leaves the surprisal without context unchanged and lowers it given one character.

Implementation notes

• Entropies are in nats. Feature values are Bools, with false for active, present and perfect. Tables 4 and 5 are the toy languages at d = 1/4, and Table 6 at d = 1/2.
• A learner is any function from a data set, a lexeme and a cell to a measure on forms, and informational fusion is Core's surprisal. A form the learner rules out has informational fusion ∞ in the paper and the junk value 0 of Real.log here.
• The stream writes the words of independent meanings one after another and starts at a uniformly random position of the first, which makes it stationary. The toy languages write each slot from its own alphabet (tagged), except the nonclustered language of Table 6, whose characters are morphemes tagged by category. The clustered language of Table 6 is the agglutinative language of Table 4.
• The appendix's second argument assumes only that the first feature is independent of the second, and its step dropping the fused part's information about the third needs joint independence. Its third argument compares slots: dropping category clustering raises the entropy of the first slot, but also of the second, and on the stream the random start absorbs the difference without context, as the low-memory end of Figure 6 shows.

References

• N. Rathi, M. Hahn, R. Futrell, Toward an information-theoretic model of morphological fusion based on an efficient tradeoff of memory and surprisal (2026)
• N. Rathi, M. Hahn, R. Futrell, An information-theoretic characterization of morphological fusion (2021)
• M. Hahn, J. Degen, R. Futrell, Modeling word and morpheme order in natural language as an efficient trade-off of memory and surprisal (2021)
• S. Wu, R. Cotterell, T. O'Donnell, Morphological irregularity correlates with frequency (2019)
• J. Mansfield, S. Stoll, B. Bickel, Category clustering: a probabilistic bias in the morphology of verbal agreement marking (2020)
• T. M. Cover, J. A. Thomas, Elements of information theory (2006)

Informational fusion

noncomputable def RathiHahnFutrell2026.fusion {Lex : Type u_1} {K : Type u_2} {Form : Type u_3} {V : K → Type u_4} [MeasurableSpace Form] (learner : Set (Lex × ((k : K) → V k) × Form) → Lex → ((k : K) → V k) → MeasureTheory.Measure Form) (L : Lex → ((k : K) → V k) → Form) (J : Set K) (ℓ : Lex) (σ : (k : K) → V k) : ℝ

The fusion of the form of the lexeme ℓ in the cell σ of the language L, over the categories J, is its surprisal under a learner trained on the words of L whose cells differ from σ in some category of J. A cell gives each category k a value in V k, and a word is a lexeme, a cell and a form. Where fusion holds out cells, [WCOD19]'s irregularity holds out a lexeme.

Equations

• RathiHahnFutrell2026.fusion learner L J ℓ σ = InformationTheory.surprisal (learner {w : Lex × ((k : K) → V k) × Form | (w.2.1 ∉ J.pi fun (k : K) => {σ k}) ∧ w.2.2 = L w.1 w.2.1} ℓ σ) (L ℓ σ)

theorem RathiHahnFutrell2026.fusion_univ {Lex : Type u_1} {K : Type u_2} {Form : Type u_3} {V : K → Type u_4} [MeasurableSpace Form] (learner : Set (Lex × ((k : K) → V k) × Form) → Lex → ((k : K) → V k) → MeasureTheory.Measure Form) (L : Lex → ((k : K) → V k) → Form) (ℓ : Lex) (σ : (k : K) → V k) : fusion learner L Set.univ ℓ σ = InformationTheory.surprisal (learner {w : Lex × ((k : K) → V k) × Form | w.2.1 ≠ σ ∧ w.2.2 = L w.1 w.2.1} ℓ σ) (L ℓ σ)

Over all categories, fusion is the paper's informational fusion, which holds out the words of the cell σ itself.

theorem RathiHahnFutrell2026.fusion_pair_eq_fusion_univ {Lex : Type u_1} {K : Type u_2} {Form : Type u_3} {V : K → Type u_4} [MeasurableSpace Form] (learner : Set (Lex × ((k : K) → V k) × Form) → Lex → ((k : K) → V k) → MeasureTheory.Measure Form) (L : Lex → ((k : K) → V k) → Form) {k₁ k₂ : K} (h : ∀ (k : K), k = k₁ ∨ k = k₂) : fusion learner L {k₁, k₂} = fusion learner L Set.univ

In a language with two categories, pairwise fusion is informational fusion.

The appendix's arguments

theorem RathiHahnFutrell2026.entropy_fused_eq {Ω : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {F : Type u_5} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace S₁] [MeasurableSingletonClass S₁] [Fintype S₁] [MeasurableSpace S₂] [MeasurableSingletonClass S₂] [Fintype S₂] [MeasurableSpace F] [MeasurableSingletonClass F] [Fintype F] {X₁ : Ω → S₁} {X₂ : Ω → S₂} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) {g : S₁ → S₂ → F} (hg : ∀ (a : S₁), Function.Injective (g a)) : InformationTheory.entropy (fun (ω : Ω) => g (X₁ ω) (X₂ ω)) μ = InformationTheory.condEntropy X₂ X₁ μ + InformationTheory.mutualInfo (fun (ω : Ω) => g (X₁ ω) (X₂ ω)) X₁ μ

A part fusing two features that still identifies the second once the first is known has the entropy of the second feature given the first, plus what it keeps of the first.

theorem RathiHahnFutrell2026.condEntropy_le_entropy_fused {Ω : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {F : Type u_5} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace S₁] [MeasurableSingletonClass S₁] [Fintype S₁] [MeasurableSpace S₂] [MeasurableSingletonClass S₂] [Fintype S₂] [MeasurableSpace F] [MeasurableSingletonClass F] [Fintype F] {X₁ : Ω → S₁} {X₂ : Ω → S₂} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) {g : S₁ → S₂ → F} (hg : ∀ (a : S₁), Function.Injective (g a)) : InformationTheory.condEntropy X₂ X₁ μ ≤ InformationTheory.entropy (fun (ω : Ω) => g (X₁ ω) (X₂ ω)) μ

Such a part has at least the entropy of the second feature given the first, the bound of the appendix's first argument. An agglutinative part has the entropy of the second feature.

theorem RathiHahnFutrell2026.condEntropy_le_condEntropy_fused {Ω : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {S₃ : Type u_4} {F : Type u_5} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [MeasurableSpace S₁] [MeasurableSingletonClass S₁] [Fintype S₁] [MeasurableSpace S₂] [MeasurableSingletonClass S₂] [Fintype S₂] [MeasurableSpace S₃] [MeasurableSingletonClass S₃] [Fintype S₃] [MeasurableSpace F] [MeasurableSingletonClass F] [Fintype F] {X₁ : Ω → S₁} {X₂ : Ω → S₂} {X₃ : Ω → S₃} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₃ : Measurable X₃) (hind : ProbabilityTheory.IndepFun X₁ (fun (ω : Ω) => (X₂ ω, X₃ ω)) μ) (g : S₁ → S₂ → F) : InformationTheory.condEntropy X₃ X₂ μ ≤ InformationTheory.condEntropy X₃ (fun (ω : Ω) => g (X₁ ω) (X₂ ω)) μ

A part fusing a feature independent of the other two with the second leaves the third feature at least its entropy given the second, the appendix's second argument.

theorem RathiHahnFutrell2026.condEntropy_xor_eq_entropy {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V D : Ω → Bool} (hV : Measurable V) (hD : Measurable D) (hind : ProbabilityTheory.IndepFun V D μ) : InformationTheory.condEntropy (fun (ω : Ω) => V ω ^^ D ω) D μ = InformationTheory.entropy V μ

XOR with a bit independent of D keeps that bit's entropy given D.

theorem RathiHahnFutrell2026.entropy_xor_eq_log_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V D : Ω → Bool} (hV : Measurable V) (hD : Measurable D) (hind : ProbabilityTheory.IndepFun V D μ) (hfair : InformationTheory.entropy V μ = Real.log 2) : InformationTheory.entropy (fun (ω : Ω) => V ω ^^ D ω) μ = Real.log 2

XOR with a fair bit independent of D is a fair bit.

Independent words

def RathiHahnFutrell2026.tagged {M : Type u_1} {B : Type u_2} {ι : Type u_3} (L : M → ι → B) (m : M) (p : ι) : ι × B

A language whose slots have disjoint alphabets writes each slot's value tagged by the slot, as the paper's toy languages write A or B first and C or D second.

Equations

• RathiHahnFutrell2026.tagged L m p = (p, L m p)

theorem RathiHahnFutrell2026.entropy_eval {M : Type u_1} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] {S : Type u_4} [MeasurableSpace S] (f : M → S) (n : ℕ) : InformationTheory.entropy (fun (w : ℕ → M) => f (w n)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P) = InformationTheory.entropy f P

theorem RathiHahnFutrell2026.condEntropy_eval {M : Type u_1} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] {S : Type u_4} {T : Type u_5} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [Fintype S] [MeasurableSingletonClass T] [Fintype T] (f : M → S) (g : M → T) (n : ℕ) : InformationTheory.condEntropy (fun (w : ℕ → M) => f (w n)) (fun (w : ℕ → M) => g (w n)) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P) = InformationTheory.condEntropy f g P

theorem RathiHahnFutrell2026.condEntropy_eval_of_ne {M : Type u_1} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] {S : Type u_4} {T : Type u_5} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [Fintype S] [MeasurableSingletonClass T] [Fintype T] (f : M → S) (g : M → T) {n n' : ℕ} (h : n ≠ n') : InformationTheory.condEntropy (fun (w : ℕ → M) => f (w n)) (fun (w : ℕ → M) => g (w n')) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P) = InformationTheory.entropy f P

theorem RathiHahnFutrell2026.entropy_eval_pair {M : Type u_1} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] {S : Type u_4} {T : Type u_5} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSingletonClass S] [Fintype S] [MeasurableSingletonClass T] [Fintype T] (f : M → S) (g : M → T) {n n' : ℕ} (h : n ≠ n') : InformationTheory.entropy (fun (w : ℕ → M) => (f (w n), g (w n'))) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P) = InformationTheory.entropy f P + InformationTheory.entropy g P

The character stream

The paper measures a language by the surprisal of its characters under an (t + 1)-gram model, the forms of independent meanings written one after another. Read from a uniformly random position of the first word, that stream is stationary, and its surprisal given t characters of context is pastCondEntropy (char L) (stream k P) t.

def RathiHahnFutrell2026.char {M : Type u_1} {A : Type u_2} {k : ℕ} [NeZero k] (L : M → Fin k → A) (t : ℕ) (ω : Fin k × (ℕ → M)) : A

The character at time t of the stream of the language L, whose words have k characters, read from position ω.1 of the first of the words ω.2.

Equations

• RathiHahnFutrell2026.char L t ω = L (ω.2 ((t + ↑ω.1) / k)) (Fin.ofNat k (t + ↑ω.1))

def RathiHahnFutrell2026.advance {M : Type u_1} {k : ℕ} [NeZero k] (ω : Fin k × (ℕ → M)) : Fin k × (ℕ → M)

Advancing the stream by one character moves the start one position on, and past the last position on to the next word.

Equations

• RathiHahnFutrell2026.advance ω = (ω.1 + 1, if ↑ω.1 + 1 = k then fun (n : ℕ) => ω.2 (n + 1) else ω.2)

theorem RathiHahnFutrell2026.char_succ {M : Type u_1} {A : Type u_2} {k : ℕ} [NeZero k] (L : M → Fin k → A) (t : ℕ) : char L (t + 1) = char L t ∘ advance

theorem RathiHahnFutrell2026.char_zero {M : Type u_1} {A : Type u_2} {k : ℕ} [NeZero k] (L : M → Fin k → A) : char L 0 = fun (ω : Fin k × (ℕ → M)) => L (ω.2 0) ω.1

theorem RathiHahnFutrell2026.map_add_uniformOn {k : ℕ} [NeZero k] (c : Fin k) : MeasureTheory.Measure.map (fun (x : Fin k) => x + c) (ProbabilityTheory.uniformOn Set.univ) = ProbabilityTheory.uniformOn Set.univ

noncomputable def RathiHahnFutrell2026.stream {M : Type u_1} [MeasurableSpace M] (k : ℕ) (P : MeasureTheory.Measure M) : MeasureTheory.Measure (Fin k × (ℕ → M))

Words of independent meanings with law P, read from a uniformly random position of the first.

Equations

• RathiHahnFutrell2026.stream k P = (ProbabilityTheory.uniformOn Set.univ).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P)

theorem RathiHahnFutrell2026.measureReal_fst {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] (j : Fin k) : (stream k P).real (Prod.fst ⁻¹' {j}) = (↑k)⁻¹

instance RathiHahnFutrell2026.instIsProbabilityMeasureProdFinForallNatStream {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] : MeasureTheory.IsProbabilityMeasure (stream k P)

theorem RathiHahnFutrell2026.measurePreserving_advance {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] : MeasureTheory.MeasurePreserving advance (stream k P) (stream k P)

theorem RathiHahnFutrell2026.cond_fst {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] (j : Fin k) : (stream k P)[|Prod.fst ⁻¹' {j}] = (MeasureTheory.Measure.dirac j).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P)

Given where the stream starts, its words are independent with law P.

theorem RathiHahnFutrell2026.entropy_fst {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] : InformationTheory.entropy Prod.fst (stream k P) = Real.log ↑k

theorem RathiHahnFutrell2026.entropy_fst_prod {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] {S : Type u_3} [MeasurableSpace S] {X : Fin k → (ℕ → M) → S} (hX : ∀ (j : Fin k), Measurable (X j)) [MeasurableSingletonClass S] [Fintype S] : InformationTheory.entropy (fun (ω : Fin k × (ℕ → M)) => (ω.1, X ω.1 ω.2)) (stream k P) = Real.log ↑k + (↑k)⁻¹ * ∑ j : Fin k, InformationTheory.entropy (X j) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P)

The entropy of the start together with a variable that depends on it averages over the starts.

theorem RathiHahnFutrell2026.condEntropy_fst_prod {M : Type u_1} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] {S : Type u_3} {T : Type u_4} [MeasurableSpace S] {X : Fin k → (ℕ → M) → S} (hX : ∀ (j : Fin k), Measurable (X j)) [MeasurableSingletonClass S] [Fintype S] [MeasurableSpace T] [MeasurableSingletonClass T] [Fintype T] {Y : Fin k → (ℕ → M) → T} (hY : ∀ (j : Fin k), Measurable (Y j)) : InformationTheory.condEntropy (fun (ω : Fin k × (ℕ → M)) => X ω.1 ω.2) (fun (ω : Fin k × (ℕ → M)) => (ω.1, Y ω.1 ω.2)) (stream k P) = (↑k)⁻¹ * ∑ j : Fin k, InformationTheory.condEntropy (X j) (Y j) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => P)

Given the start as well, conditional entropy averages over the starts.

theorem RathiHahnFutrell2026.measurable_char {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] (L : M → Fin k → A) (t : ℕ) : Measurable (char L t)

theorem RathiHahnFutrell2026.isStationary_char {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] (L : M → Fin k → A) : ProbabilityTheory.IsStationary (char L) (stream k P)

The character stream is stationary.

theorem RathiHahnFutrell2026.le_pastCondEntropy_char {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] (L : M → Fin k → A) [MeasurableSingletonClass A] [Fintype A] (t : ℕ) : (↑k)⁻¹ * InformationTheory.entropy (fun (m : M) => L m) P ≤ InformationTheory.pastCondEntropy (char L) (stream k P) t

With any context, a character of the stream has at least the entropy of a word per character.

theorem RathiHahnFutrell2026.condEntropy_char_one {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] (L : M → Fin k → A) [MeasurableSingletonClass A] [Fintype A] : InformationTheory.condEntropy (char L 1) (fun (ω : Fin k × (ℕ → M)) => (ω.1, char L 0 ω)) (stream k P) = (↑k)⁻¹ * ∑ j : Fin k, if ↑j + 1 < k then InformationTheory.condEntropy (fun (m : M) => L m (j + 1)) (fun (m : M) => L m j) P else InformationTheory.entropy (fun (m : M) => L m 0) P

Given the start, one character of context leaves the next the entropy of its position given the previous one, or at the start of a word its entropy.

theorem RathiHahnFutrell2026.pastCondEntropy_char_of_le {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] {L : M → Fin k → A} [MeasurableSingletonClass A] [Fintype A] {pos : A → Fin k} (hpos : ∀ (m : M) (p : Fin k), pos (L m p) = p) {t : ℕ} (ht : 0 < t) (hkt : k ≤ t + 1) : InformationTheory.pastCondEntropy (char L) (stream k P) t = (↑k)⁻¹ * InformationTheory.entropy (fun (m : M) => L m) P

Once the context spans a word, a language whose characters reveal their position has the entropy of a word per character.

theorem RathiHahnFutrell2026.entropyRate_char {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] {L : M → Fin k → A} [MeasurableSingletonClass A] [Fintype A] {pos : A → Fin k} (hpos : ∀ (m : M) (p : Fin k), pos (L m p) = p) : InformationTheory.entropyRate (char L) (stream k P) = (↑k)⁻¹ * InformationTheory.entropy (fun (m : M) => L m) P

Its entropy rate is the entropy of a word per character.

theorem RathiHahnFutrell2026.pastCondEntropy_char_zero {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] {L : M → Fin k → A} [MeasurableSingletonClass A] [Fintype A] {pos : A → Fin k} (hpos : ∀ (m : M) (p : Fin k), pos (L m p) = p) : InformationTheory.pastCondEntropy (char L) (stream k P) 0 = Real.log ↑k + (↑k)⁻¹ * ∑ p : Fin k, InformationTheory.entropy (fun (m : M) => L m p) P

With no context, it has log k plus the average entropy of a position.

theorem RathiHahnFutrell2026.pastCondEntropy_char_one {M : Type u_1} {A : Type u_2} {k : ℕ} [MeasurableSpace M] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] [NeZero k] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace A] {L : M → Fin k → A} [MeasurableSingletonClass A] [Fintype A] {pos : A → Fin k} (hpos : ∀ (m : M) (p : Fin k), pos (L m p) = p) : InformationTheory.pastCondEntropy (char L) (stream k P) 1 = InformationTheory.condEntropy (char L 1) (fun (ω : Fin k × (ℕ → M)) => (ω.1, char L 0 ω)) (stream k P)

With one character of context, knowing the start adds nothing, since the character reveals it.

theorem RathiHahnFutrell2026.pastCondEntropy_tagged_zero {M : Type u_1} {B : Type u_2} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace B] [MeasurableSingletonClass B] [Fintype B] {k : ℕ} [NeZero k] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] (L : M → Fin k → B) : InformationTheory.pastCondEntropy (char (tagged L)) (stream k P) 0 = Real.log ↑k + (↑k)⁻¹ * ∑ p : Fin k, InformationTheory.entropy (fun (m : M) => L m p) P

With no context, a language tagged by slot has log k plus the average entropy of a slot.

theorem RathiHahnFutrell2026.pastCondEntropy_tagged_one {M : Type u_1} {B : Type u_2} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace B] [MeasurableSingletonClass B] [Fintype B] {k : ℕ} [NeZero k] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] (L : M → Fin k → B) : InformationTheory.pastCondEntropy (char (tagged L)) (stream k P) 1 = (↑k)⁻¹ * ∑ j : Fin k, if ↑j + 1 < k then InformationTheory.condEntropy (fun (m : M) => L m (j + 1)) (fun (m : M) => L m j) P else InformationTheory.entropy (fun (m : M) => L m 0) P

With one character of context, it has the entropy of a slot given the one before it, averaged with the entropy of the first slot.

theorem RathiHahnFutrell2026.pastCondEntropy_tagged_of_le {M : Type u_1} {B : Type u_2} [MeasurableSpace M] [MeasurableSingletonClass M] [Fintype M] [MeasurableSpace B] [MeasurableSingletonClass B] [Fintype B] {k : ℕ} [NeZero k] (P : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure P] (L : M → Fin k → B) {t : ℕ} (ht : 0 < t) (hkt : k ≤ t + 1) : InformationTheory.pastCondEntropy (char (tagged L)) (stream k P) t = (↑k)⁻¹ * InformationTheory.entropy (fun (m : M) => L m) P

Once the context spans a word, it has the entropy of a word per character.

The toy languages

noncomputable def RathiHahnFutrell2026.half : ↑unitInterval

The fair coin as a point of the unit interval.

Equations

• RathiHahnFutrell2026.half = ⟨2⁻¹, RathiHahnFutrell2026.half._proof_4⟩

noncomputable def RathiHahnFutrell2026.bits {n : ℕ} (p : Fin n → ↑unitInterval) : MeasureTheory.Measure (Fin n → Bool)

Independent bits, bit i being true with probability p i.

Equations

• RathiHahnFutrell2026.bits p = MeasureTheory.Measure.pi fun (i : Fin n) => ProbabilityTheory.bernoulliMeasure true false (p i)

instance RathiHahnFutrell2026.instIsProbabilityMeasureForallFinBoolBits {n : ℕ} (p : Fin n → ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (bits p)

theorem RathiHahnFutrell2026.iIndepFun_bits {n : ℕ} (p : Fin n → ↑unitInterval) : ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Fin n → Bool) => ω i) (bits p)

theorem RathiHahnFutrell2026.entropy_bit {n : ℕ} (p : Fin n → ↑unitInterval) (i : Fin n) : InformationTheory.entropy (fun (ω : Fin n → Bool) => ω i) (bits p) = Real.binEntropy ↑(p i)

theorem RathiHahnFutrell2026.bits_real_singleton {n : ℕ} (p : Fin n → ↑unitInterval) (x : Fin n → Bool) : (bits p).real {x} = ∏ i : Fin n, if x i = true then ↑(p i) else 1 - ↑(p i)

A sequence of bits has the product of their probabilities.

Fusion lowers local surprisal, Table 4

noncomputable def RathiHahnFutrell2026.VoiceTense.meanings (d : ↑unitInterval) : MeasureTheory.Measure (Fin 2 → Bool)

The meanings of Tables 4 and 6 when tense disagrees with voice with probability d. The first bit is the voice, a fair coin, and the second says whether tense disagrees with voice.

Equations

• RathiHahnFutrell2026.VoiceTense.meanings d = RathiHahnFutrell2026.bits ![RathiHahnFutrell2026.half, d]

def RathiHahnFutrell2026.VoiceTense.voice (ω : Fin 2 → Bool) : Bool

The voice feature, false for active.

Equations

• RathiHahnFutrell2026.VoiceTense.voice ω = ω 0

def RathiHahnFutrell2026.VoiceTense.tense (ω : Fin 2 → Bool) : Bool

The tense feature, false for present.

Equations

• RathiHahnFutrell2026.VoiceTense.tense ω = (ω 0 ^^ ω 1)

instance RathiHahnFutrell2026.VoiceTense.instIsProbabilityMeasureForallFinOfNatNatBoolMeanings (d : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (meanings d)

theorem RathiHahnFutrell2026.VoiceTense.meanings_real (d : ↑unitInterval) (v t : Bool) : (meanings d).real {ω : Fin 2 → Bool | voice ω = v ∧ tense ω = t} = (if v = t then 1 - ↑d else ↑d) / 2

Voice and tense agree with probability 1 - d, as in the probabilities of Table 4.

theorem RathiHahnFutrell2026.VoiceTense.entropy_voice (d : ↑unitInterval) : InformationTheory.entropy voice (meanings d) = Real.log 2

theorem RathiHahnFutrell2026.VoiceTense.condEntropy_tense_voice (d : ↑unitInterval) : InformationTheory.condEntropy tense voice (meanings d) = Real.binEntropy ↑d

theorem RathiHahnFutrell2026.VoiceTense.entropy_tense (d : ↑unitInterval) : InformationTheory.entropy tense (meanings d) = Real.log 2

theorem RathiHahnFutrell2026.VoiceTense.mutualInfo_tense_voice (d : ↑unitInterval) : InformationTheory.mutualInfo tense voice (meanings d) = Real.log 2 - Real.binEntropy ↑d

def RathiHahnFutrell2026.VoiceTense.agg (ω : Fin 2 → Bool) : Fin 2 → Bool

The agglutinative language Lagg writes voice in its first slot and tense in its second. Tagged by slot, it is also the language Lclustered of Table 6, which writes the voice morpheme and then the tense morpheme, the category clustering of [MSB20].

Equations

• RathiHahnFutrell2026.VoiceTense.agg ω = ![RathiHahnFutrell2026.VoiceTense.voice ω, RathiHahnFutrell2026.VoiceTense.tense ω]

def RathiHahnFutrell2026.VoiceTense.fus (ω : Fin 2 → Bool) : Fin 2 → Bool

The fusional language Lfus writes voice and then the exclusive or of the two features.

Equations

• RathiHahnFutrell2026.VoiceTense.fus ω = ![RathiHahnFutrell2026.VoiceTense.voice ω, RathiHahnFutrell2026.VoiceTense.voice ω ^^ RathiHahnFutrell2026.VoiceTense.tense ω]

theorem RathiHahnFutrell2026.VoiceTense.entropy_fus_one (d : ↑unitInterval) : InformationTheory.entropy (fun (ω : Fin 2 → Bool) => fus ω 1) (meanings d) = Real.binEntropy ↑d

theorem RathiHahnFutrell2026.VoiceTense.pastCondEntropy_fus_lt_agg_zero_iff (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged fus)) (stream 2 (meanings d)) 0 < InformationTheory.pastCondEntropy (char (tagged agg)) (stream 2 (meanings d)) 0 ↔ ↑d ≠ 2⁻¹

With no context, the fusional language is less surprising exactly when the features are dependent.

theorem RathiHahnFutrell2026.VoiceTense.pastCondEntropy_fus_eq_agg (d : ↑unitInterval) {t : ℕ} (ht : 0 < t) : InformationTheory.pastCondEntropy (char (tagged fus)) (stream 2 (meanings d)) t = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 2 (meanings d)) t

With any context, the two languages are equally surprising: fusion helps only without context.

theorem RathiHahnFutrell2026.VoiceTense.mutualInfo_disagree_tense (d : ↑unitInterval) : InformationTheory.mutualInfo (fun (ω : Fin 2 → Bool) => ω 1) tense (meanings d) = 0

Voice, a fair coin, masks the disagreement bit, so tense carries no information about it.

theorem RathiHahnFutrell2026.VoiceTense.condEntropy_fused_lt (d : ↑unitInterval) (h₀ : 0 < ↑d) (h₁ : ↑d < 1) (hd : ↑d ≠ 2⁻¹) : InformationTheory.mutualInfo (fun (ω : Fin 2 → Bool) => ω 1) voice (meanings d) = 0 ∧ InformationTheory.mutualInfo (fun (ω : Fin 2 → Bool) => ω 1) tense (meanings d) = 0 ∧ 0 < InformationTheory.mutualInfo tense voice (meanings d) ∧ InformationTheory.condEntropy tense (fun (ω : Fin 2 → Bool) => (ω 1, voice ω)) (meanings d) < InformationTheory.condEntropy tense voice (meanings d)

The hypotheses the appendix states for its second argument do not suffice. Take the disagreement bit as a first feature: it is independent of voice and of tense, and voice and tense share information, yet a part that fuses it with voice determines tense.

Category clustering, Table 6

def RathiHahnFutrell2026.VoiceTense.nonclustered (ω : Fin 2 → Bool) : Fin 2 → Fin 2 × Bool

The language Lnonclustered of Table 6 writes the tense morpheme first when tense disagrees with voice. A morpheme is its category, 0 for voice and 1 for tense, and its value.

Equations

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

theorem RathiHahnFutrell2026.VoiceTense.entropy_nonclustered_fst (d : ↑unitInterval) : InformationTheory.entropy (fun (ω : Fin 2 → Bool) => nonclustered ω 0) (meanings d) = Real.log 2 + Real.binEntropy ↑d

Without category clustering the first slot identifies the meaning, so its entropy exceeds the clustered language's by binEntropy d.

theorem RathiHahnFutrell2026.VoiceTense.entropy_nonclustered_fst_half : InformationTheory.entropy (fun (ω : Fin 2 → Bool) => nonclustered ω 0) (meanings half) = 2 * InformationTheory.entropy voice (meanings half)

At the paper's uniform weights, dropping category clustering doubles the entropy of the first slot, as the appendix says.

theorem RathiHahnFutrell2026.VoiceTense.entropy_nonclustered_snd (d : ↑unitInterval) : InformationTheory.entropy (fun (ω : Fin 2 → Bool) => nonclustered ω 1) (meanings d) = Real.log 2 + Real.binEntropy ↑d

The second slot of Lnonclustered identifies the meaning as well, against the appendix's statement that its surprisal is unchanged.

theorem RathiHahnFutrell2026.VoiceTense.pastCondEntropy_nonclustered_zero (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char nonclustered) (stream 2 (meanings d)) 0 = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 2 (meanings d)) 0

Without context, dropping category clustering leaves the surprisal unchanged: the uniformly random start averages away which category comes first.

theorem RathiHahnFutrell2026.VoiceTense.pastCondEntropy_tagged_agg_one_le (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged agg)) (stream 2 (meanings d)) 1 ≤ InformationTheory.pastCondEntropy (char nonclustered) (stream 2 (meanings d)) 1

With one character of context, the clustered language is no more surprising.

theorem RathiHahnFutrell2026.VoiceTense.pastCondEntropy_tagged_agg_one_lt : InformationTheory.pastCondEntropy (char (tagged agg)) (stream 2 (meanings half)) 1 < InformationTheory.pastCondEntropy (char nonclustered) (stream 2 (meanings half)) 1

At the paper's uniform weights, the clustered language is strictly less surprising with one character of context: in the nonclustered stream two consecutive characters still carry information about where the stream started, since two voice morphemes in a row cross a word boundary.

Fusing independent features raises long-range surprisal, Table 5

noncomputable def RathiHahnFutrell2026.VoiceAspectTense.meanings (d : ↑unitInterval) : MeasureTheory.Measure (Fin 3 → Bool)

The meanings of Table 5 when tense disagrees with aspect with probability d. Voice and aspect are fair coins, and the third bit says whether tense disagrees with aspect.

Equations

• RathiHahnFutrell2026.VoiceAspectTense.meanings d = RathiHahnFutrell2026.bits ![RathiHahnFutrell2026.half, RathiHahnFutrell2026.half, d]

def RathiHahnFutrell2026.VoiceAspectTense.voice (ω : Fin 3 → Bool) : Bool

The voice feature, false for active.

Equations

• RathiHahnFutrell2026.VoiceAspectTense.voice ω = ω 0

def RathiHahnFutrell2026.VoiceAspectTense.aspect (ω : Fin 3 → Bool) : Bool

The aspect feature, false for perfect.

Equations

• RathiHahnFutrell2026.VoiceAspectTense.aspect ω = ω 1

def RathiHahnFutrell2026.VoiceAspectTense.tense (ω : Fin 3 → Bool) : Bool

The tense feature, false for present.

Equations

• RathiHahnFutrell2026.VoiceAspectTense.tense ω = (ω 1 ^^ ω 2)

def RathiHahnFutrell2026.VoiceAspectTense.agg (ω : Fin 3 → Bool) : Fin 3 → Bool

The agglutinative language Lagg writes each feature in its own slot.

Equations

• RathiHahnFutrell2026.VoiceAspectTense.agg ω = ![RathiHahnFutrell2026.VoiceAspectTense.voice ω, RathiHahnFutrell2026.VoiceAspectTense.aspect ω, RathiHahnFutrell2026.VoiceAspectTense.tense ω]

def RathiHahnFutrell2026.VoiceAspectTense.fuseLow (ω : Fin 3 → Bool) : Fin 3 → Bool

The language Lfuse-low fuses the independent voice and aspect in its second slot.

Equations

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

def RathiHahnFutrell2026.VoiceAspectTense.fuseHigh (ω : Fin 3 → Bool) : Fin 3 → Bool

The language Lfuse-high fuses the dependent aspect and tense in its third slot.

Equations

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

instance RathiHahnFutrell2026.VoiceAspectTense.instIsProbabilityMeasureForallFinOfNatNatBoolMeanings (d : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (meanings d)

theorem RathiHahnFutrell2026.VoiceAspectTense.meanings_real (d : ↑unitInterval) (v a t : Bool) : (meanings d).real {ω : Fin 3 → Bool | voice ω = v ∧ aspect ω = a ∧ tense ω = t} = (if a = t then 1 - ↑d else ↑d) / 4

Aspect and tense agree with probability 1 - d, as in the probabilities of Table 5.

theorem RathiHahnFutrell2026.VoiceAspectTense.condEntropy_tense_aspect (d : ↑unitInterval) : InformationTheory.condEntropy tense aspect (meanings d) = Real.binEntropy ↑d

theorem RathiHahnFutrell2026.VoiceAspectTense.entropy_tense (d : ↑unitInterval) : InformationTheory.entropy tense (meanings d) = Real.log 2

theorem RathiHahnFutrell2026.VoiceAspectTense.condEntropy_fuseHigh (d : ↑unitInterval) : InformationTheory.condEntropy (fun (ω : Fin 3 → Bool) => fuseHigh ω 2) (fun (ω : Fin 3 → Bool) => fuseHigh ω 1) (meanings d) = Real.binEntropy ↑d

Fusing the dependent aspect and tense costs nothing, since the third slot given the second keeps the entropy of tense given aspect.

theorem RathiHahnFutrell2026.VoiceAspectTense.condEntropy_agg_le_fuseLow (d : ↑unitInterval) : InformationTheory.condEntropy (fun (ω : Fin 3 → Bool) => agg ω 2) (fun (ω : Fin 3 → Bool) => agg ω 1) (meanings d) ≤ InformationTheory.condEntropy (fun (ω : Fin 3 → Bool) => fuseLow ω 2) (fun (ω : Fin 3 → Bool) => fuseLow ω 1) (meanings d)

Fusing voice with aspect leaves the third slot at least the entropy of tense given aspect, as the appendix's second argument says, since voice is independent of aspect and tense together.

theorem RathiHahnFutrell2026.VoiceAspectTense.condEntropy_fuseLow (d : ↑unitInterval) : InformationTheory.condEntropy (fun (ω : Fin 3 → Bool) => fuseLow ω 2) (fun (ω : Fin 3 → Bool) => fuseLow ω 1) (meanings d) = Real.log 2

Fusing the independent voice and aspect hides aspect from the second slot, so the third slot given the second keeps the whole entropy of tense.

theorem RathiHahnFutrell2026.VoiceAspectTense.pastCondEntropy_fuseLow_zero (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged fuseLow)) (stream 3 (meanings d)) 0 = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) 0

With no context, fusing the independent voice and aspect leaves the surprisal unchanged.

theorem RathiHahnFutrell2026.VoiceAspectTense.pastCondEntropy_fuseHigh_lt_agg_zero_iff (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged fuseHigh)) (stream 3 (meanings d)) 0 < InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) 0 ↔ ↑d ≠ 2⁻¹

With no context, fusing the dependent aspect and tense lowers the surprisal exactly when they are dependent.

theorem RathiHahnFutrell2026.VoiceAspectTense.pastCondEntropy_fuseHigh_one (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged fuseHigh)) (stream 3 (meanings d)) 1 = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) 1

With one character of context, fusing the dependent aspect and tense costs nothing.

theorem RathiHahnFutrell2026.VoiceAspectTense.pastCondEntropy_agg_lt_fuseLow_one_iff (d : ↑unitInterval) : InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) 1 < InformationTheory.pastCondEntropy (char (tagged fuseLow)) (stream 3 (meanings d)) 1 ↔ ↑d ≠ 2⁻¹

With one character of context, fusing the independent voice and aspect raises the surprisal exactly when aspect and tense are dependent: the second character no longer reveals aspect.

theorem RathiHahnFutrell2026.VoiceAspectTense.pastCondEntropy_eq_agg (d : ↑unitInterval) {t : ℕ} (ht : 2 ≤ t) : InformationTheory.pastCondEntropy (char (tagged fuseLow)) (stream 3 (meanings d)) t = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) t ∧ InformationTheory.pastCondEntropy (char (tagged fuseHigh)) (stream 3 (meanings d)) t = InformationTheory.pastCondEntropy (char (tagged agg)) (stream 3 (meanings d)) t

Once the context spans a word, the three languages are equally surprising.