prob
plain-language theorem explainer
Normalized Gibbs probability of one virtue action given a moral state and a finite candidate list: unnormalized Boltzmann weight over the partition function. Anyone wiring RS thermodynamics into an RL policy cites this. The body is a one-line quotient; no proof content.
Claim. Given a Gibbs policy $g$ (recognition temperature $T_R>0$ and cost $J$), a moral state $s$, a finite list of virtue actions, and a candidate action $a$, the selection probability is $$p_g(a\mid s)=\frac{w_g(s,a)}{Z_g(s,\mathrm{actions})},$$ the normalized Boltzmann weight of $a$ under $g$.
background
The ambient 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 LACompletion, and thermodynamic policies. The design goal is p(a|s) ∝ exp(−J(s,a)/T_R), the RS form of maximum-entropy / soft actor-critic exploration.
A GibbsPolicy packages a positive recognition temperature T_R and a cost map J on (MoralState, VirtueAction). MoralState carries the lightweight RS ledger quantities (skew σ, energy budget, value V, max harm, spectral gap). VirtueAction is a 14-coefficient vector over the DREAM-complete virtue generators; the policy explores in that basis, not raw moves.
The free-energy identity recorded next to this definition, F_R = E[J] − T_R S_R(p) with F_R(q)−F_R(Gibbs)=T_R D_KL(q∥Gibbs), is the thermodynamic reason this normalization exists.
proof idea
Pure definition, not a theorem. The body is the single quotient
g.weight s a / g.partitionFn s actions
i.e. unnormalized Boltzmann weight of the chosen action divided by the partition function of the supplied discrete action list. No lemmas are applied; well-definedness as a real rests on whatever noncomputable arithmetic Mathlib supplies for ℝ division.
why it matters
This is the concrete p(a|s) object promised by the module's "thermodynamic learning" bullet and by the GibbsPolicy docstring ("RS thermodynamic form, equivalent to soft actor-critic / maximum entropy RL but grounded in the RS cost J"). Downstream bridge code that samples, scores, or proves properties of Gibbs policies goes through this normalizer; the module reports dozens of use sites.
It sits next to the free-energy / KL identity that justifies why the Gibbs policy is the unique minimizer of F_R, and it inherits the eight-tick cadence constraint (T6 / T7) from the surrounding RL loop: evaluation windows are forced 8-tick, not arbitrarily discounted. Together with LACompletion (propose then project to σ=0) it separates creative proposal from hard RS feasibility.
It does not itself close any forcing-chain step (T0–T8); it is infrastructure that makes the RS cost J usable as an RL energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.