Pith. sign in
module module moderate

IndisputableMonolith.Verification.RecognitionStabilityAudit.RStoRL

show as:
view Lean formalization →

Defines a lightweight moral state for reinforcement-learning training built from Recognition Science quantities: reciprocity skew σ, an available recognition-cost energy budget, and the value functional V = κ·I(A;E) − C_J*. Supplies virtue actions, norms, temperance and σ-feasibility predicates, and an LA-completion interface. The Recognition Stability Audit umbrella imports it. Structure is definitional scaffolding rather than a proved theorem chain.

claimA moral state for RL is a triple $(\sigma, E, V)$ where $\sigma$ is reciprocity skew (imbalance), $E$ is the available recognition-cost budget, and $V = \kappa\, I(A;E) - C_{J}^{*}$ is net value. The module equips this state with zero, norm, scale, and add; names virtue actions; defines energy cost and a temperance predicate; and records $\sigma$-feasibility and LA-completion conditions used by the stability audit.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law. Recognition budgets and mutual-information terms appear when agents act under that cost. This module sits in the Verification domain and packages those RS scalars into a form usable by RL training loops.

The module doc states the essential quantities explicitly: skew $\sigma$ (reciprocity imbalance), energy (available recognition cost budget), and value $V=\kappa\cdot I(A;E)-C_J^{*}$. Sibling definitions introduce MoralState, virtue actions, algebraic operations (zero, norm, scale, add), an interpreter over named virtues, energy cost, temperance satisfaction, $\sigma$-feasibility, and LA-completion.

Upstream imports are Cost (J-cost infrastructure) and Constants (RS-native units, including the tick $\tau_0$). No forcing-chain theorems are proved here; the file only re-expresses RS bookkeeping for audit and training.

proof idea

This is a definition module, not a proof module. It declares the moral-state record, virtue-action vocabulary, and the algebraic and feasibility predicates listed among the siblings. There is no tactic script discharging a global theorem; downstream audit code consumes the types and predicates directly.

why it matters in Recognition Science

The parent consumer is the Recognition Stability Audit umbrella (IndisputableMonolith.Verification.RecognitionStabilityAudit), which re-exports the RSA core so clients can import a single module. That umbrella points at papers/tex/Recognition_Stability_Audit.tex. By giving RSA a concrete RS-to-RL state (skew, energy budget, net value against $C_J^{*}$), the file lets stability checks talk about temperance, $\sigma$-feasibility, and LA-completion without re-deriving cost primitives. It does not itself close T5–T8 or the mass ladder; it only supplies the moral-state interface those audits need when agents are trained under RS costs.

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)