satisfiesTemperance
plain-language theorem explainer
Temperance is the hard energy gate on a virtue action: its energy cost must not exceed the allotted budget divided by φ. Anyone wiring the RS→RL bridge or auditing lexicographic goal checks cites this predicate. It is a one-line definitional inequality, not a derived theorem.
Claim. A virtue action $a$ (a $14$-coefficient vector over the virtue generators) satisfies temperance for a real energy budget $E$ when its energy cost obeys $\mathrm{cost}(a) \le E/\varphi$, where $\varphi$ is the golden ratio fixed by self-similarity.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry ledger, bonds, skew, and energy; admissible moves are the 14 virtue generators guaranteed complete and minimal by the DREAM theorem. Policies output coefficients in that basis rather than raw controls.
Temperance is the thermodynamic throttle on those coefficients. The sibling energyCost scores how expensive a coefficient vector is; the budget is an external real parameter. Division by $\varphi$ (the self-similar fixed point forced at T6) is the RS-native scale, not an arbitrary discount.
The surrounding module also installs $\sigma=0$ feasibility via LACompletion, a lexicographic multi-objective selector, Gibbs policies $p(a|s)\propto\exp(-J(s,a)/T_R)$, and eight-tick evaluation windows. Temperance sits among those hard constraints before value or robustness are scored.
proof idea
Definitional: the predicate is exactly the inequality energyCost a ≤ energyBudget / φ. No tactics, no lemmas. Downstream goal_temperance_check unfolds it by rfl.
why it matters
Feeds goal_temperance_check in the RL goals module, which exposes the same inequality as an audit theorem (again by reflexivity). In the framework this is the temperance slot of the virtue basis: energy must stay below budget scaled by $\varphi$, consistent with T6 forcing of $\varphi$ and with the eight-tick, undiscounted window design of the bridge.
It does not itself prove conservation or $\sigma=0$; those are handled by LACompletion and the feasibility predicate. It only names the energy gate so the lexicographic selector (feasible → harm-minimax → value → robustness) and Gibbs policy can treat temperance as a first-class, φ-scaled constraint rather than an ad-hoc clip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.