goal_temperance_check
plain-language theorem explainer
Temperance for a virtue action is exactly the inequality that its energy cost is at most the budget divided by φ. RL and audit authors cite it as the gold goal that pins the temperance predicate to its φ-scaled energy bound. The proof is definitional reflexivity: the two sides are the same Prop by unfolding.
Claim. For any virtue action $a$ (a $14$-coefficient real vector on the virtue generators) and any real budget $B$, $a$ satisfies temperance at budget $B$ if and only if its energy cost is at most $B/\varphi$, where $\varphi$ is the golden ratio.
background
This lives in the RSA reinforcement-learning layer of the Recognition Stability Audit. That module exposes whitelisted simp and milestone lemmas so an agent can close short audit goals inside Lean; the present declaration is one of the canonical gold goals used for training and checklist reward.
A virtue action is a real $14$-vector of coefficients on the DREAM-complete minimal generating set of ethical transformations. Its energy cost is the $\ell^1$ mass of those coefficients: $\sum_{i=0}^{13}|c_i|$. Temperance is the named predicate that this cost stays within a φ-scaled budget: energy $\le B/\varphi$. The factor $\varphi$ is the self-similar fixed point forced in the RS chain (T6), so the temperance cut is not an arbitrary hyperparameter.
Upstream, satisfiesTemperance is defined exactly as that inequality, and energyCost is the sum of absolute coefficients. The biconditional therefore records definitional identity rather than a new analytic bound.
proof idea
One-line rfl. After unfolding the definition of the temperance predicate, the left-hand side is literally energyCost a ≤ budget / φ, so the two Propositions are definitionally equal and reflexivity closes the goal. No lemmas beyond the definition are applied.
why it matters
In the RSA-to-RL bridge, temperance is the energy-budget gate on virtue actions: the policy may only emit coefficient vectors whose $\ell^1$ cost respects $B/\varphi$. This gold theorem makes that gate a closed, sorry-free training target for rsa_step / rsa_simp agents, so reward can be given for recognizing the φ-scaled bound rather than inventing a fresh inequality.
The φ in the denominator ties the audit constraint to the RS forcing chain (T6: φ as self-similar fixed point) and to the broader virtue/DREAM story that the $14$ generators are a complete minimal ethical basis. No downstream theorems currently depend on it (used_by is empty); its role is checklist and agent training inside the RL module, not a step in a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.