IndisputableMonolith.Verification.RecognitionStabilityAudit.RL.Attr
Attribute registry for the Recognition Stability Audit reinforcement-learning layer in Lean. It declares the custom tags that whitelist simplification lemmas and mark milestone lemmas for automated RSA tactics. The parent RL module imports it so search stays inside a curated lemma set. Pure metaprogramming scaffolding: no theorems and no physics content.
claimRegisters two custom Lean attributes for the Recognition Stability Audit automation layer: one tagging whitelisted rewrite and unfold lemmas for the RSA simplifier, and one tagging milestone lemmas admissible to the RSA step tactic.
background
The Recognition Stability Audit (RSA) is a verification pipeline in IndisputableMonolith that checks stability properties of recognition-theoretic constructions. Its RL subpackage makes that pipeline reinforcement-learning friendly inside Lean by restricting which lemmas automated tactics may apply.
This Attr module is the attribute registry for that restriction. Downstream documentation states that one tag marks whitelisted rewrite/unfold lemmas used by the RSA simplifier, and the other marks milestone lemmas the RSA step tactic is allowed to apply. Authors place those tags on lemmas; the tactics discover them by attribute query.
The module imports only Mathlib.Init. It is Lean attribute scaffolding for tactic control, not an algebra or physics development.
proof idea
This is a definition module, no proofs. It registers custom Lean attributes (attribute declarations / registration hooks) so downstream RSA tactics can query tagged lemmas. Structure is attribute surface only; no mathematical argument.
why it matters in Recognition Science
Feeds the parent module Verification.RecognitionStabilityAudit.RL, which makes the RSA pipeline RL-friendly inside Lean. That parent documents the two tags: one for whitelisted rewrite/unfold lemmas used by the RSA simplifier, and one for milestone lemmas the RSA step tactic may apply.
Without this registry, automated RSA search would lack a controlled whitelist and milestone set. The attributes are the control surface that keeps RL-style proof search inside a curated lemma environment rather than the full Mathlib/monolith context. They sit in the verification domain and do not encode Recognition Science landmarks (forcing chain T0-T8, RCL, phi, eight-tick octave, or mass ladder).
scope and limits
- Does not prove any RSA stability or recognition-theoretic theorem.
- Does not implement the RSA simplifier or step tactics.
- Does not itself whitelist lemmas; only provides attribute hooks.
- Does not encode physics content (J-cost, phi-ladder, forcing chain).
- Does not constrain lemmas lacking the registered tags.