Pierrehumbert (2001): Exemplar dynamics: Word frequency, lenition and contrast

This file formalizes Pierrehumbert's exemplar model of production. A category is a list of remembered tokens, each weighted by its age. To produce the category a speaker picks a target, either an exemplar drawn with probability proportional to its weight or, under entrenchment, the memory-weighted mean, and adds production noise and a constant lenition bias. Every produced token is stored, so the list is drawn from a prediction rule (rule) and its law is ProbabilityTheory.seqLaw.

The paper presents its results as simulations. Here they are exact statements about the expected memory-weighted mean and spread. Each production moves the expected mean by the bias divided by the total memory weight (integral_memoryMean), so a leniting change is further advanced the more a word is used, and slows as memory accumulates. Without entrenchment the expected spread grows at every production, and lenition adds to it; with entrenchment it stays below the variance that noise and bias add at a production, and below the spread without entrenchment.

Main statements

• lenition_advances_with_use: under a leniting bias the expected mean falls with every use.
• spread_grows, lenition_blurs: without entrenchment the expected spread grows with every use, and lenition widens it.
• entrenchment_narrows: entrenchment keeps the expected spread below the bare model's.

Implementation notes

• Every production is stored, the idealization of §3.1. The single-label loop of the appendix stores a token only if its score (1) is nonzero, a filter the theorems leave out.
• Entrenchment is its large-neighborhood limit, the memory-weighted mean (appendix); the rule of Fig. 4, the mean of the 500 nearest exemplars, is not formalized.
• The decay factor γ is exp (-1/τ) for the paper's memory time τ, and γ = 1 is no decay. The noise is any centered square-integrable law; the paper's is uniform on [-0.1, 0.1].
• Section, figure and equation numbers are those of the author's manuscript of June 2000.

TODO

• The score function (1), the two-label loop of the appendix, and the neutralization of §4 (Fig. 5), in which a leniting marked category is absorbed by a stable unmarked one.

References

• [Pie01]

The memory

noncomputable def Pierrehumbert2001.totalWeight (γ : NNReal) (n : ℕ) : ℝ

The total weight of n exemplars, the ith of which has age n - 1 - i.

Equations

• Pierrehumbert2001.totalWeight γ n = ∑ i : Fin n, ↑γ ^ ↑i.rev

noncomputable def Pierrehumbert2001.memoryMean (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : ℝ

The memory-weighted mean of an exemplar list.

Equations

• Pierrehumbert2001.memoryMean γ e = (∑ i : Fin n, ↑γ ^ ↑i.rev * e i) / Pierrehumbert2001.totalWeight γ n

noncomputable def Pierrehumbert2001.memorySpread (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : ℝ

The memory-weighted spread of an exemplar list about its mean.

Equations

• Pierrehumbert2001.memorySpread γ e = (∑ i : Fin n, ↑γ ^ ↑i.rev * (e i - Pierrehumbert2001.memoryMean γ e) ^ 2) / Pierrehumbert2001.totalWeight γ n

theorem Pierrehumbert2001.totalWeight_succ (γ : NNReal) {n : ℕ} : totalWeight γ (n + 1) = ↑γ * totalWeight γ n + 1

theorem Pierrehumbert2001.totalWeight_succ' (γ : NNReal) {n : ℕ} : totalWeight γ (n + 1) = totalWeight γ n + ↑γ ^ n

theorem Pierrehumbert2001.totalWeight_nonneg (γ : NNReal) {n : ℕ} : 0 ≤ totalWeight γ n

theorem Pierrehumbert2001.one_le_totalWeight (γ : NNReal) {n : ℕ} (hn : n ≠ 0) : 1 ≤ totalWeight γ n

theorem Pierrehumbert2001.totalWeight_pos (γ : NNReal) {n : ℕ} (hn : n ≠ 0) : 0 < totalWeight γ n

theorem Pierrehumbert2001.totalWeight_mono (γ : NNReal) : Monotone (totalWeight γ)

theorem Pierrehumbert2001.totalWeight_mul_one_sub_le (γ : NNReal) {n : ℕ} (hγ : γ ≤ 1) : totalWeight γ n * (1 - ↑γ) ≤ 1

theorem Pierrehumbert2001.totalWeight_mul_one_sub_lt (γ : NNReal) {n : ℕ} (hγ0 : 0 < γ) (hγ : γ ≤ 1) : totalWeight γ n * (1 - ↑γ) < 1

theorem Pierrehumbert2001.totalWeight_mul_memoryMean (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : totalWeight γ n * memoryMean γ e = ∑ i : Fin n, ↑γ ^ ↑i.rev * e i

theorem Pierrehumbert2001.totalWeight_mul_memorySpread (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : totalWeight γ n * memorySpread γ e = ∑ i : Fin n, ↑γ ^ ↑i.rev * (e i - memoryMean γ e) ^ 2

theorem Pierrehumbert2001.sum_mul_sub_sq (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) (c : ℝ) : ∑ i : Fin n, ↑γ ^ ↑i.rev * (e i - c) ^ 2 = totalWeight γ n * memorySpread γ e + totalWeight γ n * (memoryMean γ e - c) ^ 2

theorem Pierrehumbert2001.memoryMean_snoc (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) (x : ℝ) : memoryMean γ (Fin.snoc e x) = (↑γ * totalWeight γ n * memoryMean γ e + x) / totalWeight γ (n + 1)

theorem Pierrehumbert2001.memorySpread_snoc (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) (x : ℝ) : memorySpread γ (Fin.snoc e x) = ↑γ * totalWeight γ n / totalWeight γ (n + 1) * memorySpread γ e + ↑γ * totalWeight γ n / totalWeight γ (n + 1) ^ 2 * (x - memoryMean γ e) ^ 2

theorem Pierrehumbert2001.measurable_memoryMean (γ : NNReal) {n : ℕ} : Measurable (memoryMean γ)

Production

noncomputable def Pierrehumbert2001.recency (γ : NNReal) (n : ℕ) : MeasureTheory.Measure (Fin n)

The recency distribution of the appendix, picking a position with probability proportional to its weight.

Equations

• Pierrehumbert2001.recency γ n = ∑ i : Fin n, (↑γ ^ ↑i.rev / Pierrehumbert2001.totalWeight γ n).toNNReal • MeasureTheory.Measure.dirac i

theorem Pierrehumbert2001.integral_recency (γ : NNReal) {n : ℕ} (f : Fin n → ℝ) : ∫ (i : Fin n), f i ∂recency γ n = ∑ i : Fin n, ↑γ ^ ↑i.rev / totalWeight γ n * f i

instance Pierrehumbert2001.instIsProbabilityMeasureFinHAddNatOfNatRecency (γ : NNReal) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (recency γ (n + 1))

inductive Pierrehumbert2001.Target : Type

The production target of the appendix, an exemplar picked by recency or the memory-weighted mean, to which entrenchment fixes the target in the limit of a large neighborhood.

• exemplar : Target
• average : Target

noncomputable def Pierrehumbert2001.target (γ : NNReal) {n : ℕ} : Target → ProbabilityTheory.Kernel (Fin n → ℝ) ℝ

The law of the production target given the exemplar list.

Equations

• One or more equations did not get rendered due to their size.
• Pierrehumbert2001.target γ Pierrehumbert2001.Target.average = ProbabilityTheory.Kernel.deterministic (Pierrehumbert2001.memoryMean γ) ⋯

theorem Pierrehumbert2001.target_exemplar_apply (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : (target γ Target.exemplar) e = MeasureTheory.Measure.map e (recency γ n)

theorem Pierrehumbert2001.target_average_apply (γ : NNReal) {n : ℕ} (e : Fin n → ℝ) : (target γ Target.average) e = MeasureTheory.Measure.dirac (memoryMean γ e)

instance Pierrehumbert2001.instIsMarkovKernelForallFinHAddNatOfNatRealTarget (γ : NNReal) {n : ℕ} (tgt : Target) : ProbabilityTheory.IsMarkovKernel (target γ tgt)

noncomputable def Pierrehumbert2001.produce (γ : NNReal) {n : ℕ} (tgt : Target) (ν : MeasureTheory.Measure ℝ) (bias : ℝ) : ProbabilityTheory.Kernel (Fin n → ℝ) ℝ

Production as in (2), the target plus noise drawn from ν plus the lenition bias.

Equations

• Pierrehumbert2001.produce γ tgt ν bias = ((Pierrehumbert2001.target γ tgt).prod (ProbabilityTheory.Kernel.const (Fin n → ℝ) ν)).map fun (p : ℝ × ℝ) => p.1 + p.2 + bias

instance Pierrehumbert2001.instIsMarkovKernelForallFinHAddNatOfNatRealProduce (γ : NNReal) {n : ℕ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (tgt : Target) (bias : ℝ) : ProbabilityTheory.IsMarkovKernel (produce γ tgt ν bias)

theorem Pierrehumbert2001.produce_apply (γ : NNReal) {n : ℕ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (tgt : Target) (bias : ℝ) (e : Fin (n + 1) → ℝ) : (produce γ tgt ν bias) e = MeasureTheory.Measure.map (fun (x : ℝ) => x + bias) (((target γ tgt) e).conv ν)

theorem Pierrehumbert2001.memLp_target (γ : NNReal) {n : ℕ} (tgt : Target) (e : Fin (n + 1) → ℝ) : MeasureTheory.MemLp id 2 ((target γ tgt) e)

theorem Pierrehumbert2001.integral_target (γ : NNReal) {n : ℕ} (tgt : Target) (e : Fin (n + 1) → ℝ) : ∫ (t : ℝ), t ∂(target γ tgt) e = memoryMean γ e

theorem Pierrehumbert2001.variance_target (γ : NNReal) {n : ℕ} (tgt : Target) (e : Fin (n + 1) → ℝ) : ProbabilityTheory.variance id ((target γ tgt) e) = match tgt with | Target.exemplar => memorySpread γ e | Target.average => 0

theorem Pierrehumbert2001.memLp_produce (γ : NNReal) {n : ℕ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (tgt : Target) (bias : ℝ) (hν : MeasureTheory.MemLp id 2 ν) (e : Fin (n + 1) → ℝ) : MeasureTheory.MemLp id 2 ((produce γ tgt ν bias) e)

theorem Pierrehumbert2001.integral_produce (γ : NNReal) {n : ℕ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (tgt : Target) (bias : ℝ) (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (e : Fin (n + 1) → ℝ) : ∫ (x : ℝ), x ∂(produce γ tgt ν bias) e = memoryMean γ e + bias

theorem Pierrehumbert2001.integral_produce_sub_sq (γ : NNReal) {n : ℕ} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (tgt : Target) (bias : ℝ) (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (e : Fin (n + 1) → ℝ) : ∫ (x : ℝ), (x - memoryMean γ e) ^ 2 ∂(produce γ tgt ν bias) e = (match tgt with | Target.exemplar => memorySpread γ e | Target.average => 0) + ProbabilityTheory.variance id ν + bias ^ 2

The exemplar list

noncomputable def Pierrehumbert2001.rule (γ : NNReal) (tgt : Target) (ν : MeasureTheory.Measure ℝ) (bias seed : ℝ) (n : ℕ) : ProbabilityTheory.Kernel (Fin n → ℝ) ℝ

The prediction rule of the exemplar list, which starts from the seed and stores every production.

Equations

• Pierrehumbert2001.rule γ tgt ν bias seed 0 = ProbabilityTheory.Kernel.const (Fin 0 → ℝ) (MeasureTheory.Measure.dirac seed)
• Pierrehumbert2001.rule γ tgt ν bias seed n.succ = Pierrehumbert2001.produce γ tgt ν bias

theorem Pierrehumbert2001.rule_succ {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} (n : ℕ) : rule γ tgt ν bias seed (n + 1) = produce γ tgt ν bias

theorem Pierrehumbert2001.seqLaw_rule_one {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} : ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) 1 = MeasureTheory.Measure.dirac fun (x : Fin 1) => seed

instance Pierrehumbert2001.instIsMarkovKernelForallFinRealRule {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : ProbabilityTheory.IsMarkovKernel (rule γ tgt ν bias seed n)

theorem Pierrehumbert2001.memLp_memoryMean {γ : NNReal} {n : ℕ} {μ : MeasureTheory.Measure (Fin n → ℝ)} (h : ∀ (i : Fin n), MeasureTheory.MemLp (fun (e : Fin n → ℝ) => e i) 2 μ) : MeasureTheory.MemLp (memoryMean γ) 2 μ

theorem Pierrehumbert2001.integrable_memorySpread {γ : NNReal} {n : ℕ} {μ : MeasureTheory.Measure (Fin n → ℝ)} (h : ∀ (i : Fin n), MeasureTheory.MemLp (fun (e : Fin n → ℝ) => e i) 2 μ) : MeasureTheory.Integrable (memorySpread γ) μ

theorem Pierrehumbert2001.memLp_apply {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) (i : Fin (n + 1)) : MeasureTheory.MemLp (fun (e : Fin (n + 1) → ℝ) => e i) 2 (ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1))

theorem Pierrehumbert2001.integral_memoryMean_snoc {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) {n : ℕ} (e : Fin (n + 1) → ℝ) : ∫ (x : ℝ), memoryMean γ (Fin.snoc e x) ∂(rule γ tgt ν bias seed (n + 1)) e = memoryMean γ e + bias / totalWeight γ (n + 2)

theorem Pierrehumbert2001.integral_memoryMean {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) : ∫ (e : Fin (n + 1) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1) = seed + bias * ∑ k ∈ Finset.range n, (totalWeight γ (k + 2))⁻¹

The expected memory-weighted mean after n productions: each production moves it by the bias divided by the total memory weight (§3.2).

theorem Pierrehumbert2001.integral_memorySpread_snoc {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} {bias seed : ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) {n : ℕ} (e : Fin (n + 1) → ℝ) : ∫ (x : ℝ), memorySpread γ (Fin.snoc e x) ∂(rule γ tgt ν bias seed (n + 1)) e = ↑γ * totalWeight γ (n + 1) / totalWeight γ (n + 2) * memorySpread γ e + ↑γ * totalWeight γ (n + 1) / totalWeight γ (n + 2) ^ 2 * ((match tgt with | Target.exemplar => memorySpread γ e | Target.average => 0) + ProbabilityTheory.variance id ν + bias ^ 2)

Growth of the spread

noncomputable def Pierrehumbert2001.spreadGrowth (γ : NNReal) : Target → ℕ → ℝ

The expected spread after n productions in units of the variance that noise and bias add at a production. A production keeps the older exemplars' share of the spread and adds the new token's deviation from the mean, which a picked exemplar inherits from the memory and the mean target does not.

Equations

• One or more equations did not get rendered due to their size.
• Pierrehumbert2001.spreadGrowth γ x✝ 0 = 0

theorem Pierrehumbert2001.spreadGrowth_nonneg (γ : NNReal) (tgt : Target) (n : ℕ) : 0 ≤ spreadGrowth γ tgt n

theorem Pierrehumbert2001.spreadGrowth_pos (γ : NNReal) (hγ0 : 0 < γ) (tgt : Target) (n : ℕ) : 0 < spreadGrowth γ tgt (n + 1)

theorem Pierrehumbert2001.spreadGrowth_exemplar_succ (γ : NNReal) (n : ℕ) : spreadGrowth γ Target.exemplar (n + 1) = spreadGrowth γ Target.exemplar n + (↑γ * totalWeight γ (n + 1) - spreadGrowth γ Target.exemplar n) / totalWeight γ (n + 2) ^ 2

theorem Pierrehumbert2001.spreadGrowth_exemplar_le (γ : NNReal) (hγ : γ ≤ 1) (n : ℕ) : spreadGrowth γ Target.exemplar n ≤ totalWeight γ (n + 1) - 1

theorem Pierrehumbert2001.spreadGrowth_exemplar_strictMono (γ : NNReal) (hγ0 : 0 < γ) (hγ : γ ≤ 1) : StrictMono (spreadGrowth γ Target.exemplar)

theorem Pierrehumbert2001.spreadGrowth_average_le_one (γ : NNReal) (n : ℕ) : spreadGrowth γ Target.average n ≤ 1

theorem Pierrehumbert2001.spreadGrowth_average_le_exemplar (γ : NNReal) (n : ℕ) : spreadGrowth γ Target.average n ≤ spreadGrowth γ Target.exemplar n

Predictions

theorem Pierrehumbert2001.integral_memorySpread {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) : ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1) = (ProbabilityTheory.variance id ν + bias ^ 2) * spreadGrowth γ tgt n

The expected memory-weighted spread after n productions.

theorem Pierrehumbert2001.lenition_advances_with_use {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (hbias : bias < 0) : StrictAnti fun (n : ℕ) => ∫ (e : Fin (n + 1) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1)

Under a leniting bias the expected memory mean falls with every production, so a change in progress is further advanced in a word the more it is used (§3.2, Fig. 3).

theorem Pierrehumbert2001.integral_memoryMean_succ_sub {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) : ∫ (e : Fin (n + 2) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 2) - ∫ (e : Fin (n + 1) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1) = bias / totalWeight γ (n + 2)

theorem Pierrehumbert2001.lenition_slows_with_experience {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) : Antitone fun (n : ℕ) => |∫ (e : Fin (n + 2) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 2) - ∫ (e : Fin (n + 1) → ℝ), memoryMean γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 1)|

The more exemplars a speaker has stored, the less a production moves the expected mean (§3.2).

theorem Pierrehumbert2001.spread_grows {γ : NNReal} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (hγ0 : 0 < γ) (hγ : γ ≤ 1) (hc : 0 < ProbabilityTheory.variance id ν + bias ^ 2) : StrictMono fun (n : ℕ) => ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ Target.exemplar ν bias seed) (n + 1)

Without entrenchment the expected spread grows with every production, noise and bias alike widening the category (§3.1–3.2, Figs. 2 and 3).

theorem Pierrehumbert2001.lenition_blurs {γ : NNReal} {tgt : Target} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (hγ0 : 0 < γ) (hbias : bias ≠ 0) (n : ℕ) : ∫ (e : Fin (n + 2) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν 0 seed) (n + 2) < ∫ (e : Fin (n + 2) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ tgt ν bias seed) (n + 2)

Lenition widens the category as well as shifting it, "much as a photograph of a moving object shows a blur" (§3.2).

theorem Pierrehumbert2001.integral_memorySpread_le {γ : NNReal} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (hγ : γ ≤ 1) (n : ℕ) : ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ Target.exemplar ν bias seed) (n + 1) ≤ (ProbabilityTheory.variance id ν + bias ^ 2) * (totalWeight γ (n + 1) - 1)

Without entrenchment the expected spread stays below the noise and bias of all but one memory's worth of productions, totalWeight γ (n + 1) - 1, which tends to γ / (1 - γ).

theorem Pierrehumbert2001.entrenchment_narrows {γ : NNReal} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) : ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ Target.average ν bias seed) (n + 1) ≤ ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ Target.exemplar ν bias seed) (n + 1)

Entrenchment narrows the category, since averaging over the memory keeps the expected spread below the spread of the bare model (§3.3, Fig. 4).

theorem Pierrehumbert2001.integral_memorySpread_average_le {γ : NNReal} {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] {bias seed : ℝ} (hν : MeasureTheory.MemLp id 2 ν) (hν0 : ∫ (x : ℝ), x ∂ν = 0) (n : ℕ) : ∫ (e : Fin (n + 1) → ℝ), memorySpread γ e ∂ProbabilityTheory.seqLaw (rule γ Target.average ν bias seed) (n + 1) ≤ ProbabilityTheory.variance id ν + bias ^ 2

With entrenchment the expected spread never exceeds what noise and bias add at a single production, however long the change runs (§3.3).