Cache-Seeded RSA Reification

Fast-path reification for RSA score-level expressions. Instead of letting the generic reifyToRExpr discover leaf values by unfolding through 8+ RSA definition layers (~15,000 unfoldDefinition? calls at ~1ms each), this module pre-seeds the reification cache with L0 policy values for every (latent, utterance, world) triple.

When the generic reifier subsequently processes L1 scores, it only needs to unfold through the L1/S1 structure (~3-4 layers), hitting cache on every L0 policy sub-expression. The kernel verification is correct by construction because the generic reifier builds the RExpr tree by tracing the actual definition chain.

Falls back to the generic reifier with no pre-seeding if config detection fails.

partial def Linglib.Tactics.RSAPredict.findL1AgentCfg (e : Lean.Expr) (depth : ℕ := 20) : Lean.MetaM (Option Lean.Expr)

Scan an expression tree for RSA.RSAConfig.L1agent applied to a cfg argument. Returns the cfg Expr if found. Handles:

• Direct: RationalAction.score (L1agent cfg) u w
• Marginal: Finset.sum finset (fun w => score (L1agent cfg) u w)

partial def Linglib.Tactics.RSAPredict.findL1AgentCfg.findL1AgentCfgInBody (body : Lean.Expr) (depth : ℕ) : Lean.MetaM (Option Lean.Expr)

def Linglib.Tactics.RSAPredict.tryPreseedRSACache (cache : ReifyCache) (lhs rhs : Lean.Expr) : Lean.MetaM Bool

Try cache-seeded RSA reification for score-level expressions.

1. Detect RSAConfig from the expression
2. Pre-seed cache with L0 policies and S1 scores
3. Return none — the caller's generic reifyToRExpr will then run with a warm cache, hitting cache hits on inner expressions

This is not a replacement for reifyToRExpr — it's a cache warmer. Returns true if pre-seeding was done.

Equations

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