getRsaMilestoneNames
plain-language theorem explainer
Reads the current Lean environment and returns every declaration name registered under the RSA milestone attribute. The bounded audit tactic uses this list when it tries one milestone application per step. Implementation is a one-line environment-extension lookup, not a mathematical proof.
Claim. In the Lean metaprogramming monad, return the list of all declaration names currently stored in the Recognition Stability Audit milestone attribute extension state of the environment.
background
The Recognition Stability Audit (RSA) RL module turns the audit pipeline into a closed Lean loop an external agent can drive. Two custom tags structure the action space: @[rsa_simp] whitelists rewrite and unfold lemmas for a restricted simplifier, and @[rsa_milestone] marks the high-level lemmas the one-step tactic may apply.
Milestone lemmas are the intentional, named bridges in the audit (boundary hits, Schur conditions, sensor blow-ups, and similar wrappers). Keeping them behind an attribute extension prevents the step tactic from unfolding those wrappers away before they can fire.
This helper is the read side of that registry: given the live environment, it materializes the milestone name list the step tactic will iterate.
proof idea
Pure metaprogram definition. Fetch the environment with getEnv, read the RSA milestone extension state, and convert that collection to a List Name. No tactics, no lemmas, no arithmetic.
why it matters
Without a deterministic milestone roster, the RL step cannot prefer high-level audit lemmas over blind simplification. The module doc states the intended loop: an LLM proposes rsa_step / rsa_simp / apply, and Lean rewards goal closure on a small library of proved gold theorems.
This definition is the name source that step consults before falling back to whitelist simplification. It does not encode physics content from the forcing chain (T5–T8, RCL, phi, eight-tick); it only stabilizes the verification interface those results are audited through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.