satisfiesTemperanceWindow
plain-language theorem explainer
Temperance over a full eight-tick cadence holds exactly when the cadence's total energy stays at or below a real budget. Control and RL workers bridging Recognition Science cite it as the hard resource bound on virtue-coefficient trajectories. It is a one-line Prop definition: the inequality totalEnergy(c) ≤ budget, not a proved theorem.
Claim. Given an eight-tick cadence $c$ (states and virtue-actions on ticks $0..7$) and a real budget $B$, the temperance window predicate holds if and only if the total energy of $c$ satisfies $E(c)\le B$.
background
The ambient module is the RS→RL bridge: Recognition Science is treated as a specified control theory with MoralState, fourteen virtue generators as admissible actions, σ=0 feasibility via LACompletion, and undiscounted eight-tick evaluation forced by T6 minimality (the eight-tick octave of the forcing chain).
EightTickCadence packages one such atomic window: a map Fin 8 → MoralState together with actions Fin 8 → VirtueAction. RS forbids arbitrary discount factors; the unique aggregator is the undiscounted sum over this period-8 block. Temperance is the resource side of that window: keep total energy inside a budget.
Upstream, totalEnergy is the trajectory energy functional (Hamiltonian evaluation along the path). Here it is applied to the whole cadence rather than a single Newtonian curve, matching the module's thermodynamic and ledger bookkeeping.
proof idea
Definitional, not a proof. The predicate is the bare inequality totalEnergy c ≤ budget. Unfolding replaces the name by that comparison; no lemmas, tactics, or algebraic reduction are involved.
why it matters
In the RS→RL stack, virtues are not soft preferences: temperance is a hard energy window on eight-tick blocks, aligned with T6/T7 (unique eight-tick aggregator, no exponential discount). It sits beside sibling checks such as satisfiesTemperance and energyCost, and with feasibility (SigmaFeasible, LACompletion) and the lexicographic selector (feasible → harm-minimax → value → robustness).
No downstream theorems currently depend on it (used_by is empty), so it is interface surface for policy filters and audits rather than a link in a proved chain. It does not itself force φ, J-uniqueness, or the mass ladder; it only names the budget constraint those structures would impose on an RL agent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.