exercisedPatience
plain-language theorem explainer
Patience on an eight-tick cadence means the agent issues the zero virtue action on every tick before the last, waiting until full eight-tick information is in. Anyone building RS-native RL evaluation or audit checks would cite this predicate. It is a pure definitional proposition: universal quantification over ticks 0..6 with equality to the zero action.
Claim. Given an eight-tick cadence $c$ (states and virtue-actions on $\mathrm{Fin}\,8$), the agent exercised patience if for every tick $t$ with $t<7$, the action $c.a(t)$ equals the zero virtue action.
background
The RS→RL bridge treats Recognition Science as control theory: moral states, 14 virtue generators as actions, σ=0 projection, lexicographic multi-objective selection, and a Gibbs policy from the RS cost $J$. Temporal aggregation is not an arbitrary discount factor. By T6 minimality the unique window is the undiscounted eight-tick cadence: states and actions indexed by $\mathrm{Fin},8$, evaluated as an atomic block.
EightTickCadence packages that window and the action schedule. Virtue actions are 14-coefficient vectors over the admissible generators; the zero action is the null coefficient vector (no transformation proposed). Patience is the audit predicate that the schedule stays at zero until the final tick, i.e. the agent does not commit before the full eight-tick information is available.
This sits in the evaluation layer alongside total undiscounted window value, Gibbs thermodynamics, and LACompletion projection, not in the forcing chain itself.
proof idea
Definitional, not a proved theorem. The body is the proposition $\forall t:\mathrm{Fin},8,; t.val<7\to c.actions,t=\mathrm{VirtueAction.zero}$. No lemmas or tactics; downstream code unfolds or applies this Prop as a hypothesis or goal.
why it matters
Closes a named evaluation check in the RS→RL interface: "did the agent wait for full information?" The module design insists on eight-tick windows forced by T6 (and aligned with the T7 eight-tick octave), with no exponential discount. Patience formalizes delayed commitment inside that window so audits can separate premature action from end-of-window choice.
It feeds the complete environment bundle (MoralState, VirtueAction, LACompletion, LexicographicSelector, GibbsPolicy, EightTickCadence) used to train or score agents natively in RS units. No downstream theorems currently depend on it in the graph; it is infrastructure for stability and ethics audits rather than a step in the T0–T8 forcing chain. Related landmarks: eight-tick cadence, virtue basis, σ=0 feasibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.