Pith. sign in
module module moderate

IndisputableMonolith.Verification.RecognitionStabilityAudit.RStoRL

show as:
view Lean formalization →

Defines a lightweight moral state for reinforcement-learning agents grounded in Recognition Science. The state packages reciprocity skew σ, an available recognition-cost energy budget, and a value functional V = κ·I(A;E) − C_J*. Downstream RSA code imports it as the RS-to-RL bridge. The module is definitional: structures, norms, virtue actions, and feasibility predicates, not deep theorems.

claimA moral state is a triple $(\sigma, E, V)$ where $\sigma$ is reciprocity skew (imbalance), $E$ is the available recognition-cost budget, and $V = \kappa \cdot I(A;E) - C_{J}^{*}$ is the net value of action $A$ in environment $E$. Virtue actions act on this state by scaling, addition, and energy cost; temperance and $\sigma$-feasibility constrain admissible updates.

background

Recognition Stability Audit (RSA) asks whether agents whose rewards track Recognition Science costs remain stable. This submodule supplies the RS-native state that an RL loop would observe and update.

The essential quantities are taken from the RS cost layer: skew $\sigma$ measures reciprocity imbalance; energy is a budget in units of the $J$-cost $C_J$ (the unique cost forced by the Recognition Composition Law); value is mutual information reward minus residual $J$-cost. Constants such as the tick $\tau_0$ enter only as the ambient RS time quantum.

Sibling definitions introduce MoralState, vector-like operations (zero, norm, scale, add), a finite menu of virtue actions with names and interpretations, an energy-cost map, and predicates for temperance and $\sigma$-feasibility, plus an LA-completion marker.

proof idea

This is a definition module, not a theorem module. It declares the moral-state structure, algebraic operations on it, virtue-action labels and their interpretive map, energy-cost accounting, and feasibility predicates (temperance, $\sigma$-feasibility, LA completion). No substantial proof obligations are discharged here; downstream audit code consumes these types and predicates as the RS-to-RL interface.

why it matters in Recognition Science

The parent umbrella RecognitionStabilityAudit re-exports this bridge so that RSA developments can import a single path and obtain an RL-ready moral state. Paper reference: papers/tex/Recognition_Stability_Audit.tex. By packaging $\sigma$, recognition energy, and $V = \kappa\cdot I(A;E) - C_J^{*}$ in one object, the module lets stability claims be stated as constraints on trajectories in moral-state space rather than as ad-hoc reward hacks. It sits in the verification domain: it does not re-derive $J$-uniqueness (T5) or the forcing chain, but assumes the Cost and Constants layers and exposes only what an RL trainer needs.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (51)