Sequential RSA: prefix-meaning composition

@cite{cohn-gordon-goodman-potts-2019} @cite{degen-etal-2020} @cite{waldon-degen-2021} @cite{schlotterbeck-wang-2023}

The Product-of-Experts (PoE) prefix meaning underlying noisy / incremental RSA models: a per-word lex function lex : U → W → R is composed multiplicatively over a list of tokens. Higher layers (Noisy.lean, Incremental.lean) bundle this with RSAConfig builders.

The substrate exists because two distinct study files (@cite{waldon-degen-2021}, @cite{schlotterbeck-wang-2023}) independently restipulated lexContinuousQ, prefixMeaningQ, and the order-independence swap lemmas. With this file, both reduce to corollaries of List.Perm.prod_eq from mathlib.

Generality

prefixMeaning is polymorphic over any [CommMonoid R]. The default arithmetic instance is ℚ for computable studies (S&W, W&D), but the same operator applies over ℝ (proof studies) or PMF-valued semantics (future mathlib-PMF migration, see MEMORY.md). Order-related lemmas (prefixMeaning_nonneg, _pos) require the additional structure that ℚ and ℝ both provide.

def RSA.prefixMeaning {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (pfx : List U) (w : W) : R

Prefix-meaning: the per-word lex composed multiplicatively over a list. Generic over any commutative monoid R.

Equations

• RSA.prefixMeaning lex pfx w = (List.map (fun (x : U) => lex x w) pfx).prod

@[simp]

theorem RSA.prefixMeaning_nil {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (w : W) : prefixMeaning lex [] w = 1

@[simp]

theorem RSA.prefixMeaning_cons {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (u : U) (pfx : List U) (w : W) : prefixMeaning lex (u :: pfx) w = lex u w * prefixMeaning lex pfx w

theorem RSA.prefixMeaning_append {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (pfx₁ pfx₂ : List U) (w : W) : prefixMeaning lex (pfx₁ ++ pfx₂) w = prefixMeaning lex pfx₁ w * prefixMeaning lex pfx₂ w

theorem RSA.prefixMeaning_singleton {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (u : U) (w : W) : prefixMeaning lex [u] w = lex u w

theorem RSA.prefixMeaning_perm {U W : Type} {R : Type u_1} [CommMonoid R] {lex : U → W → R} {pfx pfx' : List U} (h : pfx.Perm pfx') (w : W) : prefixMeaning lex pfx w = prefixMeaning lex pfx' w

Order-independence of prefix-meaning. Any permutation of the prefix yields the same product — the headline structural fact behind the noisy sequential RSA "swap" theorems.

theorem RSA.prefixMeaning_swap {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (a b : U) (w : W) : prefixMeaning lex [a, b] w = prefixMeaning lex [b, a] w

Two-element swap — canonical instance of prefixMeaning_perm.

theorem RSA.prefixMeaning_swap_head {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (a b : U) (rest : List U) (w : W) : prefixMeaning lex (a :: b :: rest) w = prefixMeaning lex (b :: a :: rest) w

Swap the first two elements of a prefix (any tail). Generalized head-swap for n-element prefixes.

theorem RSA.foldl_mul_lex_eq_acc_mul_prefixMeaning {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (w : W) (acc : R) (pfx : List U) : List.foldl (fun (a : R) (u : U) => a * lex u w) acc pfx = acc * prefixMeaning lex pfx w

Foldl-prod bridge. prefixMeaning agrees with the imperative foldl (· * lex ·) form, generalized over any starting accumulator. Polymorphic version of the W&D study-file helper.

theorem RSA.prefixMeaning_eq_foldl_mul {U W : Type} {R : Type u_1} [CommMonoid R] (lex : U → W → R) (pfx : List U) (w : W) : prefixMeaning lex pfx w = List.foldl (fun (a : R) (u : U) => a * lex u w) 1 pfx

The PoE prefix product, expressed as a foldl from the unit accumulator. The form W&D and S&W's original code used.

theorem RSA.prefixMeaning_nonneg {U W : Type} {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {lex : U → W → R} (h : ∀ (u : U) (w : W), 0 ≤ lex u w) (pfx : List U) (w : W) : 0 ≤ prefixMeaning lex pfx w

theorem RSA.prefixMeaning_pos {U W : Type} {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [NeZero 1] {lex : U → W → R} (h : ∀ (u : U) (w : W), 0 < lex u w) (pfx : List U) (w : W) : 0 < prefixMeaning lex pfx w