getRsaSimpNames
plain-language theorem explainer
Reads the current Lean environment and returns every declaration name registered under the RSA simplification whitelist attribute. Tactic authors and the RL training loop cite it when they need the exact set of rewrites `rsa_simp` is allowed to use. The body is a one-line environment lookup of the attribute extension state.
Claim. In the Lean metaprogramming monad, return the list of declaration names currently stored in the RSA simplification-whitelist attribute extension of the active environment.
background
The Recognition Stability Audit (RSA) RL module turns the audit pipeline into a closed training loop inside Lean. Two custom attributes partition the allowed moves: one marks rewrite and unfold lemmas that simplification may use; the other marks milestone lemmas that a single bounded step may apply.
The simplification tactic is deliberately not open-ended simp. It runs only against the whitelist (plus Lean's built-in simp only constants), so an external agent proposing steps cannot smuggle arbitrary lemmas into a proof. This definition is the metaprogram that materializes that whitelist as a concrete list of names from the live environment.
The sibling milestone-name reader follows the same pattern against a different attribute extension. Together they feed the bounded step tactic and the reward signal used when an LLM proposes the next audit move.
proof idea
One-line metaprogram: obtain the current environment, read the RSA simp-lemma attribute extension state, and convert that state to a List Name. No search, filtering, or proof work occurs.
why it matters
Without a live dump of the whitelist, the restricted simplification tactic and the RL loop cannot know which rewrites are legal. The sibling milestone-name reader reuses the same environment-extension pattern, and both sit under the RSA RL module whose purpose is to make audit steps machine-checkable and rewardable.
This is infrastructure, not a physics claim. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or mass-ladder numerics. Its value is verification hygiene: every simplification step in a gold RSA goal stays inside a named, auditable set of lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.