@cite{bylinina-nouwen-2020} on mathlib PMF (Shape A migration pilot)

@cite{bylinina-nouwen-2020}

PMF-shaped re-formalisation of BylininaNouwen2020.lean's 3 findings:

• lb_rsa_strengthens_two: L1("two") prefers c2 over c3
• lb_rsa_strengthens_one: L1("one") prefers c1 over c2
• lb_three_peaked: L1("three") prefers c3 over c2

All three are Shape A (uniform world prior, Latent := Unit, no cost factor, α = 1 → S1 is just normalize of L0).

Friction surface: degenerate world .c0

At .c0, NO utterance applies (one requires ≥1, etc.). So the speaker score at .c0 is identically zero — PMF.normalize is undefined.

We use the conditional fallback pattern (same as Nouwen2024PMF's adjSpeaker_warmAt): at degenerate worlds, S1 falls back to a vacuous PMF.pure .one. Doesn't affect the L1 findings (which compare non-degenerate worlds), but the bundled API silently uses a similar guard via if l0 = 0 then 0 in s1Score.

Reused from BylininaNouwen2020.lean

• NCard, NUtt, lbNuttMeaning — domain + Boolean meaning matrix

§1. L0 — uniform on extension via RSA.L0OfBoolMeaning

@[reducible, inline]

abbrev BylininaNouwen2020.PMF.extension (u : NUtt) : Finset NCard

Equations

• BylininaNouwen2020.PMF.extension u = RSA.extensionOf BylininaNouwen2020.lbNuttMeaning u

theorem BylininaNouwen2020.PMF.extension_nonempty (u : NUtt) : (extension u).Nonempty

noncomputable def BylininaNouwen2020.PMF.L0 (u : NUtt) : PMF NCard

Equations

• BylininaNouwen2020.PMF.L0 u = RSA.L0OfBoolMeaning BylininaNouwen2020.lbNuttMeaning u ⋯

@[simp]

theorem BylininaNouwen2020.PMF.mem_support_L0_iff (u : NUtt) (w : NCard) : w ∈ (L0 u).support ↔ lbNuttMeaning u w = true

theorem BylininaNouwen2020.PMF.L0_apply_of_true {u : NUtt} {w : NCard} (h : lbNuttMeaning u w = true) : (L0 u) w = (↑(extension u).card)⁻¹

theorem BylininaNouwen2020.PMF.L0_apply_of_false {u : NUtt} {w : NCard} (h : lbNuttMeaning u w ≠ true) : (L0 u) w = 0

§2. S1 — speaker as PMF.normalize of L0, with fallback at .c0

theorem BylininaNouwen2020.PMF.L0_tsum_utterance_ne_top (w : NCard) : ∑' (u : NUtt), (L0 u) w ≠ ⊤

noncomputable def BylininaNouwen2020.PMF.S1 (w : NCard) : PMF NUtt

Pragmatic speaker: PMF.normalize (L0 · w) at non-degenerate worlds, PMF.pure .one at .c0 (where no utterance applies).

Equations

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

theorem BylininaNouwen2020.PMF.S1_eq_normalize {w : NCard} (h : ∑' (u : NUtt), (L0 u) w ≠ 0) : S1 w = PMF.normalize (fun (u : NUtt) => (L0 u) w) h ⋯

At reachable (w ≠ .c0) worlds, S1 unfolds to PMF.normalize.

§3. L1 — Bayesian inversion against the uniform world prior

instance BylininaNouwen2020.PMF.instNonemptyNCard : Nonempty NCard

instance BylininaNouwen2020.PMF.instNonemptyNUtt : Nonempty NUtt

noncomputable def BylininaNouwen2020.PMF.worldPrior : PMF NCard

Equations

• BylininaNouwen2020.PMF.worldPrior = PMF.uniformOfFintype BylininaNouwen2020.NCard

theorem BylininaNouwen2020.PMF.worldPrior_ne_zero (w : NCard) : worldPrior w ≠ 0

theorem BylininaNouwen2020.PMF.L1_marginal_ne_zero (u : NUtt) : PMF.marginal S1 worldPrior u ≠ 0

Each utterance has an applicable world, so the L1 marginal is positive.

noncomputable def BylininaNouwen2020.PMF.L1 (u : NUtt) : PMF NCard

Equations

• BylininaNouwen2020.PMF.L1 u = PMF.posterior BylininaNouwen2020.PMF.S1 BylininaNouwen2020.PMF.worldPrior u ⋯

§4. Findings (per-world S1 leaves sorry'd; structural shell complete)

theorem BylininaNouwen2020.PMF.S1_c3_lt_S1_c2_for_two : (S1 NCard.c3) NUtt.two < (S1 NCard.c2) NUtt.two

Per-world S1 leaf for lb_rsa_strengthens_two: at .c3 the speaker has 3 applicable utterances (one, two, three), reducing the share for "two"; at .c2 only "one" and "two" apply. So S1 .c3 .two < S1 .c2 .two.

Discharge via partition-strict-monotonicity (same pattern as S1_c2_lt_S1_c1_for_one):

• Numerator equality: L0 .two .c3 = L0 .two .c2
• Partition strict: tsum g .c2 < tsum f .c3 via strict witness at .three (L0 .three .c2 = 0 < 1 = L0 .three .c3).

theorem BylininaNouwen2020.PMF.lb_rsa_strengthens_two : (L1 NUtt.two) NCard.c2 > (L1 NUtt.two) NCard.c3

Headline: L1("two") prefers .c2 over .c3.

theorem BylininaNouwen2020.PMF.S1_c2_lt_S1_c1_for_one : (S1 NCard.c2) NUtt.one < (S1 NCard.c1) NUtt.one

Per-world S1 leaf for lb_rsa_strengthens_one.

Discharge via partition-strict-monotonicity (the structural shape):

• Numerator equality: L0 .one .c1 = L0 .one .c2 (both = ((extension .one).card)⁻¹)
• Numerator positive: L0 .one .c1 ≠ 0
• Partition strict: Σ' u, L0 u .c1 < Σ' u, L0 u .c2 via pointwise tsum_lt_tsum with strict witness at u = .two (L0 .two .c1 = 0 < 1/2 = L0 .two .c2).

theorem BylininaNouwen2020.PMF.lb_rsa_strengthens_one : (L1 NUtt.one) NCard.c1 > (L1 NUtt.one) NCard.c2

Headline: L1("one") prefers .c1 over .c2.

theorem BylininaNouwen2020.PMF.S1_c2_lt_S1_c3_for_three : (S1 NCard.c2) NUtt.three < (S1 NCard.c3) NUtt.three

Per-world S1 leaf for lb_three_peaked: .three doesn't apply at .c2 (since 2 < 3), so S1 .c2 .three = 0. At .c3, S1 .c3 .three > 0.

Discharged via PMF.normalize_lt_of_apply_zero_pos (vacuous-zero pattern). The conditional fallback unfolds via S1_eq_normalize since both .c2 and .c3 are non-degenerate (other utterances do apply).

theorem BylininaNouwen2020.PMF.lb_three_peaked : (L1 NUtt.three) NCard.c3 > (L1 NUtt.three) NCard.c2

Headline: L1("three") trivially peaks at .c3.