[Ken15] on mathlib PMF (Shape A migration)

[Ken15] [FG12]

PMF-shaped re-formalisation of Kennedy2015.lean's 7 RSA L1 findings. Domain: KCard = Fin 6, KUtt = 5 numeral alternatives. Same-observation findings discharge via the canonical template + vacuous-zero/partition- dominance patterns.

Migration coverage

5 of 7 findings discharged structurally:

• 3 vacuous-zero: classA_no_competition_at_boundary, bare_peaked_with_kennedy_alternatives, upper_classA_no_competition (utterance inapplicable at one of the worlds)
• 2 partition-dominance pending: classB_strengthened_above_bare, upper_classB_strengthened_below_bare (numerators equal, partitions don't pointwise dominate — non-uniform-applicability case)
• 2 cross-observation pending: classB_competition_at_boundary, upper_classB_competition (different utterances, same world; needs posterior_apply_cross_obs_lt-style lemma — new API gap)

Reused from Kennedy2015.lean

• KCard, KUtt — domain types
• kMean — the meaning matrix, consumed directly by RSA.extensionOf

instance Kennedy2015.PMF.instNonemptyKCard : Nonempty KCard

instance Kennedy2015.PMF.instNonemptyKUtt : Nonempty KUtt

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

@[reducible, inline]

noncomputable abbrev Kennedy2015.PMF.extension (u : KUtt) : Finset KCard

Equations

• Kennedy2015.PMF.extension u = RSA.extensionOf Kennedy2015.kMean u

theorem Kennedy2015.PMF.extension_nonempty (u : KUtt) : (extension u).Nonempty

noncomputable def Kennedy2015.PMF.L0 (u : KUtt) : PMF KCard

Equations

• Kennedy2015.PMF.L0 u = RSA.L0OfPred Kennedy2015.kMean u ⋯

@[simp]

theorem Kennedy2015.PMF.mem_support_L0_iff (u : KUtt) (w : KCard) : w ∈ (L0 u).support ↔ kMean u w

theorem Kennedy2015.PMF.L0_apply_of_true {u : KUtt} {w : KCard} (h : kMean u w) : (L0 u) w = (↑(extension u).card)⁻¹

theorem Kennedy2015.PMF.L0_apply_of_false {u : KUtt} {w : KCard} (h : ¬kMean u w) : (L0 u) w = 0

§2. S1 — speaker as PMF.normalize of L0 with conditional fallback

At every world in 0..5, at least one utterance applies (e.g. .atMost3 applies at 0..3, .atLeast3 applies at 3..5). So S1 is well-defined everywhere — no fallback needed in this domain (all worlds have a witness).

Still using the conditional pattern for compatibility with the Shape A template.

theorem Kennedy2015.PMF.L0_tsum_utterance_ne_top (w : KCard) : ∑' (u : KUtt), (L0 u) w ≠ ⊤

noncomputable def Kennedy2015.PMF.S1 (w : KCard) : PMF KUtt

Equations

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

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

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

noncomputable def Kennedy2015.PMF.worldPrior : PMF KCard

Equations

• Kennedy2015.PMF.worldPrior = PMF.uniformOfFintype Kennedy2015.KCard

theorem Kennedy2015.PMF.worldPrior_ne_zero (w : KCard) : worldPrior w ≠ 0

theorem Kennedy2015.PMF.L1_marginal_ne_zero (u : KUtt) : PMF.marginal S1 worldPrior u ≠ 0

noncomputable def Kennedy2015.PMF.L1 (u : KUtt) : PMF KCard

Equations

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

§4. Findings — vacuous-zero discharges

theorem Kennedy2015.PMF.S1_3_lt_S1_4_for_moreThan3 : (S1 3) KUtt.moreThan3 < (S1 4) KUtt.moreThan3

"moreThan3" doesn't apply at .3 → S1 .3 .moreThan3 = 0 (vacuous-zero).

theorem Kennedy2015.PMF.classA_no_competition_at_boundary : (L1 KUtt.moreThan3) 4 > (L1 KUtt.moreThan3) 3

L1("moreThan3") prefers .4 over .3 — Class A excludes the boundary semantically.

theorem Kennedy2015.PMF.S1_4_lt_S1_3_for_bare3 : (S1 4) KUtt.bare3 < (S1 3) KUtt.bare3

"bare3" doesn't apply at .4 → S1 .4 .bare3 = 0 (vacuous-zero).

theorem Kennedy2015.PMF.bare_peaked_with_kennedy_alternatives : (L1 KUtt.bare3) 3 > (L1 KUtt.bare3) 4

L1("bare 3") peaked at .3 — bare numeral exact reading.

theorem Kennedy2015.PMF.S1_3_lt_S1_2_for_fewerThan3 : (S1 3) KUtt.fewerThan3 < (S1 2) KUtt.fewerThan3

"fewerThan3" doesn't apply at .3 → S1 .3 .fewerThan3 = 0 (vacuous-zero, mirror of moreThan3).

theorem Kennedy2015.PMF.upper_classA_no_competition : (L1 KUtt.fewerThan3) 2 > (L1 KUtt.fewerThan3) 3

L1("fewerThan3") prefers .2 over .3 — upper Class A excludes boundary.

§5. Findings — partition-dominance leaves

The S1 partition Z(w) = ∑_u L0(u)(w) differs across worlds; with equal numerators, L1 favours the world with the smaller partition. We evaluate the partitions FG12-style and cancel the shared alternatives — no reflection.

theorem Kennedy2015.PMF.classB_strengthened_above_bare : (L1 KUtt.atLeast3) 4 > (L1 KUtt.atLeast3) 3

Class B: L1 of "atLeast3" prefers .4 over .3. Equal numerators (1/3); world 3 has the larger partition (more competing alternatives), so L1 shifts toward .4.

theorem Kennedy2015.PMF.upper_classB_strengthened_below_bare : (L1 KUtt.atMost3) 2 > (L1 KUtt.atMost3) 3

Upper Class B: L1 of "atMost3" prefers .2 over .3 (mirror of classB_strengthened_above_bare).

§6. Findings — cross-observation (different utterance, same world)

theorem Kennedy2015.PMF.classB_competition_at_boundary : (L1 KUtt.bare3) 3 > (L1 KUtt.atLeast3) 3

Class B competition at the boundary: L1("bare 3" | .3) > L1("at least 3" | .3).

Structural discharge (post-0.230.409 lemma posterior_lt_of_score_cross_lt):

1. gt_iff_lt flips to < shape
2. unfold L1, posterior_lt_of_score_cross_lt
3. Reduces to cross-multiplied score comparison: S1 .3 .atLeast3 * marginal .bare3 < S1 .3 .bare3 * marginal .atLeast3

Remaining leaf: the cross-multiplied numeric inequality requires computing marginal .bare3 and marginal .atLeast3 (each a tsum over Fin 6). Same partition-computation friction as classB_strengthened_above_bare — would close once a pmf_partition_compute helper exists.

theorem Kennedy2015.PMF.upper_classB_competition : (L1 KUtt.bare3) 3 > (L1 KUtt.atMost3) 3

Upper Class B competition. Same shape as classB_competition_at_boundary.