IndisputableMonolith.Verification.RecognitionStabilityAudit.RL
Automation layer for the Recognition Stability Audit: a single bounded proof step that tries assumption, then applies a registered milestone lemma, then falls back to a whitelisted simplifier. Physicists auditing RSA goal suites cite it as the driver that keeps high-level wrappers (boundary hits, sensors, Schur gates) from being unfolded away. The module also ships the default milestone and simp registries plus a small suite of named RSA goals.
claimA bounded audit step $\mathsf{rsa\_step}$ on a Recognition Stability Audit goal: close by assumption if possible; otherwise apply one registered milestone lemma and discharge trivial subgoals; otherwise run the RSA-whitelisted simplifier. The module also exposes the default milestone and simp name lists and the standard RSA goal forms (pole implies boundary hit, obstruction implies sensor blow-up, $\theta$ inversion identities).
background
The Recognition Stability Audit (RSA) is the formal companion to papers/tex/Recognition_Stability_Audit.tex. The umbrella module re-exports the core interface; this file is the tactic and goal layer that sits on top of it.
Attributes live in a separate import to avoid initialization-order issues: @[rsa_simp] marks lemmas allowed in the RSA simplifier, and @[rsa_milestone] marks lemmas the step tactic may apply. Milestone application is deliberately tried before simplification so high-level wrappers such as boundary-hit predicates, Schur-on gates, and sensor-from-obstruction maps are not unfolded away.
Sibling content includes name collectors for the two whitelists, definitional bridges for the main RSA predicates, and a short goal suite covering $\theta$ division and inversion identities, pole-to-boundary-hit, and obstruction-to-sensor blow-up.
proof idea
This is a tactic and registry module, not a theorem file. The main elaborator runs three stages in order: (1) assumption and return on success; (2) iterate registered milestone names, apply each candidate, then try assumption and rsa_simp on all subgoals; (3) if no milestone fires, run rsa_simp alone and try assumption again. Failure of all three stages raises a fixed error. Supporting declarations are pure name collectors, def bridges for RSA predicates, and named goal statements used as targets for the step tactic.
why it matters in Recognition Science
RSA proofs need a controlled, non-unfolding automation path so stability claims stay stated at the level of boundary hits, sensors, and Schur conditions rather than raw algebraic noise. This module is that path: milestones preserve the paper-level vocabulary, while the simp whitelist keeps rewrites inside the audit fragment. It sits under the Verification domain and imports only the RSA umbrella and the attribute file. No downstream Lean dependents are recorded yet; its consumers are interactive RSA goal scripts and any future end-to-end stability theorems that drive the audit by repeated bounded steps rather than open-ended search.
scope and limits
- Does not prove any RSA stability theorem; it only drives one bounded tactic step.
- Does not invent lemmas: only `@[rsa_milestone]` and `@[rsa_simp]` entries may fire.
- Does not perform open-ended search or backtracking beyond a single milestone pass.
- Does not define the RSA predicates themselves beyond thin def bridges and goal forms.
- Does not depend on physics constants (phi, alpha, eight-tick); pure verification automation.
depends on (2)
declarations in this module (31)
-
def
getRsaSimpNames -
def
getRsaMilestoneNames -
theorem
BoundaryHitAt_def -
theorem
SchurOn_def -
theorem
Problem_XiFromSensor_def -
theorem
SensorBlowsUpAt_def -
theorem
sensorOfObstruction_def -
theorem
goal_theta_eq_div -
theorem
goal_theta_invTheta -
theorem
goal_invTheta_theta -
theorem
goal_pole_implies_boundaryHit -
theorem
goal_obstruction_to_sensor_blowup -
theorem
goal_frontEnd_from_candidate_obligations -
theorem
goal_boundaryHit_value -
theorem
goal_boundaryHit_forces_const_one -
theorem
goal_backEnd_const_zero -
theorem
goal_correctness_trivial_univ -
theorem
goal_correctness_usage -
theorem
goal_virtueAction_zero_norm -
theorem
goal_virtueAction_norm_nonneg -
theorem
goal_virtueAction_scale_norm -
theorem
goal_lexBetter_irrefl -
theorem
goal_gibbs_weight_pos -
theorem
goal_gibbs_partitionFn_pos -
theorem
goal_eightTick_value_finite -
theorem
goal_sigma_feasibility -
theorem
goal_harm_bound_zero -
theorem
goal_consent_condition -
theorem
goal_parasitism_threshold_phi -
theorem
goal_LACompletion_identity_project -
theorem
goal_temperance_check