RSAPredict — Verified RSA Predictions via Reflection

The rsa_predict tactic proves ℝ comparison goals on RSA models by:

1. Trying native_decide (handles ℚ, Bool, finite types directly)
2. Reifying both sides to RExpr (rational expression trees)
3. Evaluating via exact ℚ arithmetic or tree-based intervals
4. Building kernel-verifiable proofs from the interval separation

All ~400 invocations across 38 study files use this reflection path exclusively.

Supported Goal Forms

• cfg.L0 l u w₁ > cfg.L0 l u w₂ — L0 world comparison
• cfg.L0_marginal l u P₁ > cfg.L0_marginal l u P₂ — L0 marginal comparison
• cfg.L1 u w₁ > cfg.L1 u w₂ — L1 world comparison
• ¬(cfg.L1 u w₁ > cfg.L1 u w₂) — L1 non-strict (implicature canceled)
• cfg.L1_latent u l₁ > cfg.L1_latent u l₂ — latent variable inference
• cfg.S1 l w u₁ > cfg.S1 l w u₂ — S1 speaker comparison
• ¬(cfg.S1 l w u₁ > cfg.S1 l w u₂) — S1 non-strict
• cfg.S2 w₁ u > cfg.S2 w₂ u — S2 cross-world endorsement
• cfg.S1 l w u₁ = cfg.S1 l w u₂ — S1 equality (score symmetry)
• cfg.L1 u w₁ = cfg.L1 u w₂ — L1 equality (score symmetry)
• Σ s, cfg.L1 u (s, a₁) > Σ s, cfg.L1 u (s, a₂) — marginal comparison
• cfg.L1_marginal u P₁ > cfg.L1_marginal u P₂ — marginal via predicate
• cfg.L1 u₁ w₁ +... > cfg.L1 u₂ w₃ +... — cross-utterance sum
• cfg₁.L1 u₁ w₁ +... > cfg₂.L1 u₂ w₃ +... — cross-config sum

Usage

theorem prediction : cfg.L1 u w₁ > cfg.L1 u w₂ := by rsa_predict

def Linglib.Tactics.tacticRsa_predict : Lean.ParserDescr

rsa_predict proves RSA prediction goals by RExpr reflection.

The tactic reifies both sides of a comparison to RExpr (rational expression trees), then proves the comparison via exact ℚ evaluation or tree-based interval arithmetic. The kernel verifies that RExpr.denote matches the original ℝ expression via iota-reduction.

Equations

• Linglib.Tactics.tacticRsa_predict = Lean.ParserDescr.node `Linglib.Tactics.tacticRsa_predict 1024 (Lean.ParserDescr.nonReservedSymbol "rsa_predict" false)