module module high

`IndisputableMonolith.Verification.RecognitionStabilityAudit.RL`

Automation layer for the Recognition Stability Audit: a single bounded tactic step that closes RSA goals by assumption, by applying a whitelisted milestone lemma, or by falling back to a restricted simplifier. Verification authors cite it when scripting short, deterministic RSA proof scripts. The control flow is pure tactic search over attribute-tagged lemmas, not a mathematical derivation.

claimA bounded audit step $\mathsf{rsa\_step}$ on an RSA goal $G$: close $G$ if it is already an assumption; else try $\mathsf{apply}\, L$ for some lemma $L$ tagged $\mathsf{rsa\_milestone}$, discharging residual subgoals by assumption or restricted simplification; else run $\mathsf{rsa\_simp}$. Fail if no milestone applies.

background

Recognition Stability Audit (RSA) is the formal companion to papers/tex/Recognition_Stability_Audit.tex. The umbrella module re-exports the core RSA interface (boundary hits, Schur-type constraints, sensor blow-ups, obstruction maps) so downstream files import one path.

This file sits under Verification.RecognitionStabilityAudit.RL and implements the interactive/automation half of that stack. Companion module RL.Attr defines two attribute whitelists: @[rsa_simp] (allowed unfold/rewrite lemmas for the restricted simplifier) and @[rsa_milestone] (allowed apply targets for a single audit step). Keeping attributes separate avoids Lean initialization-order cycles.

Sibling declarations expose the milestone and simp name tables, definitional bridges for RSA predicates (boundary hit at a point, Schur-on, sensor-from-obstruction, sensor blow-up), and named goal forms used by the step tactic (theta identities, pole-implies-boundary, obstruction-to-sensor).

proof idea

This is a tactic module, not a theorem module. The main elaborator rsa_step runs a fixed three-stage search: (1) try assumption and return on success; (2) enumerate @[rsa_milestone] names, attempt apply, then all_goals cleanup via assumption and rsa_simp; return on the first successful apply; (3) fall back to rsa_simp plus residual assumption. If every stage fails, throw a deterministic error that no milestone applied. Supporting defs only register names and goal shapes; they carry no proof content.

why it matters in Recognition Science

RSA proofs must stay inside a closed lemma economy so audit scripts remain reproducible and do not silently unfold high-level wrappers (e.g. boundary-hit predicates). This module is the single bounded step that enforces that economy: milestones fire before simplification, so wrapper structure is preserved. It feeds no named parent theorem directly (used_by is empty); instead it is infrastructure for human and scripted RSA discharges under the umbrella RecognitionStabilityAudit import. In the broader Recognition stack it is verification scaffolding around stability claims, not a link in the T0–T8 forcing chain.

scope and limits

Does not prove any RSA stability theorem; only automates goal discharge.
Does not search outside `@[rsa_milestone]` and `@[rsa_simp]` whitelists.
Does not perform multi-step planning; each invocation is one bounded step.
Does not alter RSA definitions or paper-level claims in Recognition_Stability_Audit.tex.
Does not guarantee progress: may fail with an explicit no-milestone error.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.RecognitionStabilityAudit module_import
IndisputableMonolith.Verification.RecognitionStabilityAudit.RL.Attr module_import

declarations in this module (31)

def getRsaSimpNames L42
def getRsaMilestoneNames L46
theorem BoundaryHitAt_def L108
theorem SchurOn_def L111
theorem Problem_XiFromSensor_def L114
theorem SensorBlowsUpAt_def L117
theorem sensorOfObstruction_def L120
theorem goal_theta_eq_div L146
theorem goal_theta_invTheta L150
theorem goal_invTheta_theta L154
theorem goal_pole_implies_boundaryHit L158
theorem goal_obstruction_to_sensor_blowup L164
theorem goal_frontEnd_from_candidate_obligations L173
theorem goal_boundaryHit_value L192
theorem goal_boundaryHit_forces_const_one L199
theorem goal_backEnd_const_zero L211
theorem goal_correctness_trivial_univ L227
theorem goal_correctness_usage L238
theorem goal_virtueAction_zero_norm L260
theorem goal_virtueAction_norm_nonneg L264
theorem goal_virtueAction_scale_norm L268
theorem goal_lexBetter_irrefl L273
theorem goal_gibbs_weight_pos L277
theorem goal_gibbs_partitionFn_pos L282
theorem goal_eightTick_value_finite L288
theorem goal_sigma_feasibility L293
theorem goal_harm_bound_zero L298
theorem goal_consent_condition L303
theorem goal_parasitism_threshold_phi L308
theorem goal_LACompletion_identity_project L313
theorem goal_temperance_check L318