RSA Bottom-Up RExpr Builder

Constructs RExpr trees for RSA expressions bottom-up from evaluated leaf values, completely bypassing the generic reifier's top-down unfoldDefinition? chain.

The generic reifier discovers expression structure by unfolding definitions one at a time (~31K unfoldDefinition? calls for the first cross-utterance theorem). The builder knows the RSA layered structure and constructs RExpr trees directly:

1. Leaf evaluation: Evaluate meaning Bool values natively, reify priors/costs via the generic reifier (small expressions, ~0.1ms each).
2. Layer composition: Build L0 → S1 → L1 RExpr trees by direct construction.
3. Direct return: Return the full RExpr to the caller, bypassing reifyToRExpr.

The kernel verifies denote(rexpr) ≡ original_expr by reducing both sides. The builder's RExpr matches because:

• Left-fold sums match Finset.sum reduction (via 0 + x ≡ x for ℝ)
• iteZero matches if totalScore = 0 then 0 else score / totalScore
• expMulLogSub matches exp(α * (log x - c))
• Leaf values are reified by the generic reifier (denote matches by construction)

structure Tactics.RSAPredict.RSABuildResult : Type

Stored state for a built RSA model — all layer RExprs indexed by (l, u, w).

• nU : ℕ
• nW : ℕ
• nL : ℕ
• l1Scores : Array (Lean.Expr × MetaBounds)

  L1.score(u, w): index u * nW + w

• l1Totals : Array (Lean.Expr × MetaBounds)

  L1.totalScore(u): index u

opaque Tactics.RSAPredict.persistentBuildCache : IO.Ref (Std.HashMap UInt64 (Array Lean.Expr × Array Lean.Expr × RSABuildResult))

Module-scope cache for RSA build results. Keyed by config expression hash. Avoids rebuilding the full layer stack (L0→S1→L1) when the same RSAConfig is used across multiple theorems in the same file.

partial def 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.

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

def Tactics.RSAPredict.tryRSABuild (cache : ReifyCache) (activeLhs activeRhs : Lean.Expr) : Lean.Elab.Tactic.TacticM (Option (Lean.Expr × MetaBounds × Lean.Expr × MetaBounds))

Try to build RExpr trees for an RSA comparison, bypassing the generic reifier. Returns (lhsRExpr, lhsBounds, rhsRExpr, rhsBounds) on success.

Equations

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

partial def Tactics.RSAPredict.buildAndSeedL1 (cache : ReifyCache) (cfg : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Build L1 and L1_latent RExprs for an RSAConfig by:

1. Instantiating the s1Score lambda body directly (bypassing S1→S1agent→policy chain)
2. Reifying each instantiated body via the generic reifier
3. Assembling S1→L1 layers algebraically

This avoids the expensive whnf chain through cfg.S1 l w u → (S1agent l).policy w u → RationalAction.policy → iteZero → Finset.sum. Instead, we substitute concrete L0 policy function + args into the s1Score body and reify the resulting simple arithmetic expression (ite/exp/log/Finset.sum).

Seeds the reification cache with L1/L1_latent values so the generic reifier finds them immediately when processing S2Utility or similar composite expressions.

Recursively detects nested RSA configs in worldPrior/meaning (e.g., seqAdjCfg's worldPrior is (evalCfg mu).L1) and builds them first.

def Tactics.RSAPredict.tryPreseedL1 (cache : ReifyCache) (lhs rhs : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Pre-seed the reification cache with L1/L1_latent values for RSAConfig references found in the expression. Call before reifyToRExpr to avoid expensive whnf of nested L1 computations (e.g., in S2Utility).

Equations

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