weight
plain-language theorem explainer
Unnormalized Gibbs weight of a virtue action in a moral state under a recognition-temperature policy: exp(-J(s,a)/T_R). Cited wherever the RS→RL bridge builds thermodynamic policies, partition functions, or soft action selection. The body is a one-line exponential of the policy cost scaled by inverse temperature.
Claim. For a Gibbs policy $g$ with recognition temperature $T_R>0$ and cost $J$, and for moral state $s$ and virtue action $a$, the unnormalized weight is $w_g(s,a)=\exp\bigl(-J(s,a)/T_R\bigr)\in\mathbb{R}$.
background
The module is the RS→RL bridge: Recognition Science is treated as a control theory with moral states, 14 virtue generators as the admissible action basis, σ=0 feasibility via LA-completion, and thermodynamic learning. The design principle is Gibbs selection $p(a\mid s)\propto\exp(-J(s,a)/T_R)$, aligned with soft actor-critic / maximum-entropy RL but driven by the RS cost $J$ rather than an ad hoc reward.
A GibbsPolicy packages a positive recognition temperature $T_R$ and a cost map $J:\mathrm{MoralState}\times\mathrm{VirtueAction}\to\mathbb{R}$. Moral states carry skew σ, energy budget, value $V$, max harm, and spectral gap. Virtue actions are 14-coefficient vectors over the DREAM-complete minimal generators. Upstream cost notions in the monolith (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen summed ratio weights) are the same family of non-negative recognition costs that $J$ is meant to instantiate at the RL interface.
proof idea
Definition only: evaluate the real exponential of the negated policy cost divided by the policy temperature. No lemmas, no tactics; noncomputable solely because Real.exp is.
why it matters
This is the elementary Boltzmann factor for the bridge’s thermodynamic policy. The next sibling is the partition function (normalization constant); together they define $p(a\mid s)=w(s,a)/Z(s)$. That distribution is the exploration rule the module advertises as forced by RS thermodynamics, not a training hack.
It sits under the eight-tick cadence forced by T6/T7 (undiscounted 8-tick windows) and under the multi-objective lexicographic selector (feasible → harm-minimax → value → robustness). Downstream in-module consumers include energy-cost checks, temperance constraints, σ-feasibility, and LA-completion propose-then-project loops. Framework landmarks: J from T5 uniqueness and the Recognition Composition Law; temperature as the strictness parameter dual to the cost scale set by φ-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.