EightTickCadence
plain-language theorem explainer
An eight-tick cadence is the atomic temporal package for RS-to-RL evaluation: states at ticks 0..7 paired with virtue actions at each tick. It encodes the forced period-8 ledger window so critics and policies never introduce arbitrary discount factors. Anyone wiring multi-step value, harm, σ-closure, temperance, or patience checks cites it. As a structure there is no proof body; it only fixes the window type.
Claim. An eight-tick cadence is a pair of maps $(w,a)$ with $w:\{0,\ldots,7\}\to$ moral states and $a:\{0,\ldots,7\}\to$ virtue-coefficient actions, recording one full undiscounted ledger-closure window (the unique temporal aggregator forced by eight-tick minimality).
background
This lives in the RS→RL bridge: Recognition Science is treated as a specified control theory with moral states, 14 virtue generators as admissible moves, σ=0 feasibility via propose-then-project, and lexicographic multi-objective selection. The design rule here is explicit: no arbitrary discount; evaluate trajectories in forced 8-tick blocks.
A moral state carries reciprocity skew σ, energy budget, value $V$, max harm, and a spectral-gap robustness slot. A virtue action is a 14-coefficient vector over the DREAM-complete minimal generators; the policy outputs those coefficients, not raw controls.
Upstream, the fundamental time quantum is one tick ($\tau_0=1$), and one octave is eight ticks. The structure simply types a full octave of states and actions so later window functionals (total value, total energy, max harm, σ-closure) are ordinary finite sums over Fin 8.
proof idea
Definition only: a structure with two fields, window : Fin 8 → MoralState and actions : Fin 8 → VirtueAction. No constructors beyond the implicit one, no axioms, no proof tactics. Downstream defs build finite aggregates (undiscounted sums, suprema, pointwise checks at tick 7) directly from these maps.
why it matters
This is the temporal atom of the RS→RL bridge. Module design lists it beside VirtueAction, LACompletion, LexicographicSelector, and GibbsPolicy as a main structure: policy and critic operate on 8-tick windows as atomic steps, matching the eight-tick octave (period $2^3$) rather than exponential discounting.
It feeds the window functionals totalValue, totalEnergy, maxHarm, sigmaClosed (skew returns to 0 by tick 8), satisfiesTemperanceWindow, and exercisedPatience (zero action until tick 7). Those in turn discharge audit goals such as eightTick_value_finite and goal_eightTick_value_finite (total value over a cadence is a well-defined finite real).
Without this type, the bridge would smuggle an arbitrary horizon or discount schedule into the control loop, breaking the T6/T7 minimality story that ledger closure forces period 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.